mapSquare

Mathlib.CategoryTheory.Square

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NatTrans.mapSquare

Lean4

/-- The natural transformation `F.mapSquare ⟶ G.mapSquare` induces
by a natural transformation `F ⟶ G`. -/
@[simps]
def mapSquare {F G : C ⥤ D} (τ : F ⟶ G) : F.mapSquare ⟶ G.mapSquare where
  app
    sq :=
    { τ₁ := τ.app _
      τ₂ := τ.app _
      τ₃ := τ.app _
      τ₄ := τ.app _ }

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

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

Разделы

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

Аффилиация

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