le_comap_ker — Mathlib

English

Let S be a normal subgroup of G and ρ a representation. For every g in G, the kernel of the restricted action ρ|_S is stable under ρ(g); equivalently, ρ(g) maps ker(ρ|_S) into ker(ρ|_S).

Русский

Пусть S — нормальная подгруппа G и ρ — представление. Для каждого g ∈ G ядро ограниченного действия ρ|_S сохраняется при действии ρ(g); то есть ρ(g) отображает ker(ρ|_S) в ker(ρ|_S).

LaTeX

$$$\\ker(\\rho|_{S}) \\leq ρ(g)^{-1}(\\ker(\\rho|_{S}))$ для всех $g\\in G$$$

Lean4

theorem le_comap_ker (g : G) : ker (ρ.comp S.subtype) ≤ (ker <| ρ.comp S.subtype).comap (ρ g) :=
  Submodule.span_le.2 fun _ ⟨⟨s, x⟩, hs⟩ => by
    simpa [← hs] using mem_ker_of_eq ⟨g * s * g⁻¹, Subgroup.Normal.conj_mem ‹_› s.1 s.2 g⟩ (ρ g x) _ <| by simp

Похожие утверждения