English
The coind' construction is the coinduction along φ in the algebraic setting, delivering a representation of H from a representation of G.
Русский
Конструкция coind' даёт коиндукцию вдоль φ в алгебраическом случае, порождая представление H из представления G.
LaTeX
$$$\text{coind}'_{\phi} A := \mathrm{Rep}\ k G \to \mathrm{Rep}\ k H$ (конструкция коинд$'$).$$
Lean4
/-- If `φ : G →* H` and `A : Rep k G` then `coind' φ A`, the coinduction of `A` along `φ`,
is defined as an `H`-action on `Hom_{k[G]}(k[H], A)`. If `f : k[H] → A` is `G`-equivariant
then `(h • f) (r • h₁) := r • f (h₁ * h)`, where `r : k`.
-/
@[simps]
noncomputable def _root_.Representation.coind' : Representation k H ((Action.res _ φ).obj (leftRegular k H) ⟶ A)
where
toFun
h :=
{ toFun f := (Action.res _ φ).map ((leftRegularHomEquiv (leftRegular k H)).symm (single h 1)) ≫ f
map_add' _ _ := by rfl
map_smul' _ _ := by rfl }
map_one' := by
ext x : 3
refine lhom_ext' fun _ => LinearMap.ext_ring ?_
simp [leftRegularHomEquiv_symm_apply (leftRegular k H)]
map_mul' _
_ := by
ext x : 3
refine lhom_ext' fun _ => LinearMap.ext_ring ?_
simp [leftRegularHomEquiv_symm_apply (leftRegular k H), mul_assoc]
