convolution_hom_ext_at — Mathlib

English

If a family of maps out of (F ⊛ G).obj c to v agrees on all left Kan-extension tests at c, then the two maps are equal; i.e., hom-ext at a point for convolution is determined by its action on the left Kan-extensions.

Русский

Если семейство отображений из (F ⊛ G).obj c в v согласовано по всем тестам left Kan-extension, то два отображения равны; равноправное разложение по точке для свёртки определено по действию на leftKan.

LaTeX

$$$\\forall c\\in C, f,g:(F ⊛ G).obj c ⟶ v,\\; (\\forall x,y,u,..., ) \\Rightarrow f=g$$$

Lean4

/-- Use the fact that `(F ⊛ G).obj c` is a colimit to characterize morphisms out of it at a
point. -/
theorem convolution_hom_ext_at (c : C) {v : V} {f g : (F ⊛ G).obj c ⟶ v}
    (h :
      ∀ {x y : C} (u : x ⊗ y ⟶ c),
        (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ f = (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ g) :
    f = g :=
  ((isPointwiseLeftKanExtensionUnit F G) c).hom_ext (fun j ↦ by simpa using h j.hom)

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