mathlib documentation

group_theory.subgroup

Subgroups

This file defines multiplicative and additive subgroups as an extension of submonoids, in a bundled form (unbundled subgroups are in deprecated/subgroups.lean).

We prove subgroups of a group form a complete lattice, and results about images and preimages of subgroups under group homomorphisms. The bundled subgroups use bundled monoid homomorphisms.

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

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

Main definitions

Notation used here:

Definitions in the file:

Implementation notes

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

Tags

subgroup, subgroups

def subgroup.to_submonoid {G : Type u_3} [group G] :

Reinterpret a subgroup as a submonoid.

structure subgroup (G : Type u_3) [group G] :
Type u_3

A subgroup of a group G is a subset containing 1, closed under multiplication and closed under multiplicative inverse.

structure add_subgroup (G : Type u_3) [add_group G] :
Type u_3

An additive subgroup of an additive group G is a subset containing 0, closed under addition and additive inverse.

Reinterpret an add_subgroup as an add_submonoid.

def subgroup.to_add_subgroup {G : Type u_1} [group G] :

Map from subgroups of group G to add_subgroups of additive G.

Equations
def subgroup.of_add_subgroup {G : Type u_1} [group G] :

Map from add_subgroups of additive G to subgroups of G.

Equations

Map from add_subgroups of add_group G to subgroups of multiplicative G.

Equations

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

Equations
@[instance]
def add_subgroup.set.has_coe {G : Type u_1} [add_group G] :

@[instance]
def subgroup.set.has_coe {G : Type u_1} [group G] :

Equations
@[simp]

@[simp]
theorem subgroup.coe_to_submonoid {G : Type u_1} [group G] (K : subgroup G) :

@[instance]
def subgroup.has_mem {G : Type u_1} [group G] :

Equations
@[instance]
def add_subgroup.has_mem {G : Type u_1} [add_group G] :

@[instance]

@[instance]
def subgroup.has_coe_to_sort {G : Type u_1} [group G] :

Equations
@[simp]
theorem subgroup.mem_coe {G : Type u_1} [group G] {K : subgroup G} {g : G} :
g K g K

@[simp]
theorem add_subgroup.mem_coe {G : Type u_1} [add_group G] {K : add_subgroup G} {g : G} :
g K g K

@[simp]
theorem subgroup.coe_coe {G : Type u_1} [group G] (K : subgroup G) :

@[simp]
theorem add_subgroup.coe_coe {G : Type u_1} [add_group G] (K : add_subgroup G) :

theorem add_subgroup.exists {G : Type u_1} [add_group G] {K : add_subgroup G} {p : K → Prop} :
(∃ (x : K), p x) ∃ (x : G) (H : x K), p x, H⟩

theorem subgroup.exists {G : Type u_1} [group G] {K : subgroup G} {p : K → Prop} :
(∃ (x : K), p x) ∃ (x : G) (H : x K), p x, H⟩

theorem subgroup.forall {G : Type u_1} [group G] {K : subgroup G} {p : K → Prop} :
(∀ (x : K), p x) ∀ (x : G) (H : x K), p x, H⟩

theorem add_subgroup.forall {G : Type u_1} [add_group G] {K : add_subgroup G} {p : K → Prop} :
(∀ (x : K), p x) ∀ (x : G) (H : x K), p x, H⟩

def subgroup.copy {G : Type u_1} [group G] (K : subgroup G) (s : set G) :
s = Ksubgroup G

Copy of a subgroup with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations
def add_subgroup.copy {G : Type u_1} [add_group G] (K : add_subgroup G) (s : set G) :
s = Kadd_subgroup G

Copy of an additive subgroup with a new carrier equal to the old one. Useful to fix definitional equalities

theorem add_subgroup.ext' {G : Type u_1} [add_group G] {H K : add_subgroup G} :
H = KH = K

Two add_groups are equal if the underlying subsets are equal.

theorem subgroup.ext' {G : Type u_1} [group G] {H K : subgroup G} :
H = KH = K

theorem add_subgroup.ext'_iff {G : Type u_1} [add_group G] {H K : add_subgroup G} :
H = K H = K

Two add_subgroups are equal if and only if the underlying subsets are equal.

theorem subgroup.ext'_iff {G : Type u_1} [group G] {H K : subgroup G} :
H = K H = K

@[ext]
theorem subgroup.ext {G : Type u_1} [group G] {H K : subgroup G} :
(∀ (x : G), x H x K)H = K

Two subgroups are equal if they have the same elements.

@[ext]
theorem add_subgroup.ext {G : Type u_1} [add_group G] {H K : add_subgroup G} :
(∀ (x : G), x H x K)H = K

Two add_subgroups are equal if they have the same elements.

theorem subgroup.one_mem {G : Type u_1} [group G] (H : subgroup G) :
1 H

A subgroup contains the group's 1.

theorem add_subgroup.zero_mem {G : Type u_1} [add_group G] (H : add_subgroup G) :
0 H

An add_subgroup contains the group's 0.

theorem add_subgroup.add_mem {G : Type u_1} [add_group G] (H : add_subgroup G) {x y : G} :
x Hy Hx + y H

An add_subgroup is closed under addition.

theorem subgroup.mul_mem {G : Type u_1} [group G] (H : subgroup G) {x y : G} :
x Hy Hx * y H

A subgroup is closed under multiplication.

theorem subgroup.inv_mem {G : Type u_1} [group G] (H : subgroup G) {x : G} :
x Hx⁻¹ H

A subgroup is closed under inverse.

theorem add_subgroup.neg_mem {G : Type u_1} [add_group G] (H : add_subgroup G) {x : G} :
x H-x H

An add_subgroup is closed under inverse.

@[simp]
theorem add_subgroup.neg_mem_iff {G : Type u_1} [add_group G] (H : add_subgroup G) {x : G} :
-x H x H

@[simp]
theorem subgroup.inv_mem_iff {G : Type u_1} [group G] (H : subgroup G) {x : G} :
x⁻¹ H x H

theorem add_subgroup.add_mem_cancel_right {G : Type u_1} [add_group G] (H : add_subgroup G) {x y : G} :
x H(y + x H y H)

theorem subgroup.mul_mem_cancel_right {G : Type u_1} [group G] (H : subgroup G) {x y : G} :
x H(y * x H y H)

