functor — Mathlib

English

The canonical functor between structured-arrow categories on the diagonal is an equivalence.

Русский

Канонический функтор между категориальными стрелками над диагональю образует эквивалентность.

LaTeX

$$$\mathrm{ofDiagEquivalence}(X): \mathrm{StructuredArrow}(X,\mathrm{diag}) \simeq \mathrm{StructuredArrow}(X.2, \mathrm{Under.forget}(X.1))$$$

Lean4

/-- The canonical functor from the structured arrow category on the diagonal functor
`T ⥤ T × T` to the structured arrow category on `Under.forget`. -/
@[simps!]
def functor (X : T × T) : StructuredArrow X (Functor.diag _) ⥤ StructuredArrow X.2 (Under.forget X.1) :=
  Functor.toStructuredArrow
    (Functor.toUnder (StructuredArrow.proj X _) _ (fun f => by exact f.hom.1) (fun m => by have := m.w; cat_disch)) _ _
    (fun f => f.hom.2) (fun m => by have := m.w; cat_disch)

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