ofDiagEquivalence' — Mathlib

English

A swapped-projection version of the diagonal equivalence exists between StructuredArrow X (diag) and Under.forget.

Русский

Существует эквивалентность со сменой ролей проекций между StructuredArrow X (diag) и Under.forget.

LaTeX

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

Lean4

/-- A version of `StructuredArrow.ofDiagEquivalence` with the roles of the first and second
projection swapped. -/
-- noncomputability is only for performance

noncomputable def ofDiagEquivalence' (X : T × T) :
    StructuredArrow X (Functor.diag _) ≌ StructuredArrow X.1 (Under.forget X.2) :=
  (ofDiagEquivalence X).trans <|
    (ofStructuredArrowProjEquivalence (𝟭 T) X.1 X.2).trans <| StructuredArrow.mapNatIso (Under.forget X.2).rightUnitor

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