theorem subgroup.mul_mem_cancel_left {G : Type u_1} [group G] (H : subgroup G) {x y : G} :
x H(x * y H y H)

theorem add_subgroup.add_mem_cancel_left {G : Type u_1} [add_group G] (H : add_subgroup G) {x y : G} :
x H(x + y H y H)

theorem subgroup.list_prod_mem {G : Type u_1} [group G] (K : subgroup G) {l : list G} :
(∀ (x : G), x lx K)l.prod K

Product of a list of elements in a subgroup is in the subgroup.

theorem add_subgroup.list_sum_mem {G : Type u_1} [add_group G] (K : add_subgroup G) {l : list G} :
(∀ (x : G), x lx K)l.sum K

Sum of a list of elements in an add_subgroup is in the add_subgroup.

theorem add_subgroup.multiset_sum_mem {G : Type u_1} [add_comm_group G] (K : add_subgroup G) (g : multiset G) :
(∀ (a : G), a ga K)g.sum K

Sum of a multiset of elements in an add_subgroup of an add_comm_group is in the add_subgroup.

theorem subgroup.multiset_prod_mem {G : Type u_1} [comm_group G] (K : subgroup G) (g : multiset G) :
(∀ (a : G), a ga K)g.prod K

Product of a multiset of elements in a subgroup of a comm_group is in the subgroup.

theorem add_subgroup.sum_mem {G : Type u_1} [add_comm_group G] (K : add_subgroup G) {ι : Type u_2} {t : finset ι} {f : ι → G} :
(∀ (c : ι), c tf c K)∑ (c : ι) in t, f c K

Sum of elements in an add_subgroup of an add_comm_group indexed by a finset is in the add_subgroup.

theorem subgroup.prod_mem {G : Type u_1} [comm_group G] (K : subgroup G) {ι : Type u_2} {t : finset ι} {f : ι → G} :
(∀ (c : ι), c tf c K)∏ (c : ι) in t, f c K

Product of elements of a subgroup of a comm_group indexed by a finset is in the subgroup.

theorem subgroup.pow_mem {G : Type u_1} [group G] (K : subgroup G) {x : G} (hx : x K) (n : ) :
x ^ n K

theorem subgroup.gpow_mem {G : Type u_1} [group G] (K : subgroup G) {x : G} (hx : x K) (n : ) :
x ^ n K

def subgroup.of_div {G : Type u_1} [group G] (s : set G) :
s.nonempty(∀ (x y : G), x sy sx * y⁻¹ s)subgroup G

Construct a subgroup from a nonempty set that is closed under division.

Equations
def add_subgroup.of_sub {G : Type u_1} [add_group G] (s : set G) :
s.nonempty(∀ (x y : G), x sy sx + -y s)add_subgroup G

Construct a subgroup from a nonempty set that is closed under subtraction

@[instance]
def subgroup.has_mul {G : Type u_1} [group G] (H : subgroup G) :

A subgroup of a group inherits a multiplication.

Equations
@[instance]
def add_subgroup.has_add {G : Type u_1} [add_group G] (H : add_subgroup G) :

An add_subgroup of an add_group inherits an addition.

@[instance]
def subgroup.has_one {G : Type u_1} [group G] (H : subgroup G) :

A subgroup of a group inherits a 1.

Equations
@[instance]
def add_subgroup.has_zero {G : Type u_1} [add_group G] (H : add_subgroup G) :

An add_subgroup of an add_group inherits a zero.

@[instance]
def add_subgroup.has_neg {G : Type u_1} [add_group G] (H : add_subgroup G) :

A add_subgroup of a add_group inherits an inverse.

@[instance]
def subgroup.has_inv {G : Type u_1} [group G] (H : subgroup G) :

A subgroup of a group inherits an inverse.

Equations
@[simp]
theorem add_subgroup.coe_add {G : Type u_1} [add_group G] (H : add_subgroup G) (x y : H) :
(x + y) = x + y

@[simp]
theorem subgroup.coe_mul {G : Type u_1} [group G] (H : subgroup G) (x y : H) :
x * y = (x) * y

@[simp]
theorem add_subgroup.coe_zero {G : Type u_1} [add_group G] (H : add_subgroup G) :
0 = 0

@[simp]
theorem subgroup.coe_one {G : Type u_1} [group G] (H : subgroup G) :
1 = 1

@[simp]
theorem add_subgroup.coe_neg {G : Type u_1} [add_group G] (H : add_subgroup G) (x : H) :

@[simp]
theorem subgroup.coe_inv {G : Type u_1} [group G] (H : subgroup G) (x : H) :

@[simp]
theorem add_subgroup.coe_mk {G : Type u_1} [add_group G] (H : add_subgroup G) (x : G) (hx : x H) :
x, hx⟩ = x

@[simp]
theorem subgroup.coe_mk {G : Type u_1} [group G] (H : subgroup G) (x : G) (hx : x H) :
x, hx⟩ = x

@[instance]
def subgroup.to_group {G : Type u_1} [group G] (H : subgroup G) :

A subgroup of a group inherits a group structure.

Equations
@[instance]
def add_subgroup.to_add_group {G : Type u_1} [add_group G] (H : add_subgroup G) :

An add_subgroup of an add_group inherits an add_group structure.

@[instance]
def subgroup.to_comm_group {G : Type u_1} [comm_group G] (H : subgroup G) :

A subgroup of a comm_group is a comm_group.

Equations
def subgroup.subtype {G : Type u_1} [group G] (H : subgroup G) :

The natural group hom from a subgroup of group G to G.

Equations
def add_subgroup.subtype {G : Type u_1} [add_group G] (H : add_subgroup G) :

The natural group hom from an add_subgroup of add_group G to G.

@[simp]
theorem subgroup.coe_subtype {G : Type u_1} [group G] (H : subgroup G) :

@[simp]
theorem add_subgroup.coe_subtype {G : Type u_1} [add_group G] (H : add_subgroup G) :

@[simp]
theorem subgroup.coe_pow {G : Type u_1} [group G] (H : subgroup G) (x : H) (n : ) :
(x ^ n) = x ^ n

@[simp]
theorem subgroup.coe_gpow {G : Type u_1} [group G] (H : subgroup G) (x : H) (n : ) :
(x ^ n) = x ^ n

