English
The diagonal-StructuredArrow equivalence is an equivalence with explicit functor and inverse, forming an adjoint pair with unit and counit identities.
Русский
Эквивалентность структурированных стрелок по диагонали содержит явный функтор и обратный функтор, образуя пару с единичными и контр-единичными натуральными преобразованиями.
LaTeX
$$$\mathrm{ofDiagEquivalence}(X): \mathrm{StructuredArrow}(X,\mathrm{diag}) \simeq \mathrm{StructuredArrow}(X.2,\mathrm{Under.forget}(X.1))$$$
Lean4
/-- Characterization of the costructured arrow category on the diagonal functor `T ⥤ T × T`. -/
def ofDiagEquivalence (X : T × T) : CostructuredArrow (Functor.diag _) X ≌ CostructuredArrow (Over.forget X.1) X.2
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)
