factorThru_right — Mathlib

English

Let X --f--> Y --g--> Z be morphisms in a category, and let h be a factorization of g through a subobject P of Z. Then f followed by P.factorThru g h equals P.factorThru (f∘g) with the induced factor through.

Русский

Пусть X с отн. f к Y, Y к Z, и h — факторизация g через подобъект P ⊆ Z. Тогда f ; P.factorThru g h = P.factorThru (f ∘ g) с соответствующим отображением факторизации.

LaTeX

$$$f\;\gg\;P.\text{factorThru}(g,h) = P.\text{factorThru}(f\circ g, \text{factors_of_factors_right } f h)$$$

Lean4

theorem factorThru_right {X Y Z : C} {P : Subobject Z} (f : X ⟶ Y) (g : Y ⟶ Z) (h : P.Factors g) :
    f ≫ P.factorThru g h = P.factorThru (f ≫ g) (factors_of_factors_right f h) :=
  by
  apply (cancel_mono P.arrow).mp
  simp

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