English
Given a G →* H, the coinduced representation coind φ A is defined as an H-action on the space of G-equivariant functions H → A, with (h • f)(h1) = f(h1 h).
Русский
Дана гомоморфия φ: G →* H, коиндукция коind φ A действует на пространстве функций H → A так, что (h • f)(h1) = f(h1 h).
LaTeX
$$$\text{coind }\phi\ A:\ Type\_k\ H\text{ acting on } (H \to A)\text{ with } (h\cdot f)(h_1)=f(h_1\,h).$$$
Lean4
/-- If `ρ : Representation k G A` and `φ : G →* H` then `coind φ ρ` is the representation
coinduced by `ρ` along `φ`, defined as the following action of `H` on the submodule `coindV φ ρ`
of `G`-equivariant functions from `H` to `A`: we let `h : H` send the function `f : H → A`
to the function sending `h₁` to `f (h₁ * h)`.
See also `Rep.coind` and `Representation.coind'` for variants involving the category `Rep k G`.
-/
@[simps]
def coind : Representation k H (coindV φ ρ)
where
toFun h := (LinearMap.funLeft _ _ (· * h)).restrict fun x hx g h₁ => by simpa [mul_assoc] using hx g (h₁ * h)
map_one' := by ext; simp
map_mul' _ _ := by ext; simp [mul_assoc]
