factor_map — Mathlib

English

If HasImage f and Epi (image.ι f) and Epi (factorThruImage f) then Epi f.

Русский

Если образ f существует и image.ι f эпиморфизм, и factorThruImage f эпиморфизм, то f эпиморфизм.

LaTeX

$$$ [HasImage f] \\; [Epi (image.ι f)] \\; [Epi (factorThruImage f)] \\Rightarrow Epi f $$$

Lean4

@[reassoc (attr := simp)]
theorem factor_map {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) (m : ImageMap sq) :
    factorThruImage f.hom ≫ m.map = sq.left ≫ factorThruImage g.hom :=
  (cancel_mono (image.ι g.hom)).1 <| by simp

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