factorThruImage_comp_hom — Mathlib

English

A variant asserting that if HasSplitEqualizer holds, then G preserves the corresponding limit for parallelPair f g.

Русский

Вариант утверждения: если есть HasSplitEqualizer, то G сохраняет соответствующий предел для parallelPair f g.

LaTeX

$$$\\text{HasSplitEqualizer}(f,g) \\Rightarrow \\operatorname{PreservesLimit}(\\operatorname{parallelPair}(f,g), G).$$$

Lean4

@[reassoc]
theorem factorThruImage_comp_hom {X Y : A} (f : X ⟶ Y) :
    factorThruImage (L.map f) ≫ (iso L f).hom = L.map (factorThruImage f) := by simp

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