functor — Mathlib

Lean4
/-- Given `w : TwoSquare T L R B` and a morphism `g : R.obj X₂ ⟶ B.obj X₃`, this is
the obvious functor `w.StructuredArrowRightwards g ⥤ w.CostructuredArrowDownwards g`. -/
@[simps]
def functor : w.StructuredArrowRightwards g ⥤ w.CostructuredArrowDownwards g
    where
  obj
    f :=
    CostructuredArrow.mk (Y := StructuredArrow.mk f.hom.left)
      (StructuredArrow.homMk f.right.hom (by simpa using CostructuredArrow.w f.hom))
  map {f₁ f₂}
    φ :=
    CostructuredArrow.homMk (StructuredArrow.homMk φ.right.left (by dsimp; rw [← StructuredArrow.w φ]; rfl))
      (by ext; exact CostructuredArrow.w φ.right)
  map_id _ := rfl
  map_comp _ _ := rfl
Похожие утверждения