hom_ext — Mathlib

English

Uniqueness of morphisms between left extensions follows from the universal property of pointwise extensions: any two such morphisms coincide if they agree on the universal arrows.

Русский

Уникальность морфизмов между левыми расширениями следует из универсального свойства точечных расширений: любые два такие морфизма совпадают на универсальных стрелках.

LaTeX

$$$\\forall G, f_1,f_2:\\; f_1=f_2$$$

Lean4

theorem hom_ext {G : LeftExtension L F} {f₁ f₂ : E ⟶ G} : f₁ = f₂ :=
  by
  ext Y
  apply (h Y).hom_ext
  intro X
  have eq₁ := congr_app (StructuredArrow.w f₁) X.left
  have eq₂ := congr_app (StructuredArrow.w f₂) X.left
  dsimp at eq₁ eq₂ ⊢
  simp only [assoc, NatTrans.naturality]
  rw [reassoc_of% eq₁, reassoc_of% eq₂]

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