English
For a given φ, the coinduced representation coind φ A provides an explicit H-representation whose carrier is the set of G-equivariant functions H → A.
Русский
Для данной φ, коиндукция coind φ A образует явное H-предствавление, носитель которого — множество G-эквариантных функций H → A.
LaTeX
$$$\text{coind }\phi\ A:\ Representation\ k\ H\ (coindV \ phi \ A).$$$
Lean4
/-- If `φ : G →* H` and `A : Rep k G` then `coind φ A` is the coinduction of `A` along `φ`,
defined by letting `H` act on the `G`-equivariant functions `H → A` by `(h • f) h₁ := f (h₁ * h)`.
-/
noncomputable abbrev coind : Rep k H :=
Rep.of (Representation.coind φ A.ρ)
