homEquiv_def — Mathlib

English

The hom-equivalence for ihom coincides with the standard Rep.homEquiv; the two adjunctions agree.

Русский

Гом-эквивалентность IHom совпадает с обычной HomEquiv для Rep; две сопряжённости совпадают.

LaTeX

$$$$ (\\ihom.adjunction A).homEquiv B C = Rep.homEquiv A B C. $$$$

Lean4

@[simp]
theorem homEquiv_def (A B C : Rep k G) : (ihom.adjunction A).homEquiv B C = Rep.homEquiv A B C :=
  congrFun (congrFun (Adjunction.mkOfHomEquiv_homEquiv _) _) _

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