Factor-through on a subset

This file defines the set-restricted variant of mathlib's Function.FactorsThrough: g factors through f on a subset s of the domain when, for a b ∈ s, equality of f a and f b forces equality of g a and g b.

Main definitions

• Function.FactorsThroughOn g f s: g factors through f on s.

Main results

• Function.factorsThroughOn_univ: equivalent to Function.FactorsThrough on Set.univ.
• Function.FactorsThrough.factorsThroughOn: a global factor-through restricts to any subset.
• Function.not_factorsThroughOn_iff_exists_witness: refutation by a pair of in-set points agreeing on f and differing on g.

def Function.FactorsThroughOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : α → γ) (f : α → β) (s : Set α) : Prop

g factors through f on s: for a b ∈ s, f a = f b implies g a = g b.

Equations

• Function.FactorsThroughOn g f s = ∀ ⦃a b : α⦄, a ∈ s → b ∈ s → f a = f b → g a = g b

theorem Function.factorsThroughOn_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : α → γ) (f : α → β) : FactorsThroughOn g f Set.univ ↔ FactorsThrough g f

theorem Function.FactorsThrough.factorsThroughOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : α → γ} {f : α → β} (h : FactorsThrough g f) (s : Set α) : FactorsThroughOn g f s

theorem Function.not_factorsThroughOn_iff_exists_witness {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : α → γ} {f : α → β} {s : Set α} : ¬FactorsThroughOn g f s ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ f a = f b ∧ g a ≠ g b

theorem Function.factorsThroughOn_iff_exists_eqOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty γ] {g : α → γ} {f : α → β} {s : Set α} : FactorsThroughOn g f s ↔ ∃ (h : β → γ), Set.EqOn g (h ∘ f) s

Factoring through on s, existentially: g agrees on s with some function of f. The mirror of Function.factorsThrough_iff for the set-restricted variant.

theorem Function.factorsThrough_iff_of_idempotent {α : Type u_1} {γ : Type u_3} {g : α → γ} {f : α → α} (hf : ∀ (a : α), f (f a) = f a) : FactorsThrough g f ↔ ∀ (a : α), g a = g (f a)

For an idempotent f, g factors through f iff g is f-invariant (pointwise g = g ∘ f).

@[implicit_reducible]

instance Function.instDecidableFactorsThroughOnOfFintypeOfDecidablePredMemSetOfDecidableEq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : α → γ} {f : α → β} {s : Set α} [Fintype α] [DecidablePred fun (x : α) => x ∈ s] [DecidableEq β] [DecidableEq γ] : Decidable (FactorsThroughOn g f s)

Equations

• Function.instDecidableFactorsThroughOnOfFintypeOfDecidablePredMemSetOfDecidableEq = id inferInstance