doc-next-gen

Mathlib.Algebra.Group.Subgroup.Lattice

Module docstring

{"# 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 "}

Subgroup.toAddSubgroup definition
: Subgroup G ≃o AddSubgroup (Additive G)
Full source 
/-- Subgroups of a group `G` are isomorphic to additive subgroups of `Additive G`. -/
@[simps!]
def Subgroup.toAddSubgroup : SubgroupSubgroup G ≃o AddSubgroup (Additive G) where
  toFun S := { Submonoid.toAddSubmonoid S.toSubmonoid with neg_mem' := S.inv_mem' }
  invFun S := { AddSubmonoid.toSubmonoid S.toAddSubmonoid with inv_mem' := S.neg_mem' }
  left_inv x := by cases x; rfl
  right_inv x := by cases x; rfl
  map_rel_iff' := Iff.rfl
Order isomorphism between subgroups and additive subgroups
Informal description
The function `Subgroup.toAddSubgroup` establishes an order isomorphism between subgroups of a group `G` and additive subgroups of the additive group `Additive G`. Specifically: - The forward map takes a subgroup $S \subseteq G$ to the additive subgroup $\{x \mid \text{Additive.toMul}(x) \in S\}$. - The inverse map takes an additive subgroup $T \subseteq \text{Additive } G$ to the subgroup $\{x \mid \text{Additive.ofMul}(x) \in T\}$. This isomorphism preserves the order structure (inclusion of subgroups).
AddSubgroup.toSubgroup' abbrev
: AddSubgroup (Additive G) ≃o Subgroup G
Full source 
/-- Additive subgroup of an additive group `Additive G` are isomorphic to subgroup of `G`. -/
abbrev AddSubgroup.toSubgroup' : AddSubgroupAddSubgroup (Additive G) ≃o Subgroup G :=
  Subgroup.toAddSubgroup.symm
Order isomorphism between additive subgroups of $\text{Additive } G$ and subgroups of $G$
Informal description
The function `AddSubgroup.toSubgroup'` establishes an order isomorphism between additive subgroups of the additive group `Additive G` and subgroups of the group `G`. Specifically: - The forward map takes an additive subgroup $S \subseteq \text{Additive } G$ to the subgroup $\{x \mid \text{Additive.ofMul}(x) \in S\}$. - The inverse map takes a subgroup $T \subseteq G$ to the additive subgroup $\{x \mid \text{Additive.toMul}(x) \in T\}$. This isomorphism preserves the order structure (inclusion of subgroups).
AddSubgroup.toSubgroup definition
: AddSubgroup A ≃o Subgroup (Multiplicative A)
Full source 
/-- Additive subgroups of an additive group `A` are isomorphic to subgroups of `Multiplicative A`.
-/
@[simps!]
def AddSubgroup.toSubgroup : AddSubgroupAddSubgroup A ≃o Subgroup (Multiplicative A) where
  toFun S := { AddSubmonoid.toSubmonoid S.toAddSubmonoid with inv_mem' := S.neg_mem' }
  invFun S := { Submonoid.toAddSubmonoid S.toSubmonoid with neg_mem' := S.inv_mem' }
  left_inv x := by cases x; rfl
  right_inv x := by cases x; rfl
  map_rel_iff' := Iff.rfl
Order isomorphism between additive subgroups and multiplicative subgroups
Informal description
The function `AddSubgroup.toSubgroup` establishes an order isomorphism between additive subgroups of an additive group `A` and multiplicative subgroups of the multiplicative group `Multiplicative A`. Specifically: - The forward map takes an additive subgroup `S` of `A` to the multiplicative subgroup of `Multiplicative A` consisting of all elements whose underlying additive elements belong to `S`. - The inverse map takes a multiplicative subgroup `T` of `Multiplicative A` to the additive subgroup of `A` consisting of all elements whose multiplicative counterparts belong to `T`. This isomorphism preserves the order structure, meaning that for any two additive subgroups `S₁` and `S₂`, we have `S₁ ≤ S₂` if and only if their corresponding multiplicative subgroups satisfy the same inequality.
Subgroup.toAddSubgroup' abbrev
: Subgroup (Multiplicative A) ≃o AddSubgroup A
Full source 
/-- Subgroups of an additive group `Multiplicative A` are isomorphic to additive subgroups of `A`.
-/
abbrev Subgroup.toAddSubgroup' : SubgroupSubgroup (Multiplicative A) ≃o AddSubgroup A :=
  AddSubgroup.toSubgroup.symm
Order isomorphism between multiplicative subgroups and additive subgroups
Informal description
There exists an order isomorphism between the lattice of subgroups of the multiplicative group `Multiplicative A` and the lattice of additive subgroups of the additive group `A`. Specifically: - The forward map takes a multiplicative subgroup `S` of `Multiplicative A` to the additive subgroup of `A` consisting of all elements whose multiplicative counterparts belong to `S`. - The inverse map takes an additive subgroup `T` of `A` to the multiplicative subgroup of `Multiplicative A` consisting of all elements whose underlying additive elements belong to `T`. This isomorphism preserves the order structure, meaning that for any two multiplicative subgroups `S₁` and `S₂`, we have `S₁ ≤ S₂` if and only if their corresponding additive subgroups satisfy the same inequality.
Subgroup.topEquiv definition
: (⊤ : Subgroup G) ≃* G
Full source 
/-- The top subgroup is isomorphic to the group.

