unit_hom_ext — Mathlib

English

Extensionality principle for unit morphisms of DayFunctor via νNatTrans

Русский

Принцип экстенсиональности единичных морфизмов DayFunctor через νNatTrans.

LaTeX

$$$\\text{unit_hom_ext} : \\alpha = \\beta \\;\\text{given} \\; ν ≫ α.natTrans.app = ν ≫ β.natTrans.app$$$

Lean4

theorem unit_hom_ext {F : C ⊛⥤ V} {α β : 𝟙_ (C ⊛⥤ V) ⟶ F}
    (h : ν C V ≫ α.natTrans.app (𝟙_ C) = ν C V ≫ β.natTrans.app (𝟙_ C)) : α = β :=
  by
  ext1
  apply Functor.hom_ext_of_isLeftKanExtension (𝟙_ (C ⊛⥤ V)).functor (νNatTrans C V)
  ext
  exact h

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