tensor_hom_ext — Mathlib

English

The component of η composed with the isomorphism giving the pointwise left Kan extension hom equals a colimit ι expression

Русский

Компонента η при композиции с изоморфизмом pointwiseLeftKanExtension совпадает с выражением через индексный морфизм colimit ι.

LaTeX

$$$ (\\eta F G)_{(x,y)} \\;\\circ \\; (\\mathrm{isoPointwiseLeftKanExtension} F G)_{(x \\otimes y)}^{\\mathrm{hom}} = \\mathrm{colimit.ι}(...) $$$

Lean4

theorem tensor_hom_ext {F G H : C ⊛⥤ V} {α β : F ⊗ G ⟶ H}
    (h : ∀ (x y : C), (η F G).app (x, y) ≫ α.natTrans.app (x ⊗ y) = (η F G).app (x, y) ≫ β.natTrans.app (x ⊗ y)) :
    α = β := by
  ext : 1
  apply Functor.hom_ext_of_isLeftKanExtension (F ⊗ G).functor (η F G) _
  ext ⟨x, y⟩
  exact h x y

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