trans

Mathlib.CategoryTheory.ConcreteCategory.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.HasForget₂.trans

Lean4

/-- Composition of `HasForget₂` instances. -/
@[reducible]
def trans (C : Type u) [Category.{v} C] [HasForget.{w} C] (D : Type u') [Category.{v'} D] [HasForget.{w} D]
    (E : Type u'') [Category.{v''} E] [HasForget.{w} E] [HasForget₂ C D] [HasForget₂ D E] : HasForget₂ C E
    where
  forget₂ := CategoryTheory.forget₂ C D ⋙ CategoryTheory.forget₂ D E
  forget_comp :=
    by
    change (CategoryTheory.forget₂ _ D) ⋙ (CategoryTheory.forget₂ D E ⋙ CategoryTheory.forget E) = _
    simp only [HasForget₂.forget_comp]

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

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

Разделы

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

Аффилиация

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