mapSquare — Mathlib

Lean4
/-- The functor `Square C ⥤ Square D` induced by a functor `C ⥤ D`. -/
@[simps]
def mapSquare (F : C ⥤ D) : Square C ⥤ Square D
    where
  obj sq := sq.map F
  map
    φ :=
    { τ₁ := F.map φ.τ₁
      τ₂ := F.map φ.τ₂
      τ₃ := F.map φ.τ₃
      τ₄ := F.map φ.τ₄
      comm₁₂ := by simpa only [Functor.map_comp] using F.congr_map φ.comm₁₂
      comm₁₃ := by simpa only [Functor.map_comp] using F.congr_map φ.comm₁₃
      comm₂₄ := by simpa only [Functor.map_comp] using F.congr_map φ.comm₂₄
      comm₃₄ := by simpa only [Functor.map_comp] using F.congr_map φ.comm₃₄ }
Похожие утверждения