inverse — Mathlib

English

The inverse functor to the equivalence of StructuredArrow given by ofDiagEquivalence.functor is explicitly constructed as described.

Русский

Обратный функтор эквивалентности StructuredArrow, задаваемой через ofDiagEquivalence.functor, конструктивно задан явно.

LaTeX

$$$ \text{inverse}(X) : \text{StructuredArrow} \to \text{StructuredArrow} $ (explicitly constructed as in the statement)$$

Lean4

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

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