English
The natural isomorphism IndCoindNatIso is compatible with the action maps and the functors, ensuring the naturality of the Ind-Coind correspondence.
Русский
Естественное изоморфизнование IndCoindNatIso совместимо с отображениями действия и функторов, обеспечивая естественность соответствия Ind-Coind.
LaTeX
$$$$\text{IndCoindNatIso}(k,S)\;\text{is natural in }k,S.$$$$
Lean4
/-- Given a finite index subgroup `S ≤ G`, this is a natural isomorphism between the `Ind_S^G` and
`Coind_G^S` functors `Rep k S ⥤ Rep k G`. -/
@[simps! hom_app inv_app]
noncomputable def indCoindNatIso : indFunctor k S.subtype ≅ coindFunctor k S.subtype :=
NatIso.ofComponents (fun _ => indCoindIso _) fun f => by simp only [indFunctor_obj, coindFunctor_obj]; ext;
simp [indToCoindAux_comm]
