Saturated subgroups

Tags

subgroup, subgroups

def Submonoid.PowSaturated {G : Type u_1} [Monoid G] (H : Submonoid G) : Prop

A submonoid H of G is saturated if for all n : ℕ and g : G with g^n ∈ H we have n = 0 or g ∈ H. We use the name PowSaturated to distinguish from Submonoid.MulSaturated.

Equations

• H.PowSaturated = ∀ ⦃n : ℕ⦄ ⦃g : G⦄, g ^ n ∈ H → n = 0 ∨ g ∈ H

def AddSubmonoid.NSMulSaturated {G : Type u_1} [AddMonoid G] (H : AddSubmonoid G) : Prop

An additive submonoid H of G is saturated if for all n : ℕ and g : G with n•g ∈ H we have n = 0 or g ∈ H. We use the name NSMulSaturated to distinguish from Submonoid.MulSaturated.

Equations

• H.NSMulSaturated = ∀ ⦃n : ℕ⦄ ⦃g : G⦄, n • g ∈ H → n = 0 ∨ g ∈ H

theorem Submonoid.powSaturated_iff_npow {G : Type u_1} [Monoid G] {H : Submonoid G} : H.PowSaturated ↔ ∀ (n : ℕ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H

theorem AddSubmonoid.nsmulSaturated_iff_nsmul {G : Type u_1} [AddMonoid G] {H : AddSubmonoid G} : H.NSMulSaturated ↔ ∀ (n : ℕ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H

theorem Subgroup.saturated_iff_zpow {G : Type u_1} [Group G] {H : Subgroup G} : H.PowSaturated ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H

theorem AddSubgroup.saturated_iff_zsmul {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.NSMulSaturated ↔ ∀ (n : ℤ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H

theorem AddSubmonoid.ker_saturated {A₁ : Type u_1} {A₂ : Type u_2} [AddGroup A₁] [AddMonoid A₂] [IsAddTorsionFree A₂] (f : A₁ →+ A₂) : f.ker.NSMulSaturated