English
Let S ≤ G be a finite-index subgroup. The restriction functor from G-representations to S-representations has Ind_S^G as right adjoint, and this adjunction is realized by resIndAdjunction.
Русский
Пусть S ≤ G имеет конечный индекс. Функтор ограничения представлений G на представления S имеет в качестве правого смежного F(S)Ind_S^G, и это смежность реализуется через resIndAdjunction.
LaTeX
$$$\text{resIndAdjunction } k S \dashv\ indFunctor k S.\subtype$$$
Lean4
/-- Let `S ≤ G` be a finite index subgroup, `g₁, ..., gₙ` a set of right coset representatives of
`S`, and `A` a `k`-linear `S`-representation. This is the `k`-linear map
`Coind_S^G(A) →ₗ[k] Ind_S^G(A)` sending `f : G → A` to `∑ᵢ ⟦gᵢ ⊗ₜ[k] f(gᵢ)⟧` for `1 ≤ i ≤ n`. -/
@[simps]
noncomputable def coindToInd : coind S.subtype A →ₗ[k] ind S.subtype A
where
toFun
f :=
∑ g : Quotient (QuotientGroup.rightRel S),
Quotient.liftOn g (fun g => IndV.mk S.subtype _ g (f.1 g)) fun g₁ g₂ ⟨s, (hs : _ * _ = _)⟩ =>
(Submodule.Quotient.eq _).2 <|
Coinvariants.mem_ker_of_eq s (single g₂ 1 ⊗ₜ[k] f.1 g₂) _ <| by have := f.2 s g₂; simp_all
map_add' _
_ := by
simpa [← Finset.sum_add_distrib, TensorProduct.tmul_add] using
Finset.sum_congr rfl fun z _ => Quotient.inductionOn z fun _ => by simp
map_smul' _
_ := by simpa [Finset.smul_sum] using Finset.sum_congr rfl fun z _ => Quotient.inductionOn z fun _ => by simp
