English
A repeated variant of lift_mk_comp showing the same identity in a broader setting.
Русский
Повторная вариация lift_mk_comp, показывающая ту же самую идентичность в более общем контексте.
LaTeX
$$$\text{Lift mk comp (variant)}: \; image.lift { I := image g, m := ι g, e := (f ≫ h) } ≫ image.ι g = image.ι (f ≫ g).$$$
Lean4
@[reassoc (attr := simp)]
theorem lift_mk_comp {C : Type u} [Category.{v} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasImage g] [HasImage (f ≫ g)]
(h : Y ⟶ image g) (H : (f ≫ h) ≫ image.ι g = f ≫ g) :
image.lift { I := image g, m := ι g, e := (f ≫ h) } ≫ image.ι g = image.ι (f ≫ g) :=
image.lift_fac
_
-- TODO we could put a category structure on `MonoFactorisation f`,
-- with the morphisms being `g : I ⟶ I'` commuting with the `m`s
-- (they then automatically commute with the `e`s)
-- and show that an `imageOf f` gives an initial object there
-- (uniqueness of the lift comes for free).
