English
If W is a G-invariant submodule of V, then the quotient V/W inherits a natural representation of G induced by ρ, defined by the induced endomorphisms on the quotient.
Русский
Если W является инвариантным подмодулем, то тождественное отображение на V/W получает естественное представление от G, индуцированное ρ.
LaTeX
$$$\\rho^{V/W}(g) : V/W \\to V/W, \\; (\\rho^{V/W}(g))(v+W) = (\\rho(g)v) + W$$$
Lean4
/-- Given a `k`-linear `G`-representation `(V, ρ)` and a `G`-invariant `k`-submodule `W ≤ V`, this
is the representation induced on `V ⧸ W` by `ρ`. -/
@[simps]
def quotient (W : Submodule k V) (le_comap : ∀ g, W ≤ W.comap (ρ g)) : Representation k G (V ⧸ W)
where
toFun g := Submodule.mapQ _ _ (ρ g) <| le_comap g
map_one' := by ext; simp
map_mul' _ _ := by ext; simp
