English
Let S ≤ G be finite index and A a representation of S. There is a natural isomorphism between Ind_S^G(A) and Coind_S^G(A).
Русский
Пусть S ≤ G имеет конечный индекс, и A — репрезентация над S. Существует естественное изоморождение между Ind_S^G(A) и Coind_S^G(A).
LaTeX
$$$\text{IndCoindNatIso}:\; \text{indFunctor } k S.\text{subtype} \cong \text{coindFunctor } k S.\text{subtype}$$$
Lean4
/-- Let `S ≤ G` be a subgroup and `(A, ρ)` a `k`-linear `S`-representation. Then given `g : G` and
`a : A`, this is the function `G → A` sending `sg` to `ρ(s)(a)` for all `s : S` and everything else
to 0. -/
noncomputable def indToCoindAux (g : G) : A →ₗ[k] (G → A) :=
LinearMap.pi
(fun g₁ =>
if h : (QuotientGroup.rightRel S).r g₁ g then
A.ρ ⟨g₁ * g⁻¹, by rcases h with ⟨s, rfl⟩; exact mul_inv_cancel_right s.1 g ▸ s.2⟩
else 0)
