inverse — Mathlib

English

There is an inverse functor to the diagonal-structured-arrow functor, reversing the construction.

Русский

Существует обратный функтор к диагональному функтору структуры стрелок, обращающий конструктор.

LaTeX

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

Lean4

/-- The inverse functor of `ofDiagEquivalence.functor`. -/
@[simps!]
def inverse (X : T × T) : CostructuredArrow (Over.forget X.1) X.2 ⥤ CostructuredArrow (Functor.diag _) X :=
  Functor.toCostructuredArrow (CostructuredArrow.proj _ _ ⋙ Over.forget _) _ X (fun f => (f.left.hom, f.hom))
    (fun m => by have := m.w; cat_disch)

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