doc-next-gen

Mathlib.Algebra.Group.Subgroup.Basic

Module docstring

{"# Basic results on subgroups

We prove basic results on the definitions of subgroups. The bundled subgroups use bundled monoid homomorphisms.

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

Main definitions

Notation used here:

  • G N are Groups

  • A is an AddGroup

  • H K are Subgroups of G or AddSubgroups of A

  • x is an element of type G or type A

  • f g : N →* G are group homomorphisms

  • s k are sets of elements of type G

Definitions in the file:

  • Subgroup.prod H K : the product of subgroups H, K of groups G, N respectively, H × K is a subgroup of G × N

Implementation notes

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

Tags

subgroup, subgroups "}

div_mem_comm_iff theorem
{a b : G} : a / b ∈ H ↔ b / a ∈ H
Full source 
@[to_additive]
theorem div_mem_comm_iff {a b : G} : a / b ∈ Ha / b ∈ H ↔ b / a ∈ H :=
  inv_div b a ▸ inv_mem_iff
Quotient Membership Criterion in Subgroups: $a/b \in H \leftrightarrow b/a \in H$
Informal description
For any elements $a$ and $b$ in a group $G$ and any subgroup $H$ of $G$, the quotient $a / b$ belongs to $H$ if and only if the reverse quotient $b / a$ belongs to $H$, i.e., $a / b \in H \leftrightarrow b / a \in H$.
Subgroup.div_mem_comm_iff theorem
{a b : G} : a / b ∈ H ↔ b / a ∈ H
Full source 
@[to_additive]
protected theorem div_mem_comm_iff {a b : G} : a / b ∈ Ha / b ∈ H ↔ b / a ∈ H :=
  div_mem_comm_iff
Quotient Membership Criterion in Subgroups: $a/b \in H \leftrightarrow b/a \in H$
Informal description
For any elements $a$ and $b$ in a group $G$ and any subgroup $H$ of $G$, the quotient $a / b$ belongs to $H$ if and only if the reverse quotient $b / a$ belongs to $H$, i.e., $a / b \in H \leftrightarrow b / a \in H$.
Subgroup.prod definition
(H : Subgroup G) (K : Subgroup N) : Subgroup (G × N)
Full source 
/-- Given `Subgroup`s `H`, `K` of groups `G`, `N` respectively, `H × K` as a subgroup of `G × N`. -/
@[to_additive prod
      "Given `AddSubgroup`s `H`, `K` of `AddGroup`s `A`, `B` respectively, `H × K`
      as an `AddSubgroup` of `A × B`."]
def prod (H : Subgroup G) (K : Subgroup N) : Subgroup (G × N) :=
  { Submonoid.prod H.toSubmonoid K.toSubmonoid with
    inv_mem' := fun hx => ⟨H.inv_mem' hx.1, K.inv_mem' hx.2⟩ }
Product of subgroups
Informal description
Given subgroups $H$ of a group $G$ and $K$ of a group $N$, the product subgroup $H \times K$ is defined as the subgroup of $G \times N$ consisting of all pairs $(g, n)$ where $g \in H$ and $n \in K$. This subgroup is closed under the group operation and taking inverses.
Subgroup.coe_prod theorem
(H : Subgroup G) (K : Subgroup N) : (H.prod K : Set (G × N)) = (H : Set G) ×ˢ (K : Set N)
Full source 
@[to_additive coe_prod]
theorem coe_prod (H : Subgroup G) (K : Subgroup N) :
    (H.prod K : Set (G × N)) = (H : Set G) ×ˢ (K : Set N) :=
  rfl
Underlying Set of Product Subgroup Equals Cartesian Product of Underlying Sets
Informal description
For any subgroups $H$ of a group $G$ and $K$ of a group $N$, the underlying set of the product subgroup $H \times K$ is equal to the Cartesian product of the underlying sets of $H$ and $K$, i.e., $(H \times K) = H \timesˢ K$ as subsets of $G \times N$.
Subgroup.mem_prod theorem
{H : Subgroup G} {K : Subgroup N} {p : G × N} : p ∈ H.prod K ↔ p.1 ∈ H ∧ p.2 ∈ K
Full source 
@[to_additive mem_prod]
theorem mem_prod {H : Subgroup G} {K : Subgroup N} {p : G × N} : p ∈ H.prod Kp ∈ H.prod K ↔ p.1 ∈ H ∧ p.2 ∈ K :=
  Iff.rfl
Membership Criterion for Product Subgroup: $(g, n) \in H \times K \leftrightarrow g \in H \land n \in K$
Informal description
For any subgroups $H$ of a group $G$ and $K$ of a group $N$, and for any element $p = (g, n) \in G \times N$, we have $p \in H \times K$ if and only if $g \in H$ and $n \in K$.
Subgroup.prod_mono theorem
: ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) (@prod G _ N _) (@prod G _ N _)
Full source 
@[to_additive prod_mono]
theorem prod_mono : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) (@prod G _ N _) (@prod G _ N _) :=
  fun _s _s' hs _t _t' ht => Set.prod_mono hs ht
Monotonicity of Subgroup Product with Respect to Inclusion
Informal description
For any groups $G$ and $N$, the product operation on subgroups is monotone with respect to subgroup inclusion. That is, if $H_1 \leq H_2$ and $K_1 \leq K_2$ are subgroups of $G$ and $N$ respectively, then $H_1 \times K_1 \leq H_2 \times K_2$ as subgroups of $G \times N$.
Subgroup.prod_mono_right theorem
(K : Subgroup G) : Monotone fun t : Subgroup N => K.prod t
Full source 
@[to_additive prod_mono_right]
theorem prod_mono_right (K : Subgroup G) : Monotone fun t : Subgroup N => K.prod t :=
  prod_mono (le_refl K)
Monotonicity of Right Product Subgroup Construction
Informal description
For any subgroup $K$ of a group $G$, the function that takes a subgroup $t$ of a group $N$ to the product subgroup $K \times t$ is monotone with respect to the subgroup inclusion relation. That is, if $t_1 \leq t_2$ are subgroups of $N$, then $K \times t_1 \leq K \times t_2$ as subgroups of $G \times N$.
Subgroup.prod_mono_left theorem
(H : Subgroup N) : Monotone fun K : Subgroup G => K.prod H
Full source 
@[to_additive prod_mono_left]
theorem prod_mono_left (H : Subgroup N) : Monotone fun K : Subgroup G => K.prod H := fun _ _ hs =>
  prod_mono hs (le_refl H)
Monotonicity of Left Subgroup Product with Respect to Inclusion
Informal description
For any subgroup $H$ of a group $N$, the function that takes a subgroup $K$ of $G$ to the product subgroup $K \times H$ is monotone with respect to the subgroup inclusion relation. That is, if $K_1 \leq K_2$ are subgroups of $G$, then $K_1 \times H \leq K_2 \times H$ as subgroups of $G \times N$.
Subgroup.prod_top theorem
(K : Subgroup G) : K.prod (⊤ : Subgroup N) = K.comap (MonoidHom.fst G N)
Full source 
@[to_additive prod_top]
theorem prod_top (K : Subgroup G) : K.prod (⊤ : Subgroup N) = K.comap (MonoidHom.fst G N) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_fst]
Product Subgroup with Trivial Subgroup Equals Preimage under First Projection
Informal description
For any subgroup $K$ of a group $G$, the product subgroup $K \times \top$ (where $\top$ is the trivial subgroup of a group $N$) is equal to the preimage of $K$ under the first projection homomorphism $G \times N \to G$.
Subgroup.top_prod theorem
(H : Subgroup N) : (⊤ : Subgroup G).prod H = H.comap (MonoidHom.snd G N)
Full source 
@[to_additive top_prod]
theorem top_prod (H : Subgroup N) : (⊤ : Subgroup G).prod H = H.comap (MonoidHom.snd G N) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_snd]
Product of Top Subgroup with $H$ Equals Preimage under Second Projection
Informal description
For any subgroup $H$ of a group $N$, the product of the top subgroup of $G$ with $H$ is equal to the preimage of $H$ under the second projection homomorphism from $G \times N$ to $N$. That is, $(\top : \text{Subgroup } G) \times H = \text{comap}(\text{snd}_{G,N})(H)$, where $\text{snd}_{G,N} \colon G \times N \to N$ is the projection onto the second component.
Subgroup.top_prod_top theorem
: (⊤ : Subgroup G).prod (⊤ : Subgroup N) = ⊤
Full source 
@[to_additive (attr := simp) top_prod_top]
theorem top_prod_top : (⊤ : Subgroup G).prod (⊤ : Subgroup N) = ⊤ :=
  (top_prod _).trans <| comap_top _
Product of Top Subgroups is Top Subgroup
Informal description
The product of the top subgroups of groups $G$ and $N$ is equal to the top subgroup of $G \times N$, i.e., $\top \times \top = \top$.
Subgroup.bot_prod_bot theorem
: (⊥ : Subgroup G).prod (⊥ : Subgroup N) = ⊥
Full source 
@[to_additive (attr := simp) bot_prod_bot]
theorem bot_prod_bot : (⊥ : Subgroup G).prod (⊥ : Subgroup N) = ⊥ :=
  SetLike.coe_injective <| by simp [coe_prod]
Trivial Subgroup Product Identity: $\bot \times \bot = \bot$
Informal description
The product of the trivial subgroups of groups $G$ and $N$ is equal to the trivial subgroup of $G \times N$, i.e., $\bot \times \bot = \bot$.
Subgroup.le_prod_iff theorem
{H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} : J ≤ H.prod K ↔ map (MonoidHom.fst G N) J ≤ H ∧ map (MonoidHom.snd G N) J ≤ K
Full source 
@[to_additive le_prod_iff]
theorem le_prod_iff {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
    J ≤ H.prod K ↔ map (MonoidHom.fst G N) J ≤ H ∧ map (MonoidHom.snd G N) J ≤ K := by
  simpa only [← Subgroup.toSubmonoid_le] using Submonoid.le_prod_iff
Criterion for Subgroup Containment in Product: $J \leq H \times K \leftrightarrow \pi_1(J) \leq H \land \pi_2(J) \leq K$
Informal description
Let $G$ and $N$ be groups, with subgroups $H \leq G$, $K \leq N$, and $J \leq G \times N$. Then $J$ is contained in the product subgroup $H \times K$ if and only if the image of $J$ under the first projection homomorphism $\pi_1: G \times N \to G$ is contained in $H$ and the image of $J$ under the second projection homomorphism $\pi_2: G \times N \to N$ is contained in $K$. In other words: $$J \leq H \times K \leftrightarrow \pi_1(J) \leq H \land \pi_2(J) \leq K$$
Subgroup.prod_le_iff theorem
{H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} : H.prod K ≤ J ↔ map (MonoidHom.inl G N) H ≤ J ∧ map (MonoidHom.inr G N) K ≤ J
Full source 
@[to_additive prod_le_iff]
theorem prod_le_iff {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
    H.prod K ≤ J ↔ map (MonoidHom.inl G N) H ≤ J ∧ map (MonoidHom.inr G N) K ≤ J := by
  simpa only [← Subgroup.toSubmonoid_le] using Submonoid.prod_le_iff
Product Subgroup Containment Criterion via Inclusion Maps
Informal description
Let $G$ and $N$ be groups, with subgroups $H \leq G$, $K \leq N$, and $J \leq G \times N$. Then the product subgroup $H \times K$ is contained in $J$ if and only if both: 1. The image of $H$ under the left inclusion homomorphism $G \to G \times N$ (mapping $g \mapsto (g,1)$) is contained in $J$, and 2. The image of $K$ under the right inclusion homomorphism $N \to G \times N$ (mapping $n \mapsto (1,n)$) is contained in $J$.
Subgroup.prod_eq_bot_iff theorem
{H : Subgroup G} {K : Subgroup N} : H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥
Full source 
@[to_additive (attr := simp) prod_eq_bot_iff]
theorem prod_eq_bot_iff {H : Subgroup G} {K : Subgroup N} : H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥ := by
  simpa only [← Subgroup.toSubmonoid_inj] using Submonoid.prod_eq_bot_iff
Product Subgroup is Trivial if and only if Both Factors are Trivial
Informal description
For subgroups $H$ of a group $G$ and $K$ of a group $N$, the product subgroup $H \times K$ is trivial (equal to $\{\bot\}$) if and only if both $H$ and $K$ are trivial subgroups of their respective groups.
Subgroup.closure_prod theorem
{s : Set G} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) : closure (s ×ˢ t) = (closure s).prod (closure t)
Full source 
@[to_additive closure_prod]
theorem closure_prod {s : Set G} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) :
    closure (s ×ˢ t) = (closure s).prod (closure t) :=
  le_antisymm
    (closure_le _ |>.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, subset_closure⟩)
    (prod_le_iff.2 ⟨
      map_le_iff_le_comap.2 <| closure_le _ |>.2 fun _x hx => subset_closure ⟨hx, ht⟩,
      map_le_iff_le_comap.2 <| closure_le _ |>.2 fun _y hy => subset_closure ⟨hs, hy⟩⟩)
