lift — Mathlib

English

The image factorization of f satisfies the universal property: given any mono factorization F', there is a unique map image f ⟶ F'.I making the diagram commute.

Русский

Факторизация образа f удовлетворяет универсальному свойству: для любой MonoFactorisation F' существует единственный морфизм image(f) ⟶ F'.I, делающий диаграмму коммутативной.

LaTeX

$$$\\text{IsImage}(\\mathrm{monoFactorisation}(f)) \\;\\Rightarrow \\text{universal property of image factorisation}$$$

Lean4

/-- The universal property for the image factorisation -/
noncomputable def lift (F' : MonoFactorisation f) : image f ⟶ F'.I :=
  ofHom
    { toFun := (fun x => F'.e (Classical.indefiniteDescription _ x.2).1 : image f → F'.I)
      map_add' := fun x y => by
        apply (mono_iff_injective F'.m).1
        · infer_instance
        rw [LinearMap.map_add]
        change (F'.e ≫ F'.m) _ = (F'.e ≫ F'.m) _ + (F'.e ≫ F'.m) _
        simp_rw [F'.fac, (Classical.indefiniteDescription (fun z => f z = _) _).2]
        rfl
      map_smul' := fun c x => by
        apply (mono_iff_injective F'.m).1
        · infer_instance
        rw [LinearMap.map_smul]
        change (F'.e ≫ F'.m) _ = _ • (F'.e ≫ F'.m) _
        simp_rw [F'.fac, (Classical.indefiniteDescription (fun z => f z = _) _).2]
        rfl }

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