preComp_comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The two step comparison map
  `image (f ≫ (g ≫ h)) ⟶ image (g ≫ h) ⟶ image h`
agrees with the one step comparison map
  `image (f ≫ (g ≫ h)) ≅ image ((f ≫ g) ≫ h) ⟶ image h`.
-/
theorem preComp_comp {W : C} (h : Z ⟶ W) [HasImage (g ≫ h)] [HasImage (f ≫ g ≫ h)] [HasImage h]
    [HasImage ((f ≫ g) ≫ h)] :
    image.preComp f (g ≫ h) ≫ image.preComp g h = image.eqToHom (Category.assoc f g h).symm ≫ image.preComp (f ≫ g) h :=
  by
  apply (cancel_mono (image.ι h)).1
  simp only [preComp, Category.assoc, fac, lift_mk_comp, eqToHom]
  rw [image.lift_fac]

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