Mathlib.Algebra.Group.Subgroup.Pointwise

inv_coe_set theorem

[InvolutiveInv G] [SetLike S G] [InvMemClass S G] {H : S} : (H : Set G)⁻¹ = H

Full source

@[to_additive (attr := simp, norm_cast)]
theorem inv_coe_set [InvolutiveInv G] [SetLike S G] [InvMemClass S G] {H : S} : (H : Set G)⁻¹ = H :=
  Set.ext fun _ => inv_mem_iff

Pointwise Inverse of Subgroup's Carrier Set Equals Itself

Informal description

Let $G$ be a group with an involutive inversion operation, and let $S$ be a set-like structure for $G$ that is closed under inversion. For any subset $H$ of $G$ (represented by an element of $S$), the pointwise inverse of the carrier set of $H$ is equal to $H$ itself, i.e., $(H : \text{Set } G)^{-1} = H$.

smul_coe_set theorem

[Group G] [SetLike S G] [SubgroupClass S G] {s : S} {a : G} (ha : a ∈ s) : a • (s : Set G) = s

Full source

@[to_additive (attr := simp)]
lemma smul_coe_set [Group G] [SetLike S G] [SubgroupClass S G] {s : S} {a : G} (ha : a ∈ s) :
    a • (s : Set G) = s := by
  ext; simp [Set.mem_smul_set_iff_inv_smul_mem, mul_mem_cancel_left, ha]

Left Action of Group Element Preserves Subgroup Set

Informal description

Let $G$ be a group and $S$ a set-like structure with elements of type $G$ that forms a subgroup class. For any subgroup $s$ in $S$ and any element $a \in s$, the left action of $a$ on the underlying set of $s$ is equal to $s$ itself, i.e., $a \cdot (s : \text{Set } G) = s$.

coe_set_eq_one theorem

[Group G] {s : Subgroup G} : (s : Set G) = 1 ↔ s = ⊥

Full source