This is the group version of `Submonoid.topEquiv`. -/
@[to_additive (attr := simps!)
      "The top additive subgroup is isomorphic to the additive group.

      This is the additive group version of `AddSubmonoid.topEquiv`."]
def topEquiv : (⊤ : Subgroup G) ≃* G :=
  Submonoid.topEquiv
Isomorphism between top subgroup and group
Informal description
The multiplicative isomorphism between the top subgroup (the entire group) and the group itself, where the isomorphism maps each element to itself and its inverse maps each element to the corresponding element in the top subgroup.
Subgroup.instBot instance
: Bot (Subgroup G)
Full source 
/-- The trivial subgroup `{1}` of a group `G`. -/
@[to_additive "The trivial `AddSubgroup` `{0}` of an `AddGroup` `G`."]
instance : Bot (Subgroup G) :=
  ⟨{ (⊥ : Submonoid G) with inv_mem' := by simp}⟩
The Trivial Subgroup as the Bottom Element
Informal description
For any group $G$, the trivial subgroup $\{1\}$ is the bottom element in the lattice of subgroups of $G$.
Subgroup.instInhabited instance
: Inhabited (Subgroup G)
Full source 
@[to_additive]
instance : Inhabited (Subgroup G) :=
  ⟨⊥⟩
Nonempty Collection of Subgroups
Informal description
For any group $G$, the collection of subgroups of $G$ is nonempty.
Subgroup.mem_bot theorem
{x : G} : x ∈ (⊥ : Subgroup G) ↔ x = 1
Full source 
@[to_additive (attr := simp)]
theorem mem_bot {x : G} : x ∈ (⊥ : Subgroup G)x ∈ (⊥ : Subgroup G) ↔ x = 1 :=
  Iff.rfl
Characterization of Elements in the Trivial Subgroup: $x \in \bot \leftrightarrow x = 1$
Informal description
For any element $x$ in a group $G$, $x$ belongs to the trivial subgroup (denoted $\bot$) if and only if $x$ is the identity element of $G$, i.e., $x \in \bot \leftrightarrow x = 1$.
Subgroup.mem_top theorem
(x : G) : x ∈ (⊤ : Subgroup G)
Full source 
@[to_additive (attr := simp)]
theorem mem_top (x : G) : x ∈ (⊤ : Subgroup G) :=
  Set.mem_univ x
Universal Membership in Top Subgroup
Informal description
For any element $x$ of a group $G$, $x$ belongs to the top subgroup $\top$ of $G$ (i.e., the subgroup containing all elements of $G$).
Subgroup.coe_top theorem
: ((⊤ : Subgroup G) : Set G) = Set.univ
Full source 
@[to_additive (attr := simp)]
theorem coe_top : ((⊤ : Subgroup G) : Set G) = Set.univ :=
  rfl
Top Subgroup as Universal Set
Informal description
The underlying set of the top subgroup of a group $G$ (i.e., the subgroup containing all elements of $G$) is equal to the universal set of $G$.
Subgroup.coe_bot theorem
: ((⊥ : Subgroup G) : Set G) = { 1 }
Full source 
@[to_additive (attr := simp)]
theorem coe_bot : ((⊥ : Subgroup G) : Set G) = {1} :=
  rfl
Bottom Subgroup as Identity Singleton
Informal description
The underlying set of the bottom subgroup $\bot$ in the lattice of subgroups of a group $G$ is the singleton set containing the identity element $1$ of $G$, i.e., $(\bot : \text{Subgroup } G) = \{1\}$.
Subgroup.top_toSubmonoid theorem
: (⊤ : Subgroup G).toSubmonoid = ⊤
Full source 
@[to_additive (attr := simp)]
theorem top_toSubmonoid : (⊤ : Subgroup G).toSubmonoid = ⊤ :=
  rfl
Top Subgroup's Submonoid is Top Submonoid
Informal description
For any group $G$, the underlying submonoid of the top subgroup $\top$ in the lattice of subgroups of $G$ is equal to the top submonoid $\top$ in the lattice of submonoids of $G$.
Subgroup.bot_toSubmonoid theorem
: (⊥ : Subgroup G).toSubmonoid = ⊥
Full source 
@[to_additive (attr := simp)]
theorem bot_toSubmonoid : (⊥ : Subgroup G).toSubmonoid = ⊥ :=
  rfl
Trivial Subgroup's Underlying Submonoid is Trivial
Informal description
For any group $G$, the underlying submonoid of the trivial subgroup $\bot$ (which consists of only the identity element) is equal to the trivial submonoid $\bot$ of $G$.
Subgroup.coe_eq_univ theorem
{H : Subgroup G} : (H : Set G) = Set.univ ↔ H = ⊤
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_eq_univ {H : Subgroup G} : (H : Set G) = Set.univ ↔ H = ⊤ :=
  (SetLike.ext'_iff.trans (by rfl)).symm
Subgroup Equals Universal Set iff It Is the Full Group
Informal description
For any subgroup $H$ of a group $G$, the underlying set of $H$ is equal to the universal set of $G$ if and only if $H$ is the top subgroup (i.e., $H$ is the entire group $G$).
Subgroup.coe_eq_singleton theorem
{H : Subgroup G} : (∃ g : G, (H : Set G) = { g }) ↔ H = ⊥
Full source 
@[to_additive]
theorem coe_eq_singleton {H : Subgroup G} : (∃ g : G, (H : Set G) = {g}) ↔ H = ⊥ :=
  ⟨fun ⟨g, hg⟩ =>
    haveI : Subsingleton (H : Set G) := by
      rw [hg]
      infer_instance
    H.eq_bot_of_subsingleton,
    fun h => ⟨1, SetLike.ext'_iff.mp h⟩⟩
Subgroup is Trivial iff its Underlying Set is a Singleton
Informal description
For any subgroup $H$ of a group $G$, the underlying set of $H$ is a singleton $\{g\}$ for some $g \in G$ if and only if $H$ is the trivial subgroup $\{\text{1}\}$.
Subgroup.nontrivial_iff_exists_ne_one theorem
(H : Subgroup G) : Nontrivial H ↔ ∃ x ∈ H, x ≠ (1 : G)
Full source 
@[to_additive]
theorem nontrivial_iff_exists_ne_one (H : Subgroup G) : NontrivialNontrivial H ↔ ∃ x ∈ H, x ≠ (1 : G) := by
  rw [Subtype.nontrivial_iff_exists_ne (fun x => x ∈ H) (1 : H)]
  simp
Nontrivial Subgroup Criterion: Existence of Non-Identity Element
Informal description
A subgroup $H$ of a group $G$ is nontrivial if and only if there exists an element $x \in H$ such that $x \neq 1$.
Subgroup.nontrivial_iff_ne_bot theorem
(H : Subgroup G) : Nontrivial H ↔ H ≠ ⊥
Full source 
@[to_additive]
theorem nontrivial_iff_ne_bot (H : Subgroup G) : NontrivialNontrivial H ↔ H ≠ ⊥ := by
  rw [nontrivial_iff_exists_ne_one, ne_eq, eq_bot_iff_forall]
  simp only [ne_eq, not_forall, exists_prop]
Nontrivial Subgroup Criterion: $H$ is Nontrivial if and only if $H \neq \{\mathbf{1}\}$
Informal description
For a subgroup $H$ of a group $G$, $H$ is nontrivial if and only if $H$ is not the trivial subgroup $\{1\}$.
Subgroup.bot_or_nontrivial theorem
(H : Subgroup G) : H = ⊥ ∨ Nontrivial H
Full source 
/-- A subgroup is either the trivial subgroup or nontrivial. -/
@[to_additive "A subgroup is either the trivial subgroup or nontrivial."]
theorem bot_or_nontrivial (H : Subgroup G) : H = ⊥ ∨ Nontrivial H := by
  have := nontrivial_iff_ne_bot H
  tauto
Subgroup Dichotomy: Trivial or Nontrivial
Informal description
For any subgroup $H$ of a group $G$, either $H$ is the trivial subgroup $\{1\}$ or $H$ is nontrivial (i.e., contains at least two distinct elements).
Subgroup.bot_or_exists_ne_one theorem
(H : Subgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ (1 : G)
Full source 
/-- A subgroup is either the trivial subgroup or contains a non-identity element. -/
@[to_additive "A subgroup is either the trivial subgroup or contains a nonzero element."]
theorem bot_or_exists_ne_one (H : Subgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ (1 : G) := by
  convert H.bot_or_nontrivial
  rw [nontrivial_iff_exists_ne_one]
Subgroup Dichotomy: Trivial or Contains Non-Identity Element
Informal description
For any subgroup $H$ of a group $G$, either $H$ is the trivial subgroup $\{1\}$ or there exists an element $x \in H$ such that $x \neq 1$.
Subgroup.ne_bot_iff_exists_ne_one theorem
{H : Subgroup G} : H ≠ ⊥ ↔ ∃ a : ↥H, a ≠ 1
Full source 
@[to_additive]
lemma ne_bot_iff_exists_ne_one {H : Subgroup G} : H ≠ ⊥H ≠ ⊥ ↔ ∃ a : ↥H, a ≠ 1 := by
  rw [← nontrivial_iff_ne_bot, nontrivial_iff_exists_ne_one]
  simp only [ne_eq, Subtype.exists, mk_eq_one, exists_prop]
Nontrivial Subgroup Criterion: Existence of Non-Identity Element
Informal description
For any subgroup $H$ of a group $G$, $H$ is not the trivial subgroup $\{1\}$ if and only if there exists an element $a \in H$ such that $a \neq 1$.
Subgroup.instMin instance
: Min (Subgroup G)
Full source 
/-- The inf of two subgroups is their intersection. -/
@[to_additive "The inf of two `AddSubgroup`s is their intersection."]
instance : Min (Subgroup G) :=
  ⟨fun H₁ H₂ =>
    { H₁.toSubmonoid ⊓ H₂.toSubmonoid with
      inv_mem' := fun ⟨hx, hx'⟩ => ⟨H₁.inv_mem hx, H₂.inv_mem hx'⟩ }⟩
Intersection of Subgroups is a Subgroup
Informal description
For any group $G$, the intersection of two subgroups of $G$ is again a subgroup of $G$.
Subgroup.coe_inf theorem
(p p' : Subgroup G) : ((p ⊓ p' : Subgroup G) : Set G) = (p : Set G) ∩ p'
Full source 
@[to_additive (attr := simp)]
theorem coe_inf (p p' : Subgroup G) : ((p ⊓ p' : Subgroup G) : Set G) = (p : Set G) ∩ p' :=
  rfl
Underlying Set of Subgroup Intersection Equals Set Intersection
Informal description
For any two subgroups $p$ and $p'$ of a group $G$, the underlying set of their infimum $p \sqcap p'$ is equal to the intersection of their underlying sets, i.e., $(p \sqcap p') = p \cap p'$.
Subgroup.mem_inf theorem
{p p' : Subgroup G} {x : G} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
Full source 
@[to_additive (attr := simp)]
theorem mem_inf {p p' : Subgroup G} {x : G} : x ∈ p ⊓ p'x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p' :=
  Iff.rfl
Characterization of Membership in the Intersection of Subgroups
Informal description
For any subgroups $p$ and $p'$ of a group $G$, and any element $x \in G$, we have $x \in p \sqcap p'$ if and only if $x \in p$ and $x \in p'$.
Subgroup.instInfSet instance
: InfSet (Subgroup G)
Full source 
@[to_additive]
instance : InfSet (Subgroup G) :=
  ⟨fun s =>
    { (⨅ S ∈ s, Subgroup.toSubmonoid S).copy (⋂ S ∈ s, ↑S) (by simp) with
      inv_mem' := fun {x} hx =>
        Set.mem_biInter fun i h => i.inv_mem (by apply Set.mem_iInter₂.1 hx i h) }⟩
Infimum Structure on Subgroups of a Group
Informal description
For any group $G$, the collection of subgroups of $G$ has an infimum structure, where the infimum of a family of subgroups is given by their intersection.
Subgroup.coe_sInf theorem
(H : Set (Subgroup G)) : ((sInf H : Subgroup G) : Set G) = ⋂ s ∈ H, ↑s
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_sInf (H : Set (Subgroup G)) : ((sInf H : Subgroup G) : Set G) = ⋂ s ∈ H, ↑s :=
  rfl
Infimum of Subgroups as Intersection of Underlying Sets
Informal description
For any set $H$ of subgroups of a group $G$, the underlying set of the infimum of $H$ is equal to the intersection of the underlying sets of all subgroups in $H$. That is, \[ \bigcap_{s \in H} s = \inf H. \]
Subgroup.mem_sInf theorem
{S : Set (Subgroup G)} {x : G} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
Full source 
@[to_additive (attr := simp)]
theorem mem_sInf {S : Set (Subgroup G)} {x : G} : x ∈ sInf Sx ∈ sInf S ↔ ∀ p ∈ S, x ∈ p :=
  Set.mem_iInter₂
Characterization of Membership in Intersection of Subgroups
Informal description
For any set $S$ of subgroups of a group $G$ and any element $x \in G$, the element $x$ belongs to the infimum of $S$ (i.e., the intersection of all subgroups in $S$) if and only if $x$ belongs to every subgroup in $S$. In symbols: $$x \in \bigcap S \leftrightarrow \forall p \in S, x \in p$$
Subgroup.mem_iInf theorem
{ι : Sort*} {S : ι → Subgroup G} {x : G} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i
Full source 
@[to_additive]
theorem mem_iInf {ι : Sort*} {S : ι → Subgroup G} {x : G} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by
  simp only [iInf, mem_sInf, Set.forall_mem_range]
Characterization of Membership in Infimum of Subgroups
Informal description
For any group $G$, any family of subgroups $(S_i)_{i \in \iota}$ of $G$, and any element $x \in G$, the element $x$ belongs to the infimum $\bigsqcap_i S_i$ of the subgroups if and only if $x$ belongs to every subgroup $S_i$ in the family.
Subgroup.coe_iInf theorem
{ι : Sort*} {S : ι → Subgroup G} : (↑(⨅ i, S i) : Set G) = ⋂ i, S i
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_iInf {ι : Sort*} {S : ι → Subgroup G} : (↑(⨅ i, S i) : Set G) = ⋂ i, S i := by
  simp only [iInf, coe_sInf, Set.biInter_range]
Infimum of Subgroups Equals Intersection of Underlying Sets
Informal description
For any family of subgroups $\{S_i\}_{i \in \iota}$ of a group $G$, the underlying set of the infimum of the subgroups is equal to the intersection of their underlying sets. In symbols: \[ \left(\bigsqcap_{i \in \iota} S_i\right) = \bigcap_{i \in \iota} S_i. \]
Subgroup.instCompleteLattice instance
: CompleteLattice (Subgroup G)
Full source 
/-- Subgroups of a group form a complete lattice. -/
@[to_additive "The `AddSubgroup`s of an `AddGroup` form a complete lattice."]
instance : CompleteLattice (Subgroup G) :=
  { completeLatticeOfInf (Subgroup G) fun _s =>
      IsGLB.of_image SetLike.coe_subset_coe isGLB_biInf with
    bot := ⊥
    bot_le := fun S _x hx => (mem_bot.1 hx).symm ▸ S.one_mem
    top := ⊤
    le_top := fun _S x _hx => mem_top x
    inf := (· ⊓ ·)
    le_inf := fun _a _b _c ha hb _x hx => ⟨ha hx, hb hx⟩
    inf_le_left := fun _a _b _x => And.left
    inf_le_right := fun _a _b _x => And.right }
Complete Lattice Structure on Subgroups of a Group
Informal description
The collection of all subgroups of a group $G$ forms a complete lattice, where the partial order is given by inclusion, the infimum of a family of subgroups is their intersection, and the supremum is the subgroup generated by their union.
Subgroup.mem_sup_left theorem
{S T : Subgroup G} : ∀ {x : G}, x ∈ S → x ∈ S ⊔ T
Full source 
@[to_additive]
theorem mem_sup_left {S T : Subgroup G} : ∀ {x : G}, x ∈ S → x ∈ S ⊔ T :=
  have : S ≤ S ⊔ T := le_sup_left; fun h ↦ this h
Membership in Left Subgroup Implies Membership in Supremum of Subgroups
Informal description
For any two subgroups $S$ and $T$ of a group $G$, if an element $x \in G$ belongs to $S$, then $x$ also belongs to the supremum (join) subgroup $S \sqcup T$.
Subgroup.mem_sup_right theorem
{S T : Subgroup G} : ∀ {x : G}, x ∈ T → x ∈ S ⊔ T
Full source 
@[to_additive]
theorem mem_sup_right {S T : Subgroup G} : ∀ {x : G}, x ∈ T → x ∈ S ⊔ T :=
  have : T ≤ S ⊔ T := le_sup_right; fun h ↦ this h
Element in Right Subgroup Implies Element in Supremum of Subgroups
Informal description
For any subgroups $S$ and $T$ of a group $G$, if an element $x \in G$ belongs to $T$, then $x$ also belongs to the supremum (join) subgroup $S \sqcup T$.
Subgroup.mul_mem_sup theorem
{S T : Subgroup G} {x y : G} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T
Full source 
@[to_additive]
theorem mul_mem_sup {S T : Subgroup G} {x y : G} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T :=
  (S ⊔ T).mul_mem (mem_sup_left hx) (mem_sup_right hy)
Product of Elements from Two Subgroups Belongs to Their Join
Informal description
For any two subgroups $S$ and $T$ of a group $G$, and any elements $x, y \in G$ such that $x \in S$ and $y \in T$, the product $x * y$ belongs to the supremum (join) subgroup $S \sqcup T$.
Subgroup.mem_iSup_of_mem theorem
{ι : Sort*} {S : ι → Subgroup G} (i : ι) : ∀ {x : G}, x ∈ S i → x ∈ iSup S
Full source 
@[to_additive]
theorem mem_iSup_of_mem {ι : Sort*} {S : ι → Subgroup G} (i : ι) :
    ∀ {x : G}, x ∈ S i → x ∈ iSup S :=
  have : S i ≤ iSup S := le_iSup _ _; fun h ↦ this h
Element in Subgroup Implies Element in Supremum of Subgroups
Informal description
For any family of subgroups $S_i$ of a group $G$ indexed by a type $\iota$, and for any index $i \in \iota$, if an element $x \in G$ belongs to the subgroup $S_i$, then $x$ also belongs to the supremum $\bigsqcup_i S_i$ of the family of subgroups.
Subgroup.mem_sSup_of_mem theorem
{S : Set (Subgroup G)} {s : Subgroup G} (hs : s ∈ S) : ∀ {x : G}, x ∈ s → x ∈ sSup S
Full source 
@[to_additive]
theorem mem_sSup_of_mem {S : Set (Subgroup G)} {s : Subgroup G} (hs : s ∈ S) :
    ∀ {x : G}, x ∈ s → x ∈ sSup S :=
  have : s ≤ sSup S := le_sSup hs; fun h ↦ this h
Element in Subgroup Implies Element in Supremum of Subgroups
Informal description
Let $G$ be a group and let $S$ be a collection of subgroups of $G$. For any subgroup $s \in S$ and any element $x \in G$, if $x$ belongs to $s$, then $x$ also belongs to the supremum (join) of all subgroups in $S$.
Subgroup.subsingleton_iff theorem
: Subsingleton (Subgroup G) ↔ Subsingleton G
Full source 
@[to_additive (attr := simp)]
theorem subsingleton_iff : SubsingletonSubsingleton (Subgroup G) ↔ Subsingleton G :=
  ⟨fun _ =>
    ⟨fun x y =>
      have : ∀ i : G, i = 1 := fun i =>
        mem_bot.mp <| Subsingleton.elim (⊤ : Subgroup G) ⊥ ▸ mem_top i
      (this x).trans (this y).symm⟩,
    fun _ => ⟨fun x y => Subgroup.ext fun i => Subsingleton.elim 1 i ▸ by simp [Subgroup.one_mem]⟩⟩
Subsingleton Subgroups if and only if Subsingleton Group
Informal description
The type of subgroups of a group $G$ is a subsingleton (i.e., has at most one element) if and only if $G$ itself is a subsingleton.
Subgroup.nontrivial_iff theorem
: Nontrivial (Subgroup G) ↔ Nontrivial G
Full source 
@[to_additive (attr := simp)]
theorem nontrivial_iff : NontrivialNontrivial (Subgroup G) ↔ Nontrivial G :=
  not_iff_not.mp
    ((not_nontrivial_iff_subsingleton.trans subsingleton_iff).trans
      not_nontrivial_iff_subsingleton.symm)
Nontriviality of Subgroups and Group Equivalence: $\text{Nontrivial}\,(\text{Subgroup}\,G) \leftrightarrow \text{Nontrivial}\,G$
Informal description
The type of subgroups of a group $G$ is nontrivial (i.e., contains at least two distinct elements) if and only if $G$ itself is nontrivial.
Subgroup.instNontrivial instance
[Nontrivial G] : Nontrivial (Subgroup G)
Full source 
@[to_additive]
instance [Nontrivial G] : Nontrivial (Subgroup G) :=
  nontrivial_iff.mpr ‹_›
Nontriviality of Subgroups in Nontrivial Groups
Informal description
For any nontrivial group $G$, the collection of subgroups of $G$ is also nontrivial (i.e., contains at least two distinct subgroups).
Subgroup.instNontrivialSubtypeMemTop instance
[Nontrivial G] : Nontrivial (⊤ : Subgroup G)
Full source 
@[to_additive]
instance [Nontrivial G] : Nontrivial (⊤ : Subgroup G) := by
  rw [nontrivial_iff_ne_bot]
  exact top_ne_bot
Nontriviality of the Full Subgroup in Nontrivial Groups
Informal description
For any nontrivial group $G$, the subgroup consisting of all elements of $G$ (denoted $\top$) is itself a nontrivial type.
Subgroup.closure definition
(k : Set G) : Subgroup G
Full source 
/-- The `Subgroup` generated by a set. -/
@[to_additive "The `AddSubgroup` generated by a set"]
def closure (k : Set G) : Subgroup G :=
  sInf { K | k ⊆ K }
Subgroup generated by a set
Informal description
The subgroup generated by a subset $k$ of a group $G$ is the smallest subgroup of $G$ containing $k$, defined as the infimum of all subgroups of $G$ that contain $k$.
Subgroup.mem_closure theorem
{x : G} : x ∈ closure k ↔ ∀ K : Subgroup G, k ⊆ K → x ∈ K
Full source 
@[to_additive]
theorem mem_closure {x : G} : x ∈ closure kx ∈ closure k ↔ ∀ K : Subgroup G, k ⊆ K → x ∈ K :=
  mem_sInf
Characterization of Membership in Generated Subgroup
Informal description
For any element $x$ in a group $G$, $x$ belongs to the subgroup generated by a subset $k \subseteq G$ if and only if $x$ is contained in every subgroup $K$ of $G$ that includes $k$. In symbols: $$x \in \langle k \rangle \leftrightarrow \forall K \leq G,\ k \subseteq K \to x \in K$$
Subgroup.subset_closure theorem
: k ⊆ closure k
Full source 
/-- The subgroup generated by a set includes the set. -/
@[to_additive (attr := simp, aesop safe 20 apply (rule_sets := [SetLike]))
  "The `AddSubgroup` generated by a set includes the set."]
theorem subset_closure : k ⊆ closure k := fun _ hx => mem_closure.2 fun _ hK => hK hx
Generated Subgroup Contains Original Set
Informal description
For any subset $k$ of a group $G$, the subgroup generated by $k$ contains $k$ as a subset. In other words, $k \subseteq \langle k \rangle$, where $\langle k \rangle$ denotes the subgroup generated by $k$.
Subgroup.not_mem_of_not_mem_closure theorem
{P : G} (hP : P ∉ closure k) : P ∉ k
Full source 
@[to_additive]
theorem not_mem_of_not_mem_closure {P : G} (hP : P ∉ closure k) : P ∉ k := fun h =>
  hP (subset_closure h)
Non-membership in Generated Subgroup Implies Non-membership in Original Set
Informal description
For any element $P$ in a group $G$, if $P$ does not belong to the subgroup generated by a subset $k \subseteq G$, then $P$ does not belong to $k$. In symbols: $$P \notin \langle k \rangle \implies P \notin k$$
Subgroup.closure_le theorem
: closure k ≤ K ↔ k ⊆ K
Full source 
/-- A subgroup `K` includes `closure k` if and only if it includes `k`. -/
@[to_additive (attr := simp)
  "An additive subgroup `K` includes `closure k` if and only if it includes `k`"]
theorem closure_le : closureclosure k ≤ K ↔ k ⊆ K :=
  ⟨Subset.trans subset_closure, fun h => sInf_le h⟩
Subgroup Generated by Set is Contained in Subgroup if and only if Set is Subset
Informal description
For any subset $k$ of a group $G$ and any subgroup $K$ of $G$, the subgroup generated by $k$ is contained in $K$ if and only if $k$ is a subset of $K$. In other words, $\langle k \rangle \leq K \leftrightarrow k \subseteq K$.
Subgroup.closure_eq_of_le theorem
(h₁ : k ⊆ K) (h₂ : K ≤ closure k) : closure k = K
Full source 
@[to_additive]
theorem closure_eq_of_le (h₁ : k ⊆ K) (h₂ : K ≤ closure k) : closure k = K :=
  le_antisymm ((closure_le <| K).2 h₁) h₂
Subgroup Generation Equality: $\langle k \rangle = K$ under containment conditions
Informal description
For any subset $k$ of a group $G$ and any subgroup $K$ of $G$, if $k$ is contained in $K$ and $K$ is contained in the subgroup generated by $k$, then the subgroup generated by $k$ equals $K$. In other words, if $k \subseteq K \leq \langle k \rangle$, then $\langle k \rangle = K$.
Subgroup.closure_induction theorem
{p : (g : G) → g ∈ closure k → Prop} (mem : ∀ x (hx : x ∈ k), p x (subset_closure hx)) (one : p 1 (one_mem _)) (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) (inv : ∀ x hx, p x hx → p x⁻¹ (inv_mem hx)) {x} (hx : x ∈ closure k) : p x hx
Full source 
/-- 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`. -/
@[to_additive (attr := elab_as_elim)
      "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 closure_induction {p : (g : G) → g ∈ closure k → Prop}
    (mem : ∀ x (hx : x ∈ k), p x (subset_closure hx)) (one : p 1 (one_mem _))
    (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
    (inv : ∀ x hx, p x hx → p x⁻¹ (inv_mem hx)) {x} (hx : x ∈ closure k) : p x hx :=
  let K : Subgroup G :=
    { carrier := { x | ∃ hx, p x hx }
      mul_mem' := fun ⟨_, ha⟩ ⟨_, hb⟩ ↦ ⟨_, mul _ _ _ _ ha hb⟩
      one_mem' := ⟨_, one⟩
      inv_mem' := fun ⟨_, hb⟩ ↦ ⟨_, inv _ _ hb⟩ }
  closure_le (K := K) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id
Induction Principle for Subgroup Generated by a Set
Informal description
Let $G$ be a group and $k$ a subset of $G$. Suppose $p$ is a predicate on elements of the subgroup $\langle k \rangle$ generated by $k$ such that: 1. $p(x)$ holds for all $x \in k$, 2. $p(1)$ holds (where $1$ is the identity element), 3. For any $x, y \in \langle k \rangle$, if $p(x)$ and $p(y)$ hold, then $p(xy)$ holds, 4. For any $x \in \langle k \rangle$, if $p(x)$ holds, then $p(x^{-1})$ holds. Then $p(x)$ holds for all $x \in \langle k \rangle$.
Subgroup.closure_induction₂ theorem
{p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop} (mem : ∀ (x) (y) (hx : x ∈ k) (hy : y ∈ k), p x y (subset_closure hx) (subset_closure hy)) (one_left : ∀ x hx, p 1 x (one_mem _) hx) (one_right : ∀ x hx, p x 1 hx (one_mem _)) (mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz) (mul_right : ∀ y z x hy hz hx, p x y hx hy → p x z hx hz → p x (y * z) hx (mul_mem hy hz)) (inv_left : ∀ x y hx hy, p x y hx hy → p x⁻¹ y (inv_mem hx) hy) (inv_right : ∀ x y hx hy, p x y hx hy → p x y⁻¹ hx (inv_mem hy)) {x y : G} (hx : x ∈ closure k) (hy : y ∈ closure k) : p x y hx hy
Full source 
/-- An induction principle for closure membership for predicates with two arguments. -/
@[to_additive (attr := elab_as_elim)
      "An induction principle for additive closure membership, for
      predicates with two arguments."]
theorem closure_induction₂ {p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop}
    (mem : ∀ (x) (y) (hx : x ∈ k) (hy : y ∈ k), p x y (subset_closure hx) (subset_closure hy))
    (one_left : ∀ x hx, p 1 x (one_mem _) hx) (one_right : ∀ x hx, p x 1 hx (one_mem _))
    (mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
    (mul_right : ∀ y z x hy hz hx, p x y hx hy → p x z hx hz → p x (y * z) hx (mul_mem hy hz))
    (inv_left : ∀ x y hx hy, p x y hx hy → p x⁻¹ y (inv_mem hx) hy)
    (inv_right : ∀ x y hx hy, p x y hx hy → p x y⁻¹ hx (inv_mem hy))
    {x y : G} (hx : x ∈ closure k) (hy : y ∈ closure k) : p x y hx hy := by
  induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem _ _ h hz
    | one => exact one_left _ (subset_closure hz)
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | inv _ _ h => exact inv_left _ _ _ _ h
  | one => exact one_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂
  | inv _ _ h => exact inv_right _ _ _ _ h
Double Induction Principle for Subgroup Generated by a Set
Informal description
Let $G$ be a group and $k$ a subset of $G$. Suppose $p$ is a predicate on pairs of elements from the subgroup $\langle k \rangle$ generated by $k$ such that: 1. $p(x,y)$ holds for all $x, y \in k$, 2. $p(1,x)$ and $p(x,1)$ hold for all $x \in \langle k \rangle$ (where $1$ is the identity element), 3. For any $x, y, z \in \langle k \rangle$, if $p(x,z)$ and $p(y,z)$ hold, then $p(xy,z)$ holds, 4. For any $x, y, z \in \langle k \rangle$, if $p(x,y)$ and $p(x,z)$ hold, then $p(x,yz)$ holds, 5. For any $x, y \in \langle k \rangle$, if $p(x,y)$ holds, then $p(x^{-1},y)$ holds, 6. For any $x, y \in \langle k \rangle$, if $p(x,y)$ holds, then $p(x,y^{-1})$ holds. Then $p(x,y)$ holds for all $x, y \in \langle k \rangle$.
Subgroup.closure_closure_coe_preimage theorem
{k : Set G} : closure (((↑) : closure k → G) ⁻¹' k) = ⊤
Full source 
@[to_additive (attr := simp)]
theorem closure_closure_coe_preimage {k : Set G} : closure (((↑) : closure k → G) ⁻¹' k) = ⊤ :=
  eq_top_iff.2 fun x _ ↦ Subtype.recOn x fun _ hx' ↦
    closure_induction (fun _ h ↦ subset_closure h) (one_mem _) (fun _ _ _ _ ↦ mul_mem)
      (fun _ _ ↦ inv_mem) hx'
Subgroup Generated by Preimage Equals Full Subgroup
Informal description
For any subset $k$ of a group $G$, the subgroup generated by the preimage of $k$ under the canonical inclusion map from the subgroup $\langle k \rangle$ to $G$ is the entire subgroup $\langle k \rangle$ itself. In other words, $\langle \langle k \rangle \cap k \rangle = \langle k \rangle$.
Subgroup.gi definition
: GaloisInsertion (@closure G _) (↑)
Full source 
/-- `closure` forms a Galois insertion with the coercion to set. -/
@[to_additive "`closure` forms a Galois insertion with the coercion to set."]
protected def gi : GaloisInsertion (@closure G _) (↑) where
  choice s _ := closure s
  gc s t := @closure_le _ _ t s
  le_l_u _s := subset_closure
  choice_eq _s _h := rfl
Galois insertion between subset closure and subgroup coercion
Informal description
The pair of functions `(closure, (↑))` forms a Galois insertion between the powerset of a group `G` and the lattice of subgroups of `G`. Here, `closure` is the function that takes a subset of `G` to the smallest subgroup containing it, and `(↑)` is the coercion from a subgroup to its underlying set. This means: 1. For any subset `s` of `G` and any subgroup `t` of `G`, we have `closure s ≤ t ↔ s ⊆ t` (the Galois connection property). 2. The composition `closure ∘ (↑)` is the identity on subgroups (i.e., the closure of a subgroup's underlying set is the subgroup itself).
Subgroup.closure_mono theorem
⦃h k : Set G⦄ (h' : h ⊆ k) : closure h ≤ closure k
Full source 
/-- Subgroup closure of a set is monotone in its argument: if `h ⊆ k`,
then `closure h ≤ closure k`. -/
@[to_additive (attr := gcongr)
      "Additive subgroup closure of a set is monotone in its argument: if `h ⊆ k`,
      then `closure h ≤ closure k`"]
theorem closure_mono ⦃h k : Set G⦄ (h' : h ⊆ k) : closure h ≤ closure k :=
  (Subgroup.gi G).gc.monotone_l h'
Monotonicity of Subgroup Closure: $h \subseteq k \Rightarrow \text{closure}(h) \leq \text{closure}(k)$
Informal description
For any subsets $h$ and $k$ of a group $G$, if $h \subseteq k$, then the subgroup generated by $h$ is contained in the subgroup generated by $k$, i.e., $\text{closure}(h) \leq \text{closure}(k)$.
Subgroup.closure_eq theorem
: closure (K : Set G) = K
Full source 
/-- Closure of a subgroup `K` equals `K`. -/
@[to_additive (attr := simp) "Additive closure of an additive subgroup `K` equals `K`"]
theorem closure_eq : closure (K : Set G) = K :=
  (Subgroup.gi G).l_u_eq K
Subgroup Closure Identity: $\text{closure}(K) = K$
Informal description
For any subgroup $K$ of a group $G$, the closure of the underlying set of $K$ is equal to $K$ itself, i.e., $\text{closure}(K) = K$.
Subgroup.closure_empty theorem
: closure (∅ : Set G) = ⊥
Full source 
@[to_additive (attr := simp)]
theorem closure_empty : closure (∅ : Set G) = ⊥ :=
  (Subgroup.gi G).gc.l_bot
Trivial Subgroup as Closure of Empty Set
Informal description
The subgroup generated by the empty set in a group $G$ is the trivial subgroup $\{1\}$ (denoted by $\bot$ in the lattice of subgroups), i.e., $\text{closure}(\emptyset) = \bot$.
Subgroup.closure_univ theorem
: closure (univ : Set G) = ⊤
Full source 
@[to_additive (attr := simp)]
theorem closure_univ : closure (univ : Set G) = ⊤ :=
  @coe_top G _ ▸ closure_eq ⊤
Universal Set Generates Full Subgroup
Informal description
For any group $G$, the subgroup generated by the universal set (the set of all elements of $G$) is equal to the top subgroup of $G$, i.e., $\text{closure}(\text{univ}) = \top$.
Subgroup.closure_union theorem
(s t : Set G) : closure (s ∪ t) = closure s ⊔ closure t
Full source 
@[to_additive]
theorem closure_union (s t : Set G) : closure (s ∪ t) = closureclosure s ⊔ closure t :=
  (Subgroup.gi G).gc.l_sup
Subgroup Generated by Union Equals Supremum of Subgroups
Informal description
For any subsets $s$ and $t$ of a group $G$, the subgroup generated by the union $s \cup t$ is equal to the supremum of the subgroups generated by $s$ and $t$ individually, i.e., $\text{closure}(s \cup t) = \text{closure}(s) \sqcup \text{closure}(t)$.
Subgroup.sup_eq_closure theorem
(H H' : Subgroup G) : H ⊔ H' = closure ((H : Set G) ∪ (H' : Set G))
Full source 
@[to_additive]
theorem sup_eq_closure (H H' : Subgroup G) : H ⊔ H' = closure ((H : Set G) ∪ (H' : Set G)) := by
  simp_rw [closure_union, closure_eq]
Supremum of Subgroups Equals Generated Union
Informal description
For any two subgroups $H$ and $H'$ of a group $G$, the supremum $H \sqcup H'$ in the lattice of subgroups is equal to the subgroup generated by the union of the underlying sets of $H$ and $H'$, i.e., \[ H \sqcup H' = \langle H \cup H' \rangle. \]
Subgroup.closure_iUnion theorem
{ι} (s : ι → Set G) : closure (⋃ i, s i) = ⨆ i, closure (s i)
Full source 
@[to_additive]
theorem closure_iUnion {ι} (s : ι → Set G) : closure (⋃ i, s i) = ⨆ i, closure (s i) :=
  (Subgroup.gi G).gc.l_iSup
Subgroup Closure of Union Equals Supremum of Closures
Informal description
For any indexed family of subsets $(s_i)_{i \in \iota}$ of a group $G$, the subgroup generated by their union $\bigcup_i s_i$ is equal to the supremum of the subgroups generated by each individual subset $s_i$, i.e., \[ \langle \bigcup_{i} s_i \rangle = \bigsqcup_{i} \langle s_i \rangle. \]
Subgroup.closure_eq_bot_iff theorem
: closure k = ⊥ ↔ k ⊆ { 1 }
Full source 
@[to_additive (attr := simp)]
theorem closure_eq_bot_iff : closureclosure k = ⊥ ↔ k ⊆ {1} := le_bot_iff.symm.trans <| closure_le _
Triviality Criterion for Generated Subgroup: $\langle k \rangle = \bot \leftrightarrow k \subseteq \{1\}$
Informal description
For any subset $k$ of a group $G$, the subgroup generated by $k$ is the trivial subgroup $\{1\}$ if and only if $k$ is a subset of $\{1\}$. In other words, $\langle k \rangle = \bot \leftrightarrow k \subseteq \{1\}$.
Subgroup.iSup_eq_closure theorem
{ι : Sort*} (p : ι → Subgroup G) : ⨆ i, p i = closure (⋃ i, (p i : Set G))
Full source 
@[to_additive]
theorem iSup_eq_closure {ι : Sort*} (p : ι → Subgroup G) :
    ⨆ i, p i = closure (⋃ i, (p i : Set G)) := by simp_rw [closure_iUnion, closure_eq]
Supremum of Subgroups Equals Closure of Their Union
Informal description
For any indexed family of subgroups $(p_i)_{i \in \iota}$ of a group $G$, the supremum $\bigsqcup_i p_i$ is equal to the subgroup generated by the union of the underlying sets $\bigcup_i p_i$, i.e., \[ \bigsqcup_{i} p_i = \langle \bigcup_{i} p_i \rangle. \]
Subgroup.mem_closure_singleton theorem
{x y : G} : y ∈ closure ({ x } : Set G) ↔ ∃ n : ℤ, x ^ n = y
Full source 
/-- The subgroup generated by an element of a group equals the set of integer number powers of
    the element. -/
@[to_additive
      "The `AddSubgroup` generated by an element of an `AddGroup` equals the set of
      natural number multiples of the element."]
theorem mem_closure_singleton {x y : G} : y ∈ closure ({x} : Set G)y ∈ closure ({x} : Set G) ↔ ∃ n : ℤ, x ^ n = y := by
  refine
    ⟨fun hy => closure_induction ?_ ?_ ?_ ?_ hy, fun ⟨n, hn⟩ =>
      hn ▸ zpow_mem (subset_closure <| mem_singleton x) n⟩
  · intro y hy
    rw [eq_of_mem_singleton hy]
    exact ⟨1, zpow_one x⟩
  · exact ⟨0, zpow_zero x⟩
  · rintro _ _ _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    exact ⟨n + m, zpow_add x n m⟩
  rintro _ _ ⟨n, rfl⟩
  exact ⟨-n, zpow_neg x n⟩
Characterization of Elements in Cyclic Subgroup: $y \in \langle x \rangle \leftrightarrow \exists n \in \mathbb{Z}, y = x^n$
Informal description
For any elements $x$ and $y$ in a group $G$, the element $y$ belongs to the subgroup generated by $\{x\}$ if and only if there exists an integer $n$ such that $y = x^n$.
Subgroup.closure_singleton_one theorem
: closure ({ 1 } : Set G) = ⊥
Full source 
@[to_additive]
theorem closure_singleton_one : closure ({1} : Set G) = ⊥ := by
  simp [eq_bot_iff_forall, mem_closure_singleton]
Trivial Subgroup as Closure of Identity Element: $\closure(\{1\}) = \bot$
Informal description
The subgroup generated by the singleton set containing the identity element $1$ of a group $G$ is equal to the trivial subgroup $\bot$.
Subgroup.le_closure_toSubmonoid theorem
(S : Set G) : Submonoid.closure S ≤ (closure S).toSubmonoid
Full source 
@[to_additive]
theorem le_closure_toSubmonoid (S : Set G) : Submonoid.closure S ≤ (closure S).toSubmonoid :=
  Submonoid.closure_le.2 subset_closure
Submonoid Closure is Contained in Subgroup Closure's Submonoid
Informal description
For any subset $S$ of a group $G$, the submonoid generated by $S$ is contained in the underlying submonoid of the subgroup generated by $S$. In other words, $\text{closure}_{\text{submonoid}}(S) \leq (\text{closure}_{\text{subgroup}}(S)).\text{toSubmonoid}$.
Subgroup.closure_eq_top_of_mclosure_eq_top theorem
{S : Set G} (h : Submonoid.closure S = ⊤) : closure S = ⊤
Full source 
@[to_additive]
theorem closure_eq_top_of_mclosure_eq_top {S : Set G} (h : Submonoid.closure S = ⊤) :
    closure S = ⊤ :=
  (eq_top_iff' _).2 fun _ => le_closure_toSubmonoid _ <| h.symm ▸ trivial
Subgroup Closure Equals Top When Submonoid Closure Does
Informal description
For any subset $S$ of a group $G$, if the submonoid generated by $S$ is the entire group $G$ (i.e., $\text{Submonoid.closure}(S) = \top$), then the subgroup generated by $S$ is also the entire group $G$ (i.e., $\text{Subgroup.closure}(S) = \top$).
Subgroup.closure_insert_one theorem
(s : Set G) : closure (insert 1 s) = closure s
Full source 
@[to_additive (attr := simp)]
theorem closure_insert_one (s : Set G) : closure (insert 1 s) = closure s := by
  rw [insert_eq, closure_union]
  simp [one_mem]
Subgroup Generation Unaffected by Adding Identity Element: $\langle \{1\} \cup s \rangle = \langle s \rangle$
Informal description
For any subset $s$ of a group $G$, the subgroup generated by the set obtained by inserting the identity element $1$ into $s$ is equal to the subgroup generated by $s$ itself, i.e., $\langle \{1\} \cup s \rangle = \langle s \rangle$.
Subgroup.toAddSubgroup_closure theorem
(S : Set G) : (Subgroup.closure S).toAddSubgroup = AddSubgroup.closure (Additive.toMul ⁻¹' S)
Full source 
theorem toAddSubgroup_closure (S : Set G) :
    (Subgroup.closure S).toAddSubgroup = AddSubgroup.closure (Additive.toMulAdditive.toMul ⁻¹' S) :=
  le_antisymm (toAddSubgroup.le_symm_apply.mp <|
      (closure_le _).mpr (AddSubgroup.subset_closure (G := Additive G)))
    ((AddSubgroup.closure_le _).mpr (subset_closure (G := G)))
Subgroup-to-AddSubgroup Closure Correspondence: $\text{toAddSubgroup}(\langle S \rangle) = \langle \text{Additive.toMul}^{-1}(S) \rangle$
Informal description
For any subset $S$ of a group $G$, the image of the subgroup generated by $S$ under the order isomorphism `Subgroup.toAddSubgroup` is equal to the additive subgroup generated by the preimage of $S$ under the map `Additive.toMul`. In other words, \[ \text{toAddSubgroup}(\langle S \rangle) = \langle \text{Additive.toMul}^{-1}(S) \rangle, \] where $\langle \cdot \rangle$ denotes the subgroup (resp. additive subgroup) generated by a set.
AddSubgroup.toSubgroup_closure theorem
{A : Type*} [AddGroup A] (S : Set A) : (AddSubgroup.closure S).toSubgroup = Subgroup.closure (Multiplicative.toAdd ⁻¹' S)
Full source 
theorem _root_.AddSubgroup.toSubgroup_closure {A : Type*} [AddGroup A] (S : Set A) :
    (AddSubgroup.closure S).toSubgroup = Subgroup.closure (Multiplicative.toAddMultiplicative.toAdd ⁻¹' S) :=
  Subgroup.toAddSubgroup.injective (Subgroup.toAddSubgroup_closure _ ).symm
Additive-to-Multiplicative Subgroup Closure Correspondence: $\text{toSubgroup}(\langle S \rangle) = \langle \text{Multiplicative.toAdd}^{-1}(S) \rangle$
Informal description
Let $A$ be an additive group and $S$ a subset of $A$. The image of the additive subgroup generated by $S$ under the order isomorphism `AddSubgroup.toSubgroup` is equal to the multiplicative subgroup generated by the preimage of $S$ under the map `Multiplicative.toAdd`. In other words, \[ \text{toSubgroup}(\langle S \rangle) = \langle \text{Multiplicative.toAdd}^{-1}(S) \rangle, \] where $\langle \cdot \rangle$ denotes the additive subgroup (resp. multiplicative subgroup) generated by a set.
Subgroup.toAddSubgroup'_closure theorem
{A : Type*} [AddGroup A] (S : Set (Multiplicative A)) : (closure S).toAddSubgroup' = AddSubgroup.closure (Multiplicative.ofAdd ⁻¹' S)
Full source 
theorem toAddSubgroup'_closure {A : Type*} [AddGroup A] (S : Set (Multiplicative A)) :
    (closure S).toAddSubgroup' = AddSubgroup.closure (Multiplicative.ofAddMultiplicative.ofAdd ⁻¹' S) :=
  le_antisymm (toAddSubgroup'.to_galoisConnection.l_le <|
      (closure_le _).mpr <| AddSubgroup.subset_closure (G := A))
    ((AddSubgroup.closure_le _).mpr <| Subgroup.subset_closure (G := Multiplicative A))
Correspondence between multiplicative subgroup closure and additive subgroup closure via $\text{Multiplicative.ofAdd}$
Informal description
Let $A$ be an additive group and $S$ a subset of the multiplicative group $\text{Multiplicative}\, A$. The additive subgroup corresponding to the subgroup generated by $S$ in $\text{Multiplicative}\, A$ is equal to the additive subgroup generated by the preimage of $S$ under the multiplicative-to-additive map $\text{Multiplicative.ofAdd}$. In symbols: \[ (\langle S \rangle).\text{toAddSubgroup}' = \langle \text{Multiplicative.ofAdd}^{-1}(S) \rangle \] where $\langle \cdot \rangle$ denotes the subgroup closure operation.
AddSubgroup.toSubgroup'_closure theorem
(S : Set (Additive G)) : (AddSubgroup.closure S).toSubgroup' = Subgroup.closure (Additive.ofMul ⁻¹' S)
Full source 
theorem _root_.AddSubgroup.toSubgroup'_closure (S : Set (Additive G)) :
    (AddSubgroup.closure S).toSubgroup' = Subgroup.closure (Additive.ofMulAdditive.ofMul ⁻¹' S) :=
  congr_arg AddSubgroup.toSubgroup' (toAddSubgroup'_closure _).symm
Correspondence between additive subgroup closure and subgroup closure via $\text{Additive.ofMul}$
Informal description
Let $G$ be a group and $S$ a subset of the additive group $\text{Additive}\, G$. The subgroup corresponding to the additive subgroup generated by $S$ in $\text{Additive}\, G$ is equal to the subgroup generated by the preimage of $S$ under the additive-to-multiplicative map $\text{Additive.ofMul}$. In symbols: \[ (\langle S \rangle_{\text{Add}}).\text{toSubgroup}' = \langle \text{Additive.ofMul}^{-1}(S) \rangle \] where $\langle \cdot \rangle_{\text{Add}}$ denotes the additive subgroup closure operation and $\langle \cdot \rangle$ denotes the subgroup closure operation.
Subgroup.mem_iSup_of_directed theorem
{ι} [hι : Nonempty ι] {K : ι → Subgroup G} (hK : Directed (· ≤ ·) K) {x : G} : x ∈ (iSup K : Subgroup G) ↔ ∃ i, x ∈ K i
Full source 
@[to_additive]
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {K : ι → Subgroup G} (hK : Directed (· ≤ ·) K)
    {x : G} : x ∈ (iSup K : Subgroup G)x ∈ (iSup K : Subgroup G) ↔ ∃ i, x ∈ K i := by
  refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup K i hi⟩
  suffices x ∈ closure (⋃ i, (K i : Set G)) → ∃ i, x ∈ K i by
    simpa only [closure_iUnion, closure_eq (K _)] using this
  refine fun hx ↦ closure_induction (fun _ ↦ mem_iUnion.1) ?_ ?_ ?_ hx
  · exact hι.elim fun i ↦ ⟨i, (K i).one_mem⟩
  · rintro x y _ _ ⟨i, hi⟩ ⟨j, hj⟩
    rcases hK i j with ⟨k, hki, hkj⟩
    exact ⟨k, mul_mem (hki hi) (hkj hj)⟩
  · rintro _ _ ⟨i, hi⟩
    exact ⟨i, inv_mem hi⟩
Characterization of Membership in Directed Supremum of Subgroups: $x \in \bigsqcup_i K_i \leftrightarrow \exists i, x \in K_i$
Informal description
Let $G$ be a group and $\{K_i\}_{i \in \iota}$ be a directed family of subgroups of $G$ (i.e., for any $i, j \in \iota$, there exists $k \in \iota$ such that $K_i \leq K_k$ and $K_j \leq K_k$). Then for any element $x \in G$, $x$ belongs to the supremum $\bigsqcup_i K_i$ of the subgroups $K_i$ if and only if there exists an index $i \in \iota$ such that $x \in K_i$.
Subgroup.coe_iSup_of_directed theorem
{ι} [Nonempty ι] {S : ι → Subgroup G} (hS : Directed (· ≤ ·) S) : ((⨆ i, S i : Subgroup G) : Set G) = ⋃ i, S i
Full source 
@[to_additive]
theorem coe_iSup_of_directed {ι} [Nonempty ι] {S : ι → Subgroup G} (hS : Directed (· ≤ ·) S) :
    ((⨆ i, S i : Subgroup G) : Set G) = ⋃ i, S i :=
  Set.ext fun x ↦ by simp [mem_iSup_of_directed hS]
Underlying Set of Directed Supremum of Subgroups Equals Union of Underlying Sets
Informal description
Let $G$ be a group and $\{S_i\}_{i \in \iota}$ be a directed family of subgroups of $G$ (i.e., for any $i, j \in \iota$, there exists $k \in \iota$ such that $S_i \leq S_k$ and $S_j \leq S_k$). Then the underlying set of the supremum $\bigsqcup_i S_i$ of the subgroups $S_i$ is equal to the union $\bigcup_i S_i$ of their underlying sets.
Subgroup.mem_sSup_of_directedOn theorem
{K : Set (Subgroup G)} (Kne : K.Nonempty) (hK : DirectedOn (· ≤ ·) K) {x : G} : x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s
Full source 
@[to_additive]
theorem mem_sSup_of_directedOn {K : Set (Subgroup G)} (Kne : K.Nonempty) (hK : DirectedOn (· ≤ ·) K)
    {x : G} : x ∈ sSup Kx ∈ sSup K ↔ ∃ s ∈ K, x ∈ s := by
  haveI : Nonempty K := Kne.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed hK.directed_val, SetCoe.exists, Subtype.coe_mk,
    exists_prop]
Characterization of Membership in Directed Supremum of Subgroups: $x \in \mathrm{sSup}(K) \leftrightarrow \exists s \in K, x \in s$
Informal description
Let $G$ be a group and $K$ be a nonempty set of subgroups of $G$ that is directed with respect to inclusion (i.e., for any two subgroups $s, t \in K$, there exists a subgroup $u \in K$ such that $s \leq u$ and $t \leq u$). Then for any element $x \in G$, $x$ belongs to the supremum $\mathrm{sSup}(K)$ of the subgroups in $K$ if and only if there exists a subgroup $s \in K$ such that $x \in s$.
Subgroup.mem_sup theorem
: x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
Full source 
@[to_additive]
theorem mem_sup : x ∈ s ⊔ tx ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x :=
  ⟨fun h => by
    rw [sup_eq_closure] at h
    refine Subgroup.closure_induction ?_ ?_ ?_ ?_ h
    · rintro y (h | h)
      · exact ⟨y, h, 1, t.one_mem, by simp⟩
      · exact ⟨1, s.one_mem, y, h, by simp⟩
    · exact ⟨1, s.one_mem, 1, ⟨t.one_mem, mul_one 1⟩⟩
    · rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
      exact ⟨_, mul_mem hy₁ hy₂, _, mul_mem hz₁ hz₂, by simp [mul_assoc, mul_left_comm]⟩
    · rintro _ _ ⟨y, hy, z, hz, rfl⟩
      exact ⟨_, inv_mem hy, _, inv_mem hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩, by
    rintro ⟨y, hy, z, hz, rfl⟩; exact mul_mem_sup hy hz⟩
Characterization of Membership in the Join of Two Subgroups
Informal description
For any elements $x, y, z$ in a group $G$ and any subgroups $s, t$ of $G$, the element $x$ belongs to the supremum (join) of $s$ and $t$ if and only if there exist elements $y \in s$ and $z \in t$ such that $y \cdot z = x$.
Subgroup.mem_sup' theorem
: x ∈ s ⊔ t ↔ ∃ (y : s) (z : t), (y : C) * z = x
Full source 
@[to_additive]
theorem mem_sup' : x ∈ s ⊔ tx ∈ s ⊔ t ↔ ∃ (y : s) (z : t), (y : C) * z = x :=
  mem_sup.trans <| by simp only [SetLike.exists, coe_mk, exists_prop]
Characterization of Membership in Join of Subgroups via Product Representation
Informal description
For any element $x$ in a group $G$ and any subgroups $s$ and $t$ of $G$, the element $x$ belongs to the supremum (join) of $s$ and $t$ if and only if there exist elements $y \in s$ and $z \in t$ such that $y \cdot z = x$.
Subgroup.mem_closure_pair theorem
{x y z : C} : z ∈ closure ({ x, y } : Set C) ↔ ∃ m n : ℤ, x ^ m * y ^ n = z
Full source 
@[to_additive]
theorem mem_closure_pair {x y z : C} :
    z ∈ closure ({x, y} : Set C)z ∈ closure ({x, y} : Set C) ↔ ∃ m n : ℤ, x ^ m * y ^ n = z := by
  rw [← Set.singleton_union, Subgroup.closure_union, mem_sup]
  simp_rw [mem_closure_singleton, exists_exists_eq_and]
Characterization of Membership in Subgroup Generated by Two Elements via Integer Powers
Informal description
For any elements $x, y, z$ in a group $G$, the element $z$ belongs to the subgroup generated by $\{x, y\}$ if and only if there exist integers $m, n \in \mathbb{Z}$ such that $x^m \cdot y^n = z$.
Subgroup.disjoint_def theorem
{H₁ H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1
Full source 
@[to_additive]
theorem disjoint_def {H₁ H₂ : Subgroup G} : DisjointDisjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1 :=
  disjoint_iff_inf_le.trans <| by simp only [Disjoint, SetLike.le_def, mem_inf, mem_bot, and_imp]
Characterization of Disjoint Subgroups via Identity Element
Informal description
Two subgroups $H_1$ and $H_2$ of a group $G$ are disjoint if and only if the only element common to both subgroups is the identity element $1 \in G$. In other words, for any $x \in G$, if $x \in H_1$ and $x \in H_2$, then $x = 1$.
Subgroup.disjoint_def' theorem
{H₁ H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1
Full source 
@[to_additive]
theorem disjoint_def' {H₁ H₂ : Subgroup G} :
    DisjointDisjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1 :=
  disjoint_def.trans ⟨fun h _x _y hx hy hxy ↦ h hx <| hxy.symm ▸ hy, fun h _x hx hx' ↦ h hx hx' rfl⟩
Disjoint Subgroups Characterization via Equal Elements and Identity
Informal description
Two subgroups $H_1$ and $H_2$ of a group $G$ are disjoint if and only if for any elements $x, y \in G$ such that $x \in H_1$, $y \in H_2$, and $x = y$, it follows that $x = 1$ (where $1$ is the identity element of $G$).
Subgroup.disjoint_iff_mul_eq_one theorem
{H₁ H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x * y = 1 → x = 1 ∧ y = 1
Full source 
@[to_additive]
theorem disjoint_iff_mul_eq_one {H₁ H₂ : Subgroup G} :
    DisjointDisjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x * y = 1 → x = 1 ∧ y = 1 :=
  disjoint_def'.trans
    ⟨fun h x y hx hy hxy =>
      let hx1 : x = 1 := h hx (H₂.inv_mem hy) (eq_inv_iff_mul_eq_one.mpr hxy)
      ⟨hx1, by simpa [hx1] using hxy⟩,
      fun h _ _ hx hy hxy => (h hx (H₂.inv_mem hy) (mul_inv_eq_one.mpr hxy)).1⟩
Disjoint Subgroups Characterization via Product Identity Condition: $H_1 \cap H_2 = \{1\} \Leftrightarrow (x \cdot y = 1 \Rightarrow x = 1 \land y = 1)$
Informal description
Two subgroups $H_1$ and $H_2$ of a group $G$ are disjoint if and only if for any elements $x \in H_1$ and $y \in H_2$, the equation $x \cdot y = 1$ implies that both $x = 1$ and $y = 1$, where $1$ is the identity element of $G$.
Subgroup.mul_injective_of_disjoint theorem
{H₁ H₂ : Subgroup G} (h : Disjoint H₁ H₂) : Function.Injective (fun g => g.1 * g.2 : H₁ × H₂ → G)
Full source 
@[to_additive]
theorem mul_injective_of_disjoint {H₁ H₂ : Subgroup G} (h : Disjoint H₁ H₂) :
    Function.Injective (fun g => g.1 * g.2 : H₁ × H₂ → G) := by
  intro x y hxy
  rw [← inv_mul_eq_iff_eq_mul, ← mul_assoc, ← mul_inv_eq_one, mul_assoc] at hxy
  replace hxy := disjoint_iff_mul_eq_one.mp h (y.1⁻¹ * x.1).prop (x.2 * y.2⁻¹).prop hxy
  rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
Injectivity of Product Map for Disjoint Subgroups: $(h_1, h_2) \mapsto h_1 \cdot h_2$ is injective when $H_1 \cap H_2 = \{1\}$
Informal description
Let $H_1$ and $H_2$ be subgroups of a group $G$ such that $H_1 \cap H_2 = \{1\}$. Then the multiplication map $(h_1, h_2) \mapsto h_1 \cdot h_2$ from $H_1 \times H_2$ to $G$ is injective.