coconeOfRepresentable_naturality — Mathlib

English

The identity functor yields a left Kan extension with preservation properties.

Русский

Идентичность образует левое Kan-расширение с сохранением свойств.

LaTeX

$$$L.IsLeftKanExtension(\mathrm{Id}_{\mathrm{uliftYoneda}})$$$

Lean4

/-- The legs of the cocone `coconeOfRepresentable` are natural in the choice of presheaf. -/
theorem coconeOfRepresentable_naturality {P₁ P₂ : Cᵒᵖ ⥤ Type max w v₁} (α : P₁ ⟶ P₂) (j : P₁.Elementsᵒᵖ) :
    (coconeOfRepresentable P₁).ι.app j ≫ α = (coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j) :=
  by
  ext T f
  simp [uliftYonedaEquiv, FunctorToTypes.naturality]

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