Lattice structure of subgroups

We prove subgroups of a group form a complete lattice.

There are also theorems about the subgroups generated by an element or a subset of a group, defined both inductively and as the infimum of the set of subgroups containing a given element/subset.

Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.

Main definitions

Notation used here:

• G is a Group

• k is a set of elements of type G

Definitions in the file:

• CompleteLattice (Subgroup G) : the subgroups of G form a complete lattice

• Subgroup.closure k : the minimal subgroup that includes the set k

• Subgroup.gi : closure forms a Galois insertion with the coercion to set

Implementation notes

Subgroup inclusion is denoted ≤ rather than ⊆, although ∈ is defined as membership of a subgroup's underlying set.

Tags

subgroup, subgroups

Conversion to/from Additive/Multiplicative

def Subgroup.toAddSubgroup {G : Type u_1} [Group G] : Subgroup G ≃o AddSubgroup (Additive G)

Subgroups of a group G are isomorphic to additive subgroups of Additive G.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Subgroup.coe_toAddSubgroup_apply {G : Type u_1} [Group G] (S : Subgroup G) : ↑(toAddSubgroup S) = ⇑Additive.toMul ⁻¹' ↑S

@[simp]

theorem Subgroup.coe_toAddSubgroup_symm_apply {G : Type u_1} [Group G] (S : AddSubgroup (Additive G)) : ↑((RelIso.symm toAddSubgroup) S) = ⇑Multiplicative.toAdd ⁻¹' ↑S

@[reducible, inline]

abbrev AddSubgroup.toSubgroup' {G : Type u_1} [Group G] : AddSubgroup (Additive G) ≃o Subgroup G

Additive subgroup of an additive group Additive G are isomorphic to subgroup of G.

Equations

• AddSubgroup.toSubgroup' = Subgroup.toAddSubgroup.symm

def AddSubgroup.toSubgroup {A : Type u_2} [AddGroup A] : AddSubgroup A ≃o Subgroup (Multiplicative A)

Additive subgroups of an additive group A are isomorphic to subgroups of Multiplicative A.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddSubgroup.coe_toSubgroup_symm_apply {A : Type u_2} [AddGroup A] (S : Subgroup (Multiplicative A)) : ↑((RelIso.symm toSubgroup) S) = ⇑Additive.toMul ⁻¹' ↑S

@[simp]

theorem AddSubgroup.coe_toSubgroup_apply {A : Type u_2} [AddGroup A] (S : AddSubgroup A) : ↑(toSubgroup S) = ⇑Multiplicative.toAdd ⁻¹' ↑S

@[reducible, inline]

abbrev Subgroup.toAddSubgroup' {A : Type u_2} [AddGroup A] : Subgroup (Multiplicative A) ≃o AddSubgroup A

Subgroups of an additive group Multiplicative A are isomorphic to additive subgroups of A.

Equations

• Subgroup.toAddSubgroup' = AddSubgroup.toSubgroup.symm

instance Subgroup.instTop {G : Type u_1} [Group G] : Top (Subgroup G)

The subgroup G of the group G.

Equations