@[instance]
def add_subgroup.has_le {G : Type u_1} [add_group G] :

@[instance]
def subgroup.has_le {G : Type u_1} [group G] :

Equations
theorem subgroup.le_def {G : Type u_1} [group G] {H K : subgroup G} :
H K ∀ ⦃x : G⦄, x Hx K

theorem add_subgroup.le_def {G : Type u_1} [add_group G] {H K : add_subgroup G} :
H K ∀ ⦃x : G⦄, x Hx K

@[simp]
theorem add_subgroup.coe_subset_coe {G : Type u_1} [add_group G] {H K : add_subgroup G} :
H K H K

@[simp]
theorem subgroup.coe_subset_coe {G : Type u_1} [group G] {H K : subgroup G} :
H K H K

@[instance]

@[instance]
def subgroup.partial_order {G : Type u_1} [group G] :

Equations
@[instance]
def add_subgroup.has_top {G : Type u_1} [add_group G] :

The add_subgroup G of the add_group G.

@[instance]
def subgroup.has_top {G : Type u_1} [group G] :

The subgroup G of the group G.

Equations
@[instance]
def add_subgroup.has_bot {G : Type u_1} [add_group G] :

The trivial add_subgroup {0} of an add_group G.

@[instance]
def subgroup.has_bot {G : Type u_1} [group G] :

The trivial subgroup {1} of an group G.

Equations
@[instance]
def add_subgroup.inhabited {G : Type u_1} [add_group G] :

@[instance]
def subgroup.inhabited {G : Type u_1} [group G] :

Equations
@[simp]
theorem subgroup.mem_bot {G : Type u_1} [group G] {x : G} :
x x = 1

@[simp]
theorem add_subgroup.mem_bot {G : Type u_1} [add_group G] {x : G} :
x x = 0

@[simp]
theorem add_subgroup.mem_top {G : Type u_1} [add_group G] (x : G) :

@[simp]
theorem subgroup.mem_top {G : Type u_1} [group G] (x : G) :

@[simp]
theorem subgroup.coe_top {G : Type u_1} [group G] :

@[simp]
theorem add_subgroup.coe_top {G : Type u_1} [add_group G] :

@[simp]
theorem add_subgroup.coe_bot {G : Type u_1} [add_group G] :
= {0}

@[simp]
theorem subgroup.coe_bot {G : Type u_1} [group G] :
= {1}

theorem subgroup.eq_bot_iff_forall {G : Type u_1} [group G] (H : subgroup G) :
H = ∀ (x : G), x Hx = 1

theorem add_subgroup.eq_bot_iff_forall {G : Type u_1} [add_group G] (H : add_subgroup G) :
H = ∀ (x : G), x Hx = 0

theorem add_subgroup.nontrivial_iff_exists_ne_zero {G : Type u_1} [add_group G] (H : add_subgroup G) :
nontrivial H ∃ (x : G) (H : x H), x 0

theorem subgroup.nontrivial_iff_exists_ne_one {G : Type u_1} [group G] (H : subgroup G) :
nontrivial H ∃ (x : G) (H : x H), x 1

theorem subgroup.bot_or_nontrivial {G : Type u_1} [group G] (H : subgroup G) :

A subgroup is either the trivial subgroup or nontrivial.

theorem subgroup.bot_or_exists_ne_one {G : Type u_1} [group G] (H : subgroup G) :
H = ∃ (x : G) (H : x H), x 1

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

theorem add_subgroup.bot_or_exists_ne_zero {G : Type u_1} [add_group G] (H : add_subgroup G) :
H = ∃ (x : G) (H : x H), x 0

@[instance]
def subgroup.has_inf {G : Type u_1} [group G] :

The inf of two subgroups is their intersection.

Equations
@[instance]
def add_subgroup.has_inf {G : Type u_1} [add_group G] :

The inf of two add_subgroupss is their intersection.