@[norm_cast, to_additive]
lemma coe_set_eq_one [Group G] {s : Subgroup G} : (s : Set G) = 1 ↔ s = ⊥ :=
  (SetLike.ext'_iff.trans (by rfl)).symm

Characterization of Trivial Subgroup via Carrier Set Equality

Informal description

For any subgroup $s$ of a group $G$, the underlying set of $s$ is equal to the singleton set $\{1\}$ if and only if $s$ is the trivial subgroup (the bottom element in the lattice of subgroups).

op_smul_coe_set theorem

[Group G] [SetLike S G] [SubgroupClass S G] {s : S} {a : G} (ha : a ∈ s) : MulOpposite.op a • (s : Set G) = s

Full source

@[to_additive (attr := simp)]
lemma op_smul_coe_set [Group G] [SetLike S G] [SubgroupClass S G] {s : S} {a : G} (ha : a ∈ s) :
    MulOpposite.op a • (s : Set G) = s := by
  ext; simp [Set.mem_smul_set_iff_inv_smul_mem, mul_mem_cancel_right, ha]

Right Action of Group Element Preserves Subgroup Set via Multiplicative Opposite

Informal description

Let $G$ be a group and $S$ a set-like structure with elements of type $G$ that forms a subgroup class. For any subgroup $s$ in $S$ and any element $a \in s$, the right action of $a$ (via the multiplicative opposite) on the underlying set of $s$ is equal to $s$ itself, i.e., $\text{op}(a) \cdot (s : \text{Set } G) = s$.

coe_div_coe theorem

[SetLike S G] [DivisionMonoid G] [SubgroupClass S G] (H : S) : H / H = (H : Set G)

Full source

@[to_additive (attr := simp, norm_cast)]
lemma coe_div_coe [SetLike S G] [DivisionMonoid G] [SubgroupClass S G] (H : S) :
    H / H = (H : Set G) := by simp [div_eq_mul_inv]

Pointwise Division of Subgroup Equals Itself

Informal description

Let $G$ be a division monoid and $H$ a subgroup of $G$ (represented by a set-like structure $S$ with subgroup properties). Then the pointwise division $H / H$ is equal to $H$ as a subset of $G$.

Set.mul_subgroupClosure theorem

(hs : s.Nonempty) : s * closure s = closure s

Full source

@[to_additive (attr := simp)]
lemma mul_subgroupClosure (hs : s.Nonempty) : s * closure s = closure s := by
  rw [← smul_eq_mul, ← Set.iUnion_smul_set]
  have h a (ha : a ∈ s) : a • (closure s : Set G) = closure s :=
    smul_coe_set <| subset_closure ha
  simp +contextual [h, hs]

Product of Set with Generated Subgroup Equals Subgroup

Informal description

For any nonempty subset $s$ of a group $G$, the product set $s \cdot \langle s \rangle$ is equal to the subgroup $\langle s \rangle$ generated by $s$, where $\langle s \rangle$ denotes the smallest subgroup of $G$ containing $s$.

Set.subgroupClosure_mul theorem

(hs : s.Nonempty) : closure s * s = closure s

Full source

@[to_additive (attr := simp)]
lemma subgroupClosure_mul (hs : s.Nonempty) : closure s * s = closure s := by
  rw [← Set.iUnion_op_smul_set]
  have h a (ha : a ∈ s) :  (closure s : Set G) <• a = closure s :=
    op_smul_coe_set <| subset_closure ha
  simp +contextual [h, hs]

Subgroup Closure Stability under Right Multiplication

Informal description

For any nonempty subset $s$ of a group $G$, the product of the subgroup generated by $s$ with $s$ itself equals the subgroup generated by $s$, i.e., $\langle s \rangle * s = \langle s \rangle$.

Set.pow_mul_subgroupClosure theorem

(hs : s.Nonempty) : ∀ n, s ^ n * closure s = closure s

Full source

@[to_additive (attr := simp)]
lemma pow_mul_subgroupClosure (hs : s.Nonempty) : ∀ n, s ^ n * closure s = closure s
  | 0 => by simp
  | n + 1 => by rw [pow_succ, mul_assoc, mul_subgroupClosure hs, pow_mul_subgroupClosure hs]

Power Set Multiplication with Generated Subgroup Equals Subgroup: $s^n \cdot \langle s \rangle = \langle s \rangle$

Informal description

For any nonempty subset $s$ of a group $G$ and any natural number $n$, the product of the $n$-th power set $s^n$ with the subgroup $\langle s \rangle$ generated by $s$ equals $\langle s \rangle$ itself, i.e., $s^n \cdot \langle s \rangle = \langle s \rangle$.

Set.subgroupClosure_mul_pow theorem

(hs : s.Nonempty) : ∀ n, closure s * s ^ n = closure s

Full source

@[to_additive (attr := simp)]
lemma subgroupClosure_mul_pow (hs : s.Nonempty) : ∀ n, closure s * s ^ n = closure s
  | 0 => by simp
  | n + 1 => by rw [pow_succ', ← mul_assoc, subgroupClosure_mul hs, subgroupClosure_mul_pow hs]

Subgroup Closure Stability under Left Multiplication by Powers: $\langle s \rangle \cdot s^n = \langle s \rangle$

Informal description

For any nonempty subset $s$ of a group $G$ and any natural number $n$, the product of the subgroup generated by $s$ with the $n$-th power of $s$ equals the subgroup generated by $s$, i.e., $\langle s \rangle \cdot s^n = \langle s \rangle$.

Subgroup.inv_subset_closure theorem

(S : Set G) : S⁻¹ ⊆ closure S

Full source

@[to_additive (attr := simp)]
theorem inv_subset_closure (S : Set G) : S⁻¹S⁻¹ ⊆ closure S := fun s hs => by
  rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff]
  exact subset_closure (mem_inv.mp hs)

Inverse Set is Contained in Generated Subgroup: $S^{-1} \subseteq \langle S \rangle$

Informal description

For any subset $S$ of a group $G$, the set of inverses $S^{-1} = \{x^{-1} \mid x \in S\}$ is contained in the subgroup generated by $S$.

Subgroup.closure_toSubmonoid theorem

(S : Set G) : (closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)

Full source

@[to_additive]
theorem closure_toSubmonoid (S : Set G) :
    (closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹) := by
  refine le_antisymm (fun x hx => ?_) (Submonoid.closure_le.2 ?_)
  · refine
      closure_induction
        (fun x hx => Submonoid.closure_mono subset_union_left (Submonoid.subset_closure hx))
        (Submonoid.one_mem _) (fun x y _ _ hx hy => Submonoid.mul_mem _ hx hy) (fun x _ hx => ?_) hx
    rwa [← Submonoid.mem_closure_inv, Set.union_inv, inv_inv, Set.union_comm]
  · simp only [true_and, coe_toSubmonoid, union_subset_iff, subset_closure, inv_subset_closure]

Subgroup-to-Submonoid Closure Correspondence: $\langle S \rangle_{\text{submonoid}} = \langle S \cup S^{-1} \rangle$

Informal description

For any subset $S$ of a group $G$, the underlying submonoid of the subgroup generated by $S$ is equal to the submonoid generated by the union of $S$ and its set of inverses $S^{-1} = \{x^{-1} \mid x \in S\}$. In symbols: $$(\langle S \rangle)_{\text{submonoid}} = \langle S \cup S^{-1} \rangle_{\text{submonoid}}$$

Subgroup.closure_induction_left theorem

 {p : (x : G) → x ∈ closure s → Prop} (one : p 1 (one_mem _))
  (mul_left : ∀ x (hx : x ∈ s), ∀ (y) hy, p y hy → p (x * y) (mul_mem (subset_closure hx) hy))
  (inv_mul_cancel : ∀ x (hx : x ∈ s), ∀ (y) hy, p y hy → p (x⁻¹ * y) (mul_mem (inv_mem (subset_closure hx)) hy)) {x : G}
  (h : x ∈ closure s) : p x h

Full source

/-- For subgroups generated by a single element, see the simpler `zpow_induction_left`. -/
@[to_additive (attr := elab_as_elim)
  "For additive subgroups generated by a single element, see the simpler
  `zsmul_induction_left`."]
theorem closure_induction_left {p : (x : G) → x ∈ closure s → Prop} (one : p 1 (one_mem _))
    (mul_left : ∀ x (hx : x ∈ s), ∀ (y) hy, p y hy → p (x * y) (mul_mem (subset_closure hx) hy))
    (inv_mul_cancel : ∀ x (hx : x ∈ s), ∀ (y) hy, p y hy →
      p (x⁻¹ * y) (mul_mem (inv_mem (subset_closure hx)) hy))
    {x : G} (h : x ∈ closure s) : p x h := by
  revert h
  simp_rw [← mem_toSubmonoid, closure_toSubmonoid] at *
  intro h
  induction h using Submonoid.closure_induction_left with
  | one => exact one
  | mul_left x hx y hy ih =>
    cases hx with
    | inl hx => exact mul_left _ hx _ hy ih
    | inr hx => simpa only [inv_inv] using inv_mul_cancel _ hx _ hy ih

Left Induction Principle for Subgroup Generation

Informal description

Let $G$ be a group and $s$ a subset of $G$. For any predicate $p$ on elements of the subgroup generated by $s$, if: 1. $p$ holds for the identity element $1 \in G$, 2. For any $x \in s$ and any $y$ in the subgroup generated by $s$, if $p$ holds for $y$, then $p$ holds for $x * y$, and 3. For any $x \in s$ and any $y$ in the subgroup generated by $s$, if $p$ holds for $y$, then $p$ holds for $x^{-1} * y$, then $p$ holds for every element $x$ in the subgroup generated by $s$.

Subgroup.closure_induction_right theorem

 {p : (x : G) → x ∈ closure s → Prop} (one : p 1 (one_mem _))
  (mul_right : ∀ (x) hx, ∀ y (hy : y ∈ s), p x hx → p (x * y) (mul_mem hx (subset_closure hy)))
  (mul_inv_cancel : ∀ (x) hx, ∀ y (hy : y ∈ s), p x hx → p (x * y⁻¹) (mul_mem hx (inv_mem (subset_closure hy)))) {x : G}
  (h : x ∈ closure s) : p x h

Full source

/-- For subgroups generated by a single element, see the simpler `zpow_induction_right`. -/
@[to_additive (attr := elab_as_elim)
  "For additive subgroups generated by a single element, see the simpler
  `zsmul_induction_right`."]
theorem closure_induction_right {p : (x : G) → x ∈ closure s → Prop} (one : p 1 (one_mem _))
    (mul_right : ∀ (x) hx, ∀ y (hy : y ∈ s), p x hx → p (x * y) (mul_mem hx (subset_closure hy)))
    (mul_inv_cancel : ∀ (x) hx, ∀ y (hy : y ∈ s), p x hx →
      p (x * y⁻¹) (mul_mem hx (inv_mem (subset_closure hy))))
    {x : G} (h : x ∈ closure s) : p x h :=
  closure_induction_left (s := MulOpposite.unopMulOpposite.unop ⁻¹' s)
    (p := fun m hm => p m.unop <| by rwa [← op_closure] at hm)
    one
    (fun _x hx _y _ => mul_right _ _ _ hx)
    (fun _x hx _y _ => mul_inv_cancel _ _ _ hx)
    (by rwa [← op_closure])

Right Induction Principle for Subgroup Generation

Informal description

Let $G$ be a group and $s$ a subset of $G$. For any predicate $p$ on elements of the subgroup generated by $s$, if: 1. $p$ holds for the identity element $1 \in G$, 2. For any $x$ in the subgroup generated by $s$ and any $y \in s$, if $p$ holds for $x$, then $p$ holds for $x * y$, and 3. For any $x$ in the subgroup generated by $s$ and any $y \in s$, if $p$ holds for $x$, then $p$ holds for $x * y^{-1}$, then $p$ holds for every element $x$ in the subgroup generated by $s$.

Subgroup.closure_inv theorem

(s : Set G) : closure s⁻¹ = closure s

Full source

@[to_additive (attr := simp)]
theorem closure_inv (s : Set G) : closure s⁻¹ = closure s := by
  simp only [← toSubmonoid_inj, closure_toSubmonoid, inv_inv, union_comm]

Subgroup Closure Invariance under Inversion: $\langle s^{-1} \rangle = \langle s \rangle$

Informal description

For any subset $s$ of a group $G$, the subgroup generated by the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$ is equal to the subgroup generated by $s$ itself. In symbols: $$\langle s^{-1} \rangle = \langle s \rangle$$

Subgroup.closure_singleton_inv theorem

(x : G) : closure {x⁻¹} = closure { x }

Full source

@[to_additive (attr := simp)]
lemma closure_singleton_inv (x : G) : closure {x⁻¹} = closure {x} := by
  rw [← Set.inv_singleton, closure_inv]

Subgroup Generated by Inverse Equals Subgroup Generated by Element: $\langle \{x^{-1}\} \rangle = \langle \{x\} \rangle$

Informal description

For any element $x$ in a group $G$, the subgroup generated by the singleton set $\{x^{-1}\}$ is equal to the subgroup generated by the singleton set $\{x\}$. In symbols: $$\langle \{x^{-1}\} \rangle = \langle \{x\} \rangle$$

Subgroup.closure_induction'' theorem

 {p : (g : G) → g ∈ closure s → Prop} (mem : ∀ x (hx : x ∈ s), p x (subset_closure hx))
  (inv_mem : ∀ x (hx : x ∈ s), p x⁻¹ (inv_mem (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)) {x} (h : x ∈ closure s) : p x h

Full source

/-- An induction principle for closure membership. If `p` holds for `1` and all elements of
`k` and their inverse, and is preserved under multiplication, then `p` holds for all elements of
the closure of `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 their negation, and is preserved under addition, then `p` holds for all
  elements of the additive closure of `k`."]
theorem closure_induction'' {p : (g : G) → g ∈ closure s → Prop}
    (mem : ∀ x (hx : x ∈ s), p x (subset_closure hx))
    (inv_mem : ∀ x (hx : x ∈ s), p x⁻¹ (inv_mem (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))
    {x} (h : x ∈ closure s) : p x h :=
  closure_induction_left one (fun x hx y _ hy => mul x y _ _ (mem x hx) hy)
    (fun x hx y _ => mul x⁻¹ y _ _ <| inv_mem x hx) h

Induction Principle for Subgroup Generated by a Set

Informal description

Let $G$ be a group and $s$ a subset of $G$. For any predicate $p$ on elements of the subgroup generated by $s$, if: 1. $p$ holds for every $x \in s$, 2. For every $x \in s$, $p$ holds for $x^{-1}$, 3. $p$ holds for the identity element $1 \in G$, and 4. For any $x, y$ in the subgroup generated by $s$, if $p$ holds for $x$ and $y$, then $p$ holds for $x \cdot y$, then $p$ holds for every element $x$ in the subgroup generated by $s$.

Subgroup.iSup_induction theorem

 {ι : Sort*} (S : ι → Subgroup G) {C : G → Prop} {x : G} (hx : x ∈ ⨆ i, S i) (mem : ∀ (i), ∀ x ∈ S i, C x) (one : C 1)
  (mul : ∀ x y, C x → C y → C (x * y)) : C x

Full source

/-- An induction principle for elements of `⨆ i, S i`.
If `C` holds for `1` and all elements of `S i` for all `i`, and is preserved under multiplication,
then it holds for all elements of the supremum of `S`. -/
@[to_additive (attr := elab_as_elim) " An induction principle for elements of `⨆ i, S i`.
If `C` holds for `0` and all elements of `S i` for all `i`, and is preserved under addition,
then it holds for all elements of the supremum of `S`. "]
theorem iSup_induction {ι : Sort*} (S : ι → Subgroup G) {C : G → Prop} {x : G} (hx : x ∈ ⨆ i, S i)
    (mem : ∀ (i), ∀ x ∈ S i, C x) (one : C 1) (mul : ∀ x y, C x → C y → C (x * y)) : C x := by
  rw [iSup_eq_closure] at hx
  induction hx using closure_induction'' with
  | one => exact one
  | mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ hi
  | inv_mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ (inv_mem hi)
  | mul x y _ _ ihx ihy => exact mul x y ihx ihy

Induction Principle for Elements in the Supremum of Subgroups

Informal description

Let $G$ be a group and $(S_i)_{i \in \iota}$ be a family of subgroups of $G$. For any predicate $C$ on elements of $G$ and any element $x$ in the supremum $\bigsqcup_i S_i$, if: 1. $C$ holds for every element in each $S_i$, 2. $C$ holds for the identity element $1 \in G$, and 3. For any $x, y \in G$, if $C$ holds for $x$ and $y$, then $C$ holds for $x \cdot y$, then $C$ holds for $x$.

Subgroup.iSup_induction' theorem

 {ι : Sort*} (S : ι → Subgroup G) {C : ∀ x, (x ∈ ⨆ i, S i) → Prop}
  (hp : ∀ (i), ∀ x (hx : x ∈ S i), C x (mem_iSup_of_mem i hx)) (h1 : C 1 (one_mem _))
  (hmul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem ‹_› ‹_›)) {x : G} (hx : x ∈ ⨆ i, S i) : C x hx

Full source

/-- A dependent version of `Subgroup.iSup_induction`. -/
@[to_additive (attr := elab_as_elim) "A dependent version of `AddSubgroup.iSup_induction`. "]
theorem iSup_induction' {ι : Sort*} (S : ι → Subgroup G) {C : ∀ x, (x ∈ ⨆ i, S i) → Prop}
    (hp : ∀ (i), ∀ x (hx : x ∈ S i), C x (mem_iSup_of_mem i hx)) (h1 : C 1 (one_mem _))
    (hmul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem ‹_› ‹_›)) {x : G}
    (hx : x ∈ ⨆ i, S i) : C x hx := by
  suffices ∃ h, C x h from this.snd
  refine iSup_induction S (C := fun x => ∃ h, C x h) hx (fun i x hx => ?_) ?_ fun x y => ?_
  · exact ⟨_, hp i _ hx⟩
  · exact ⟨_, h1⟩
  · rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, hmul _ _ _ _ Cx Cy⟩

Dependent Induction Principle for Elements in the Supremum of Subgroups

Informal description

Let $G$ be a group and $(S_i)_{i \in \iota}$ be a family of subgroups of $G$. For any predicate $C$ on elements of $G$ with a proof of membership in $\bigsqcup_i S_i$, if: 1. For every index $i$ and every $x \in S_i$, $C$ holds for $x$ with its membership proof in $\bigsqcup_i S_i$, 2. $C$ holds for the identity element $1 \in G$ with its membership proof, and 3. For any $x, y \in G$ with membership proofs $hx$ and $hy$ in $\bigsqcup_i S_i$, if $C$ holds for $x$ with $hx$ and for $y$ with $hy$, then $C$ holds for $x \cdot y$ with its membership proof, then $C$ holds for any $x \in \bigsqcup_i S_i$ with its membership proof.

Subgroup.closure_mul_le theorem

(S T : Set G) : closure (S * T) ≤ closure S ⊔ closure T

Full source

@[to_additive]
theorem closure_mul_le (S T : Set G) : closure (S * T) ≤ closureclosure S ⊔ closure T :=
  sInf_le fun _x ⟨_s, hs, _t, ht, hx⟩ => hx ▸
    (closureclosure S ⊔ closure T).mul_mem (SetLike.le_def.mp le_sup_left <| subset_closure hs)
      (SetLike.le_def.mp le_sup_right <| subset_closure ht)

Subgroup Generated by Product Set is Contained in Join of Generated Subgroups

Informal description

For any two subsets $S$ and $T$ of a group $G$, the subgroup generated by the product set $S * T$ is contained in the join of the subgroups generated by $S$ and $T$, i.e., $\langle S * T \rangle \leq \langle S \rangle \sqcup \langle T \rangle$.

Subgroup.closure_pow_le theorem

: ∀ {n}, n ≠ 0 → closure (s ^ n) ≤ closure s

Full source

@[to_additive]
lemma closure_pow_le : ∀ {n}, n ≠ 0 → closure (s ^ n) ≤ closure s
  | 1, _ => by simp
  | n + 2, _ =>
    calc
      closure (s ^ (n + 2))
      _ = closure (s ^ (n + 1) * s) := by rw [pow_succ]
      _ ≤ closure (s ^ (n + 1)) ⊔ closure s := closure_mul_le ..
      _ ≤ closure s ⊔ closure s := by gcongr ?_ ⊔ _; exact closure_pow_le n.succ_ne_zero
      _ = closure s := sup_idem _

Subgroup Generated by Power Set is Contained in Original Subgroup: $\langle s^n \rangle \leq \langle s \rangle$ for $n \neq 0$

Informal description

For any natural number $n \neq 0$ and any subset $s$ of a group $G$, the subgroup generated by the $n$-th power set $s^n$ is contained in the subgroup generated by $s$, i.e., $\langle s^n \rangle \leq \langle s \rangle$.

Subgroup.closure_pow theorem

{n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : closure (s ^ n) = closure s

Full source

@[to_additive]
lemma closure_pow {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : closure (s ^ n) = closure s :=
  (closure_pow_le hn).antisymm <| by gcongr; exact subset_pow hs hn

Subgroup Generated by Power Set Equals Original Subgroup when Identity is Present: $\langle s^n \rangle = \langle s \rangle$ for $1 \in s$ and $n \neq 0$

Informal description

For any subset $s$ of a group $G$ containing the identity element $1$, and for any nonzero natural number $n$, the subgroup generated by the $n$-th power set $s^n$ is equal to the subgroup generated by $s$, i.e., $\langle s^n \rangle = \langle s \rangle$.

Subgroup.sup_eq_closure_mul theorem

(H K : Subgroup G) : H ⊔ K = closure ((H : Set G) * (K : Set G))

Full source

@[to_additive]
theorem sup_eq_closure_mul (H K : Subgroup G) : H ⊔ K = closure ((H : Set G) * (K : Set G)) :=
  le_antisymm
    (sup_le (fun h hh => subset_closure ⟨h, hh, 1, K.one_mem, mul_one h⟩) fun k hk =>
      subset_closure ⟨1, H.one_mem, k, hk, one_mul k⟩)
    ((closure_mul_le _ _).trans <| by rw [closure_eq, closure_eq])

Supremum of Subgroups Equals Closure of Their Product Set

Informal description

For any two subgroups $H$ and $K$ of a group $G$, the supremum (join) $H \sqcup K$ in the lattice of subgroups is equal to the subgroup generated by the product set $H \cdot K = \{h \cdot k \mid h \in H, k \in K\}$.

Subgroup.set_mul_normalizer_comm theorem

(S : Set G) (N : Subgroup G) (hLE : S ⊆ N.normalizer) : S * N = N * S

Full source

@[to_additive]
theorem set_mul_normalizer_comm (S : Set G) (N : Subgroup G) (hLE : S ⊆ N.normalizer) :
    S * N = N * S := by
  rw [← iUnion_mul_left_image, ← iUnion_mul_right_image]
  simp only [image_mul_left, image_mul_right, Set.preimage]
  congr! 5 with s hs x
  exact (mem_normalizer_iff'.mp (inv_mem (hLE hs)) x).symm

Commutativity of Set-Subgroup Product under Normalizer Condition

Informal description

For any subset $S$ of a group $G$ and any subgroup $N$ of $G$, if $S$ is contained in the normalizer of $N$, then the product set $S \cdot N$ is equal to $N \cdot S$.

Subgroup.set_mul_normal_comm theorem

(S : Set G) (N : Subgroup G) [hN : N.Normal] : S * (N : Set G) = (N : Set G) * S

Full source

@[to_additive]
theorem set_mul_normal_comm (S : Set G) (N : Subgroup G) [hN : N.Normal] :
    S * (N : Set G) = (N : Set G) * S := set_mul_normalizer_comm S N subset_normalizer_of_normal

Commutativity of Set-Normal Subgroup Product

Informal description

For any subset $S$ of a group $G$ and any normal subgroup $N$ of $G$, the product set $S \cdot N$ is equal to $N \cdot S$, where $S \cdot N$ denotes the set $\{s \cdot n \mid s \in S, n \in N\}$ and similarly for $N \cdot S$.

Subgroup.coe_mul_of_left_le_normalizer_right theorem

(H N : Subgroup G) (hLE : H ≤ N.normalizer) : (↑(H ⊔ N) : Set G) = H * N

Full source

/-- The carrier of `H ⊔ N` is just `↑H * ↑N` (pointwise set product)
when `H` is a subgroup of the normalizer of `N` in `G`. -/
@[to_additive "The carrier of `H ⊔ N` is just `↑H + ↑N` (pointwise set addition)
when `H` is a subgroup of the normalizer of `N` in `G`."]
theorem coe_mul_of_left_le_normalizer_right (H N : Subgroup G) (hLE : H ≤ N.normalizer) :
    (↑(H ⊔ N) : Set G) = H * N := by
  rw [sup_eq_closure_mul]
  refine Set.Subset.antisymm (fun x hx => ?_) subset_closure
  induction hx using closure_induction'' with
  | one => exact ⟨1, one_mem _, 1, one_mem _, mul_one 1⟩
  | mem _ hx => exact hx
  | inv_mem x hx =>
    obtain ⟨x, hx, y, hy, rfl⟩ := hx
    simpa only [mul_inv_rev, mul_assoc, inv_inv, inv_mul_cancel_left]
      using mul_mem_mul (inv_mem hx) ((mem_normalizer_iff.mp (hLE hx) y⁻¹).mp (inv_mem hy))
  | mul x' x' _ _ hx hx' =>
    obtain ⟨x, hx, y, hy, rfl⟩ := hx
    obtain ⟨x', hx', y', hy', rfl⟩ := hx'
    refine ⟨x * x', mul_mem hx hx', x'⁻¹ * y * x' * y', mul_mem ?_ hy', ?_⟩
    · exact (mem_normalizer_iff''.mp (hLE hx') y).mp hy
    · simp only [mul_assoc, mul_inv_cancel_left]

Join of Subgroups as Product Set under Normalizer Condition

Informal description

Let $H$ and $N$ be subgroups of a group $G$ such that $H$ is contained in the normalizer of $N$. Then the underlying set of the join $H \sqcup N$ is equal to the pointwise product $H \cdot N = \{h \cdot n \mid h \in H, n \in N\}$.

Subgroup.coe_mul_of_right_le_normalizer_left theorem

(N H : Subgroup G) (hLE : H ≤ N.normalizer) : (↑(N ⊔ H) : Set G) = N * H

Full source

/-- The carrier of `N ⊔ H` is just `↑N * ↑H` (pointwise set product) when
`H` is a subgroup of the normalizer of `N` in `G`. -/
@[to_additive "The carrier of `N ⊔ H` is just `↑N + ↑H` (pointwise set addition)
when `H` is a subgroup of the normalizer of `N` in `G`."]
theorem coe_mul_of_right_le_normalizer_left (N H : Subgroup G) (hLE : H ≤ N.normalizer) :
    (↑(N ⊔ H) : Set G) = N * H := by
  rw [← set_mul_normalizer_comm _ _ hLE, sup_comm, coe_mul_of_left_le_normalizer_right _ _ hLE]

Join of Subgroups as Product Set under Normalizer Condition (Right Version)

Informal description

Let $N$ and $H$ be subgroups of a group $G$ such that $H$ is contained in the normalizer of $N$. Then the underlying set of the join $N \sqcup H$ is equal to the pointwise product $N \cdot H = \{n \cdot h \mid n \in N, h \in H\}$.

Subgroup.mul_normal theorem

(H N : Subgroup G) [hN : N.Normal] : (↑(H ⊔ N) : Set G) = H * N

Full source

/-- The carrier of `H ⊔ N` is just `↑H * ↑N` (pointwise set product) when `N` is normal. -/
@[to_additive "The carrier of `H ⊔ N` is just `↑H + ↑N` (pointwise set addition)
when `N` is normal."]
theorem mul_normal (H N : Subgroup G) [hN : N.Normal] : (↑(H ⊔ N) : Set G) = H * N :=
  coe_mul_of_left_le_normalizer_right H N le_normalizer_of_normal

Join of Subgroup with Normal Subgroup as Product Set

Informal description

Let $H$ and $N$ be subgroups of a group $G$, with $N$ normal in $G$. Then the underlying set of the join $H \sqcup N$ is equal to the pointwise product set $H \cdot N = \{h \cdot n \mid h \in H, n \in N\}$.

Subgroup.normal_mul theorem

(N H : Subgroup G) [N.Normal] : (↑(N ⊔ H) : Set G) = N * H

Full source

/-- The carrier of `N ⊔ H` is just `↑N * ↑H` (pointwise set product) when `N` is normal. -/
@[to_additive "The carrier of `N ⊔ H` is just `↑N + ↑H` (pointwise set addition)
when `N` is normal."]
theorem normal_mul (N H : Subgroup G) [N.Normal] : (↑(N ⊔ H) : Set G) = N * H :=
  coe_mul_of_right_le_normalizer_left N H le_normalizer_of_normal

Join of Normal Subgroup with Another Subgroup as Product Set

Informal description

Let $G$ be a group with subgroups $N$ and $H$, where $N$ is normal in $G$. Then the underlying set of the join $N \sqcup H$ is equal to the pointwise product set $N \cdot H = \{n \cdot h \mid n \in N, h \in H\}$.

Subgroup.mul_inf_assoc theorem

(A B C : Subgroup G) (h : A ≤ C) : (A : Set G) * ↑(B ⊓ C) = (A : Set G) * (B : Set G) ∩ C

Full source

@[to_additive]
theorem mul_inf_assoc (A B C : Subgroup G) (h : A ≤ C) :
    (A : Set G) * ↑(B ⊓ C) = (A : Set G) * (B : Set G) ∩ C := by
  ext
  simp only [coe_inf, Set.mem_mul, Set.mem_inter_iff]
  constructor
  · rintro ⟨y, hy, z, ⟨hzB, hzC⟩, rfl⟩
    refine ⟨?_, mul_mem (h hy) hzC⟩
    exact ⟨y, hy, z, hzB, rfl⟩
  rintro ⟨⟨y, hy, z, hz, rfl⟩, hyz⟩
  refine ⟨y, hy, z, ⟨hz, ?_⟩, rfl⟩
  suffices y⁻¹y⁻¹ * (y * z) ∈ C by simpa
  exact mul_mem (inv_mem (h hy)) hyz

Product-Intersection Associativity for Subgroups: $A \cdot (B \cap C) = (A \cdot B) \cap C$ when $A \leq C$

Informal description

Let $G$ be a group with subgroups $A$, $B$, and $C$ such that $A \leq C$. Then the product set $A \cdot (B \cap C)$ is equal to $(A \cdot B) \cap C$, where $\cdot$ denotes the group multiplication and $\cap$ denotes the intersection of subgroups.

Subgroup.inf_mul_assoc theorem

(A B C : Subgroup G) (h : C ≤ A) : ((A ⊓ B : Subgroup G) : Set G) * C = (A : Set G) ∩ (↑B * ↑C)

Full source

@[to_additive]
theorem inf_mul_assoc (A B C : Subgroup G) (h : C ≤ A) :
    ((A ⊓ B : Subgroup G) : Set G) * C = (A : Set G) ∩ (↑B * ↑C) := by
  ext
  simp only [coe_inf, Set.mem_mul, Set.mem_inter_iff]
  constructor
  · rintro ⟨y, ⟨hyA, hyB⟩, z, hz, rfl⟩
    refine ⟨A.mul_mem hyA (h hz), ?_⟩
    exact ⟨y, hyB, z, hz, rfl⟩
  rintro ⟨hyz, y, hy, z, hz, rfl⟩
  refine ⟨y, ⟨?_, hy⟩, z, hz, rfl⟩
  suffices y * z * z⁻¹ ∈ A by simpa
  exact mul_mem hyz (inv_mem (h hz))

Intersection-Product Associativity for Subgroups: $(A \cap B) \cdot C = A \cap (B \cdot C)$ when $C \subseteq A$

Informal description

Let $G$ be a group and let $A, B, C$ be subgroups of $G$ such that $C \subseteq A$. Then the product of the underlying sets of the subgroups $A \cap B$ and $C$ equals the intersection of the underlying set of $A$ with the product of the underlying sets of $B$ and $C$. In symbols: $$(A \cap B) \cdot C = A \cap (B \cdot C)$$ where $\cdot$ denotes the product of subsets and $\cap$ denotes set intersection.

Subgroup.sup_normal instance

(H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊔ K).Normal

Full source

@[to_additive]
instance sup_normal (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊔ K).Normal where
  conj_mem n hmem g := by
    rw [← SetLike.mem_coe, normal_mul] at hmem ⊢
    rcases hmem with ⟨h, hh, k, hk, rfl⟩
    refine ⟨g * h * g⁻¹, hH.conj_mem h hh g, g * k * g⁻¹, hK.conj_mem k hk g, ?_⟩
    simp only [mul_assoc, inv_mul_cancel_left]

Join of Normal Subgroups is Normal

Informal description

For any normal subgroups $H$ and $K$ of a group $G$, the join $H \sqcup K$ is also a normal subgroup of $G$.

Subgroup.smul_mem_of_mem_closure_of_mem theorem

 {X : Type*} [MulAction G X] {s : Set G} {t : Set X} (hs : ∀ g ∈ s, g⁻¹ ∈ s) (hst : ∀ᵉ (g ∈ s) (x ∈ t), g • x ∈ t)
  {g : G} (hg : g ∈ Subgroup.closure s) {x : X} (hx : x ∈ t) : g • x ∈ t

Full source

@[to_additive]
theorem smul_mem_of_mem_closure_of_mem {X : Type*} [MulAction G X] {s : Set G} {t : Set X}
    (hs : ∀ g ∈ s, g⁻¹ ∈ s) (hst : ∀ᵉ (g ∈ s) (x ∈ t), g • x ∈ t) {g : G}
    (hg : g ∈ Subgroup.closure s) {x : X} (hx : x ∈ t) : g • x ∈ t := by
  induction hg using Subgroup.closure_induction'' generalizing x with
  | one => simpa
  | mem g' hg' => exact hst g' hg' x hx
  | inv_mem g' hg' => exact hst g'⁻¹ (hs g' hg') x hx
  | mul _ _ _ _ h₁ h₂ => rw [mul_smul]; exact h₁ (h₂ hx)

Stability of Subset under Group Action via Subgroup Closure

Informal description

Let $G$ be a group acting on a type $X$, $s$ a subset of $G$ closed under inversion (i.e., $g \in s$ implies $g^{-1} \in s$), and $t$ a subset of $X$ such that for every $g \in s$ and $x \in t$, the action $g \cdot x$ belongs to $t$. Then for any $g$ in the subgroup generated by $s$ and any $x \in t$, the action $g \cdot x$ also belongs to $t$.

Subgroup.smul_opposite_image_mul_preimage' theorem

 (g : G) (h : Gᵐᵒᵖ) (s : Set G) : (fun y => h • y) '' ((g * ·) ⁻¹' s) = (g * ·) ⁻¹' ((fun y => h • y) '' s)

Full source

@[to_additive]
theorem smul_opposite_image_mul_preimage' (g : G) (h : Gᵐᵒᵖ) (s : Set G) :
    (fun y => h • y) '' ((g * ·) ⁻¹' s) = (g * ·) ⁻¹' ((fun y => h • y) '' s) := by
  simp [preimage_preimage, mul_assoc]

Commutativity of Opposite Group Action with Left Multiplication Preimage

Informal description

Let $G$ be a group, $g \in G$, $h \in G^\text{op}$ (the multiplicative opposite group of $G$), and $s \subseteq G$ a subset. Then the image of the preimage of $s$ under left multiplication by $g$ under the action of $h$ equals the preimage under left multiplication by $g$ of the image of $s$ under the action of $h$. In symbols: $$ h \cdot (g^{-1}s) = g^{-1}(h \cdot s) $$ where $h \cdot$ denotes the action of $h$ and $g^{-1}s$ denotes $\{x \in G \mid gx \in s\}$.

Subgroup.smul_opposite_image_mul_preimage theorem

 {H : Subgroup G} (g : G) (h : H.op) (s : Set G) :
  (fun y => h • y) '' ((g * ·) ⁻¹' s) = (g * ·) ⁻¹' ((fun y => h • y) '' s)

Full source

@[to_additive]
theorem smul_opposite_image_mul_preimage {H : Subgroup G} (g : G) (h : H.op) (s : Set G) :
    (fun y => h • y) '' ((g * ·) ⁻¹' s) = (g * ·) ⁻¹' ((fun y => h • y) '' s) :=
  smul_opposite_image_mul_preimage' g h s

Commutativity of Subgroup Opposite Action with Left Multiplication Preimage

Informal description

Let $G$ be a group and $H$ a subgroup of $G$. For any element $g \in G$, any element $h$ in the opposite subgroup $H^\text{op}$, and any subset $s \subseteq G$, the image of the preimage of $s$ under left multiplication by $g$ under the action of $h$ equals the preimage under left multiplication by $g$ of the image of $s$ under the action of $h$. In symbols: $$ h \cdot (g^{-1}s) = g^{-1}(h \cdot s) $$ where $h \cdot$ denotes the action of $h$ and $g^{-1}s$ denotes $\{x \in G \mid gx \in s\}$.

Subgroup.pointwiseMulAction definition

: MulAction α (Subgroup G)

Full source

/-- The action on a subgroup corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseMulAction : MulAction α (Subgroup G) where
  smul a S := S.map (MulDistribMulAction.toMonoidEnd _ _ a)
  one_smul S := by
    change S.map _ = S
    simpa only [map_one] using S.map_id
  mul_smul _ _ S :=
    (congr_arg (fun f : Monoid.End G => S.map f) (MonoidHom.map_mul _ _ _)).trans
      (S.map_map _ _).symm

Pointwise action of a monoid on subgroups

Informal description

Given a monoid $\alpha$ acting distributively on a group $G$, the pointwise action of $\alpha$ on the subgroups of $G$ is defined by mapping each subgroup $S$ under the monoid endomorphism of $G$ induced by the action of $a \in \alpha$. This action satisfies: 1. The identity element of $\alpha$ acts trivially: $1 \cdot S = S$. 2. The action is compatible with multiplication in $\alpha$: $(a_1 a_2) \cdot S = a_1 \cdot (a_2 \cdot S)$.

Subgroup.pointwise_smul_def theorem

{a : α} (S : Subgroup G) : a • S = S.map (MulDistribMulAction.toMonoidEnd _ _ a)

Full source

theorem pointwise_smul_def {a : α} (S : Subgroup G) :
    a • S = S.map (MulDistribMulAction.toMonoidEnd _ _ a) :=
  rfl

Definition of Pointwise Scalar Multiplication on Subgroups

Informal description

Let $G$ be a group and $\alpha$ a monoid acting distributively on $G$. For any element $a \in \alpha$ and any subgroup $S$ of $G$, the pointwise scalar multiplication $a \cdot S$ is equal to the image of $S$ under the monoid homomorphism from $\alpha$ to the endomorphisms of $G$ induced by the action of $a$.

Subgroup.coe_pointwise_smul theorem

(a : α) (S : Subgroup G) : ↑(a • S) = a • (S : Set G)

Full source

@[simp]
theorem coe_pointwise_smul (a : α) (S : Subgroup G) : ↑(a • S) = a • (S : Set G) :=
  rfl

Pointwise Scalar Multiplication of Subgroup and Underlying Set Coincide

Informal description

For any element $a$ of a monoid $\alpha$ and any subgroup $S$ of a group $G$, the underlying set of the pointwise scalar multiplication $a \cdot S$ is equal to the pointwise scalar multiplication of $a$ with the underlying set of $S$. In other words, $\overline{a \cdot S} = a \cdot \overline{S}$, where $\overline{S}$ denotes the underlying set of $S$.

Subgroup.pointwise_smul_toSubmonoid theorem

(a : α) (S : Subgroup G) : (a • S).toSubmonoid = a • S.toSubmonoid

Full source

@[simp]
theorem pointwise_smul_toSubmonoid (a : α) (S : Subgroup G) :
    (a • S).toSubmonoid = a • S.toSubmonoid :=
  rfl

Pointwise Action Preserves Submonoid Structure

Informal description

For any element $a$ of a monoid $\alpha$ acting distributively on a group $G$, and for any subgroup $S$ of $G$, the submonoid associated with the pointwise action $a \cdot S$ is equal to the pointwise action of $a$ on the submonoid associated with $S$. In other words, $(a \cdot S).toSubmonoid = a \cdot S.toSubmonoid$.

Subgroup.smul_mem_pointwise_smul theorem

(m : G) (a : α) (S : Subgroup G) : m ∈ S → a • m ∈ a • S

Full source

theorem smul_mem_pointwise_smul (m : G) (a : α) (S : Subgroup G) : m ∈ S → a • m ∈ a • S :=
  (Set.smul_mem_smul_set : _ → _ ∈ a • (S : Set G))

Action Preserves Subgroup Membership under Pointwise Scalar Multiplication

Informal description

Let $G$ be a group and $\alpha$ a monoid acting distributively on $G$. For any element $m \in G$, any element $a \in \alpha$, and any subgroup $S$ of $G$, if $m \in S$, then the action of $a$ on $m$ is in the action of $a$ on $S$, i.e., $a \cdot m \in a \cdot S$.

Subgroup.instCovariantClassHSMulLe instance

: CovariantClass α (Subgroup G) HSMul.hSMul LE.le

Full source

instance : CovariantClass α (Subgroup G) HSMul.hSMul LE.le :=
  ⟨fun _ _ => image_subset _⟩

Preservation of Subgroup Inclusion under Pointwise Action

Informal description

For a monoid $\alpha$ acting distributively on a group $G$, the pointwise action of $\alpha$ on the subgroups of $G$ preserves the subgroup inclusion relation. That is, for any $a \in \alpha$ and subgroups $S, T \subseteq G$, if $S \subseteq T$, then $a \cdot S \subseteq a \cdot T$.

Subgroup.mem_smul_pointwise_iff_exists theorem

(m : G) (a : α) (S : Subgroup G) : m ∈ a • S ↔ ∃ s : G, s ∈ S ∧ a • s = m

Full source

theorem mem_smul_pointwise_iff_exists (m : G) (a : α) (S : Subgroup G) :
    m ∈ a • Sm ∈ a • S ↔ ∃ s : G, s ∈ S ∧ a • s = m :=
  (Set.mem_smul_set : m ∈ a • (S : Set G)m ∈ a • (S : Set G) ↔ _)

Characterization of Pointwise Action on Subgroups: $m \in a \cdot S \leftrightarrow \exists s \in S, a \cdot s = m$

Informal description

Let $G$ be a group and $\alpha$ a monoid acting on $G$. For any element $m \in G$, any $a \in \alpha$, and any subgroup $S$ of $G$, the element $m$ belongs to the pointwise action $a \cdot S$ if and only if there exists an element $s \in S$ such that $a \cdot s = m$.

Subgroup.smul_bot theorem

(a : α) : a • (⊥ : Subgroup G) = ⊥

Full source

@[simp]
theorem smul_bot (a : α) : a • (⊥ : Subgroup G) = ⊥ :=
  map_bot _

Pointwise action preserves the trivial subgroup

Informal description

For any element $a$ of a monoid $\alpha$ acting on a group $G$, the pointwise action of $a$ on the trivial subgroup $\bot$ of $G$ is the trivial subgroup, i.e., $a \cdot \bot = \bot$.

Subgroup.smul_sup theorem

(a : α) (S T : Subgroup G) : a • (S ⊔ T) = a • S ⊔ a • T

Full source

theorem smul_sup (a : α) (S T : Subgroup G) : a • (S ⊔ T) = a • S ⊔ a • T :=
  map_sup _ _ _

Distributivity of Pointwise Action over Subgroup Join

Informal description

Let $G$ be a group and $\alpha$ a monoid acting distributively on $G$. For any element $a \in \alpha$ and any subgroups $S, T$ of $G$, the action of $a$ on the join (supremum) of $S$ and $T$ equals the join of the actions of $a$ on $S$ and $T$: \[ a \cdot (S \sqcup T) = (a \cdot S) \sqcup (a \cdot T). \]

Subgroup.smul_closure theorem

(a : α) (s : Set G) : a • closure s = closure (a • s)

Full source

theorem smul_closure (a : α) (s : Set G) : a • closure s = closure (a • s) :=
  MonoidHom.map_closure _ _

Action on Generated Subgroup Equals Generated Action Subgroup

Informal description

Let $G$ be a group and $\alpha$ a monoid acting distributively on $G$. For any element $a \in \alpha$ and any subset $s \subseteq G$, the action of $a$ on the subgroup generated by $s$ equals the subgroup generated by the action of $a$ on $s$. That is: \[ a \cdot \langle s \rangle = \langle a \cdot s \rangle \]

Subgroup.pointwise_isCentralScalar instance

[MulDistribMulAction αᵐᵒᵖ G] [IsCentralScalar α G] : IsCentralScalar α (Subgroup G)

Full source

instance pointwise_isCentralScalar [MulDistribMulAction αᵐᵒᵖ G] [IsCentralScalar α G] :
    IsCentralScalar α (Subgroup G) :=
  ⟨fun _ S => (congr_arg fun f => S.map f) <| MonoidHom.ext <| op_smul_eq_smul _⟩

Central Scalar Action on Subgroups via Pointwise Multiplication

Informal description

For any monoid $\alpha$ acting distributively on a group $G$ with a central scalar action, the pointwise action of $\alpha$ on the subgroups of $G$ is also a central scalar action. This means that for any $a \in \alpha$ and any subgroup $S$ of $G$, the left action $a \cdot S$ and the right action via the multiplicative opposite $\text{op}(a) \cdot S$ coincide.

Subgroup.conj_smul_le_of_le theorem

{P H : Subgroup G} (hP : P ≤ H) (h : H) : MulAut.conj (h : G) • P ≤ H

Full source

theorem conj_smul_le_of_le {P H : Subgroup G} (hP : P ≤ H) (h : H) :
    MulAut.conj (h : G) • P ≤ H := by
  rintro - ⟨g, hg, rfl⟩
  exact H.mul_mem (H.mul_mem h.2 (hP hg)) (H.inv_mem h.2)

Conjugation by Subgroup Elements Preserves Subgroup Containment

Informal description

Let $G$ be a group with subgroups $P$ and $H$ such that $P \leq H$. For any element $h \in H$, the conjugation action of $h$ on $P$ (given by $g \mapsto hgh^{-1}$ for $g \in P$) preserves the containment in $H$, i.e., $\text{conj}_h(P) \leq H$.

Subgroup.conj_smul_subgroupOf theorem

{P H : Subgroup G} (hP : P ≤ H) (h : H) : MulAut.conj h • P.subgroupOf H = (MulAut.conj (h : G) • P).subgroupOf H

Full source

theorem conj_smul_subgroupOf {P H : Subgroup G} (hP : P ≤ H) (h : H) :
    MulAut.conj h • P.subgroupOf H = (MulAut.conj (h : G) • P).subgroupOf H := by
  refine le_antisymm ?_ ?_
  · rintro - ⟨g, hg, rfl⟩
    exact ⟨g, hg, rfl⟩
  · rintro p ⟨g, hg, hp⟩
    exact ⟨⟨g, hP hg⟩, hg, Subtype.ext hp⟩

Conjugation Action on Subgroup Intersection: $h(P \cap H)h^{-1} = (hPh^{-1}) \cap H$

Informal description

Let $G$ be a group with subgroups $P$ and $H$ such that $P \leq H$, and let $h \in H$. Then the conjugation action of $h$ on the subgroup $P \cap H$ (viewed as a subgroup of $H$) is equal to the conjugation action of $h$ (viewed as an element of $G$) on $P$, intersected with $H$ and viewed as a subgroup of $H$. In other words: \[ h \cdot (P \cap H) \cdot h^{-1} = (h \cdot P \cdot h^{-1}) \cap H \] where both sides are considered as subgroups of $H$.

Subgroup.smul_mem_pointwise_smul_iff theorem

{a : α} {S : Subgroup G} {x : G} : a • x ∈ a • S ↔ x ∈ S

Full source

@[simp]
theorem smul_mem_pointwise_smul_iff {a : α} {S : Subgroup G} {x : G} : a • x ∈ a • Sa • x ∈ a • S ↔ x ∈ S :=
  smul_mem_smul_set_iff

Membership in Pointwise Scaled Subgroup: $a \cdot x \in a \cdot S \leftrightarrow x \in S$

Informal description

For any element $a$ of a monoid $\alpha$ acting on a group $G$, any subgroup $S$ of $G$, and any element $x \in G$, the element $a \cdot x$ belongs to the pointwise scaled subgroup $a \cdot S$ if and only if $x$ belongs to $S$.

Subgroup.mem_pointwise_smul_iff_inv_smul_mem theorem

{a : α} {S : Subgroup G} {x : G} : x ∈ a • S ↔ a⁻¹ • x ∈ S

Full source

theorem mem_pointwise_smul_iff_inv_smul_mem {a : α} {S : Subgroup G} {x : G} :
    x ∈ a • Sx ∈ a • S ↔ a⁻¹ • x ∈ S :=
  mem_smul_set_iff_inv_smul_mem

Characterization of membership in scaled subgroup via inverse action: $x \in a \cdot S \leftrightarrow a^{-1} \cdot x \in S$

Informal description

For any element $a$ of a monoid $\alpha$ acting on a group $G$, any subgroup $S$ of $G$, and any element $x \in G$, we have: \[ x \in a \cdot S \leftrightarrow a^{-1} \cdot x \in S. \]

Subgroup.mem_inv_pointwise_smul_iff theorem

{a : α} {S : Subgroup G} {x : G} : x ∈ a⁻¹ • S ↔ a • x ∈ S

Full source

theorem mem_inv_pointwise_smul_iff {a : α} {S : Subgroup G} {x : G} : x ∈ a⁻¹ • Sx ∈ a⁻¹ • S ↔ a • x ∈ S :=
  mem_inv_smul_set_iff

Characterization of Membership in Inversely Scaled Subgroup: $x \in a^{-1} \cdot S \leftrightarrow a \cdot x \in S$

Informal description

For any element $a$ of a monoid $\alpha$ acting on a group $G$, any subgroup $S$ of $G$, and any element $x \in G$, we have $x \in a^{-1} \cdot S$ if and only if $a \cdot x \in S$.

Subgroup.pointwise_smul_le_pointwise_smul_iff theorem

{a : α} {S T : Subgroup G} : a • S ≤ a • T ↔ S ≤ T

Full source

@[simp]
theorem pointwise_smul_le_pointwise_smul_iff {a : α} {S T : Subgroup G} : a • S ≤ a • T ↔ S ≤ T :=
  smul_set_subset_smul_set_iff

Pointwise Action Preserves Subgroup Inclusion: $a \cdot S \leq a \cdot T \leftrightarrow S \leq T$

Informal description

For any element $a$ of a monoid $\alpha$ acting on a group $G$, and any subgroups $S$ and $T$ of $G$, the pointwise action satisfies $a \cdot S \leq a \cdot T$ if and only if $S \leq T$.

Subgroup.pointwise_smul_subset_iff theorem

{a : α} {S T : Subgroup G} : a • S ≤ T ↔ S ≤ a⁻¹ • T

Full source

theorem pointwise_smul_subset_iff {a : α} {S T : Subgroup G} : a • S ≤ T ↔ S ≤ a⁻¹ • T :=
  smul_set_subset_iff_subset_inv_smul_set

Subgroup Pointwise Action Subset Relation: $a \cdot S \subseteq T \leftrightarrow S \subseteq a^{-1} \cdot T$

Informal description

For any element $a$ of a monoid $\alpha$ acting on a group $G$, and any subgroups $S$ and $T$ of $G$, the pointwise action satisfies $a \cdot S \subseteq T$ if and only if $S \subseteq a^{-1} \cdot T$.

Subgroup.subset_pointwise_smul_iff theorem

{a : α} {S T : Subgroup G} : S ≤ a • T ↔ a⁻¹ • S ≤ T

Full source

theorem subset_pointwise_smul_iff {a : α} {S T : Subgroup G} : S ≤ a • T ↔ a⁻¹ • S ≤ T :=
  subset_smul_set_iff

Subgroup Inclusion under Pointwise Action: $S \subseteq a \cdot T \leftrightarrow a^{-1} \cdot S \subseteq T$

Informal description

For any element $a$ of a monoid $\alpha$ acting on a group $G$, and any subgroups $S$ and $T$ of $G$, the inclusion $S \subseteq a \cdot T$ holds if and only if $a^{-1} \cdot S \subseteq T$.

Subgroup.smul_inf theorem

(a : α) (S T : Subgroup G) : a • (S ⊓ T) = a • S ⊓ a • T

Full source

@[simp]
theorem smul_inf (a : α) (S T : Subgroup G) : a • (S ⊓ T) = a • S ⊓ a • T := by
  simp [SetLike.ext_iff, mem_pointwise_smul_iff_inv_smul_mem]

Action Preserves Subgroup Intersection: $a \cdot (S \cap T) = (a \cdot S) \cap (a \cdot T)$

Informal description

Let $G$ be a group and $\alpha$ a monoid acting distributively on $G$. For any element $a \in \alpha$ and any two subgroups $S, T$ of $G$, the action of $a$ on the intersection of $S$ and $T$ is equal to the intersection of the actions of $a$ on $S$ and $T$, i.e., \[ a \cdot (S \cap T) = (a \cdot S) \cap (a \cdot T). \]

Subgroup.equivSMul definition

(a : α) (H : Subgroup G) : H ≃* (a • H : Subgroup G)

Full source

/-- Applying a `MulDistribMulAction` results in an isomorphic subgroup -/
@[simps!]
def equivSMul (a : α) (H : Subgroup G) : H ≃* (a • H : Subgroup G) :=
  (MulDistribMulAction.toMulEquiv G a).subgroupMap H

Subgroup isomorphism induced by a distributive multiplicative action

Informal description

Given a group $G$ and a monoid $\alpha$ acting distributively on $G$, for any element $a \in \alpha$ and any subgroup $H$ of $G$, the map sending $h \in H$ to $a \cdot h$ defines a multiplicative equivalence (isomorphism) between $H$ and the image subgroup $a \cdot H$ under the action of $a$.

Subgroup.subgroup_mul_singleton theorem

{H : Subgroup G} {h : G} (hh : h ∈ H) : (H : Set G) * { h } = H

Full source

theorem subgroup_mul_singleton {H : Subgroup G} {h : G} (hh : h ∈ H) : (H : Set G) * {h} = H := by
  simp [preimage, mul_mem_cancel_right (inv_mem hh)]

Right Multiplication of Subgroup by Singleton Preserves Subgroup

Informal description

Let $G$ be a group and $H$ a subgroup of $G$. For any element $h \in H$, the product of the underlying set of $H$ with the singleton set $\{h\}$ equals $H$ itself, i.e., $H \cdot \{h\} = H$.

Subgroup.singleton_mul_subgroup theorem

{H : Subgroup G} {h : G} (hh : h ∈ H) : { h } * (H : Set G) = H

Full source

theorem singleton_mul_subgroup {H : Subgroup G} {h : G} (hh : h ∈ H) : {h} * (H : Set G) = H := by
  simp [preimage, mul_mem_cancel_left (inv_mem hh)]

Product of Singleton with Subgroup Equals Subgroup

Informal description

Let $G$ be a group and $H$ a subgroup of $G$. For any element $h \in H$, the product of the singleton set $\{h\}$ with the underlying set of $H$ equals $H$ itself, i.e., $\{h\} \cdot H = H$.

Subgroup.Normal.conjAct theorem

{H : Subgroup G} (hH : H.Normal) (g : ConjAct G) : g • H = H

Full source

theorem Normal.conjAct {H : Subgroup G} (hH : H.Normal) (g : ConjAct G) : g • H = H :=
  have : ∀ g : ConjAct G, g • H ≤ H :=
    fun _ => map_le_iff_le_comap.2 fun _ h => hH.conj_mem _ h _
  (this g).antisymm <| (smul_inv_smul g H).symm.trans_le (map_mono <| this _)

Invariance of Normal Subgroup under Conjugation Action

Informal description

Let $G$ be a group and $H$ a normal subgroup of $G$. For any element $g$ in the conjugation action $\text{ConjAct}\, G$, the action of $g$ on $H$ leaves $H$ invariant, i.e., $g \cdot H = H$.

Subgroup.Normal.conj_smul_eq_self theorem

(g : G) (H : Subgroup G) [h : Normal H] : MulAut.conj g • H = H

Full source

@[simp]
theorem Normal.conj_smul_eq_self (g : G) (H : Subgroup G) [h : Normal H] : MulAut.conj g • H = H :=
  h.conjAct g

Invariance of Normal Subgroup under Conjugation

Informal description

Let $G$ be a group and $H$ a normal subgroup of $G$. For any element $g \in G$, the conjugation action of $g$ on $H$ leaves $H$ invariant, i.e., $gHg^{-1} = H$.

Subgroup.Normal.of_conjugate_fixed theorem

{H : Subgroup G} (h : ∀ g : G, (MulAut.conj g) • H = H) : H.Normal

Full source

theorem Normal.of_conjugate_fixed {H : Subgroup G} (h : ∀ g : G, (MulAut.conj g) • H = H) :
    H.Normal := by
  constructor
  intro n hn g
  rw [← h g, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← map_inv, MulAut.smul_def,
    MulAut.conj_apply, inv_inv, mul_assoc, mul_assoc, inv_mul_cancel, mul_one,
    ← mul_assoc, inv_mul_cancel, one_mul]
  exact hn

Characterization of Normal Subgroups via Conjugation Invariance

Informal description

Let $G$ be a group and $H$ a subgroup of $G$. If for every element $g \in G$, the conjugation action of $g$ on $H$ leaves $H$ invariant (i.e., $gHg^{-1} = H$), then $H$ is a normal subgroup of $G$.

Subgroup.normalCore_eq_iInf_conjAct theorem

(H : Subgroup G) : H.normalCore = ⨅ (g : ConjAct G), g • H

Full source

theorem normalCore_eq_iInf_conjAct (H : Subgroup G) :
    H.normalCore = ⨅ (g : ConjAct G), g • H := by
  ext g
  simp only [Subgroup.normalCore, Subgroup.mem_iInf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem]
  refine ⟨fun h x ↦ h x⁻¹, fun h x ↦ ?_⟩
  simpa only [ConjAct.toConjAct_inv, inv_inv] using h x⁻¹

Normal Core as Intersection of Conjugates: $\text{core}(H) = \bigcap_{g \in G} gHg^{-1}$

Informal description

For any subgroup $H$ of a group $G$, the normal core of $H$ is equal to the infimum of the family of conjugate subgroups $\{gHg^{-1} \mid g \in G\}$. In other words, the normal core of $H$ is the intersection of all its conjugates in $G$.

Implementation notes