• Subgroup.instTop = { top := let __src := ⊤; { toSubmonoid := __src, inv_mem' := ⋯ } }

instance AddSubgroup.instTop {G : Type u_1} [AddGroup G] : Top (AddSubgroup G)

The AddSubgroup G of the AddGroup G.

Equations

• AddSubgroup.instTop = { top := let __src := ⊤; { toAddSubmonoid := __src, neg_mem' := ⋯ } }

def Subgroup.topEquiv {G : Type u_1} [Group G] : ↥⊤ ≃* G

The top subgroup is isomorphic to the group.

This is the group version of Submonoid.topEquiv.

Equations

• Subgroup.topEquiv = Submonoid.topEquiv

def AddSubgroup.topEquiv {G : Type u_1} [AddGroup G] : ↥⊤ ≃+ G

The top additive subgroup is isomorphic to the additive group.

This is the additive group version of AddSubmonoid.topEquiv.

Equations

• AddSubgroup.topEquiv = AddSubmonoid.topEquiv

@[simp]

theorem AddSubgroup.topEquiv_symm_apply_coe {G : Type u_1} [AddGroup G] (x : G) : ↑(topEquiv.symm x) = x

@[simp]

theorem Subgroup.topEquiv_apply {G : Type u_1} [Group G] (x : ↥⊤) : topEquiv x = ↑x

@[simp]

theorem AddSubgroup.topEquiv_apply {G : Type u_1} [AddGroup G] (x : ↥⊤) : topEquiv x = ↑x

@[simp]

theorem Subgroup.topEquiv_symm_apply_coe {G : Type u_1} [Group G] (x : G) : ↑(topEquiv.symm x) = x

instance Subgroup.instBot {G : Type u_1} [Group G] : Bot (Subgroup G)

The trivial subgroup {1} of a group G.

Equations

• Subgroup.instBot = { bot := let __src := ⊥; { toSubmonoid := __src, inv_mem' := ⋯ } }

instance AddSubgroup.instBot {G : Type u_1} [AddGroup G] : Bot (AddSubgroup G)

The trivial AddSubgroup {0} of an AddGroup G.

Equations

• AddSubgroup.instBot = { bot := let __src := ⊥; { toAddSubmonoid := __src, neg_mem' := ⋯ } }

instance Subgroup.instInhabited {G : Type u_1} [Group G] : Inhabited (Subgroup G)

Equations

• Subgroup.instInhabited = { default := ⊥ }

instance AddSubgroup.instInhabited {G : Type u_1} [AddGroup G] : Inhabited (AddSubgroup G)

Equations

• AddSubgroup.instInhabited = { default := ⊥ }

@[simp]

theorem Subgroup.mem_bot {G : Type u_1} [Group G] {x : G} : x ∈ ⊥ ↔ x = 1

@[simp]

theorem AddSubgroup.mem_bot {G : Type u_1} [AddGroup G] {x : G} : x ∈ ⊥ ↔ x = 0

@[simp]

theorem Subgroup.mem_top {G : Type u_1} [Group G] (x : G) : x ∈ ⊤

@[simp]

theorem AddSubgroup.mem_top {G : Type u_1} [AddGroup G] (x : G) : x ∈ ⊤

@[simp]

theorem Subgroup.coe_top {G : Type u_1} [Group G] : ↑⊤ = Set.univ

@[simp]

theorem AddSubgroup.coe_top {G : Type u_1} [AddGroup G] : ↑⊤ = Set.univ

@[simp]

theorem Subgroup.coe_bot {G : Type u_1} [Group G] : ↑⊥ = {1}

@[simp]

theorem AddSubgroup.coe_bot {G : Type u_1} [AddGroup G] : ↑⊥ = {0}

instance Subgroup.instUniqueSubtypeMemBot {G : Type u_1} [Group G] : Unique ↥⊥

Equations

• Subgroup.instUniqueSubtypeMemBot = { default := 1, uniq := ⋯ }

instance AddSubgroup.instUniqueSubtypeMemBot {G : Type u_1} [AddGroup G] : Unique ↥⊥

Equations

• AddSubgroup.instUniqueSubtypeMemBot = { default := 0, uniq := ⋯ }

@[simp]

theorem Subgroup.top_toSubmonoid {G : Type u_1} [Group G] : ⊤.toSubmonoid = ⊤

@[simp]

theorem AddSubgroup.top_toAddSubmonoid {G : Type u_1} [AddGroup G] : ⊤.toAddSubmonoid = ⊤

@[simp]

theorem Subgroup.bot_toSubmonoid {G : Type u_1} [Group G] : ⊥.toSubmonoid = ⊥

@[simp]

theorem AddSubgroup.bot_toAddSubmonoid {G : Type u_1} [AddGroup G] : ⊥.toAddSubmonoid = ⊥

theorem Subgroup.eq_bot_iff_forall {G : Type u_1} [Group G] (H : Subgroup G) : H = ⊥ ↔ ∀ x ∈ H, x = 1

theorem AddSubgroup.eq_bot_iff_forall {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H = ⊥ ↔ ∀ x ∈ H, x = 0

theorem Subgroup.eq_bot_of_subsingleton {G : Type u_1} [Group G] (H : Subgroup G) [Subsingleton ↥H] : H = ⊥

theorem AddSubgroup.eq_bot_of_subsingleton {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Subsingleton ↥H] : H = ⊥

@[simp]

theorem Subgroup.coe_eq_univ {G : Type u_1} [Group G] {H : Subgroup G} : ↑H = Set.univ ↔ H = ⊤

@[simp]

theorem AddSubgroup.coe_eq_univ {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : ↑H = Set.univ ↔ H = ⊤

theorem Subgroup.coe_eq_singleton {G : Type u_1} [Group G] {H : Subgroup G} : (∃ (g : G), ↑H = {g}) ↔ H = ⊥

theorem AddSubgroup.coe_eq_singleton {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : (∃ (g : G), ↑H = {g}) ↔ H = ⊥

theorem Subgroup.nontrivial_iff_exists_ne_one {G : Type u_1} [Group G] (H : Subgroup G) : Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 1

theorem AddSubgroup.nontrivial_iff_exists_ne_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 0

theorem Subgroup.exists_ne_one_of_nontrivial {G : Type u_1} [Group G] (H : Subgroup G) [Nontrivial ↥H] : ∃ x ∈ H, x ≠ 1

theorem AddSubgroup.exists_ne_zero_of_nontrivial {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Nontrivial ↥H] : ∃ x ∈ H, x ≠ 0

theorem Subgroup.nontrivial_iff_ne_bot {G : Type u_1} [Group G] (H : Subgroup G) : Nontrivial ↥H ↔ H ≠ ⊥

theorem AddSubgroup.nontrivial_iff_ne_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Nontrivial ↥H ↔ H ≠ ⊥

theorem Subgroup.bot_or_nontrivial {G : Type u_1} [Group G] (H : Subgroup G) : H = ⊥ ∨ Nontrivial ↥H

A subgroup is either the trivial subgroup or nontrivial.

theorem AddSubgroup.bot_or_nontrivial {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H = ⊥ ∨ Nontrivial ↥H

A subgroup is either the trivial subgroup or nontrivial.

theorem Subgroup.bot_or_exists_ne_one {G : Type u_1} [Group G] (H : Subgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ 1

A subgroup is either the trivial subgroup or contains a non-identity element.

theorem AddSubgroup.bot_or_exists_ne_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ 0

A subgroup is either the trivial subgroup or contains a nonzero element.

theorem Subgroup.ne_bot_iff_exists_ne_one {G : Type u_1} [Group G] {H : Subgroup G} : H ≠ ⊥ ↔ ∃ (a : ↥H), a ≠ 1

theorem AddSubgroup.ne_bot_iff_exists_ne_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H ≠ ⊥ ↔ ∃ (a : ↥H), a ≠ 0

instance Subgroup.instMin {G : Type u_1} [Group G] : Min (Subgroup G)

The inf of two subgroups is their intersection.

Equations

• Subgroup.instMin = { min := fun (H₁ H₂ : Subgroup G) => let __src := H₁.toSubmonoid ⊓ H₂.toSubmonoid; { toSubmonoid := __src, inv_mem' := ⋯ } }

instance AddSubgroup.instMin {G : Type u_1} [AddGroup G] : Min (AddSubgroup G)

The inf of two AddSubgroups is their intersection.

Equations

• AddSubgroup.instMin = { min := fun (H₁ H₂ : AddSubgroup G) => let __src := H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid; { toAddSubmonoid := __src, neg_mem' := ⋯ } }

@[simp]

theorem Subgroup.coe_inf {G : Type u_1} [Group G] (p p' : Subgroup G) : ↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem AddSubgroup.coe_inf {G : Type u_1} [AddGroup G] (p p' : AddSubgroup G) : ↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem Subgroup.mem_inf {G : Type u_1} [Group G] {p p' : Subgroup G} {x : G} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

@[simp]

theorem AddSubgroup.mem_inf {G : Type u_1} [AddGroup G] {p p' : AddSubgroup G} {x : G} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

instance Subgroup.instInfSet {G : Type u_1} [Group G] : InfSet (Subgroup G)

Equations

• Subgroup.instInfSet = { sInf := fun (s : Set (Subgroup G)) => let __src := (⨅ S ∈ s, S.toSubmonoid).copy (⋂ S ∈ s, ↑S) ⋯; { toSubmonoid := __src, inv_mem' := ⋯ } }

instance AddSubgroup.instInfSet {G : Type u_1} [AddGroup G] : InfSet (AddSubgroup G)

Equations

• AddSubgroup.instInfSet = { sInf := fun (s : Set (AddSubgroup G)) => let __src := (⨅ S ∈ s, S.toAddSubmonoid).copy (⋂ S ∈ s, ↑S) ⋯; { toAddSubmonoid := __src, neg_mem' := ⋯ } }

@[simp]

theorem Subgroup.coe_sInf {G : Type u_1} [Group G] (H : Set (Subgroup G)) : ↑(sInf H) = ⋂ s ∈ H, ↑s

@[simp]

theorem AddSubgroup.coe_sInf {G : Type u_1} [AddGroup G] (H : Set (AddSubgroup G)) : ↑(sInf H) = ⋂ s ∈ H, ↑s

@[simp]

theorem Subgroup.mem_sInf {G : Type u_1} [Group G] {S : Set (Subgroup G)} {x : G} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

@[simp]

theorem AddSubgroup.mem_sInf {G : Type u_1} [AddGroup G] {S : Set (AddSubgroup G)} {x : G} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

theorem Subgroup.mem_iInf {G : Type u_1} [Group G] {ι : Sort u_2} {S : ι → Subgroup G} {x : G} : x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

theorem AddSubgroup.mem_iInf {G : Type u_1} [AddGroup G] {ι : Sort u_2} {S : ι → AddSubgroup G} {x : G} : x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

@[simp]

theorem Subgroup.coe_iInf {G : Type u_1} [Group G] {ι : Sort u_2} {S : ι → Subgroup G} : ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

@[simp]

theorem AddSubgroup.coe_iInf {G : Type u_1} [AddGroup G] {ι : Sort u_2} {S : ι → AddSubgroup G} : ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

instance Subgroup.instCompleteLattice {G : Type u_1} [Group G] : CompleteLattice (Subgroup G)

Subgroups of a group form a complete lattice.

Equations

• One or more equations did not get rendered due to their size.

instance AddSubgroup.instCompleteLattice {G : Type u_1} [AddGroup G] : CompleteLattice (AddSubgroup G)

The AddSubgroups of an AddGroup form a complete lattice.

Equations

• One or more equations did not get rendered due to their size.

theorem Subgroup.mem_sup_left {G : Type u_1} [Group G] {S T : Subgroup G} {x : G} : x ∈ S → x ∈ S ⊔ T

theorem AddSubgroup.mem_sup_left {G : Type u_1} [AddGroup G] {S T : AddSubgroup G} {x : G} : x ∈ S → x ∈ S ⊔ T

theorem Subgroup.mem_sup_right {G : Type u_1} [Group G] {S T : Subgroup G} {x : G} : x ∈ T → x ∈ S ⊔ T

theorem AddSubgroup.mem_sup_right {G : Type u_1} [AddGroup G] {S T : AddSubgroup G} {x : G} : x ∈ T → x ∈ S ⊔ T

theorem Subgroup.mul_mem_sup {G : Type u_1} [Group G] {S T : Subgroup G} {x y : G} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T

theorem AddSubgroup.add_mem_sup {G : Type u_1} [AddGroup G] {S T : AddSubgroup G} {x y : G} (hx : x ∈ S) (hy : y ∈ T) : x + y ∈ S ⊔ T

theorem Subgroup.mem_iSup_of_mem {G : Type u_1} [Group G] {ι : Sort u_2} {S : ι → Subgroup G} (i : ι) {x : G} : x ∈ S i → x ∈ iSup S

theorem AddSubgroup.mem_iSup_of_mem {G : Type u_1} [AddGroup G] {ι : Sort u_2} {S : ι → AddSubgroup G} (i : ι) {x : G} : x ∈ S i → x ∈ iSup S

theorem Subgroup.mem_sSup_of_mem {G : Type u_1} [Group G] {S : Set (Subgroup G)} {s : Subgroup G} (hs : s ∈ S) {x : G} : x ∈ s → x ∈ sSup S

theorem AddSubgroup.mem_sSup_of_mem {G : Type u_1} [AddGroup G] {S : Set (AddSubgroup G)} {s : AddSubgroup G} (hs : s ∈ S) {x : G} : x ∈ s → x ∈ sSup S

@[simp]

theorem Subgroup.subsingleton_iff {G : Type u_1} [Group G] : Subsingleton (Subgroup G) ↔ Subsingleton G

@[simp]

theorem AddSubgroup.subsingleton_iff {G : Type u_1} [AddGroup G] : Subsingleton (AddSubgroup G) ↔ Subsingleton G

@[simp]

theorem Subgroup.nontrivial_iff {G : Type u_1} [Group G] : Nontrivial (Subgroup G) ↔ Nontrivial G

@[simp]

theorem AddSubgroup.nontrivial_iff {G : Type u_1} [AddGroup G] : Nontrivial (AddSubgroup G) ↔ Nontrivial G

instance Subgroup.instUniqueOfSubsingleton {G : Type u_1} [Group G] [Subsingleton G] : Unique (Subgroup G)

Equations

• Subgroup.instUniqueOfSubsingleton = { default := ⊥, uniq := ⋯ }

instance AddSubgroup.instUniqueOfSubsingleton {G : Type u_1} [AddGroup G] [Subsingleton G] : Unique (AddSubgroup G)

Equations

• AddSubgroup.instUniqueOfSubsingleton = { default := ⊥, uniq := ⋯ }

instance Subgroup.instNontrivial {G : Type u_1} [Group G] [Nontrivial G] : Nontrivial (Subgroup G)

instance AddSubgroup.instNontrivial {G : Type u_1} [AddGroup G] [Nontrivial G] : Nontrivial (AddSubgroup G)

instance Subgroup.instNontrivialSubtypeMemTop {G : Type u_1} [Group G] [Nontrivial G] : Nontrivial ↥⊤

instance AddSubgroup.instNontrivialSubtypeMemTop {G : Type u_1} [AddGroup G] [Nontrivial G] : Nontrivial ↥⊤

theorem Subgroup.eq_top_iff' {G : Type u_1} [Group G] (H : Subgroup G) : H = ⊤ ↔ ∀ (x : G), x ∈ H

theorem AddSubgroup.eq_top_iff' {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H = ⊤ ↔ ∀ (x : G), x ∈ H

def Subgroup.closure {G : Type u_1} [Group G] (k : Set G) : Subgroup G

The Subgroup generated by a set.

Equations

• Subgroup.closure k = sInf {K : Subgroup G | k ⊆ ↑K}

def AddSubgroup.closure {G : Type u_1} [AddGroup G] (k : Set G) : AddSubgroup G

The AddSubgroup generated by a set

Equations

• AddSubgroup.closure k = sInf {K : AddSubgroup G | k ⊆ ↑K}

theorem Subgroup.mem_closure {G : Type u_1} [Group G] {k : Set G} {x : G} : x ∈ closure k ↔ ∀ (K : Subgroup G), k ⊆ ↑K → x ∈ K

theorem AddSubgroup.mem_closure {G : Type u_1} [AddGroup G] {k : Set G} {x : G} : x ∈ closure k ↔ ∀ (K : AddSubgroup G), k ⊆ ↑K → x ∈ K

@[simp]

theorem Subgroup.subset_closure {G : Type u_1} [Group G] {k : Set G} : k ⊆ ↑(closure k)

The subgroup generated by a set includes the set.

@[simp]

theorem AddSubgroup.subset_closure {G : Type u_1} [AddGroup G] {k : Set G} : k ⊆ ↑(closure k)

The AddSubgroup generated by a set includes the set.

theorem Subgroup.mem_closure_of_mem {G : Type u_1} [Group G] {s : Set G} {x : G} (hx : x ∈ s) : x ∈ closure s

theorem AddSubgroup.mem_closure_of_mem {G : Type u_1} [AddGroup G] {s : Set G} {x : G} (hx : x ∈ s) : x ∈ closure s

theorem Subgroup.notMem_of_notMem_closure {G : Type u_1} [Group G] {k : Set G} {P : G} (hP : P ∉ closure k) : P ∉ k

theorem AddSubgroup.notMem_of_notMem_closure {G : Type u_1} [AddGroup G] {k : Set G} {P : G} (hP : P ∉ closure k) : P ∉ k

@[deprecated AddSubgroup.notMem_of_notMem_closure (since := "2025-05-23")]

theorem AddSubgroup.not_mem_of_not_mem_closure {G : Type u_1} [AddGroup G] {k : Set G} {P : G} (hP : P ∉ closure k) : P ∉ k

Alias of AddSubgroup.notMem_of_notMem_closure.

@[deprecated Subgroup.notMem_of_notMem_closure (since := "2025-05-23")]

theorem Subgroup.not_mem_of_not_mem_closure {G : Type u_1} [Group G] {k : Set G} {P : G} (hP : P ∉ closure k) : P ∉ k

Alias of Subgroup.notMem_of_notMem_closure.

@[simp]

theorem Subgroup.closure_le {G : Type u_1} [Group G] (K : Subgroup G) {k : Set G} : closure k ≤ K ↔ k ⊆ ↑K

A subgroup K includes closure k if and only if it includes k.

@[simp]

theorem AddSubgroup.closure_le {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {k : Set G} : closure k ≤ K ↔ k ⊆ ↑K

An additive subgroup K includes closure k if and only if it includes k

theorem Subgroup.closure_eq_of_le {G : Type u_1} [Group G] (K : Subgroup G) {k : Set G} (h₁ : k ⊆ ↑K) (h₂ : K ≤ closure k) : closure k = K

theorem AddSubgroup.closure_eq_of_le {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {k : Set G} (h₁ : k ⊆ ↑K) (h₂ : K ≤ closure k) : closure k = K

theorem Subgroup.closure_induction {G : Type u_1} [Group G] {k : Set G} {p : (g : G) → g ∈ closure k → Prop} (mem : ∀ (x : G) (hx : x ∈ k), p x ⋯) (one : p 1 ⋯) (mul : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x hx → p y hy → p (x * y) ⋯) (inv : ∀ (x : G) (hx : x ∈ closure k), p x hx → p x⁻¹ ⋯) {x : G} (hx : x ∈ closure k) : p x hx

An induction principle for closure membership. If p holds for 1 and all elements of k, and is preserved under multiplication and inverse, then p holds for all elements of the closure of k.

See also Subgroup.closure_induction_left and Subgroup.closure_induction_right for versions that only require showing p is preserved by multiplication by elements in k.

theorem AddSubgroup.closure_induction {G : Type u_1} [AddGroup G] {k : Set G} {p : (g : G) → g ∈ closure k → Prop} (mem : ∀ (x : G) (hx : x ∈ k), p x ⋯) (zero : p 0 ⋯) (add : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x hx → p y hy → p (x + y) ⋯) (neg : ∀ (x : G) (hx : x ∈ closure k), p x hx → p (-x) ⋯) {x : G} (hx : x ∈ closure k) : p x hx

An induction principle for additive closure membership. If p holds for 0 and all elements of k, and is preserved under addition and inverses, then p holds for all elements of the additive closure of k.

See also AddSubgroup.closure_induction_left and AddSubgroup.closure_induction_left for versions that only require showing p is preserved by addition by elements in k.

theorem Subgroup.closure_induction₂ {G : Type u_1} [Group G] {k : Set G} {p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop} (mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯) (one_left : ∀ (x : G) (hx : x ∈ closure k), p 1 x ⋯ hx) (one_right : ∀ (x : G) (hx : x ∈ closure k), p x 1 hx ⋯) (mul_left : ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) (mul_right : ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) (inv_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x⁻¹ y ⋯ hy) (inv_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x y⁻¹ hx ⋯) {x y : G} (hx : x ∈ closure k) (hy : y ∈ closure k) : p x y hx hy

An induction principle for closure membership for predicates with two arguments.

theorem AddSubgroup.closure_induction₂ {G : Type u_1} [AddGroup G] {k : Set G} {p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop} (mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯) (zero_left : ∀ (x : G) (hx : x ∈ closure k), p 0 x ⋯ hx) (zero_right : ∀ (x : G) (hx : x ∈ closure k), p x 0 hx ⋯) (add_left : ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (neg_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p (-x) y ⋯ hy) (neg_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x (-y) hx ⋯) {x y : G} (hx : x ∈ closure k) (hy : y ∈ closure k) : p x y hx hy

An induction principle for additive closure membership, for predicates with two arguments.

@[simp]

theorem Subgroup.closure_closure_coe_preimage {G : Type u_1} [Group G] {k : Set G} : closure (Subtype.val ⁻¹' k) = ⊤

@[simp]

theorem AddSubgroup.closure_closure_coe_preimage {G : Type u_1} [AddGroup G] {k : Set G} : closure (Subtype.val ⁻¹' k) = ⊤

def Subgroup.gi (G : Type u_1) [Group G] : GaloisInsertion closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations

• Subgroup.gi G = { choice := fun (s : Set G) (x : ↑(Subgroup.closure s) ≤ s) => Subgroup.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

def AddSubgroup.gi (G : Type u_1) [AddGroup G] : GaloisInsertion closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations

• AddSubgroup.gi G = { choice := fun (s : Set G) (x : ↑(AddSubgroup.closure s) ≤ s) => AddSubgroup.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

theorem Subgroup.closure_mono {G : Type u_1} [Group G] ⦃h k : Set G⦄ (h' : h ⊆ k) : closure h ≤ closure k

Subgroup closure of a set is monotone in its argument: if h ⊆ k, then closure h ≤ closure k.

theorem AddSubgroup.closure_mono {G : Type u_1} [AddGroup G] ⦃h k : Set G⦄ (h' : h ⊆ k) : closure h ≤ closure k

Additive subgroup closure of a set is monotone in its argument: if h ⊆ k, then closure h ≤ closure k

@[simp]

theorem Subgroup.closure_eq {G : Type u_1} [Group G] (K : Subgroup G) : closure ↑K = K

Closure of a subgroup K equals K.

@[simp]

theorem AddSubgroup.closure_eq {G : Type u_1} [AddGroup G] (K : AddSubgroup G) : closure ↑K = K

Additive closure of an additive subgroup K equals K

@[simp]

theorem Subgroup.closure_empty {G : Type u_1} [Group G] : closure ∅ = ⊥

@[simp]

theorem AddSubgroup.closure_empty {G : Type u_1} [AddGroup G] : closure ∅ = ⊥

@[simp]

theorem Subgroup.closure_univ {G : Type u_1} [Group G] : closure Set.univ = ⊤

@[simp]

theorem AddSubgroup.closure_univ {G : Type u_1} [AddGroup G] : closure Set.univ = ⊤

theorem Subgroup.closure_union {G : Type u_1} [Group G] (s t : Set G) : closure (s ∪ t) = closure s ⊔ closure t

theorem AddSubgroup.closure_union {G : Type u_1} [AddGroup G] (s t : Set G) : closure (s ∪ t) = closure s ⊔ closure t

theorem Subgroup.sup_eq_closure {G : Type u_1} [Group G] (H H' : Subgroup G) : H ⊔ H' = closure (↑H ∪ ↑H')

theorem AddSubgroup.sup_eq_closure {G : Type u_1} [AddGroup G] (H H' : AddSubgroup G) : H ⊔ H' = closure (↑H ∪ ↑H')

theorem Subgroup.closure_iUnion {G : Type u_1} [Group G] {ι : Sort u_2} (s : ι → Set G) : closure (⋃ (i : ι), s i) = ⨆ (i : ι), closure (s i)

theorem AddSubgroup.closure_iUnion {G : Type u_1} [AddGroup G] {ι : Sort u_2} (s : ι → Set G) : closure (⋃ (i : ι), s i) = ⨆ (i : ι), closure (s i)

@[simp]

theorem Subgroup.closure_eq_bot_iff {G : Type u_1} [Group G] {k : Set G} : closure k = ⊥ ↔ k ⊆ {1}

@[simp]

theorem AddSubgroup.closure_eq_bot_iff {G : Type u_1} [AddGroup G] {k : Set G} : closure k = ⊥ ↔ k ⊆ {0}

theorem Subgroup.iSup_eq_closure {G : Type u_1} [Group G] {ι : Sort u_2} (p : ι → Subgroup G) : ⨆ (i : ι), p i = closure (⋃ (i : ι), ↑(p i))

theorem AddSubgroup.iSup_eq_closure {G : Type u_1} [AddGroup G] {ι : Sort u_2} (p : ι → AddSubgroup G) : ⨆ (i : ι), p i = closure (⋃ (i : ι), ↑(p i))

theorem Subgroup.mem_closure_singleton {G : Type u_1} [Group G] {x y : G} : y ∈ closure {x} ↔ ∃ (n : ℤ), x ^ n = y

The subgroup generated by an element of a group equals the set of integer number powers of the element.

theorem AddSubgroup.mem_closure_singleton {G : Type u_1} [AddGroup G] {x y : G} : y ∈ closure {x} ↔ ∃ (n : ℤ), n • x = y

The AddSubgroup generated by an element of an AddGroup equals the set of natural number multiples of the element.

theorem Subgroup.closure_singleton_one {G : Type u_1} [Group G] : closure {1} = ⊥

theorem AddSubgroup.closure_singleton_zero {G : Type u_1} [AddGroup G] : closure {0} = ⊥

@[simp]

theorem Subgroup.mem_closure_singleton_self {G : Type u_1} [Group G] (x : G) : x ∈ closure {x}

@[simp]

theorem AddSubgroup.mem_closure_singleton_self {G : Type u_1} [AddGroup G] (x : G) : x ∈ closure {x}

theorem Subgroup.le_closure_toSubmonoid {G : Type u_1} [Group G] (S : Set G) : Submonoid.closure S ≤ (closure S).toSubmonoid

theorem AddSubgroup.le_closure_toAddSubmonoid {G : Type u_1} [AddGroup G] (S : Set G) : AddSubmonoid.closure S ≤ (closure S).toAddSubmonoid

theorem Subgroup.closure_eq_top_of_mclosure_eq_top {G : Type u_1} [Group G] {S : Set G} (h : Submonoid.closure S = ⊤) : closure S = ⊤

theorem AddSubgroup.closure_eq_top_of_mclosure_eq_top {G : Type u_1} [AddGroup G] {S : Set G} (h : AddSubmonoid.closure S = ⊤) : closure S = ⊤

@[simp]

theorem Subgroup.closure_insert_one {G : Type u_1} [Group G] (s : Set G) : closure (insert 1 s) = closure s

@[simp]

theorem AddSubgroup.closure_insert_zero {G : Type u_1} [AddGroup G] (s : Set G) : closure (insert 0 s) = closure s

theorem Subgroup.closure_union_one {G : Type u_1} [Group G] (s : Set G) : closure (s ∪ {1}) = closure s

theorem AddSubgroup.closure_union_zero {G : Type u_1} [AddGroup G] (s : Set G) : closure (s ∪ {0}) = closure s

@[simp]

theorem Subgroup.closure_diff_one {G : Type u_1} [Group G] (s : Set G) : closure (s \ {1}) = closure s

@[simp]

theorem AddSubgroup.closure_diff_zero {G : Type u_1} [AddGroup G] (s : Set G) : closure (s \ {0}) = closure s

theorem Subgroup.toAddSubgroup_closure {G : Type u_1} [Group G] (S : Set G) : toAddSubgroup (closure S) = AddSubgroup.closure (⇑Additive.toMul ⁻¹' S)

theorem AddSubgroup.toSubgroup_closure {A : Type u_2} [AddGroup A] (S : Set A) : toSubgroup (closure S) = Subgroup.closure (⇑Multiplicative.toAdd ⁻¹' S)

theorem Subgroup.toAddSubgroup'_closure {A : Type u_2} [AddGroup A] (S : Set (Multiplicative A)) : toAddSubgroup' (closure S) = AddSubgroup.closure (⇑Multiplicative.ofAdd ⁻¹' S)

theorem AddSubgroup.toSubgroup'_closure {G : Type u_1} [Group G] (S : Set (Additive G)) : toSubgroup' (closure S) = Subgroup.closure (⇑Additive.ofMul ⁻¹' S)

theorem Subgroup.mem_biSup_of_directedOn {G : Type u_1} [Group G] {ι : Type u_2} {p : ι → Prop} {K : ι → Subgroup G} {i : ι} (hp : p i) (hK : DirectedOn (Function.onFun (fun (x1 x2 : Subgroup G) => x1 ≤ x2) K) {i : ι | p i}) {x : G} : x ∈ ⨆ (i : ι), ⨆ (_ : p i), K i ↔ ∃ (i : ι), p i ∧ x ∈ K i

theorem AddSubgroup.mem_biSup_of_directedOn {G : Type u_1} [AddGroup G] {ι : Type u_2} {p : ι → Prop} {K : ι → AddSubgroup G} {i : ι} (hp : p i) (hK : DirectedOn (Function.onFun (fun (x1 x2 : AddSubgroup G) => x1 ≤ x2) K) {i : ι | p i}) {x : G} : x ∈ ⨆ (i : ι), ⨆ (_ : p i), K i ↔ ∃ (i : ι), p i ∧ x ∈ K i

theorem Subgroup.mem_iSup_of_directed {G : Type u_1} [Group G] {ι : Sort u_2} [hι : Nonempty ι] {K : ι → Subgroup G} (hK : Directed (fun (x1 x2 : Subgroup G) => x1 ≤ x2) K) {x : G} : x ∈ iSup K ↔ ∃ (i : ι), x ∈ K i

theorem AddSubgroup.mem_iSup_of_directed {G : Type u_1} [AddGroup G] {ι : Sort u_2} [hι : Nonempty ι] {K : ι → AddSubgroup G} (hK : Directed (fun (x1 x2 : AddSubgroup G) => x1 ≤ x2) K) {x : G} : x ∈ iSup K ↔ ∃ (i : ι), x ∈ K i

@[simp]

theorem Subgroup.mem_iSup_prop {G : Type u_1} [Group G] {p : Prop} {K : p → Subgroup G} {x : G} : x ∈ ⨆ (h : p), K h ↔ x = 1 ∨ ∃ (h : p), x ∈ K h

@[simp]

theorem AddSubgroup.mem_iSup_prop {G : Type u_1} [AddGroup G] {p : Prop} {K : p → AddSubgroup G} {x : G} : x ∈ ⨆ (h : p), K h ↔ x = 0 ∨ ∃ (h : p), x ∈ K h

theorem Subgroup.coe_iSup_of_directed {G : Type u_1} [Group G] {ι : Sort u_2} [Nonempty ι] {S : ι → Subgroup G} (hS : Directed (fun (x1 x2 : Subgroup G) => x1 ≤ x2) S) : ↑(⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)

theorem AddSubgroup.coe_iSup_of_directed {G : Type u_1} [AddGroup G] {ι : Sort u_2} [Nonempty ι] {S : ι → AddSubgroup G} (hS : Directed (fun (x1 x2 : AddSubgroup G) => x1 ≤ x2) S) : ↑(⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)

theorem Subgroup.mem_sSup_of_directedOn {G : Type u_1} [Group G] {K : Set (Subgroup G)} (Kne : K.Nonempty) (hK : DirectedOn (fun (x1 x2 : Subgroup G) => x1 ≤ x2) K) {x : G} : x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s

theorem AddSubgroup.mem_sSup_of_directedOn {G : Type u_1} [AddGroup G] {K : Set (AddSubgroup G)} (Kne : K.Nonempty) (hK : DirectedOn (fun (x1 x2 : AddSubgroup G) => x1 ≤ x2) K) {x : G} : x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s

theorem Subgroup.mem_sup {C : Type u_2} [CommGroup C] {s t : Subgroup C} {x : C} : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

theorem AddSubgroup.mem_sup {C : Type u_2} [AddCommGroup C] {s t : AddSubgroup C} {x : C} : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x

theorem Subgroup.mem_sup' {C : Type u_2} [CommGroup C] {s t : Subgroup C} {x : C} : x ∈ s ⊔ t ↔ ∃ (y : ↥s) (z : ↥t), ↑y * ↑z = x

theorem AddSubgroup.mem_sup' {C : Type u_2} [AddCommGroup C] {s t : AddSubgroup C} {x : C} : x ∈ s ⊔ t ↔ ∃ (y : ↥s) (z : ↥t), ↑y + ↑z = x

theorem Subgroup.mem_closure_pair {C : Type u_2} [CommGroup C] {x y z : C} : z ∈ closure {x, y} ↔ ∃ (m : ℤ) (n : ℤ), x ^ m * y ^ n = z

theorem AddSubgroup.mem_closure_pair {C : Type u_2} [AddCommGroup C] {x y z : C} : z ∈ closure {x, y} ↔ ∃ (m : ℤ) (n : ℤ), m • x + n • y = z

theorem Subgroup.disjoint_def {G : Type u_1} [Group G] {H₁ H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1

theorem AddSubgroup.disjoint_def {G : Type u_1} [AddGroup G] {H₁ H₂ : AddSubgroup G} : Disjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 0

theorem Subgroup.disjoint_def' {G : Type u_1} [Group G] {H₁ H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1

theorem AddSubgroup.disjoint_def' {G : Type u_1} [AddGroup G] {H₁ H₂ : AddSubgroup G} : Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 0

theorem Subgroup.disjoint_iff_mul_eq_one {G : Type u_1} [Group G] {H₁ H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x * y = 1 → x = 1 ∧ y = 1

theorem AddSubgroup.disjoint_iff_add_eq_zero {G : Type u_1} [AddGroup G] {H₁ H₂ : AddSubgroup G} : Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x + y = 0 → x = 0 ∧ y = 0

theorem Subgroup.mul_injective_of_disjoint {G : Type u_1} [Group G] {H₁ H₂ : Subgroup G} (h : Disjoint H₁ H₂) : Function.Injective fun (g : ↥H₁ × ↥H₂) => ↑g.1 * ↑g.2

theorem AddSubgroup.add_injective_of_disjoint {G : Type u_1} [AddGroup G] {H₁ H₂ : AddSubgroup G} (h : Disjoint H₁ H₂) : Function.Injective fun (g : ↥H₁ × ↥H₂) => ↑g.1 + ↑g.2