@[simp]
theorem subgroup.coe_inf {G : Type u_1} [group G] (p p' : subgroup G) :
(p p') = p p'

@[simp]
theorem add_subgroup.coe_inf {G : Type u_1} [add_group G] (p p' : add_subgroup G) :
(p p') = p p'

@[simp]
theorem add_subgroup.mem_inf {G : Type u_1} [add_group G] {p p' : add_subgroup G} {x : G} :
x p p' x p x p'

@[simp]
theorem subgroup.mem_inf {G : Type u_1} [group G] {p p' : subgroup G} {x : G} :
x p p' x p x p'

@[instance]
def add_subgroup.has_Inf {G : Type u_1} [add_group G] :

@[instance]
def subgroup.has_Inf {G : Type u_1} [group G] :

Equations
@[simp]
theorem subgroup.coe_Inf {G : Type u_1} [group G] (H : set (subgroup G)) :
(Inf H) = ⋂ (s : subgroup G) (H : s H), s

@[simp]
theorem add_subgroup.coe_Inf {G : Type u_1} [add_group G] (H : set (add_subgroup G)) :
(Inf H) = ⋂ (s : add_subgroup G) (H : s H), s

@[simp]
theorem add_subgroup.mem_Inf {G : Type u_1} [add_group G] {S : set (add_subgroup G)} {x : G} :
x Inf S ∀ (p : add_subgroup G), p Sx p

@[simp]
theorem subgroup.mem_Inf {G : Type u_1} [group G] {S : set (subgroup G)} {x : G} :
x Inf S ∀ (p : subgroup G), p Sx p

theorem subgroup.mem_infi {G : Type u_1} [group G] {ι : Sort u_2} {S : ι → subgroup G} {x : G} :
(x ⨅ (i : ι), S i) ∀ (i : ι), x S i

theorem add_subgroup.mem_infi {G : Type u_1} [add_group G] {ι : Sort u_2} {S : ι → add_subgroup G} {x : G} :
(x ⨅ (i : ι), S i) ∀ (i : ι), x S i

@[simp]
theorem subgroup.coe_infi {G : Type u_1} [group G] {ι : Sort u_2} {S : ι → subgroup G} :
(⨅ (i : ι), S i) = ⋂ (i : ι), (S i)

@[simp]
theorem add_subgroup.coe_infi {G : Type u_1} [add_group G] {ι : Sort u_2} {S : ι → add_subgroup G} :
(⨅ (i : ι), S i) = ⋂ (i : ι), (S i)

@[instance]

Subgroups of a group form a complete lattice.

Equations
@[instance]

The add_subgroups of an add_group form a complete lattice.

theorem subgroup.mem_sup_left {G : Type u_1} [group G] {S T : subgroup G} {x : G} :
x Sx S T

theorem add_subgroup.mem_sup_left {G : Type u_1} [add_group G] {S T : add_subgroup G} {x : G} :
x Sx S T

theorem subgroup.mem_sup_right {G : Type u_1} [group G] {S T : subgroup G} {x : G} :
x Tx S T

theorem add_subgroup.mem_sup_right {G : Type u_1} [add_group G] {S T : add_subgroup G} {x : G} :
x Tx S T

theorem subgroup.mem_supr_of_mem {G : Type u_1} [group G] {ι : Type u_2} {S : ι → subgroup G} (i : ι) {x : G} :
x S ix supr S

theorem add_subgroup.mem_supr_of_mem {G : Type u_1} [add_group G] {ι : Type u_2} {S : ι → add_subgroup G} (i : ι) {x : G} :
x S ix supr S

theorem subgroup.mem_Sup_of_mem {G : Type u_1} [group G] {S : set (subgroup G)} {s : subgroup G} (hs : s S) {x : G} :
x sx Sup S

theorem add_subgroup.mem_Sup_of_mem {G : Type u_1} [add_group G] {S : set (add_subgroup G)} {s : add_subgroup G} (hs : s S) {x : G} :
x sx Sup S

def add_subgroup.closure {G : Type u_1} [add_group G] :

The add_subgroup generated by a set

def subgroup.closure {G : Type u_1} [group G] :
set Gsubgroup G

The subgroup generated by a set.

Equations
theorem subgroup.mem_closure {G : Type u_1} [group G] {k : set G} {x : G} :
x subgroup.closure k ∀ (K : subgroup G), k Kx K

theorem add_subgroup.mem_closure {G : Type u_1} [add_group G] {k : set G} {x : G} :
x add_subgroup.closure k ∀ (K : add_subgroup G), k Kx K

@[simp]
theorem subgroup.subset_closure {G : Type u_1} [group G] {k : set G} :

The subgroup generated by a set includes the set.

@[simp]
theorem add_subgroup.subset_closure {G : Type u_1} [add_group G] {k : set G} :

The add_subgroup generated by a set includes the set.

@[simp]
theorem subgroup.closure_le {G : Type u_1} [group G] (K : subgroup G) {k : set G} :

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

@[simp]
theorem add_subgroup.closure_le {G : Type u_1} [add_group G] (K : add_subgroup G) {k : set G} :

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

theorem subgroup.closure_eq_of_le {G : Type u_1} [group G] (K : subgroup G) {k : set G} :

theorem add_subgroup.closure_eq_of_le {G : Type u_1} [add_group G] (K : add_subgroup G) {k : set G} :

theorem subgroup.closure_induction {G : Type u_1} [group G] {k : set G} {p : G → Prop} {x : G} :
x subgroup.closure k(∀ (x : G), x kp x)p 1(∀ (x y : G), p xp yp (x * y))(∀ (x : G), p xp x⁻¹)p x

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

theorem add_subgroup.closure_induction {G : Type u_1} [add_group G] {k : set G} {p : G → Prop} {x : G} :
x add_subgroup.closure k(∀ (x : G), x kp x)p 0(∀ (x y : G), p xp yp (x + y))(∀ (x : G), p xp (-x))p x

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

closure forms a Galois insertion with the coercion to set.

closure forms a Galois insertion with the coercion to set.

Equations
theorem subgroup.closure_mono {G : Type u_1} [group G] ⦃h k : set G⦄ :

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

theorem add_subgroup.closure_mono {G : Type u_1} [add_group G] ⦃h k : set G⦄ :

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

@[simp]
theorem subgroup.closure_eq {G : Type u_1} [group G] (K : subgroup G) :

Closure of a subgroup K equals K.

@[simp]
theorem add_subgroup.closure_eq {G : Type u_1} [add_group G] (K : add_subgroup G) :

Additive closure of an additive subgroup K equals K

@[simp]

@[simp]
theorem subgroup.closure_empty {G : Type u_1} [group G] :

@[simp]
theorem subgroup.closure_univ {G : Type u_1} [group G] :

theorem subgroup.closure_union {G : Type u_1} [group G] (s t : set G) :

theorem subgroup.closure_Union {G : Type u_1} [group G] {ι : Sort u_2} (s : ι → set G) :
subgroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), subgroup.closure (s i)

theorem add_subgroup.closure_Union {G : Type u_1} [add_group G] {ι : Sort u_2} (s : ι → set G) :
add_subgroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), add_subgroup.closure (s i)

theorem subgroup.mem_closure_singleton {G : Type u_1} [group G] {x y : G} :
y subgroup.closure {x} ∃ (n : ), x ^ n = y

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

theorem subgroup.closure_singleton_one {G : Type u_1} [group G] :

theorem add_subgroup.mem_supr_of_directed {G : Type u_1} [add_group G] {ι : Sort u_2} [hι : nonempty ι] {K : ι → add_subgroup G} (hK : directed has_le.le K) {x : G} :
x supr K ∃ (i : ι), x K i

theorem subgroup.mem_supr_of_directed {G : Type u_1} [group G] {ι : Sort u_2} [hι : nonempty ι] {K : ι → subgroup G} (hK : directed has_le.le K) {x : G} :
x supr K ∃ (i : ι), x K i

theorem subgroup.coe_supr_of_directed {G : Type u_1} [group G] {ι : Sort u_2} [nonempty ι] {S : ι → subgroup G} :
directed has_le.le S((⨆ (i : ι), S i) = ⋃ (i : ι), (S i))

theorem add_subgroup.coe_supr_of_directed {G : Type u_1} [add_group G] {ι : Sort u_2} [nonempty ι] {S : ι → add_subgroup G} :
directed has_le.le S((⨆ (i : ι), S i) = ⋃ (i : ι), (S i))

theorem add_subgroup.mem_Sup_of_directed_on {G : Type u_1} [add_group G] {K : set (add_subgroup G)} (Kne : K.nonempty) (hK : directed_on has_le.le K) {x : G} :
x Sup K ∃ (s : add_subgroup G) (H : s K), x s

theorem subgroup.mem_Sup_of_directed_on {G : Type u_1} [group G] {K : set (subgroup G)} (Kne : K.nonempty) (hK : directed_on has_le.le K) {x : G} :
x Sup K ∃ (s : subgroup G) (H : s K), x s

def subgroup.comap {G : Type u_1} [group G] {N : Type u_2} [group N] :
(G →* N)subgroup Nsubgroup G

The preimage of a subgroup along a monoid homomorphism is a subgroup.

Equations
def add_subgroup.comap {G : Type u_1} [add_group G] {N : Type u_2} [add_group N] :
(G →+ N)add_subgroup Nadd_subgroup G

The preimage of an add_subgroup along an add_monoid homomorphism is an add_subgroup.

@[simp]
theorem subgroup.coe_comap {G : Type u_1} [group G] {N : Type u_3} [group N] (K : subgroup N) (f : G →* N) :

@[simp]
theorem add_subgroup.coe_comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (K : add_subgroup N) (f : G →+ N) :

@[simp]
theorem add_subgroup.mem_comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {K : add_subgroup N} {f : G →+ N} {x : G} :

@[simp]
theorem subgroup.mem_comap {G : Type u_1} [group G] {N : Type u_3} [group N] {K : subgroup N} {f : G →* N} {x : G} :

theorem add_subgroup.comap_comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {P : Type u_4} [add_group P] (K : add_subgroup P) (g : N →+ P) (f : G →+ N) :

theorem subgroup.comap_comap {G : Type u_1} [group G] {N : Type u_3} [group N] {P : Type u_4} [group P] (K : subgroup P) (g : N →* P) (f : G →* N) :

def add_subgroup.map {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] :
(G →+ N)add_subgroup Gadd_subgroup N

The image of an add_subgroup along an add_monoid homomorphism is an add_subgroup.

def subgroup.map {G : Type u_1} [group G] {N : Type u_3} [group N] :
(G →* N)subgroup Gsubgroup N

The image of a subgroup along a monoid homomorphism is a subgroup.

Equations
@[simp]
theorem add_subgroup.coe_map {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (K : add_subgroup G) :

@[simp]
theorem subgroup.coe_map {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (K : subgroup G) :

@[simp]
theorem add_subgroup.mem_map {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f : G →+ N} {K : add_subgroup G} {y : N} :
y add_subgroup.map f K ∃ (x : G) (H : x K), f x = y

@[simp]
theorem subgroup.mem_map {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {K : subgroup G} {y : N} :
y subgroup.map f K ∃ (x : G) (H : x K), f x = y

theorem add_subgroup.map_map {G : Type u_1} [add_group G] (K : add_subgroup G) {N : Type u_3} [add_group N] {P : Type u_4} [add_group P] (g : N →+ P) (f : G →+ N) :

theorem subgroup.map_map {G : Type u_1} [group G] (K : subgroup G) {N : Type u_3} [group N] {P : Type u_4} [group P] (g : N →* P) (f : G →* N) :

theorem add_subgroup.map_le_iff_le_comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f : G →+ N} {K : add_subgroup G} {H : add_subgroup N} :

theorem subgroup.map_le_iff_le_comap {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {K : subgroup G} {H : subgroup N} :

theorem subgroup.gc_map_comap {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :

theorem add_subgroup.gc_map_comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :

theorem add_subgroup.map_sup {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H K : add_subgroup G) (f : G →+ N) :

theorem subgroup.map_sup {G : Type u_1} [group G] {N : Type u_3} [group N] (H K : subgroup G) (f : G →* N) :

theorem add_subgroup.map_supr {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {ι : Sort u_2} (f : G →+ N) (s : ι → add_subgroup G) :
add_subgroup.map f (supr s) = ⨆ (i : ι), add_subgroup.map f (s i)

theorem subgroup.map_supr {G : Type u_1} [group G] {N : Type u_3} [group N] {ι : Sort u_2} (f : G →* N) (s : ι → subgroup G) :
subgroup.map f (supr s) = ⨆ (i : ι), subgroup.map f (s i)

theorem add_subgroup.comap_inf {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H K : add_subgroup N) (f : G →+ N) :

theorem subgroup.comap_inf {G : Type u_1} [group G] {N : Type u_3} [group N] (H K : subgroup N) (f : G →* N) :

theorem subgroup.comap_infi {G : Type u_1} [group G] {N : Type u_3} [group N] {ι : Sort u_2} (f : G →* N) (s : ι → subgroup N) :
subgroup.comap f (infi s) = ⨅ (i : ι), subgroup.comap f (s i)

theorem add_subgroup.comap_infi {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {ι : Sort u_2} (f : G →+ N) (s : ι → add_subgroup N) :
add_subgroup.comap f (infi s) = ⨅ (i : ι), add_subgroup.comap f (s i)

@[simp]
theorem add_subgroup.map_bot {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :

@[simp]
theorem subgroup.map_bot {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :

@[simp]
theorem subgroup.comap_top {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :

@[simp]
theorem add_subgroup.comap_top {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :

def add_subgroup.prod {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] :

Given add_subgroups H, K of add_groups A, B respectively, H × K as an add_subgroup of A × B.

def subgroup.prod {G : Type u_1} [group G] {N : Type u_3} [group N] :
subgroup Gsubgroup Nsubgroup (G × N)

Given subgroups H, K of groups G, N respectively, H × K as a subgroup of G × N.

Equations
theorem subgroup.coe_prod {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup G) (K : subgroup N) :
(H.prod K) = H.prod K

theorem add_subgroup.coe_prod {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H : add_subgroup G) (K : add_subgroup N) :
(H.prod K) = H.prod K

theorem add_subgroup.mem_prod {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {H : add_subgroup G} {K : add_subgroup N} {p : G × N} :
p H.prod K p.fst H p.snd K

theorem subgroup.mem_prod {G : Type u_1} [group G] {N : Type u_3} [group N] {H : subgroup G} {K : subgroup N} {p : G × N} :
p H.prod K p.fst H p.snd K

theorem subgroup.prod_mono {G : Type u_1} [group G] {N : Type u_3} [group N] :

theorem subgroup.prod_mono_right {G : Type u_1} [group G] {N : Type u_3} [group N] (K : subgroup G) :
monotone (λ (t : subgroup N), K.prod t)

theorem add_subgroup.prod_mono_right {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (K : add_subgroup G) :
monotone (λ (t : add_subgroup N), K.prod t)

theorem add_subgroup.prod_mono_left {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H : add_subgroup N) :
monotone (λ (K : add_subgroup G), K.prod H)

theorem subgroup.prod_mono_left {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup N) :
monotone (λ (K : subgroup G), K.prod H)

theorem add_subgroup.prod_top {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (K : add_subgroup G) :

theorem subgroup.prod_top {G : Type u_1} [group G] {N : Type u_3} [group N] (K : subgroup G) :

theorem add_subgroup.top_prod {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H : add_subgroup N) :

theorem subgroup.top_prod {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup N) :

@[simp]
theorem subgroup.top_prod_top {G : Type u_1} [group G] {N : Type u_3} [group N] :

@[simp]
theorem add_subgroup.top_prod_top {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] :

theorem subgroup.bot_prod_bot {G : Type u_1} [group G] {N : Type u_3} [group N] :

theorem add_subgroup.bot_sum_bot {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] :

def subgroup.prod_equiv {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup G) (K : subgroup N) :

Product of subgroups is isomorphic to their product as groups.

Equations
def add_subgroup.prod_equiv {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H : add_subgroup G) (K : add_subgroup N) :

Product of additive subgroups is isomorphic to their product as additive groups

@[class]
structure subgroup.normal {G : Type u_1} [group G] :
subgroup G → Prop
  • conj_mem : ∀ (n : G), n H∀ (g : G), (g * n) * g⁻¹ H

A subgroup is normal if whenever n ∈ H, then g * n * g⁻¹ ∈ H for every g : G

Instances
@[class]
structure add_subgroup.normal {A : Type u_2} [add_group A] :
add_subgroup A → Prop
  • conj_mem : ∀ (n : A), n H∀ (g : A), g + n - g H

An add_subgroup is normal if whenever n ∈ H, then g + n - g ∈ H for every g : G

Instances
@[instance]
def subgroup.normal_of_comm {G : Type u_1} [comm_group G] (H : subgroup G) :

@[instance]
def add_subgroup.normal_of_comm {G : Type u_1} [add_comm_group G] (H : add_subgroup G) :

theorem add_subgroup.normal.mem_comm {G : Type u_1} [add_group G] {H : add_subgroup G} (nH : H.normal) {a b : G} :
a + b Hb + a H

theorem subgroup.normal.mem_comm {G : Type u_1} [group G] {H : subgroup G} (nH : H.normal) {a b : G} :
a * b Hb * a H

theorem subgroup.normal.mem_comm_iff {G : Type u_1} [group G] {H : subgroup G} (nH : H.normal) {a b : G} :
a * b H b * a H

theorem add_subgroup.normal.mem_comm_iff {G : Type u_1} [add_group G] {H : add_subgroup G} (nH : H.normal) {a b : G} :
a + b H b + a H

@[instance]
def add_subgroup.bot_normal {G : Type u_1} [add_group G] :

@[instance]
def subgroup.bot_normal {G : Type u_1} [group G] :

def add_subgroup.center (G : Type u_1) [add_group G] :

The center of a group G is the set of elements that commute with everything in G

def subgroup.center (G : Type u_1) [group G] :

The center of a group G is the set of elements that commute with everything in G

Equations
theorem subgroup.mem_center_iff {G : Type u_1} [group G] {z : G} :
z subgroup.center G ∀ (g : G), g * z = z * g

theorem add_subgroup.mem_center_iff {G : Type u_1} [add_group G] {z : G} :
z add_subgroup.center G ∀ (g : G), g + z = z + g

@[instance]

@[instance]
def subgroup.center_normal {G : Type u_1} [group G] :

def add_subgroup.normalizer {G : Type u_1} [add_group G] :

The normalizer of H is the smallest subgroup of G inside which H is normal.

def subgroup.normalizer {G : Type u_1} [group G] :

The normalizer of H is the smallest subgroup of G inside which H is normal.

Equations
def subgroup.set_normalizer {G : Type u_1} [group G] :
set Gsubgroup G

The set_normalizer of S is the subgroup of G whose elements satisfy g*S*g⁻¹=S

Equations
def add_subgroup.set_normalizer {G : Type u_1} [add_group G] :

The set_normalizer of S is the subgroup of G whose elements satisfy g+S-g=S.

theorem add_subgroup.mem_normalizer_iff {G : Type u_1} [add_group G] {H : add_subgroup G} {g : G} :
g H.normalizer ∀ (n : G), n H g + n + -g H

theorem subgroup.mem_normalizer_iff {G : Type u_1} [group G] {H : subgroup G} {g : G} :
g H.normalizer ∀ (n : G), n H (g * n) * g⁻¹ H

theorem add_subgroup.le_normalizer {G : Type u_1} [add_group G] {H : add_subgroup G} :

theorem subgroup.le_normalizer {G : Type u_1} [group G] {H : subgroup G} :

@[instance]

theorem subgroup.le_normalizer_of_normal {G : Type u_1} [group G] {H K : subgroup G} [hK : (subgroup.comap K.subtype H).normal] :
H KK H.normalizer

theorem add_subgroup.le_normalizer_of_normal {G : Type u_1} [add_group G] {H K : add_subgroup G} [hK : (add_subgroup.comap K.subtype H).normal] :
H KK H.normalizer

def group.conjugates {G : Type u_1} [group G] :
G → set G

Given an element a, conjugates a is the set of conjugates.

Equations
theorem group.mem_conjugates_self {G : Type u_1} [group G] {a : G} :

def group.conjugates_of_set {G : Type u_1} [group G] :
set Gset G

Given a set s, conjugates_of_set s is the set of all conjugates of the elements of s.

Equations
theorem group.mem_conjugates_of_set_iff {G : Type u_1} [group G] {s : set G} {x : G} :
x group.conjugates_of_set s ∃ (a : G) (H : a s), is_conj a x

theorem group.subset_conjugates_of_set {G : Type u_1} [group G] {s : set G} :

theorem group.conjugates_subset_normal {G : Type u_1} [group G] {N : subgroup G} [tn : N.normal] {a : G} :

theorem group.conjugates_of_set_subset {G : Type u_1} [group G] {s : set G} {N : subgroup G} [N.normal] :

theorem group.conj_mem_conjugates_of_set {G : Type u_1} [group G] {s : set G} {x c : G} :

The set of conjugates of s is closed under conjugation.

def subgroup.normal_closure {G : Type u_1} [group G] :
set Gsubgroup G

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.

Equations
theorem subgroup.subset_normal_closure {G : Type u_1} [group G] {s : set G} :

@[instance]

The normal closure of s is a normal subgroup.

theorem subgroup.normal_closure_le_normal {G : Type u_1} [group G] {s : set G} {N : subgroup G} [N.normal] :

The normal closure of s is the smallest normal subgroup containing s.

theorem subgroup.normal_closure_subset_iff {G : Type u_1} [group G] {s : set G} {N : subgroup G} [N.normal] :

theorem subgroup.normal_closure_eq_infi {G : Type u_1} [group G] {s : set G} :
subgroup.normal_closure s = ⨅ (N : subgroup G) [_inst_3 : N.normal] (hs : s N), N

theorem add_subgroup.gsmul_mem {A : Type u_2} [add_group A] (H : add_subgroup A) {x : A} (hx : x H) (n : ) :
n •ℤ x H

theorem add_subgroup.sub_mem {A : Type u_2} [add_group A] (H : add_subgroup A) {x y : A} :
x Hy Hx - y H

theorem add_subgroup.mem_closure_singleton {A : Type u_2} [add_group A] {x y : A} :
y add_subgroup.closure {x} ∃ (n : ), n •ℤ x = y

The add_subgroup generated by an element of an add_group equals the set of natural number multiples of the element.

@[simp]
theorem add_subgroup.coe_smul {A : Type u_2} [add_group A] (H : add_subgroup A) (x : H) (n : ) :

@[simp]
theorem add_subgroup.coe_gsmul {A : Type u_2} [add_group A] (H : add_subgroup A) (x : H) (n : ) :

def add_monoid_hom.range {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] :
(G →+ N)add_subgroup N

The range of an add_monoid_hom from an add_group is an add_subgroup.

def monoid_hom.range {G : Type u_1} [group G] {N : Type u_3} [group N] :
(G →* N)subgroup N

The range of a monoid homomorphism from a group is a subgroup.

Equations
@[simp]
theorem add_monoid_hom.coe_range {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :

@[simp]
theorem monoid_hom.coe_range {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :

@[simp]
theorem monoid_hom.mem_range {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {y : N} :
y f.range ∃ (x : G), f x = y

@[simp]
theorem add_monoid_hom.mem_range {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f : G →+ N} {y : N} :
y f.range ∃ (x : G), f x = y

theorem monoid_hom.range_eq_map {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :

theorem add_monoid_hom.range_eq_map {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :

def monoid_hom.to_range {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :

The canonical surjective group homomorphism G →* f(G) induced by a group homomorphism G →* N.

Equations
def add_monoid_hom.to_range {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :

The canonical surjective add_group homomorphism G →+ f(G) induced by a group homomorphism G →+ N.

theorem monoid_hom.map_range {G : Type u_1} [group G] {N : Type u_3} {P : Type u_4} [group N] [group P] (g : N →* P) (f : G →* N) :

theorem add_monoid_hom.map_range {G : Type u_1} [add_group G] {N : Type u_3} {P : Type u_4} [add_group N] [add_group P] (g : N →+ P) (f : G →+ N) :

theorem monoid_hom.range_top_iff_surjective {G : Type u_1} [group G] {N : Type u_2} [group N] {f : G →* N} :

theorem add_monoid_hom.range_top_iff_surjective {G : Type u_1} [add_group G] {N : Type u_2} [add_group N] {f : G →+ N} :

theorem monoid_hom.range_top_of_surjective {G : Type u_1} [group G] {N : Type u_2} [group N] (f : G →* N) :

The range of a surjective monoid homomorphism is the whole of the codomain.

theorem add_monoid_hom.range_top_of_surjective {G : Type u_1} [add_group G] {N : Type u_2} [add_group N] (f : G →+ N) :

The range of a surjective add_monoid homomorphism is the whole of the codomain.

def add_monoid_hom.cod_restrict {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (S : add_subgroup N) :
(∀ (x : G), f x S)G →+ S

Restriction of an add_group hom to an add_subgroup of the codomain.

def monoid_hom.cod_restrict {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (S : subgroup N) :
(∀ (x : G), f x S)G →* S

Restriction of a group hom to a subgroup of the codomain.

Equations
def monoid_hom.ker {G : Type u_1} [group G] {N : Type u_3} [group N] :
(G →* N)subgroup G

The multiplicative kernel of a monoid homomorphism is the subgroup of elements x : G such that f x = 1

Equations
def add_monoid_hom.ker {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] :
(G →+ N)add_subgroup G

The additive kernel of an add_monoid homomorphism is the add_subgroup of elements such that f x = 0

theorem monoid_hom.mem_ker {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) {x : G} :
x f.ker f x = 1

theorem add_monoid_hom.mem_ker {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) {x : G} :
x f.ker f x = 0

theorem add_monoid_hom.comap_ker {G : Type u_1} [add_group G] {N : Type u_3} {P : Type u_4} [add_group N] [add_group P] (g : N →+ P) (f : G →+ N) :

theorem monoid_hom.comap_ker {G : Type u_1} [group G] {N : Type u_3} {P : Type u_4} [group N] [group P] (g : N →* P) (f : G →* N) :

theorem add_monoid_hom.to_range_ker {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :

theorem monoid_hom.to_range_ker {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :

def monoid_hom.eq_locus {G : Type u_1} [group G] {N : Type u_3} [group N] :
(G →* N)(G →* N)subgroup G

The subgroup of elements x : G such that f x = g x

Equations
def add_monoid_hom.eq_locus {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] :
(G →+ N)(G →+ N)add_subgroup G

The additive subgroup of elements x : G such that f x = g x

theorem add_monoid_hom.eq_on_closure {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f g : G →+ N} {s : set G} :

theorem monoid_hom.eq_on_closure {G : Type u_1} [group G] {N : Type u_3} [group N] {f g : G →* N} {s : set G} :

If two monoid homomorphisms are equal on a set, then they are equal on its subgroup closure.

theorem add_monoid_hom.eq_of_eq_on_top {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f g : G →+ N} :

theorem monoid_hom.eq_of_eq_on_top {G : Type u_1} [group G] {N : Type u_3} [group N] {f g : G →* N} :

theorem add_monoid_hom.eq_of_eq_on_dense {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {s : set G} (hs : add_subgroup.closure s = ) {f g : G →+ N} :
set.eq_on f g sf = g

theorem monoid_hom.eq_of_eq_on_dense {G : Type u_1} [group G] {N : Type u_3} [group N] {s : set G} (hs : subgroup.closure s = ) {f g : G →* N} :
set.eq_on f g sf = g

theorem monoid_hom.gclosure_preimage_le {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (s : set N) :

theorem add_monoid_hom.gclosure_preimage_le {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (s : set N) :

theorem add_monoid_hom.map_closure {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (s : set G) :

The image under an add_monoid hom of the add_subgroup generated by a set equals the add_subgroup generated by the image of the set.

theorem monoid_hom.map_closure {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (s : set G) :

The image under a monoid homomorphism of the subgroup generated by a set equals the subgroup generated by the image of the set.

def add_monoid_hom.lift_of_surjective {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (hf : function.surjective f) (g : G₁ →+ G₃) :
f.ker g.kerG₂ →+ G₃

lift_of_surjective f hf g hg is the unique additive group homomorphism φ

  • such that φ.comp f = g (lift_of_surjective_comp),
  • where f : G₁ →+* G₂ is surjective (hf),
  • and g : G₂ →+* G₃ satisfies hg : f.ker ≤ g.ker.

See lift_of_surjective_eq for the uniqueness lemma.

   G₁.
   |  \
 f |   \ g
   |    \
   v     \⌟
   G₂----> G₃
      ∃!φ
def monoid_hom.lift_of_surjective {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [group G₁] [group G₂] [group G₃] (f : G₁ →* G₂) (hf : function.surjective f) (g : G₁ →* G₃) :
f.ker g.kerG₂ →* G₃

lift_of_surjective f hf g hg is the unique group homomorphism φ

  • such that φ.comp f = g (lift_of_surjective_comp),
  • where f : G₁ →+* G₂ is surjective (hf),
  • and g : G₂ →+* G₃ satisfies hg : f.ker ≤ g.ker.

See lift_of_surjective_eq for the uniqueness lemma.

   G₁.
   |  \
 f |   \ g
   |    \
   v     \⌟
   G₂----> G₃
      ∃!φ
Equations
@[simp]
theorem add_monoid_hom.lift_of_surjective_comp_apply {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (hf : function.surjective f) (g : G₁ →+ G₃) (hg : f.ker g.ker) (x : G₁) :
(f.lift_of_surjective hf g hg) (f x) = g x

@[simp]
theorem monoid_hom.lift_of_surjective_comp_apply {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [group G₁] [group G₂] [group G₃] (f : G₁ →* G₂) (hf : function.surjective f) (g : G₁ →* G₃) (hg : f.ker g.ker) (x : G₁) :
(f.lift_of_surjective hf g hg) (f x) = g x

@[simp]
theorem monoid_hom.lift_of_surjective_comp {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [group G₁] [group G₂] [group G₃] (f : G₁ →* G₂) (hf : function.surjective f) (g : G₁ →* G₃) (hg : f.ker g.ker) :
(f.lift_of_surjective hf g hg).comp f = g

@[simp]
theorem add_monoid_hom.lift_of_surjective_comp {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (hf : function.surjective f) (g : G₁ →+ G₃) (hg : f.ker g.ker) :
(f.lift_of_surjective hf g hg).comp f = g

theorem monoid_hom.eq_lift_of_surjective {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [group G₁] [group G₂] [group G₃] (f : G₁ →* G₂) (hf : function.surjective f) (g : G₁ →* G₃) (hg : f.ker g.ker) (h : G₂ →* G₃) :
h.comp f = gh = f.lift_of_surjective hf g hg

theorem add_monoid_hom.eq_lift_of_surjective {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (hf : function.surjective f) (g : G₁ →+ G₃) (hg : f.ker g.ker) (h : G₂ →+ G₃) :
h.comp f = gh = f.lift_of_surjective hf g hg

theorem subgroup.normal.comap {G : Type u_1} [group G] {N : Type u_3} [group N] {H : subgroup N} (hH : H.normal) (f : G →* N) :

theorem add_subgroup.normal.comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {H : add_subgroup N} (hH : H.normal) (f : G →+ N) :

@[instance]
def subgroup.normal_comap {G : Type u_1} [group G] {N : Type u_3} [group N] {H : subgroup N} [nH : H.normal] (f : G →* N) :

@[instance]
def add_subgroup.normal_comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {H : add_subgroup N} [nH : H.normal] (f : G →+ N) :

@[instance]
def monoid_hom.normal_ker {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :

@[instance]
def add_monoid_hom.normal_ker {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :

def subgroup.gpowers {G : Type u_1} [group G] :
G → subgroup G

The subgroup generated by an element.

Equations
@[simp]
theorem subgroup.mem_gpowers {G : Type u_1} [group G] (g : G) :

theorem subgroup.gpowers_eq_closure {G : Type u_1} [group G] (g : G) :

@[simp]
theorem subgroup.range_gpowers_hom {G : Type u_1} [group G] (g : G) :

theorem subgroup.gpowers_subset {G : Type u_1} [group G] {a : G} {K : subgroup G} :

def add_subgroup.gmultiples {A : Type u_2} [add_group A] :
A → add_subgroup A

The subgroup generated by an element.

Equations
@[simp]
theorem add_subgroup.mem_gmultiples {A : Type u_2} [add_group A] (a : A) :

@[simp]

theorem add_subgroup.gmultiples_subset {A : Type u_2} [add_group A] {a : A} {B : add_subgroup A} :

def mul_equiv.subgroup_congr {G : Type u_1} [group G] {H K : subgroup G} :
H = KH ≃* K

Makes the identity isomorphism from a proof two subgroups of a multiplicative group are equal.

Equations
def add_equiv.add_subgroup_congr {G : Type u_1} [add_group G] {H K : add_subgroup G} :
H = KH ≃+ K

Makes the identity additive isomorphism from a proof two subgroups of an additive group are equal.