g

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g

Lean4

/-- The natural transformation `X ⟶ Y.obj t.right` for `t : Under j₀`
that is induced by `y : X ⟶ Y.obj j₀`. -/
@[simps]
def g : (Functor.const _).obj X ⟶ Under.forget j₀ ⋙ Y
    where
  app t := y ≫ Y.map t.hom
  naturality t₁ t₂
    f := by
    dsimp
    simp only [Category.id_comp, Category.assoc, ← Functor.map_comp, Under.w]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru