leftKanExtension_hom_ext — Mathlib

English

Two morphisms γ1, γ2 from L.leftKanExtension F to G are equal if their composites with leftKanExtensionUnit agree after whiskering by L.

Русский

Две гомоморфизмы γ1, γ2: L.leftKanExtension F ⟶ G равны тогда и только тогда, когда их композиции с leftKanExtensionUnit совпадают после whiskerLeft по L.

LaTeX

$$$\gamma_1 = \gamma_2$ if $leftKanExtensionUnit F \;\gg\; \gamma_1 = leftKanExtensionUnit F \;\gg\; \gamma_2$$$

Lean4

@[ext]
theorem leftKanExtension_hom_ext {G : D ⥤ H} (γ₁ γ₂ : leftKanExtension L F ⟶ G)
    (hγ : leftKanExtensionUnit L F ≫ whiskerLeft L γ₁ = leftKanExtensionUnit L F ≫ whiskerLeft L γ₂) : γ₁ = γ₂ :=
  hom_ext_of_isLeftKanExtension _ _ _ _ hγ

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