precompose

Mathlib.CategoryTheory.Limits.Types.ColimitType

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.CoconeTypes.precompose

Lean4

/-- The cocone for `G : J ⥤ Type w₀'` that is deduced from a cocone for `F : J ⥤ Type w₀`
and a natural map `G.obj j → F.obj j` for all `j : J`. -/
@[simps -fullyApplied]
def precompose (c : CoconeTypes.{w₁} F) {G : J ⥤ Type w₀'} (app : ∀ j, G.obj j → F.obj j)
    (naturality : ∀ {j j'} (f : j ⟶ j'), app j' ∘ G.map f = F.map f ∘ app j) : CoconeTypes.{w₁} G
    where
  pt := c.pt
  ι j := c.ι j ∘ app j
  ι_naturality f := by rw [Function.comp_assoc, naturality, ← Function.comp_assoc, ι_naturality]

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

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

Разделы

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

Аффилиация

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