Functions that factor through another

Lemmas on mathlib's Function.FactorsThrough. A function that factors through f takes no more values than f, and factoring through an idempotent function is invariance under it.

Factoring through on a subset s needs no predicate of its own. It is (s.domRestrict g).FactorsThrough (s.domRestrict f), and Function.factorsThrough_iff then says that g agrees on s with a function of f.

Main results

• Function.FactorsThrough.finite_range, Function.FactorsThrough.card_range_le: a function that factors through another takes no more values, so its range is finite when the other's is.
• Function.factorsThrough_iff_of_idempotent: a function factors through an idempotent f exactly when it is invariant under f.

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)

A function factors through an idempotent f exactly when it is invariant under f.

@[instance_reducible]

instance Function.instDecidableFactorsThroughOfFintypeOfDecidableEq_linglib {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : α → γ} {f : α → β} [Fintype α] [DecidableEq β] [DecidableEq γ] : Decidable (FactorsThrough g f)

Equations

• Function.instDecidableFactorsThroughOfFintypeOfDecidableEq_linglib = id inferInstance

theorem Function.FactorsThrough.card_range_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : α → γ} {f : α → β} [Finite α] (h : FactorsThrough g f) : Nat.card ↑(Set.range g) ≤ Nat.card ↑(Set.range f)

A function that factors through another takes no more values.

theorem Function.FactorsThrough.finite_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : α → γ} {f : α → β} (h : FactorsThrough g f) (hf : (Set.range f).Finite) : (Set.range g).Finite

A function that factors through a function with finite range has finite range.