instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants

English

For every g ∈ G, the kernel of ρ|_S is contained in the preimage under ρ(g) of that kernel; equivalently ker is stable under the action of g.

Русский

Для каждого g ∈ G ядро ρ|_S содержится в прообразе под ρ(g) этого ядра; ядро устойчиво по действию g.

LaTeX

$$ker (ρ.comp S.subtype) ≤ (ker (ρ.comp S.subtype)).comap (ρ g)$$

Lean4

instance : IsTrivial ((toCoinvariants ρ S).comp S.subtype) where
  out
    g := by
    ext x
    exact (Coinvariants.mk_eq_iff _).2 <| mem_ker_of_eq g x _ rfl

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