factors_iff — Mathlib

English

For a subobject P ⊆ Y and a morphism f: X ⟶ Y, P.Factors f iff the representative object of P factors f.

Русский

Для подобъекта P ⊆ Y и морфизма f: X ⟶ Y: P.Factors f эквивалентно тому, что представление P факторизует f.

LaTeX

$$$P.Factors f \\iff (\\mathrm{representative}.obj P).Factors f$$$

Lean4

theorem factors_iff {X Y : C} (P : Subobject Y) (f : X ⟶ Y) : P.Factors f ↔ (representative.obj P).Factors f :=
  Quot.inductionOn P fun _ => MonoOver.factors_congr _ (representativeIso _).symm

Похожие утверждения