Subgroup Generation of Product Sets: $\langle s \times t \rangle = \langle s \rangle \times \langle t \rangle$ when $1 \in s$ and $1 \in t$
Informal description
Let $G$ and $N$ be groups, and let $s \subseteq G$ and $t \subseteq N$ be subsets containing the identity elements of their respective groups. Then the subgroup generated by the Cartesian product $s \times t$ is equal to the product of the subgroups generated by $s$ and $t$ in $G$ and $N$ respectively. That is: $$\langle s \times t \rangle = \langle s \rangle \times \langle t \rangle.$$
Subgroup.prodEquiv definition
(H : Subgroup G) (K : Subgroup N) : H.prod K ≃* H × K
Full source 
/-- Product of subgroups is isomorphic to their product as groups. -/
@[to_additive prodEquiv
      "Product of additive subgroups is isomorphic to their product
      as additive groups"]
def prodEquiv (H : Subgroup G) (K : Subgroup N) : H.prod K ≃* H × K :=
  { Equiv.Set.prod (H : Set G) (K : Set N) with map_mul' := fun _ _ => rfl }
Isomorphism between product subgroup and direct product of subgroups
Informal description
Given subgroups \( H \) of a group \( G \) and \( K \) of a group \( N \), the product subgroup \( H \times K \) is isomorphic as a group to the direct product \( H \times K \) via the natural bijection that maps \((h, k)\) to itself. The isomorphism preserves the group multiplication operation.
Submonoid.pi definition
[∀ i, MulOneClass (f i)] (I : Set η) (s : ∀ i, Submonoid (f i)) : Submonoid (∀ i, f i)
Full source 
/-- A version of `Set.pi` for submonoids. Given an index set `I` and a family of submodules
`s : Π i, Submonoid f i`, `pi I s` is the submonoid of dependent functions `f : Π i, f i` such that
`f i` belongs to `Pi I s` whenever `i ∈ I`. -/
@[to_additive "A version of `Set.pi` for `AddSubmonoid`s. Given an index set `I` and a family
  of submodules `s : Π i, AddSubmonoid f i`, `pi I s` is the `AddSubmonoid` of dependent functions
  `f : Π i, f i` such that `f i` belongs to `pi I s` whenever `i ∈ I`."]
def _root_.Submonoid.pi [∀ i, MulOneClass (f i)] (I : Set η) (s : ∀ i, Submonoid (f i)) :
    Submonoid (∀ i, f i) where
  carrier := I.pi fun i => (s i).carrier
  one_mem' i _ := (s i).one_mem
  mul_mem' hp hq i hI := (s i).mul_mem (hp i hI) (hq i hI)
Product of submonoids
Informal description
Given an index set $I$ and a family of submonoids $(s_i)_{i \in I}$ where each $s_i$ is a submonoid of $f_i$, the submonoid $\prod_{i \in I} s_i$ consists of all dependent functions $g : \prod_{i \in I} f_i$ such that for every $i \in I$, the value $g(i)$ belongs to $s_i$. This submonoid inherits the pointwise multiplication and identity from the product type $\prod_{i \in I} f_i$.
Subgroup.pi definition
(I : Set η) (H : ∀ i, Subgroup (f i)) : Subgroup (∀ i, f i)
Full source 
/-- A version of `Set.pi` for subgroups. Given an index set `I` and a family of submodules
`s : Π i, Subgroup f i`, `pi I s` is the subgroup of dependent functions `f : Π i, f i` such that
`f i` belongs to `pi I s` whenever `i ∈ I`. -/
@[to_additive
      "A version of `Set.pi` for `AddSubgroup`s. Given an index set `I` and a family
      of submodules `s : Π i, AddSubgroup f i`, `pi I s` is the `AddSubgroup` of dependent functions
      `f : Π i, f i` such that `f i` belongs to `pi I s` whenever `i ∈ I`."]
def pi (I : Set η) (H : ∀ i, Subgroup (f i)) : Subgroup (∀ i, f i) :=
  { Submonoid.pi I fun i => (H i).toSubmonoid with
    inv_mem' := fun hp i hI => (H i).inv_mem (hp i hI) }
Product of subgroups
Informal description
Given an index set $I$ and a family of subgroups $(H_i)_{i \in I}$ where each $H_i$ is a subgroup of $f_i$, the subgroup $\prod_{i \in I} H_i$ consists of all dependent functions $g : \prod_{i \in I} f_i$ such that for every $i \in I$, the value $g(i)$ belongs to $H_i$. This subgroup inherits the pointwise multiplication and inversion operations from the product type $\prod_{i \in I} f_i$.
Subgroup.coe_pi theorem
(I : Set η) (H : ∀ i, Subgroup (f i)) : (pi I H : Set (∀ i, f i)) = Set.pi I fun i => (H i : Set (f i))
Full source 
@[to_additive]
theorem coe_pi (I : Set η) (H : ∀ i, Subgroup (f i)) :
    (pi I H : Set (∀ i, f i)) = Set.pi I fun i => (H i : Set (f i)) :=
  rfl
Underlying Set of Product Subgroup Equals Product of Underlying Sets
Informal description
For any index set $I \subseteq \eta$ and family of subgroups $(H_i)_{i \in \eta}$ where each $H_i$ is a subgroup of $f_i$, the underlying set of the product subgroup $\prod_{i \in I} H_i$ is equal to the indexed product set $\prod_{i \in I} (H_i : \text{Set}(f_i))$. That is, the elements of the product subgroup are precisely the dependent functions $g : \prod_{i \in \eta} f_i$ such that $g(i) \in H_i$ for all $i \in I$.
Subgroup.mem_pi theorem
(I : Set η) {H : ∀ i, Subgroup (f i)} {p : ∀ i, f i} : p ∈ pi I H ↔ ∀ i : η, i ∈ I → p i ∈ H i
Full source 
@[to_additive]
theorem mem_pi (I : Set η) {H : ∀ i, Subgroup (f i)} {p : ∀ i, f i} :
    p ∈ pi I Hp ∈ pi I H ↔ ∀ i : η, i ∈ I → p i ∈ H i :=
  Iff.rfl
Membership Criterion for Product Subgroup: $p \in \prod_{i \in I} H_i \leftrightarrow \forall i \in I, p_i \in H_i$
Informal description
For any index set $I \subseteq \eta$ and a family of subgroups $(H_i)_{i \in \eta}$ where each $H_i$ is a subgroup of $f_i$, an element $p \in \prod_{i \in \eta} f_i$ belongs to the product subgroup $\prod_{i \in I} H_i$ if and only if for every $i \in I$, the component $p_i$ belongs to $H_i$.
Subgroup.pi_top theorem
(I : Set η) : (pi I fun i => (⊤ : Subgroup (f i))) = ⊤
Full source 
@[to_additive]
theorem pi_top (I : Set η) : (pi I fun i => (⊤ : Subgroup (f i))) = ⊤ :=
  ext fun x => by simp [mem_pi]
Product of Full Subgroups is Full Subgroup
Informal description
For any index set $I \subseteq \eta$, the product subgroup $\prod_{i \in I} \top$ (where each $\top$ is the full subgroup of $f_i$) equals the full subgroup $\top$ of the product group $\prod_{i \in \eta} f_i$.
Subgroup.pi_empty theorem
(H : ∀ i, Subgroup (f i)) : pi ∅ H = ⊤
Full source 
@[to_additive]
theorem pi_empty (H : ∀ i, Subgroup (f i)) : pi ∅ H = ⊤ :=
  ext fun x => by simp [mem_pi]
Product Subgroup over Empty Index Set is Trivial Subgroup
Informal description
For any family of subgroups $(H_i)_{i \in \eta}$ where each $H_i$ is a subgroup of $f_i$, the product subgroup over the empty index set is equal to the trivial subgroup $\top$ of the product group $\prod_{i \in \eta} f_i$.
Subgroup.pi_bot theorem
: (pi Set.univ fun i => (⊥ : Subgroup (f i))) = ⊥
Full source 
@[to_additive]
theorem pi_bot : (pi Set.univ fun i => (⊥ : Subgroup (f i))) = ⊥ :=
  (eq_bot_iff_forall _).mpr fun p hp => by
    simp only [mem_pi, mem_bot] at *
    ext j
    exact hp j trivial
Triviality of the Universal Product of Trivial Subgroups: $\prod_{i \in \eta} \bot = \bot$
Informal description
The product subgroup over the universal index set $\eta$, where each component is the trivial subgroup $\bot$ of $f_i$, is equal to the trivial subgroup $\bot$ of the product group $\prod_{i \in \eta} f_i$.
Subgroup.le_pi_iff theorem
{I : Set η} {H : ∀ i, Subgroup (f i)} {J : Subgroup (∀ i, f i)} : J ≤ pi I H ↔ ∀ i : η, i ∈ I → map (Pi.evalMonoidHom f i) J ≤ H i
Full source 
@[to_additive]
theorem le_pi_iff {I : Set η} {H : ∀ i, Subgroup (f i)} {J : Subgroup (∀ i, f i)} :
    J ≤ pi I H ↔ ∀ i : η, i ∈ I → map (Pi.evalMonoidHom f i) J ≤ H i := by
  constructor
  · intro h i hi
    rintro _ ⟨x, hx, rfl⟩
    exact (h hx) _ hi
  · intro h x hx i hi
    exact h i hi ⟨_, hx, rfl⟩
Subgroup Containment in Product Subgroup via Evaluation Homomorphisms
Informal description
Let $I$ be a set of indices, $(H_i)_{i \in I}$ a family of subgroups of groups $(f_i)_{i \in I}$, and $J$ a subgroup of the product group $\prod_{i \in I} f_i$. Then $J$ is contained in the product subgroup $\prod_{i \in I} H_i$ if and only if for every index $i \in I$, the image of $J$ under the evaluation homomorphism at $i$ is contained in $H_i$.
Subgroup.mulSingle_mem_pi theorem
[DecidableEq η] {I : Set η} {H : ∀ i, Subgroup (f i)} (i : η) (x : f i) : Pi.mulSingle i x ∈ pi I H ↔ i ∈ I → x ∈ H i
Full source 
@[to_additive (attr := simp)]
theorem mulSingle_mem_pi [DecidableEq η] {I : Set η} {H : ∀ i, Subgroup (f i)} (i : η) (x : f i) :
    Pi.mulSinglePi.mulSingle i x ∈ pi I HPi.mulSingle i x ∈ pi I H ↔ i ∈ I → x ∈ H i := by
  constructor
  · intro h hi
    simpa using h i hi
  · intro h j hj
    by_cases heq : j = i
    · subst heq
      simpa using h hj
    · simp [heq, one_mem]
Membership of Multiplicative Single Function in Product Subgroup: $\text{mulSingle } i \, x \in \prod_{i \in I} H_i \leftrightarrow (i \in I \to x \in H_i)$
Informal description
Let $I$ be a set of indices and $(H_i)_{i \in I}$ be a family of subgroups of groups $(f_i)_{i \in I}$. For any index $i$ and element $x \in f_i$, the multiplicative single function $\text{mulSingle } i \, x$ belongs to the product subgroup $\prod_{i \in I} H_i$ if and only if whenever $i \in I$, the element $x$ belongs to $H_i$.
Subgroup.pi_eq_bot_iff theorem
(H : ∀ i, Subgroup (f i)) : pi Set.univ H = ⊥ ↔ ∀ i, H i = ⊥
Full source 
@[to_additive]
theorem pi_eq_bot_iff (H : ∀ i, Subgroup (f i)) : pipi Set.univ H = ⊥ ↔ ∀ i, H i = ⊥ := by
  classical
    simp only [eq_bot_iff_forall]
    constructor
    · intro h i x hx
      have : MonoidHom.mulSingle f i x = 1 :=
        h (MonoidHom.mulSingle f i x) ((mulSingle_mem_pi i x).mpr fun _ => hx)
      simpa using congr_fun this i
    · exact fun h x hx => funext fun i => h _ _ (hx i trivial)
Product Subgroup Triviality Criterion: $\prod_{i \in I} H_i = 1 \leftrightarrow \forall i, H_i = 1$
Informal description
For a family of subgroups $(H_i)_{i \in I}$ of groups $(f_i)_{i \in I}$, the product subgroup $\prod_{i \in I} H_i$ is equal to the trivial subgroup $\{1\}$ if and only if every subgroup $H_i$ is equal to the trivial subgroup $\{1\}$.
Subgroup.Characteristic structure
Full source 
/-- A subgroup is characteristic if it is fixed by all automorphisms.
  Several equivalent conditions are provided by lemmas of the form `Characteristic.iff...` -/
structure Characteristic : Prop where
  /-- `H` is fixed by all automorphisms -/
  fixed : ∀ ϕ : G ≃* G, H.comap ϕ.toMonoidHom = H
Characteristic subgroup
Informal description
A subgroup $H$ of a group $G$ is called characteristic if it is invariant under all automorphisms of $G$. That is, for every automorphism $\phi \colon G \to G$, the image $\phi(H)$ is contained in $H$.
AddSubgroup.Characteristic structure
Full source 
/-- An `AddSubgroup` is characteristic if it is fixed by all automorphisms.
  Several equivalent conditions are provided by lemmas of the form `Characteristic.iff...` -/
structure Characteristic : Prop where
  /-- `H` is fixed by all automorphisms -/
  fixed : ∀ ϕ : A ≃+ A, H.comap ϕ.toAddMonoidHom = H
Characteristic additive subgroup
Informal description
An additive subgroup $H$ of an additive group $G$ is called *characteristic* if it is fixed by all automorphisms of $G$, i.e., for every automorphism $\phi \colon G \to G$, we have $\phi(H) = H$.
AddSubgroup.normal_of_characteristic instance
[h : H.Characteristic] : H.Normal
Full source 
instance (priority := 100) normal_of_characteristic [h : H.Characteristic] : H.Normal :=
  ⟨fun a ha b => (SetLike.ext_iff.mp (h.fixed (AddAut.conj b)) a).mpr ha⟩
Characteristic Additive Subgroups are Normal
Informal description
For any additive subgroup $H$ of an additive group $G$, if $H$ is characteristic (i.e., fixed by all automorphisms of $G$), then $H$ is normal (i.e., closed under conjugation by any element of $G$).
Subgroup.characteristic_iff_comap_eq theorem
: H.Characteristic ↔ ∀ ϕ : G ≃* G, H.comap ϕ.toMonoidHom = H
Full source 
@[to_additive]
theorem characteristic_iff_comap_eq : H.Characteristic ↔ ∀ ϕ : G ≃* G, H.comap ϕ.toMonoidHom = H :=
  ⟨Characteristic.fixed, Characteristic.mk⟩
Characteristic Subgroup Criterion via Preimage Equality
Informal description
A subgroup $H$ of a group $G$ is characteristic if and only if for every group automorphism $\phi \colon G \to G$, the preimage of $H$ under $\phi$ is equal to $H$ itself, i.e., $\phi^{-1}(H) = H$.
Subgroup.characteristic_iff_comap_le theorem
: H.Characteristic ↔ ∀ ϕ : G ≃* G, H.comap ϕ.toMonoidHom ≤ H
Full source 
@[to_additive]
theorem characteristic_iff_comap_le : H.Characteristic ↔ ∀ ϕ : G ≃* G, H.comap ϕ.toMonoidHom ≤ H :=
  characteristic_iff_comap_eq.trans
    ⟨fun h ϕ => le_of_eq (h ϕ), fun h ϕ =>
      le_antisymm (h ϕ) fun g hg => h ϕ.symm ((congr_arg (· ∈ H) (ϕ.symm_apply_apply g)).mpr hg)⟩
Characteristic Subgroup Criterion via Preimage Inclusion
Informal description
A subgroup $H$ of a group $G$ is characteristic if and only if for every group automorphism $\phi \colon G \to G$, the preimage of $H$ under $\phi$ is contained in $H$, i.e., $\phi^{-1}(H) \leq H$.
Subgroup.characteristic_iff_le_comap theorem
: H.Characteristic ↔ ∀ ϕ : G ≃* G, H ≤ H.comap ϕ.toMonoidHom
Full source 
@[to_additive]
theorem characteristic_iff_le_comap : H.Characteristic ↔ ∀ ϕ : G ≃* G, H ≤ H.comap ϕ.toMonoidHom :=
  characteristic_iff_comap_eq.trans
    ⟨fun h ϕ => ge_of_eq (h ϕ), fun h ϕ =>
      le_antisymm (fun g hg => (congr_arg (· ∈ H) (ϕ.symm_apply_apply g)).mp (h ϕ.symm hg)) (h ϕ)⟩
Characteristic Subgroup Criterion via Subgroup Containment in Preimage
Informal description
A subgroup $H$ of a group $G$ is characteristic if and only if for every group automorphism $\phi \colon G \to G$, the subgroup $H$ is contained in the preimage of $H$ under $\phi$, i.e., $H \leq \phi^{-1}(H)$.
Subgroup.characteristic_iff_map_eq theorem
: H.Characteristic ↔ ∀ ϕ : G ≃* G, H.map ϕ.toMonoidHom = H
Full source 
@[to_additive]
theorem characteristic_iff_map_eq : H.Characteristic ↔ ∀ ϕ : G ≃* G, H.map ϕ.toMonoidHom = H := by
  simp_rw [map_equiv_eq_comap_symm']
  exact characteristic_iff_comap_eq.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩
Characteristic Subgroup Criterion via Image Equality
Informal description
A subgroup $H$ of a group $G$ is characteristic if and only if for every group automorphism $\phi \colon G \to G$, the image of $H$ under $\phi$ is equal to $H$ itself, i.e., $\phi(H) = H$.
Subgroup.characteristic_iff_map_le theorem
: H.Characteristic ↔ ∀ ϕ : G ≃* G, H.map ϕ.toMonoidHom ≤ H
Full source 
@[to_additive]
theorem characteristic_iff_map_le : H.Characteristic ↔ ∀ ϕ : G ≃* G, H.map ϕ.toMonoidHom ≤ H := by
  simp_rw [map_equiv_eq_comap_symm']
  exact characteristic_iff_comap_le.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩
Characteristic Subgroup Criterion via Image Containment
Informal description
A subgroup $H$ of a group $G$ is characteristic if and only if for every group automorphism $\phi \colon G \to G$, the image of $H$ under $\phi$ is contained in $H$, i.e., $\phi(H) \leq H$.
Subgroup.characteristic_iff_le_map theorem
: H.Characteristic ↔ ∀ ϕ : G ≃* G, H ≤ H.map ϕ.toMonoidHom
Full source 
@[to_additive]
theorem characteristic_iff_le_map : H.Characteristic ↔ ∀ ϕ : G ≃* G, H ≤ H.map ϕ.toMonoidHom := by
  simp_rw [map_equiv_eq_comap_symm']
  exact characteristic_iff_le_comap.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩
Characteristic Subgroup Criterion via Subgroup Containment in Image
Informal description
A subgroup $H$ of a group $G$ is characteristic if and only if for every group automorphism $\phi \colon G \to G$, $H$ is contained in the image of $H$ under $\phi$, i.e., $H \leq \phi(H)$.
Subgroup.normalizer_eq_top_iff theorem
: H.normalizer = ⊤ ↔ H.Normal
Full source 
@[to_additive]
theorem normalizer_eq_top_iff : H.normalizer = ⊤ ↔ H.Normal :=
  eq_top_iff.trans
    ⟨fun h => ⟨fun a ha b => (h (mem_top b) a).mp ha⟩, fun h a _ha b =>
      ⟨fun hb => h.conj_mem b hb a, fun hb => by rwa [h.mem_comm_iff, inv_mul_cancel_left] at hb⟩⟩
Normalizer Equals Top if and only if Subgroup is Normal
Informal description
For a subgroup $H$ of a group $G$, the normalizer of $H$ equals the entire group $G$ if and only if $H$ is a normal subgroup of $G$.
Subgroup.normalizer_eq_top theorem
[h : H.Normal] : H.normalizer = ⊤
Full source 
@[to_additive]
theorem normalizer_eq_top [h : H.Normal] : H.normalizer = ⊤ :=
  normalizer_eq_top_iff.mpr h
Normalizer of Normal Subgroup is Entire Group
Informal description
If $H$ is a normal subgroup of a group $G$, then the normalizer of $H$ in $G$ is equal to the entire group $G$.
Subgroup.le_normalizer_comap theorem
(f : N →* G) : H.normalizer.comap f ≤ (H.comap f).normalizer
Full source 
/-- The preimage of the normalizer is contained in the normalizer of the preimage. -/
@[to_additive "The preimage of the normalizer is contained in the normalizer of the preimage."]
theorem le_normalizer_comap (f : N →* G) :
    H.normalizer.comap f ≤ (H.comap f).normalizer := fun x => by
  simp only [mem_normalizer_iff, mem_comap]
  intro h n
  simp [h (f n)]
Preimage of Normalizer is Contained in Normalizer of Preimage
Informal description
Let $G$ and $N$ be groups, $H$ a subgroup of $G$, and $f \colon N \to G$ a group homomorphism. Then the preimage of the normalizer of $H$ under $f$ is contained in the normalizer of the preimage of $H$ under $f$. In other words, $f^{-1}(N_G(H)) \leq N_N(f^{-1}(H))$, where $N_G(H)$ denotes the normalizer of $H$ in $G$ and $N_N(f^{-1}(H))$ denotes the normalizer of $f^{-1}(H)$ in $N$.
Subgroup.le_normalizer_map theorem
(f : G →* N) : H.normalizer.map f ≤ (H.map f).normalizer
Full source 
/-- The image of the normalizer is contained in the normalizer of the image. -/
@[to_additive "The image of the normalizer is contained in the normalizer of the image."]
theorem le_normalizer_map (f : G →* N) : H.normalizer.map f ≤ (H.map f).normalizer := fun _ => by
  simp only [and_imp, exists_prop, mem_map, exists_imp, mem_normalizer_iff]
  rintro x hx rfl n
  constructor
  · rintro ⟨y, hy, rfl⟩
    use x * y * x⁻¹, (hx y).1 hy
    simp
  · rintro ⟨y, hyH, hy⟩
    use x⁻¹ * y * x
    rw [hx]
    simp [hy, hyH, mul_assoc]
Image of Normalizer is Contained in Normalizer of Image
Informal description
Let $G$ and $N$ be groups, $H$ a subgroup of $G$, and $f \colon G \to N$ a group homomorphism. Then the image of the normalizer of $H$ under $f$ is contained in the normalizer of the image of $H$ under $f$, i.e., $f(H.\text{normalizer}) \leq (f(H)).\text{normalizer}$.
Subgroup.comap_normalizer_eq_of_le_range theorem
{f : N →* G} (h : H ≤ f.range) : comap f H.normalizer = (comap f H).normalizer
Full source 
@[to_additive]
theorem comap_normalizer_eq_of_le_range {f : N →* G} (h : H ≤ f.range) :
    comap f H.normalizer = (comap f H).normalizer := by
  apply le_antisymm (le_normalizer_comap f)
  rw [← map_le_iff_le_comap]
  apply (le_normalizer_map f).trans
  rw [map_comap_eq_self h]
Preimage of Normalizer Equals Normalizer of Preimage When Subgroup is in Range
Informal description
Let $G$ and $N$ be groups, $H$ a subgroup of $G$, and $f \colon N \to G$ a group homomorphism such that $H$ is contained in the range of $f$. Then the preimage of the normalizer of $H$ under $f$ equals the normalizer of the preimage of $H$ under $f$. In symbols: \[ f^{-1}(N_G(H)) = N_N(f^{-1}(H)). \]
Subgroup.subgroupOf_normalizer_eq theorem
{H N : Subgroup G} (h : H ≤ N) : H.normalizer.subgroupOf N = (H.subgroupOf N).normalizer
Full source 
@[to_additive]
theorem subgroupOf_normalizer_eq {H N : Subgroup G} (h : H ≤ N) :
    H.normalizer.subgroupOf N = (H.subgroupOf N).normalizer :=
  comap_normalizer_eq_of_le_range (h.trans_eq N.range_subtype.symm)
Normalizer Intersection Property for Subgroups
Informal description
Let $G$ be a group and $H, N$ be subgroups of $G$ such that $H \leq N$. Then the normalizer of $H$ intersected with $N$ equals the normalizer of $H \cap N$ in $N$. In other words: \[ N_G(H) \cap N = N_N(H \cap N). \]
Subgroup.normal_subgroupOf_iff_le_normalizer theorem
(h : H ≤ K) : (H.subgroupOf K).Normal ↔ K ≤ H.normalizer
Full source 
@[to_additive]
theorem normal_subgroupOf_iff_le_normalizer (h : H ≤ K) :
    (H.subgroupOf K).Normal ↔ K ≤ H.normalizer := by
  rw [← subgroupOf_eq_top, subgroupOf_normalizer_eq h, normalizer_eq_top_iff]
Normality of Subgroup Intersection Equals Normalizer Containment
Informal description
Let $G$ be a group with subgroups $H$ and $K$ such that $H \leq K$. Then the intersection $H \cap K$ is a normal subgroup of $K$ if and only if $K$ is contained in the normalizer of $H$ in $G$.
Subgroup.normal_subgroupOf_iff_le_normalizer_inf theorem
: (H.subgroupOf K).Normal ↔ K ≤ (H ⊓ K).normalizer
Full source 
@[to_additive]
theorem normal_subgroupOf_iff_le_normalizer_inf :
    (H.subgroupOf K).Normal ↔ K ≤ (H ⊓ K).normalizer :=
  inf_subgroupOf_right H K ▸ normal_subgroupOf_iff_le_normalizer inf_le_right
Normality of Subgroup Intersection Equivalence: $(H \cap K) \triangleleft K \leftrightarrow K \leq N_G(H \cap K)$
Informal description
For any subgroups $H$ and $K$ of a group $G$, the intersection $H \cap K$ is a normal subgroup of $K$ if and only if $K$ is contained in the normalizer of $H \cap K$ in $G$. In other words: $$ (H \cap K) \triangleleft K \leftrightarrow K \leq N_G(H \cap K) $$
Subgroup.le_normalizer_of_normal_subgroupOf theorem
[hK : (H.subgroupOf K).Normal] (HK : H ≤ K) : K ≤ H.normalizer
Full source 
@[to_additive]
theorem le_normalizer_of_normal_subgroupOf [hK : (H.subgroupOf K).Normal] (HK : H ≤ K) :
    K ≤ H.normalizer :=
  (normal_subgroupOf_iff_le_normalizer HK).mp hK
Normal Subgroup Intersection Implies Normalizer Containment
Informal description
Let $G$ be a group with subgroups $H$ and $K$ such that $H \leq K$. If the intersection $H \cap K$ is a normal subgroup of $K$, then $K$ is contained in the normalizer of $H$ in $G$.
Subgroup.subset_normalizer_of_normal theorem
{S : Set G} [hH : H.Normal] : S ⊆ H.normalizer
Full source 
@[to_additive]
theorem subset_normalizer_of_normal {S : Set G} [hH : H.Normal] : S ⊆ H.normalizer :=
  (@normalizer_eq_top _ _ H hH) ▸ le_top
Subset Contained in Normalizer of Normal Subgroup
Informal description
For any subset $S$ of a group $G$ and any normal subgroup $H$ of $G$, the subset $S$ is contained in the normalizer of $H$.
Subgroup.inf_normalizer_le_normalizer_inf theorem
: H.normalizer ⊓ K.normalizer ≤ (H ⊓ K).normalizer
Full source 
@[to_additive]
theorem inf_normalizer_le_normalizer_inf : H.normalizer ⊓ K.normalizer ≤ (H ⊓ K).normalizer :=
  fun _ h g ↦ and_congr (h.1 g) (h.2 g)
Intersection of Normalizers is Contained in Normalizer of Intersection
Informal description
For any two subgroups $H$ and $K$ of a group $G$, the intersection of their normalizers is contained in the normalizer of their intersection, i.e., $H.\text{normalizer} \cap K.\text{normalizer} \leq (H \cap K).\text{normalizer}$.
NormalizerCondition definition
Full source 
/-- Every proper subgroup `H` of `G` is a proper normal subgroup of the normalizer of `H` in `G`. -/
def _root_.NormalizerCondition :=
  ∀ H : Subgroup G, H < ⊤ → H < normalizer H
Normalizer condition for groups
Informal description
A group $G$ satisfies the *normalizer condition* if every proper subgroup $H$ of $G$ is strictly contained in its normalizer, i.e., $H < \text{normalizer}(H)$.
normalizerCondition_iff_only_full_group_self_normalizing theorem
: NormalizerCondition G ↔ ∀ H : Subgroup G, H.normalizer = H → H = ⊤
Full source 
/-- Alternative phrasing of the normalizer condition: Only the full group is self-normalizing.
This may be easier to work with, as it avoids inequalities and negations. -/
theorem _root_.normalizerCondition_iff_only_full_group_self_normalizing :
    NormalizerConditionNormalizerCondition G ↔ ∀ H : Subgroup G, H.normalizer = H → H = ⊤ := by
  apply forall_congr'; intro H
  simp only [lt_iff_le_and_ne, le_normalizer, le_top, Ne]
  tauto
Normalizer Condition Characterization: Only Full Group is Self-Normalizing
Informal description
A group $G$ satisfies the normalizer condition if and only if the only subgroup $H$ of $G$ that is equal to its own normalizer is the full group $G$ itself. In other words, $G$ satisfies the normalizer condition precisely when for every subgroup $H \leq G$, if $H.\text{normalizer} = H$, then $H = G$.
Group.conjugatesOfSet definition
(s : Set G) : Set G
Full source 
/-- Given a set `s`, `conjugatesOfSet s` is the set of all conjugates of
the elements of `s`. -/
def conjugatesOfSet (s : Set G) : Set G :=
  ⋃ a ∈ s, conjugatesOf a
Set of conjugates of a subset of a group
Informal description
Given a subset \( s \) of a group \( G \), the set \( \text{conjugatesOfSet}(s) \) is the union of all conjugates of elements in \( s \), i.e., it consists of all elements \( x \in G \) such that there exists \( a \in s \) and \( x \) is conjugate to \( a \).
Group.mem_conjugatesOfSet_iff theorem
{x : G} : x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x
Full source 
theorem mem_conjugatesOfSet_iff {x : G} : x ∈ conjugatesOfSet sx ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x := by
  rw [conjugatesOfSet, Set.mem_iUnion₂]
  simp only [conjugatesOf, isConj_iff, Set.mem_setOf_eq, exists_prop]
Characterization of Membership in Conjugates of a Subset
Informal description
For any element $x$ in a group $G$, $x$ belongs to the set of conjugates of a subset $s \subseteq G$ if and only if there exists an element $a \in s$ such that $x$ is conjugate to $a$.
Group.conjugatesOfSet_mono theorem
{s t : Set G} (h : s ⊆ t) : conjugatesOfSet s ⊆ conjugatesOfSet t
Full source 
theorem conjugatesOfSet_mono {s t : Set G} (h : s ⊆ t) : conjugatesOfSetconjugatesOfSet s ⊆ conjugatesOfSet t :=
  Set.biUnion_subset_biUnion_left h
Monotonicity of Conjugate Set with Respect to Subset Inclusion
Informal description
For any subsets $s$ and $t$ of a group $G$, if $s \subseteq t$, then the set of conjugates of elements in $s$ is contained in the set of conjugates of elements in $t$, i.e., $\text{conjugatesOfSet}(s) \subseteq \text{conjugatesOfSet}(t)$.
Group.conjugates_subset_normal theorem
{N : Subgroup G} [tn : N.Normal] {a : G} (h : a ∈ N) : conjugatesOf a ⊆ N
Full source 
theorem conjugates_subset_normal {N : Subgroup G} [tn : N.Normal] {a : G} (h : a ∈ N) :
    conjugatesOfconjugatesOf a ⊆ N := by
  rintro a hc
  obtain ⟨c, rfl⟩ := isConj_iff.1 hc
  exact tn.conj_mem a h c
Conjugates of Normal Subgroup Elements Remain in Subgroup
Informal description
Let $G$ be a group and $N$ a normal subgroup of $G$. For any element $a \in N$, the set of all conjugates of $a$ is contained in $N$, i.e., $\text{conjugatesOf}(a) \subseteq N$.
Group.conjugatesOfSet_subset theorem
{s : Set G} {N : Subgroup G} [N.Normal] (h : s ⊆ N) : conjugatesOfSet s ⊆ N
Full source 
theorem conjugatesOfSet_subset {s : Set G} {N : Subgroup G} [N.Normal] (h : s ⊆ N) :
    conjugatesOfSetconjugatesOfSet s ⊆ N :=
  Set.iUnion₂_subset fun _x H => conjugates_subset_normal (h H)
Conjugates of Subset in Normal Subgroup Remain in Subgroup
Informal description
Let $G$ be a group and $N$ a normal subgroup of $G$. For any subset $s \subseteq N$, the set of all conjugates of elements in $s$ is contained in $N$, i.e., $\text{conjugatesOfSet}(s) \subseteq N$.
Group.conj_mem_conjugatesOfSet theorem
{x c : G} : x ∈ conjugatesOfSet s → c * x * c⁻¹ ∈ conjugatesOfSet s
Full source 
/-- The set of conjugates of `s` is closed under conjugation. -/
theorem conj_mem_conjugatesOfSet {x c : G} :
    x ∈ conjugatesOfSet s → c * x * c⁻¹ ∈ conjugatesOfSet s := fun H => by
  rcases mem_conjugatesOfSet_iff.1 H with ⟨a, h₁, h₂⟩
  exact mem_conjugatesOfSet_iff.2 ⟨a, h₁, h₂.trans (isConj_iff.2 ⟨c, rfl⟩)⟩
Conjugation Preserves Membership in Conjugates of a Subset
Informal description
For any elements $x, c$ in a group $G$, if $x$ belongs to the set of conjugates of a subset $s \subseteq G$, then the conjugate $c x c^{-1}$ also belongs to the set of conjugates of $s$.
Subgroup.normalClosure definition
(s : Set G) : Subgroup G
Full source 
/-- The normal closure of a set `s` is the subgroup closure of all the conjugates of
elements of `s`. It is the smallest normal subgroup containing `s`. -/
def normalClosure (s : Set G) : Subgroup G :=
  closure (conjugatesOfSet s)
Normal closure of a subset in a group
Informal description
The normal closure of a subset \( s \) of a group \( G \) is the smallest normal subgroup of \( G \) containing \( s \). It is defined as the subgroup generated by all conjugates of elements of \( s \).
Subgroup.le_normalClosure theorem
{H : Subgroup G} : H ≤ normalClosure ↑H
Full source 
theorem le_normalClosure {H : Subgroup G} : H ≤ normalClosure ↑H := fun _ h =>
  subset_normalClosure h
Subgroup is Contained in its Normal Closure
Informal description
For any subgroup $H$ of a group $G$, $H$ is contained in its normal closure, i.e., $H \leq \text{normalClosure}(H)$.
Subgroup.normalClosure_normal instance
: (normalClosure s).Normal
Full source 
/-- The normal closure of `s` is a normal subgroup. -/
instance normalClosure_normal : (normalClosure s).Normal :=
  ⟨fun n h g => by
    refine Subgroup.closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_)
      (fun x _ ihx => ?_) h
    · exact conjugatesOfSet_subset_normalClosure (conj_mem_conjugatesOfSet hx)
    · simpa using (normalClosure s).one_mem
    · rw [← conj_mul]
      exact mul_mem ihx ihy
    · rw [← conj_inv]
      exact inv_mem ihx⟩
Normal Closure is a Normal Subgroup
Informal description
For any subset $s$ of a group $G$, the normal closure of $s$ is a normal subgroup of $G$.
Subgroup.normalClosure_le_normal theorem
{N : Subgroup G} [N.Normal] (h : s ⊆ N) : normalClosure s ≤ N
Full source 
/-- The normal closure of `s` is the smallest normal subgroup containing `s`. -/
theorem normalClosure_le_normal {N : Subgroup G} [N.Normal] (h : s ⊆ N) : normalClosure s ≤ N := by
  intro a w
  refine closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_) (fun x _ ihx => ?_) w
  · exact conjugatesOfSet_subset h hx
  · exact one_mem _
  · exact mul_mem ihx ihy
  · exact inv_mem ihx
Normal Closure of Subset in Normal Subgroup is Contained
Informal description
Let $G$ be a group and $N$ a normal subgroup of $G$. For any subset $s \subseteq N$, the normal closure of $s$ is contained in $N$, i.e., $\text{normalClosure}(s) \leq N$.
Subgroup.normalClosure_subset_iff theorem
{N : Subgroup G} [N.Normal] : s ⊆ N ↔ normalClosure s ≤ N
Full source 
theorem normalClosure_subset_iff {N : Subgroup G} [N.Normal] : s ⊆ Ns ⊆ N ↔ normalClosure s ≤ N :=
  ⟨normalClosure_le_normal, Set.Subset.trans subset_normalClosure⟩
Characterization of Subset Containment in Normal Subgroup via Normal Closure
Informal description
For any subset $s$ of a group $G$ and any normal subgroup $N$ of $G$, the subset $s$ is contained in $N$ if and only if the normal closure of $s$ is contained in $N$.
Subgroup.normalClosure_mono theorem
{s t : Set G} (h : s ⊆ t) : normalClosure s ≤ normalClosure t
Full source 
@[gcongr]
theorem normalClosure_mono {s t : Set G} (h : s ⊆ t) : normalClosure s ≤ normalClosure t :=
  normalClosure_le_normal (Set.Subset.trans h subset_normalClosure)
Monotonicity of Normal Closure with Respect to Subset Inclusion
Informal description
For any subsets $s$ and $t$ of a group $G$, if $s$ is a subset of $t$, then the normal closure of $s$ is contained in the normal closure of $t$, i.e., $\text{normalClosure}(s) \leq \text{normalClosure}(t)$.
Subgroup.normalClosure_eq_iInf theorem
: normalClosure s = ⨅ (N : Subgroup G) (_ : Normal N) (_ : s ⊆ N), N
Full source 
theorem normalClosure_eq_iInf :
    normalClosure s = ⨅ (N : Subgroup G) (_ : Normal N) (_ : s ⊆ N), N :=
  le_antisymm (le_iInf fun _ => le_iInf fun _ => le_iInf normalClosure_le_normal)
    (iInf_le_of_le (normalClosure s)
      (iInf_le_of_le (by infer_instance) (iInf_le_of_le subset_normalClosure le_rfl)))
Normal Closure as Infimum of Normal Subgroups Containing $s$
Informal description
For any subset $s$ of a group $G$, the normal closure of $s$ is equal to the infimum of all normal subgroups $N$ of $G$ that contain $s$. In other words, \[ \text{normalClosure}(s) = \bigsqcap_{\substack{N \leq G \\ N \text{ normal} \\ s \subseteq N}} N. \]
Subgroup.normalClosure_idempotent theorem
: normalClosure ↑(normalClosure s) = normalClosure s
Full source 
theorem normalClosure_idempotent : normalClosure ↑(normalClosure s) = normalClosure s :=
  normalClosure_eq_self _
Idempotence of Normal Closure in Groups
Informal description
For any subset $s$ of a group $G$, the normal closure of the normal closure of $s$ is equal to the normal closure of $s$, i.e., \[ \text{normalClosure}(\text{normalClosure}(s)) = \text{normalClosure}(s). \]
Subgroup.closure_le_normalClosure theorem
{s : Set G} : closure s ≤ normalClosure s
Full source 
theorem closure_le_normalClosure {s : Set G} : closure s ≤ normalClosure s := by
  simp only [subset_normalClosure, closure_le]
Subgroup Generated by a Set is Contained in its Normal Closure
Informal description
For any subset $s$ of a group $G$, the subgroup generated by $s$ is contained in the normal closure of $s$.
Subgroup.normalClosure_closure_eq_normalClosure theorem
{s : Set G} : normalClosure ↑(closure s) = normalClosure s
Full source 
@[simp]
theorem normalClosure_closure_eq_normalClosure {s : Set G} :
    normalClosure ↑(closure s) = normalClosure s :=
  le_antisymm (normalClosure_le_normal closure_le_normalClosure) (normalClosure_mono subset_closure)
Normal Closure of Generated Subgroup Equals Normal Closure of Set
Informal description
For any subset $s$ of a group $G$, the normal closure of the subgroup generated by $s$ is equal to the normal closure of $s$ itself, i.e., \[ \text{normalClosure}(\langle s \rangle) = \text{normalClosure}(s). \]
Subgroup.normalCore definition
(H : Subgroup G) : Subgroup G
Full source 
/-- The normal core of a subgroup `H` is the largest normal subgroup of `G` contained in `H`,
as shown by `Subgroup.normalCore_eq_iSup`. -/
def normalCore (H : Subgroup G) : Subgroup G where
  carrier := { a : G | ∀ b : G, b * a * b⁻¹ ∈ H }
  one_mem' a := by rw [mul_one, mul_inv_cancel]; exact H.one_mem
  inv_mem' {_} h b := (congr_arg (· ∈ H) conj_inv).mp (H.inv_mem (h b))
  mul_mem' {_ _} ha hb c := (congr_arg (· ∈ H) conj_mul).mp (H.mul_mem (ha c) (hb c))
Normal core of a subgroup
Informal description
The normal core of a subgroup $H$ of a group $G$ is the subgroup consisting of all elements $a \in G$ such that for every $b \in G$, the conjugate $b * a * b^{-1}$ belongs to $H$. It is the largest normal subgroup of $G$ contained in $H$.
Subgroup.normalCore_le theorem
(H : Subgroup G) : H.normalCore ≤ H
Full source 
theorem normalCore_le (H : Subgroup G) : H.normalCore ≤ H := fun a h => by
  rw [← mul_one a, ← inv_one, ← one_mul a]
  exact h 1
Normal Core is Contained in Subgroup
Informal description
For any subgroup $H$ of a group $G$, the normal core of $H$ is contained in $H$, i.e., $H.\text{normalCore} \leq H$.
Subgroup.normal_le_normalCore theorem
{H : Subgroup G} {N : Subgroup G} [hN : N.Normal] : N ≤ H.normalCore ↔ N ≤ H
Full source 
theorem normal_le_normalCore {H : Subgroup G} {N : Subgroup G} [hN : N.Normal] :
    N ≤ H.normalCore ↔ N ≤ H :=
  ⟨ge_trans H.normalCore_le, fun h_le n hn g => h_le (hN.conj_mem n hn g)⟩
Normal Subgroup Containment in Normal Core
Informal description
For any subgroup $H$ of a group $G$ and any normal subgroup $N$ of $G$, $N$ is contained in the normal core of $H$ if and only if $N$ is contained in $H$.
Subgroup.normalCore_mono theorem
{H K : Subgroup G} (h : H ≤ K) : H.normalCore ≤ K.normalCore
Full source 
theorem normalCore_mono {H K : Subgroup G} (h : H ≤ K) : H.normalCore ≤ K.normalCore :=
  normal_le_normalCore.mpr (H.normalCore_le.trans h)
Monotonicity of Normal Core with Respect to Subgroup Inclusion
Informal description
For any subgroups $H$ and $K$ of a group $G$, if $H$ is contained in $K$ (i.e., $H \leq K$), then the normal core of $H$ is contained in the normal core of $K$ (i.e., $H.\text{normalCore} \leq K.\text{normalCore}$).
Subgroup.normalCore_eq_iSup theorem
(H : Subgroup G) : H.normalCore = ⨆ (N : Subgroup G) (_ : Normal N) (_ : N ≤ H), N
Full source 
theorem normalCore_eq_iSup (H : Subgroup G) :
    H.normalCore = ⨆ (N : Subgroup G) (_ : Normal N) (_ : N ≤ H), N :=
  le_antisymm
    (le_iSup_of_le H.normalCore
      (le_iSup_of_le H.normalCore_normal (le_iSup_of_le H.normalCore_le le_rfl)))
    (iSup_le fun _ => iSup_le fun _ => iSup_le normal_le_normalCore.mpr)
Normal Core as Supremum of Contained Normal Subgroups
Informal description
For any subgroup $H$ of a group $G$, the normal core of $H$ is equal to the supremum of all normal subgroups $N$ of $G$ that are contained in $H$, i.e., $$ H.\text{normalCore} = \bigsqcup_{\substack{N \leq G \\ N \text{ normal} \\ N \leq H}} N. $$
Subgroup.normalCore_idempotent theorem
(H : Subgroup G) : H.normalCore.normalCore = H.normalCore
Full source 
theorem normalCore_idempotent (H : Subgroup G) : H.normalCore.normalCore = H.normalCore :=
  H.normalCore.normalCore_eq_self
Idempotence of Normal Core Operation
Informal description
For any subgroup $H$ of a group $G$, the normal core of the normal core of $H$ is equal to the normal core of $H$, i.e., $$ (H.\text{normalCore}).\text{normalCore} = H.\text{normalCore}. $$
MonoidHom.prodMap_comap_prod theorem
{G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') (S : Subgroup N) (S' : Subgroup N') : (S.prod S').comap (prodMap f g) = (S.comap f).prod (S'.comap g)
Full source 
@[to_additive prodMap_comap_prod]
theorem prodMap_comap_prod {G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →* N)
    (g : G' →* N') (S : Subgroup N) (S' : Subgroup N') :
    (S.prod S').comap (prodMap f g) = (S.comap f).prod (S'.comap g) :=
  SetLike.coe_injective <| Set.preimage_prod_map_prod f g _ _
Preimage of Product Subgroup under Product Homomorphism
Informal description
Let $G, G', N, N'$ be groups, and let $f \colon G \to N$ and $g \colon G' \to N'$ be group homomorphisms. For any subgroups $S \leq N$ and $S' \leq N'$, the preimage of the product subgroup $S \times S'$ under the product homomorphism $f \times g$ is equal to the product of the preimages of $S$ under $f$ and $S'$ under $g$. In other words, $$(f \times g)^{-1}(S \times S') = f^{-1}(S) \times g^{-1}(S').$$
MonoidHom.ker_prodMap theorem
{G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') : (prodMap f g).ker = f.ker.prod g.ker
Full source 
@[to_additive ker_prodMap]
theorem ker_prodMap {G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') :
    (prodMap f g).ker = f.ker.prod g.ker := by
  rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]
Kernel of Product Homomorphism is Product of Kernels
Informal description
Let $G, G', N, N'$ be groups, and let $f \colon G \to N$ and $g \colon G' \to N'$ be group homomorphisms. The kernel of the product homomorphism $f \times g \colon G \times G' \to N \times N'$ is equal to the product of the kernels of $f$ and $g$, i.e., $$\ker(f \times g) = \ker f \times \ker g.$$
MonoidHom.ker_fst theorem
: ker (fst G G') = .prod ⊥ ⊤
Full source 
@[to_additive (attr := simp)]
lemma ker_fst : ker (fst G G') = .prod ⊥ ⊤ := SetLike.ext fun _ => (iff_of_eq (and_true _)).symm
Kernel of First Projection Homomorphism is Trivial Subgroup Cross Full Group
Informal description
The kernel of the first projection homomorphism $\mathrm{fst} : G \times G' \to G$ is equal to the product subgroup $\{1\} \times G'$, where $\{1\}$ is the trivial subgroup of $G$ and $G'$ is considered as a subgroup of itself.
MonoidHom.ker_snd theorem
: ker (snd G G') = .prod ⊤ ⊥
Full source 
@[to_additive (attr := simp)]
lemma ker_snd : ker (snd G G') = .prod ⊤ ⊥ := SetLike.ext fun _ => (iff_of_eq (true_and _)).symm
Kernel of Second Projection Homomorphism is Trivial Product Subgroup
Informal description
The kernel of the second projection homomorphism $\text{snd} : G \times G' \to G'$ is equal to the product subgroup $\top \times \bot$, where $\top$ is the trivial subgroup of $G$ and $\bot$ is the trivial subgroup of $G'$.
Subgroup.Normal.map theorem
{H : Subgroup G} (h : H.Normal) (f : G →* N) (hf : Function.Surjective f) : (H.map f).Normal
Full source 
@[to_additive]
theorem Normal.map {H : Subgroup G} (h : H.Normal) (f : G →* N) (hf : Function.Surjective f) :
    (H.map f).Normal := by
  rw [← normalizer_eq_top_iff, ← top_le_iff, ← f.range_eq_top_of_surjective hf, f.range_eq_map,
    ← H.normalizer_eq_top]
  exact le_normalizer_map _
Image of Normal Subgroup under Surjective Homomorphism is Normal
Informal description
Let $G$ and $N$ be groups, $H$ a normal subgroup of $G$, and $f \colon G \to N$ a surjective group homomorphism. Then the image subgroup $f(H)$ is normal in $N$.
Subgroup.comap_normalizer_eq_of_surjective theorem
(H : Subgroup G) {f : N →* G} (hf : Function.Surjective f) : H.normalizer.comap f = (H.comap f).normalizer
Full source 
/-- The preimage of the normalizer is equal to the normalizer of the preimage of a surjective
  function. -/
@[to_additive
      "The preimage of the normalizer is equal to the normalizer of the preimage of
      a surjective function."]
theorem comap_normalizer_eq_of_surjective (H : Subgroup G) {f : N →* G}
    (hf : Function.Surjective f) : H.normalizer.comap f = (H.comap f).normalizer :=
  comap_normalizer_eq_of_le_range fun x _ ↦ hf x
Preimage of Normalizer Equals Normalizer of Preimage for Surjective Homomorphism
Informal description
Let $G$ and $N$ be groups, $H$ a subgroup of $G$, and $f \colon N \to G$ a surjective group homomorphism. Then the preimage of the normalizer of $H$ under $f$ equals the normalizer of the preimage of $H$ under $f$. In symbols: \[ f^{-1}(N_G(H)) = N_N(f^{-1}(H)). \]
Subgroup.map_equiv_normalizer_eq theorem
(H : Subgroup G) (f : G ≃* N) : H.normalizer.map f.toMonoidHom = (H.map f.toMonoidHom).normalizer
Full source 
/-- The image of the normalizer is equal to the normalizer of the image of an isomorphism. -/
@[to_additive
      "The image of the normalizer is equal to the normalizer of the image of an
      isomorphism."]
theorem map_equiv_normalizer_eq (H : Subgroup G) (f : G ≃* N) :
    H.normalizer.map f.toMonoidHom = (H.map f.toMonoidHom).normalizer := by
  ext x
  simp only [mem_normalizer_iff, mem_map_equiv]
  rw [f.toEquiv.forall_congr]
  intro
  simp
Image of Normalizer under Isomorphism Equals Normalizer of Image
Informal description
Let $G$ and $N$ be groups, $H$ a subgroup of $G$, and $f \colon G \to N$ a group isomorphism. Then the image of the normalizer of $H$ under $f$ is equal to the normalizer of the image of $H$ under $f$, i.e., \[ f(\text{N}_G(H)) = \text{N}_N(f(H)). \]
Subgroup.map_normalizer_eq_of_bijective theorem
(H : Subgroup G) {f : G →* N} (hf : Function.Bijective f) : H.normalizer.map f = (H.map f).normalizer
Full source 
/-- The image of the normalizer is equal to the normalizer of the image of a bijective
  function. -/
@[to_additive
      "The image of the normalizer is equal to the normalizer of the image of a bijective
        function."]
theorem map_normalizer_eq_of_bijective (H : Subgroup G) {f : G →* N} (hf : Function.Bijective f) :
    H.normalizer.map f = (H.map f).normalizer :=
  map_equiv_normalizer_eq H (MulEquiv.ofBijective f hf)
Image of Normalizer under Bijective Homomorphism Equals Normalizer of Image
Informal description
Let $G$ and $N$ be groups, $H$ a subgroup of $G$, and $f \colon G \to N$ a bijective group homomorphism. Then the image of the normalizer of $H$ under $f$ is equal to the normalizer of the image of $H$ under $f$, i.e., \[ f(\text{N}_G(H)) = \text{N}_N(f(H)). \]
MonoidHom.liftOfRightInverseAux definition
(hf : Function.RightInverse f_inv f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) : G₂ →* G₃
Full source 
/-- Auxiliary definition used to define `liftOfRightInverse` -/
@[to_additive "Auxiliary definition used to define `liftOfRightInverse`"]
def liftOfRightInverseAux (hf : Function.RightInverse f_inv f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) :
    G₂ →* G₃ where
  toFun b := g (f_inv b)
  map_one' := hg (hf 1)
  map_mul' := by
    intro x y
    rw [← g.map_mul, ← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker]
    apply hg
    rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one, f.map_mul]
    simp only [hf _]
Lift of a group homomorphism with right inverse
Informal description
Given a group homomorphism $f \colon G_1 \to G_2$ with a right inverse $f_{\text{inv}} \colon G_2 \to G_1$ (i.e., $f \circ f_{\text{inv}} = \text{id}_{G_2}$), and another group homomorphism $g \colon G_1 \to G_3$ whose kernel contains the kernel of $f$, the auxiliary function `MonoidHom.liftOfRightInverseAux` constructs a group homomorphism from $G_2$ to $G_3$ by mapping each $b \in G_2$ to $g(f_{\text{inv}}(b))$. This construction ensures that the resulting homomorphism satisfies the required properties of preserving the group structure.
MonoidHom.liftOfRightInverseAux_comp_apply theorem
(hf : Function.RightInverse f_inv f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) (x : G₁) : (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x
Full source 
@[to_additive (attr := simp)]
theorem liftOfRightInverseAux_comp_apply (hf : Function.RightInverse f_inv f) (g : G₁ →* G₃)
    (hg : f.ker ≤ g.ker) (x : G₁) : (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x := by
  dsimp [liftOfRightInverseAux]
  rw [← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker]
  apply hg
  rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one]
  simp only [hf _]
Composition Property of Lifted Homomorphism: $(\text{lift}(g) \circ f)(x) = g(x)$
Informal description
Let $f \colon G_1 \to G_2$ be a group homomorphism with a right inverse $f_{\text{inv}} \colon G_2 \to G_1$ (i.e., $f \circ f_{\text{inv}} = \text{id}_{G_2}$), and let $g \colon G_1 \to G_3$ be a group homomorphism whose kernel contains the kernel of $f$. Then for any $x \in G_1$, the composition of the lifted homomorphism $\text{liftOfRightInverseAux}(f, f_{\text{inv}}, hf, g, hg)$ with $f$ satisfies $(\text{liftOfRightInverseAux}(f, f_{\text{inv}}, hf, g, hg) \circ f)(x) = g(x)$.
MonoidHom.liftOfRightInverse definition
(hf : Function.RightInverse f_inv f) : { g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃)
Full source 
/-- `liftOfRightInverse f hf g hg` is the unique group homomorphism `φ`

* such that `φ.comp f = g` (`MonoidHom.liftOfRightInverse_comp`),
* where `f : G₁ →+* G₂` has a RightInverse `f_inv` (`hf`),
* and `g : G₂ →+* G₃` satisfies `hg : f.ker ≤ g.ker`.

See `MonoidHom.eq_liftOfRightInverse` for the uniqueness lemma.

```
   G₁.
   |  \
 f |   \ g
   |    \
   v     \⌟
   G₂----> G₃
      ∃!φ
```
-/
@[to_additive
      "`liftOfRightInverse f f_inv hf g hg` is the unique additive group homomorphism `φ`
      * such that `φ.comp f = g` (`AddMonoidHom.liftOfRightInverse_comp`),
      * where `f : G₁ →+ G₂` has a RightInverse `f_inv` (`hf`),
      * and `g : G₂ →+ G₃` satisfies `hg : f.ker ≤ g.ker`.
      See `AddMonoidHom.eq_liftOfRightInverse` for the uniqueness lemma.
      ```
         G₁.
         |  \\
       f |   \\ g
         |    \\
         v     \\⌟
         G₂----> G₃
            ∃!φ
      ```"]
def liftOfRightInverse (hf : Function.RightInverse f_inv f) :
    { g : G₁ →* G₃ // f.ker ≤ g.ker }{ g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃) where
  toFun g := f.liftOfRightInverseAux f_inv hf g.1 g.2
  invFun φ := ⟨φ.comp f, fun x hx ↦ mem_ker.mpr <| by simp [mem_ker.mp hx]⟩
  left_inv g := by
    ext
    simp only [comp_apply, liftOfRightInverseAux_comp_apply, Subtype.coe_mk]
  right_inv φ := by
    ext b
    simp [liftOfRightInverseAux, hf b]
Lift of group homomorphism with right inverse
Informal description
Given a group homomorphism \( f \colon G_1 \to G_2 \) with a right inverse \( f_{\text{inv}} \colon G_2 \to G_1 \) (i.e., \( f \circ f_{\text{inv}} = \text{id}_{G_2} \)), there is a bijection between: - The set of group homomorphisms \( g \colon G_1 \to G_3 \) whose kernel contains the kernel of \( f \), and - The set of group homomorphisms \( \varphi \colon G_2 \to G_3 \). The bijection is constructed such that for any \( g \) in the first set, the corresponding \( \varphi \) satisfies \( \varphi \circ f = g \), and conversely, any \( \varphi \) in the second set corresponds to \( \varphi \circ f \) in the first set.
MonoidHom.liftOfSurjective abbrev
(hf : Function.Surjective f) : { g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃)
Full source 
/-- A non-computable version of `MonoidHom.liftOfRightInverse` for when no computable right
inverse is available, that uses `Function.surjInv`. -/
@[to_additive (attr := simp)
      "A non-computable version of `AddMonoidHom.liftOfRightInverse` for when no
      computable right inverse is available."]
noncomputable abbrev liftOfSurjective (hf : Function.Surjective f) :
    { g : G₁ →* G₃ // f.ker ≤ g.ker }{ g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃) :=
  f.liftOfRightInverse (Function.surjInv hf) (Function.rightInverse_surjInv hf)
Lift of Group Homomorphism via Surjective Map
Informal description
Given a surjective group homomorphism $f \colon G_1 \to G_2$, there is a bijection between: - The set of group homomorphisms $g \colon G_1 \to G_3$ whose kernel contains the kernel of $f$, and - The set of group homomorphisms $\varphi \colon G_2 \to G_3$. The bijection is constructed such that for any $g$ in the first set, the corresponding $\varphi$ satisfies $\varphi \circ f = g$, and conversely, any $\varphi$ in the second set corresponds to $\varphi \circ f$ in the first set.
MonoidHom.liftOfRightInverse_comp_apply theorem
(hf : Function.RightInverse f_inv f) (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) (x : G₁) : (f.liftOfRightInverse f_inv hf g) (f x) = g.1 x
Full source 
@[to_additive (attr := simp)]
theorem liftOfRightInverse_comp_apply (hf : Function.RightInverse f_inv f)
    (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) (x : G₁) :
    (f.liftOfRightInverse f_inv hf g) (f x) = g.1 x :=
  f.liftOfRightInverseAux_comp_apply f_inv hf g.1 g.2 x
Lifted Homomorphism Evaluation: $(\text{lift}(g) \circ f)(x) = g(x)$
Informal description
Let $f \colon G_1 \to G_2$ be a group homomorphism with a right inverse $f_{\text{inv}} \colon G_2 \to G_1$ (i.e., $f \circ f_{\text{inv}} = \text{id}_{G_2}$), and let $g \colon G_1 \to G_3$ be a group homomorphism whose kernel contains the kernel of $f$. Then for any $x \in G_1$, the lifted homomorphism $\text{liftOfRightInverse}(f, f_{\text{inv}}, hf, g)$ satisfies $(\text{liftOfRightInverse}(f, f_{\text{inv}}, hf, g))(f(x)) = g(x)$.
MonoidHom.liftOfRightInverse_comp theorem
(hf : Function.RightInverse f_inv f) (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) : (f.liftOfRightInverse f_inv hf g).comp f = g
Full source 
@[to_additive (attr := simp)]
theorem liftOfRightInverse_comp (hf : Function.RightInverse f_inv f)
    (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) : (f.liftOfRightInverse f_inv hf g).comp f = g :=
  MonoidHom.ext <| f.liftOfRightInverse_comp_apply f_inv hf g
Composition of Lifted Homomorphism with Original Equals Original: $(\text{lift}(g) \circ f) = g$
Informal description
Let $f \colon G_1 \to G_2$ be a group homomorphism with a right inverse $f_{\text{inv}} \colon G_2 \to G_1$ (i.e., $f \circ f_{\text{inv}} = \text{id}_{G_2}$), and let $g \colon G_1 \to G_3$ be a group homomorphism whose kernel contains the kernel of $f$. Then the composition of the lifted homomorphism $\text{liftOfRightInverse}(f, f_{\text{inv}}, hf, g)$ with $f$ equals $g$, i.e., $$(\text{liftOfRightInverse}(f, f_{\text{inv}}, hf, g)) \circ f = g.$$
Subgroup.Normal.comap theorem
{H : Subgroup N} (hH : H.Normal) (f : G →* N) : (H.comap f).Normal
Full source 
@[to_additive]
theorem Normal.comap {H : Subgroup N} (hH : H.Normal) (f : G →* N) : (H.comap f).Normal :=
  ⟨fun _ => by simp +contextual [Subgroup.mem_comap, hH.conj_mem]⟩
Preimage of Normal Subgroup Under Homomorphism is Normal
Informal description
Let $G$ and $N$ be groups, $H$ a normal subgroup of $N$, and $f \colon G \to N$ a group homomorphism. Then the preimage $f^{-1}(H)$ is a normal subgroup of $G$.
Subgroup.normal_comap instance
{H : Subgroup N} [nH : H.Normal] (f : G →* N) : (H.comap f).Normal
Full source 
@[to_additive]
instance (priority := 100) normal_comap {H : Subgroup N} [nH : H.Normal] (f : G →* N) :
    (H.comap f).Normal :=
  nH.comap _
Preimage of Normal Subgroup Under Homomorphism is Normal
Informal description
For any groups $G$ and $N$, normal subgroup $H$ of $N$, and group homomorphism $f \colon G \to N$, the preimage $f^{-1}(H)$ is a normal subgroup of $G$.
Subgroup.Normal.subgroupOf theorem
{H : Subgroup G} (hH : H.Normal) (K : Subgroup G) : (H.subgroupOf K).Normal
Full source 
@[to_additive]
theorem Normal.subgroupOf {H : Subgroup G} (hH : H.Normal) (K : Subgroup G) :
    (H.subgroupOf K).Normal :=
  hH.comap _
Intersection of Normal Subgroup with Subgroup is Normal in Subgroup
Informal description
Let $G$ be a group, $H$ a normal subgroup of $G$, and $K$ any subgroup of $G$. Then the intersection $H \cap K$ is a normal subgroup of $K$.
Subgroup.normal_subgroupOf instance
{H N : Subgroup G} [N.Normal] : (N.subgroupOf H).Normal
Full source 
@[to_additive]
instance (priority := 100) normal_subgroupOf {H N : Subgroup G} [N.Normal] :
    (N.subgroupOf H).Normal :=
  Subgroup.normal_comap _
Intersection of a Normal Subgroup with a Subgroup is Normal
Informal description
For any subgroups $H$ and $N$ of a group $G$, if $N$ is a normal subgroup of $G$, then the intersection $N \cap H$ is a normal subgroup of $H$.
Subgroup.map_normalClosure theorem
(s : Set G) (f : G →* N) (hf : Surjective f) : (normalClosure s).map f = normalClosure (f '' s)
Full source 
theorem map_normalClosure (s : Set G) (f : G →* N) (hf : Surjective f) :
    (normalClosure s).map f = normalClosure (f '' s) := by
  have : Normal (map f (normalClosure s)) := Normal.map inferInstance f hf
  apply le_antisymm
  · simp [map_le_iff_le_comap, normalClosure_le_normal, coe_comap,
      ← Set.image_subset_iff, subset_normalClosure]
  · exact normalClosure_le_normal (Set.image_subset f subset_normalClosure)
Normal Closure Commutes with Surjective Homomorphism Image
Informal description
Let $G$ and $N$ be groups, $s$ a subset of $G$, and $f \colon G \to N$ a surjective group homomorphism. Then the image of the normal closure of $s$ under $f$ equals the normal closure of the image of $s$ under $f$, i.e., \[ f(\text{normalClosure}(s)) = \text{normalClosure}(f(s)). \]
Subgroup.comap_normalClosure theorem
(s : Set N) (f : G ≃* N) : normalClosure (f ⁻¹' s) = (normalClosure s).comap f
Full source 
theorem comap_normalClosure (s : Set N) (f : G ≃* N) :
    normalClosure (f ⁻¹' s) = (normalClosure s).comap f := by
  have := Set.preimage_equiv_eq_image_symm s f.toEquiv
  simp_all [comap_equiv_eq_map_symm, map_normalClosure s (f.symm : N →* G) f.symm.surjective]
Normal Closure Commutes with Preimage under Group Isomorphism
Informal description
Let $G$ and $N$ be groups, $s$ a subset of $N$, and $f \colon G \simeq^* N$ a group isomorphism. Then the normal closure of the preimage $f^{-1}(s)$ in $G$ is equal to the preimage under $f$ of the normal closure of $s$ in $N$, i.e., \[ \text{normalClosure}(f^{-1}(s)) = f^{-1}(\text{normalClosure}(s)). \]
Subgroup.Normal.of_map_injective theorem
{G H : Type*} [Group G] [Group H] {φ : G →* H} (hφ : Function.Injective φ) {L : Subgroup G} (n : (L.map φ).Normal) : L.Normal
Full source 
lemma Normal.of_map_injective {G H : Type*} [Group G] [Group H] {φ : G →* H}
    (hφ : Function.Injective φ) {L : Subgroup G} (n : (L.map φ).Normal) : L.Normal :=
  L.comap_map_eq_self_of_injective hφ ▸ n.comap φ
Normality Lifts Through Injective Homomorphisms
Informal description
Let $G$ and $H$ be groups, and let $\varphi \colon G \to H$ be an injective group homomorphism. For any subgroup $L$ of $G$, if the image $\varphi(L)$ is a normal subgroup of $H$, then $L$ is a normal subgroup of $G$.
Subgroup.Normal.of_map_subtype theorem
{K : Subgroup G} {L : Subgroup K} (n : (Subgroup.map K.subtype L).Normal) : L.Normal
Full source 
theorem Normal.of_map_subtype {K : Subgroup G} {L : Subgroup K}
    (n : (Subgroup.map K.subtype L).Normal) : L.Normal :=
  n.of_map_injective K.subtype_injective
Normality of Subgroup Lifts Through Inclusion Homomorphism
Informal description
Let $G$ be a group and $K$ a subgroup of $G$. For any subgroup $L$ of $K$, if the image of $L$ under the inclusion homomorphism $K \hookrightarrow G$ is a normal subgroup of $G$, then $L$ is a normal subgroup of $K$.
Subgroup.normal_subgroupOf_iff theorem
{H K : Subgroup G} (hHK : H ≤ K) : (H.subgroupOf K).Normal ↔ ∀ h k, h ∈ H → k ∈ K → k * h * k⁻¹ ∈ H
Full source 
@[to_additive]
theorem normal_subgroupOf_iff {H K : Subgroup G} (hHK : H ≤ K) :
    (H.subgroupOf K).Normal ↔ ∀ h k, h ∈ H → k ∈ K → k * h * k⁻¹ ∈ H :=
  ⟨fun hN h k hH hK => hN.conj_mem ⟨h, hHK hH⟩ hH ⟨k, hK⟩, fun hN =>
    { conj_mem := fun h hm k => hN h.1 k.1 hm k.2 }⟩
Normality Criterion for Intersection of Subgroups
Informal description
Let $H$ and $K$ be subgroups of a group $G$ with $H \leq K$. Then the subgroup $H \cap K$ (viewed as a subgroup of $K$) is normal in $K$ if and only if for all $h \in H$ and $k \in K$, the conjugate $k h k^{-1}$ belongs to $H$.
Subgroup.prod_subgroupOf_prod_normal instance
{H₁ K₁ : Subgroup G} {H₂ K₂ : Subgroup N} [h₁ : (H₁.subgroupOf K₁).Normal] [h₂ : (H₂.subgroupOf K₂).Normal] : ((H₁.prod H₂).subgroupOf (K₁.prod K₂)).Normal
Full source 
@[to_additive prod_addSubgroupOf_prod_normal]
instance prod_subgroupOf_prod_normal {H₁ K₁ : Subgroup G} {H₂ K₂ : Subgroup N}
    [h₁ : (H₁.subgroupOf K₁).Normal] [h₂ : (H₂.subgroupOf K₂).Normal] :
    ((H₁.prod H₂).subgroupOf (K₁.prod K₂)).Normal where
  conj_mem n hgHK g :=
    ⟨h₁.conj_mem ⟨(n : G × N).fst, (mem_prod.mp n.2).1⟩ hgHK.1
        ⟨(g : G × N).fst, (mem_prod.mp g.2).1⟩,
      h₂.conj_mem ⟨(n : G × N).snd, (mem_prod.mp n.2).2⟩ hgHK.2
        ⟨(g : G × N).snd, (mem_prod.mp g.2).2⟩⟩
Normality of Product Subgroups in Product Groups
Informal description
For any subgroups $H_1$ of a group $G$ and $H_2$ of a group $N$, if $H_1$ is normal in $K_1$ (viewed as a subgroup of $K_1$) and $H_2$ is normal in $K_2$ (viewed as a subgroup of $K_2$), then the product subgroup $H_1 \times H_2$ is normal in $K_1 \times K_2$ (viewed as a subgroup of $K_1 \times K_2$).
Subgroup.prod_normal instance
(H : Subgroup G) (K : Subgroup N) [hH : H.Normal] [hK : K.Normal] : (H.prod K).Normal
Full source 
@[to_additive prod_normal]
instance prod_normal (H : Subgroup G) (K : Subgroup N) [hH : H.Normal] [hK : K.Normal] :
    (H.prod K).Normal where
  conj_mem n hg g :=
    ⟨hH.conj_mem n.fst (Subgroup.mem_prod.mp hg).1 g.fst,
      hK.conj_mem n.snd (Subgroup.mem_prod.mp hg).2 g.snd⟩
Product of Normal Subgroups is Normal
Informal description
For any normal subgroups $H$ of a group $G$ and $K$ of a group $N$, the product subgroup $H \times K$ is a normal subgroup of $G \times N$.
Subgroup.inf_subgroupOf_inf_normal_of_right theorem
(A B' B : Subgroup G) [hN : (B'.subgroupOf B).Normal] : ((A ⊓ B').subgroupOf (A ⊓ B)).Normal
Full source 
@[to_additive]
theorem inf_subgroupOf_inf_normal_of_right (A B' B : Subgroup G)
    [hN : (B'.subgroupOf B).Normal] : ((A ⊓ B').subgroupOf (A ⊓ B)).Normal := by
  rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢
  rw [inf_inf_inf_comm, inf_idem]
  exact le_trans (inf_le_inf A.le_normalizer hN) (inf_normalizer_le_normalizer_inf)
Normality of Right Intersection in Subgroup Context
Informal description
Let $G$ be a group with subgroups $A$, $B'$, and $B$. If $B'$ is a normal subgroup of $B$ (when viewed as a subgroup of $B$), then the intersection $(A \cap B')$ is a normal subgroup of $(A \cap B)$ (when viewed as a subgroup of $A \cap B$).
Subgroup.inf_subgroupOf_inf_normal_of_left theorem
{A' A : Subgroup G} (B : Subgroup G) [hN : (A'.subgroupOf A).Normal] : ((A' ⊓ B).subgroupOf (A ⊓ B)).Normal
Full source 
@[to_additive]
theorem inf_subgroupOf_inf_normal_of_left {A' A : Subgroup G} (B : Subgroup G)
    [hN : (A'.subgroupOf A).Normal] : ((A' ⊓ B).subgroupOf (A ⊓ B)).Normal := by
  rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢
  rw [inf_inf_inf_comm, inf_idem]
  exact le_trans (inf_le_inf hN B.le_normalizer) (inf_normalizer_le_normalizer_inf)
Normality of Left Intersection in Subgroup Lattice
Informal description
Let $A'$ and $A$ be subgroups of a group $G$ such that $A' \cap A$ is a normal subgroup of $A$, and let $B$ be another subgroup of $G$. Then the intersection $(A' \cap B) \cap (A \cap B)$ is a normal subgroup of $A \cap B$.
Subgroup.normal_iInf_normal theorem
{ι : Type*} {a : ι → Subgroup G} (norm : ∀ i : ι, (a i).Normal) : (iInf a).Normal
Full source 
@[to_additive]
theorem normal_iInf_normal {ι : Type*} {a : ι → Subgroup G}
    (norm : ∀ i : ι, (a i).Normal) : (iInf a).Normal := by
  constructor
  intro g g_in_iInf h
  rw [Subgroup.mem_iInf] at g_in_iInf ⊢
  intro i
  exact (norm i).conj_mem g (g_in_iInf i) h
Intersection of Normal Subgroups is Normal
Informal description
Let $G$ be a group and $\{H_i\}_{i \in \iota}$ be a family of normal subgroups of $G$. Then the infimum $\bigsqcap_i H_i$ (the intersection of all $H_i$) is also a normal subgroup of $G$.
Subgroup.SubgroupNormal.mem_comm theorem
{H K : Subgroup G} (hK : H ≤ K) [hN : (H.subgroupOf K).Normal] {a b : G} (hb : b ∈ K) (h : a * b ∈ H) : b * a ∈ H
Full source 
@[to_additive]
theorem SubgroupNormal.mem_comm {H K : Subgroup G} (hK : H ≤ K) [hN : (H.subgroupOf K).Normal]
    {a b : G} (hb : b ∈ K) (h : a * b ∈ H) : b * a ∈ H := by
  have := (normal_subgroupOf_iff hK).mp hN (a * b) b h hb
  rwa [mul_assoc, mul_assoc, mul_inv_cancel, mul_one] at this
Commutativity Property for Elements in Normal Subgroup Inclusion
Informal description
Let $H$ and $K$ be subgroups of a group $G$ such that $H \leq K$ and $H$ is normal in $K$ (when viewed as a subgroup of $K$ via the inclusion $H \cap K$). For any elements $a, b \in G$ with $b \in K$ and $a \cdot b \in H$, it follows that $b \cdot a \in H$.
Subgroup.commute_of_normal_of_disjoint theorem
(H₁ H₂ : Subgroup G) (hH₁ : H₁.Normal) (hH₂ : H₂.Normal) (hdis : Disjoint H₁ H₂) (x y : G) (hx : x ∈ H₁) (hy : y ∈ H₂) : Commute x y
Full source 
/-- Elements of disjoint, normal subgroups commute. -/
@[to_additive "Elements of disjoint, normal subgroups commute."]
theorem commute_of_normal_of_disjoint (H₁ H₂ : Subgroup G) (hH₁ : H₁.Normal) (hH₂ : H₂.Normal)
    (hdis : Disjoint H₁ H₂) (x y : G) (hx : x ∈ H₁) (hy : y ∈ H₂) : Commute x y := by
  suffices x * y * x⁻¹ * y⁻¹ = 1 by
    show x * y = y * x
    · rw [mul_assoc, mul_eq_one_iff_eq_inv] at this
      simpa
  apply hdis.le_bot
  constructor
  · suffices x * (y * x⁻¹ * y⁻¹) ∈ H₁ by simpa [mul_assoc]
    exact H₁.mul_mem hx (hH₁.conj_mem _ (H₁.inv_mem hx) _)
  · show x * y * x⁻¹ * y⁻¹ ∈ H₂
    apply H₂.mul_mem _ (H₂.inv_mem hy)
    apply hH₂.conj_mem _ hy
Commutation of Elements in Disjoint Normal Subgroups
Informal description
Let $H_1$ and $H_2$ be normal subgroups of a group $G$ such that $H_1$ and $H_2$ are disjoint (i.e., $H_1 \cap H_2 = \{\text{identity}\}$). Then for any $x \in H_1$ and $y \in H_2$, the elements $x$ and $y$ commute, i.e., $x \cdot y = y \cdot x$.
Subgroup.normal_subgroupOf_of_le_normalizer theorem
{H N : Subgroup G} (hLE : H ≤ N.normalizer) : (N.subgroupOf H).Normal
Full source 
@[to_additive]
theorem normal_subgroupOf_of_le_normalizer {H N : Subgroup G}
    (hLE : H ≤ N.normalizer) : (N.subgroupOf H).Normal := by
  rw [normal_subgroupOf_iff_le_normalizer_inf]
  exact (le_inf hLE H.le_normalizer).trans inf_normalizer_le_normalizer_inf
Normality of Intersection under Normalizer Condition: $H \leq N_G(N) \Rightarrow N \cap H \triangleleft H$
Informal description
Let $H$ and $N$ be subgroups of a group $G$. If $H$ is contained in the normalizer of $N$ (i.e., $H \leq N_G(N)$), then the intersection $N \cap H$ is a normal subgroup of $H$.
Subgroup.normal_subgroupOf_sup_of_le_normalizer theorem
{H N : Subgroup G} (hLE : H ≤ N.normalizer) : (N.subgroupOf (H ⊔ N)).Normal
Full source 
@[to_additive]
theorem normal_subgroupOf_sup_of_le_normalizer {H N : Subgroup G}
    (hLE : H ≤ N.normalizer) : (N.subgroupOf (H ⊔ N)).Normal := by
  rw [normal_subgroupOf_iff_le_normalizer le_sup_right]
  exact sup_le hLE le_normalizer
Normality of Intersection with Join under Normalizer Condition
Informal description
Let $G$ be a group with subgroups $H$ and $N$ such that $H$ is contained in the normalizer of $N$. Then the intersection of $N$ with the join $H \sqcup N$ is a normal subgroup of $H \sqcup N$.
IsConj.normalClosure_eq_top_of theorem
{N : Subgroup G} [hn : N.Normal] {g g' : G} {hg : g ∈ N} {hg' : g' ∈ N} (hc : IsConj g g') (ht : normalClosure ({⟨g, hg⟩} : Set N) = ⊤) : normalClosure ({⟨g', hg'⟩} : Set N) = ⊤
Full source 
theorem normalClosure_eq_top_of {N : Subgroup G} [hn : N.Normal] {g g' : G} {hg : g ∈ N}
    {hg' : g' ∈ N} (hc : IsConj g g') (ht : normalClosure ({⟨g, hg⟩} : Set N) = ⊤) :
    normalClosure ({⟨g', hg'⟩} : Set N) = ⊤ := by
  obtain ⟨c, rfl⟩ := isConj_iff.1 hc
  have h : ∀ x : N, (MulAut.conj c) x ∈ N := by
    rintro ⟨x, hx⟩
    exact hn.conj_mem _ hx c
  have hs : Function.Surjective (((MulAut.conj c).toMonoidHom.restrict N).codRestrict _ h) := by
    rintro ⟨x, hx⟩
    refine ⟨⟨c⁻¹ * x * c, ?_⟩, ?_⟩
    · have h := hn.conj_mem _ hx c⁻¹
      rwa [inv_inv] at h
    simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply, coe_mk,
      MonoidHom.restrict_apply, Subtype.mk_eq_mk, ← mul_assoc, mul_inv_cancel, one_mul]
    rw [mul_assoc, mul_inv_cancel, mul_one]
  rw [eq_top_iff, ← MonoidHom.range_eq_top.2 hs, MonoidHom.range_eq_map]
  refine le_trans (map_mono (eq_top_iff.1 ht)) (map_le_iff_le_comap.2 (normalClosure_le_normal ?_))
  rw [Set.singleton_subset_iff, SetLike.mem_coe]
  simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply, coe_mk,
    MonoidHom.restrict_apply, mem_comap]
  exact subset_normalClosure (Set.mem_singleton _)
Conjugate Elements Generate Same Normal Closure in Normal Subgroup
Informal description
Let $G$ be a group and $N$ a normal subgroup of $G$. For any two elements $g, g' \in N$ that are conjugate in $G$ (i.e., there exists $h \in G$ such that $g' = hgh^{-1}$), if the normal closure of $\{g\}$ in $N$ is the entire group $N$, then the normal closure of $\{g'\}$ in $N$ is also the entire group $N$.
ConjClasses.noncenter definition
(G : Type*) [Monoid G] : Set (ConjClasses G)
Full source 
/-- The conjugacy classes that are not trivial. -/
def noncenter (G : Type*) [Monoid G] : Set (ConjClasses G) :=
  {x | x.carrier.Nontrivial}
Nontrivial conjugacy classes of a monoid
Informal description
The set of nontrivial conjugacy classes of a monoid $G$, defined as the collection of conjugacy classes whose carrier set contains at least two distinct elements. A conjugacy class is considered nontrivial if there exist distinct elements $x$ and $y$ in $G$ that are conjugate to each other.
ConjClasses.mem_noncenter theorem
{G} [Monoid G] (g : ConjClasses G) : g ∈ noncenter G ↔ g.carrier.Nontrivial
Full source 
@[simp] lemma mem_noncenter {G} [Monoid G] (g : ConjClasses G) :
    g ∈ noncenter Gg ∈ noncenter G ↔ g.carrier.Nontrivial := Iff.rfl
Characterization of Nontrivial Conjugacy Classes: $g \in \text{noncenter}(G) \leftrightarrow \text{carrier}(g)$ is nontrivial
Informal description
For any conjugacy class $g$ in a monoid $G$, $g$ belongs to the set of nontrivial conjugacy classes if and only if the set of all conjugates of elements in $g$ contains at least two distinct elements. In other words, $g \in \text{noncenter}(G) \leftrightarrow \text{carrier}(g)$ is a nontrivial set.
AddSubgroup.inertia definition
{M : Type*} [AddGroup M] (I : AddSubgroup M) (G : Type*) [Group G] [MulAction G M] : Subgroup G
Full source 
/-- Suppose `G` acts on `M` and `I` is a subgroup of `M`.
The inertia subgroup of `I` is the subgroup of `G` whose action is trivial mod `I`. -/
def AddSubgroup.inertia {M : Type*} [AddGroup M] (I : AddSubgroup M) (G : Type*)
    [Group G] [MulAction G M] : Subgroup G where
  carrier := { σ | ∀ x, σ • x - x ∈ I }
  mul_mem' {a b} ha hb x := by simpa [mul_smul] using add_mem (ha (b • x)) (hb x)
  one_mem' := by simp [zero_mem]
  inv_mem' {a} ha x := by simpa using sub_mem_comm_iff.mp (ha (a⁻¹ • x))
Inertia subgroup of an additive subgroup under group action
Informal description
Given an additive group $M$ and a subgroup $I$ of $M$, and a group $G$ acting multiplicatively on $M$, the inertia subgroup of $I$ in $G$ is the subgroup of $G$ consisting of all elements $\sigma \in G$ such that for every $x \in M$, the difference $\sigma \cdot x - x$ lies in $I$.
AddSubgroup.mem_inertia theorem
{M : Type*} [AddGroup M] {I : AddSubgroup M} {G : Type*} [Group G] [MulAction G M] {σ : G} : σ ∈ I.inertia G ↔ ∀ x, σ • x - x ∈ I
Full source 
@[simp] lemma AddSubgroup.mem_inertia {M : Type*} [AddGroup M] {I : AddSubgroup M} {G : Type*}
    [Group G] [MulAction G M] {σ : G} : σ ∈ I.inertia Gσ ∈ I.inertia G ↔ ∀ x, σ • x - x ∈ I := .rfl
Characterization of Elements in the Inertia Subgroup: $\sigma \in I.\text{inertia}(G) \leftrightarrow \forall x \in M, \sigma \cdot x - x \in I$
Informal description
Let $M$ be an additive group with an additive subgroup $I$, and let $G$ be a group acting multiplicatively on $M$. For any element $\sigma \in G$, $\sigma$ belongs to the inertia subgroup of $I$ in $G$ if and only if for every $x \in M$, the difference $\sigma \cdot x - x$ lies in $I$.