left_inv' — Mathlib

English

The left inverse for the initial algebra structure maps equals the identity after composition with the structure map, up to isomorphism given by the initial object.

Русский

Левый обратный для структуры начального алгебры равен тождественному после композиции с картой структуры, с учетом изоморфности начального объекта.

LaTeX

$$$\\langle \\mathrm{strInv}(h) \\circ A.\\mathrm{str}, \\text{...}\\rangle = 1_A$$$

Lean4

theorem left_inv' : ⟨strInv h ≫ A.str, by rw [← Category.assoc, F.map_comp, strInv, ← Hom.h]⟩ = 𝟙 A :=
  Limits.IsInitial.hom_ext h _ (𝟙 A)

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