English
There is a canonical isomorphism between the two coinduced representations coind φ A and coind' φ A, induced by the underlying k-linear equivalence provided by the map coindVEquiv φ A.
Русский
Существует каноническое изоморфизмическое соответствие между двумя коиндукциями: coind φ A и coind' φ A, причем линейное эквивалентное отображение задаётся через коэффициентную связь coindVEquiv φ A.
LaTeX
$$$\mathrm{coind}\_\phi A \cong \mathrm{coind}'_\phi A$$$
Lean4
/-- `coind φ A` and `coind' φ A` are isomorphic representations, with the underlying
`k`-linear equivalence given by `coindVEquiv`. -/
@[simps! hom_hom_hom inv_hom_hom]
noncomputable def coindIso : coind φ A ≅ coind' φ A :=
Action.mkIso (coindVEquiv φ A).toModuleIso fun h => by
ext
simp [ModuleCat.endRingEquiv, leftRegularHomEquiv_symm_apply (leftRegular k H)]
