ofDiagEquivalence — Mathlib

English

The equivalence on Diag expresses an isomorphism of structured-arrow categories along the diagonal functor.

Русский

Эквивалентность на диагонали выражает изоморфизм категорий структурированных стрелок по диагональному функтору.

LaTeX

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

Lean4

/-- Characterization of the structured arrow category on the diagonal functor `T ⥤ T × T`. -/
def ofDiagEquivalence (X : T × T) : StructuredArrow X (Functor.diag _) ≌ StructuredArrow X.2 (Under.forget X.1)
    where
  functor := ofDiagEquivalence.functor X
  inverse := ofDiagEquivalence.inverse X
  unitIso := NatIso.ofComponents (fun _ => Iso.refl _) (by simp)
  counitIso := NatIso.ofComponents (fun _ => Iso.refl _) (by cat_disch)

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