mathlib documentation

deprecated.subgroup

Unbundled subgroups #

This file defines unbundled multiplicative and additive subgroups is_subgroup and is_add_subgroup. These are not the preferred way to talk about subgroups and should not be used for any new projects. The preferred way in mathlib are the bundled versions subgroup G and add_subgroup G.

Main definitions #

is_add_subgroup (S : set G) : the predicate that S is the underlying subset of an additive subgroup of G. The bundled variant add_subgroup G should be used in preference to this.

is_subgroup (S : set G) : the predicate that S is the underlying subset of a subgroup of G. The bundled variant subgroup G should be used in preference to this.

Tags #

subgroup, subgroups, is_subgroup

structure is_add_subgroup {A : Type u_3} [add_group A] (s : set A) :
Prop

s is an additive subgroup: a set containing 0 and closed under addition and negation.

structure is_subgroup {G : Type u_1} [group G] (s : set G) :
Prop

s is a subgroup: a set containing 1 and closed under multiplication and inverse.

theorem is_subgroup.div_mem {G : Type u_1} [group G] {s : set G} (hs : is_subgroup s) {x y : G} (hx : x s) (hy : y s) :
x / y s
theorem is_add_subgroup.sub_mem {G : Type u_1} [add_group G] {s : set G} (hs : is_add_subgroup s) {x y : G} (hx : x s) (hy : y s) :
x - y s
theorem additive.is_add_subgroup {G : Type u_1} [group G] {s : set G} (hs : is_subgroup s) :
theorem additive.is_add_subgroup_iff {G : Type u_1} [group G] {s : set G} :
theorem multiplicative.is_subgroup {A : Type u_3} [add_group A] {s : set A} (hs : is_add_subgroup s) :
theorem is_subgroup.of_div {G : Type u_1} [group G] (s : set G) (one_mem : 1 s) (div_mem : ∀ {a b : G}, a sb sa * b⁻¹ s) :
theorem is_add_subgroup.of_add_neg {G : Type u_1} [add_group G] (s : set G) (one_mem : 0 s) (div_mem : ∀ {a b : G}, a sb sa + -b s) :
theorem is_add_subgroup.of_sub {A : Type u_3} [add_group A] (s : set A) (zero_mem : 0 s) (sub_mem : ∀ {a b : A}, a sb sa - b s) :
theorem is_add_subgroup.inter {G : Type u_1} [add_group G] {s₁ s₂ : set G} (hs₁ : is_add_subgroup s₁) (hs₂ : is_add_subgroup s₂) :
is_add_subgroup (s₁ s₂)
theorem is_subgroup.inter {G : Type u_1} [group G] {s₁ s₂ : set G} (hs₁ : is_subgroup s₁) (hs₂ : is_subgroup s₂) :
is_subgroup (s₁ s₂)
theorem is_subgroup.Inter {G : Type u_1} [group G] {ι : Sort u_2} {s : ι → set G} (hs : ∀ (y : ι), is_subgroup (s y)) :
theorem is_add_subgroup.Inter {G : Type u_1} [add_group G] {ι : Sort u_2} {s : ι → set G} (hs : ∀ (y : ι), is_add_subgroup (s y)) :
theorem is_add_subgroup_Union_of_directed {G : Type u_1} [add_group G] {ι : Type u_2} [hι : nonempty ι] {s : ι → set G} (hs : ∀ (i : ι), is_add_subgroup (s i)) (directed : ∀ (i j : ι), ∃ (k : ι), s i s k s j s k) :
is_add_subgroup (⋃ (i : ι), s i)
theorem is_subgroup_Union_of_directed {G : Type u_1} [group G] {ι : Type u_2} [hι : nonempty ι] {s : ι → set G} (hs : ∀ (i : ι), is_subgroup (s i)) (directed : ∀ (i j : ι), ∃ (k : ι), s i s k s j s k) :
is_subgroup (⋃ (i : ι), s i)
theorem is_add_subgroup.neg_mem_iff {G : Type u_1} {a : G} [add_group G] {s : set G} (hs : is_add_subgroup s) :
-a s a s
theorem is_subgroup.inv_mem_iff {G : Type u_1} {a : G} [group G] {s : set G} (hs : is_subgroup s) :
a⁻¹ s a s
theorem is_subgroup.mul_mem_cancel_right {G : Type u_1} {a b : G} [group G] {s : set G} (hs : is_subgroup s) (h : a s) :
b * a s b s
theorem is_add_subgroup.add_mem_cancel_right {G : Type u_1} {a b : G} [add_group G] {s : set G} (hs : is_add_subgroup s) (h : a s) :
b + a s b s
theorem is_add_subgroup.add_mem_cancel_left {G : Type u_1} {a b : G} [add_group G] {s : set G} (hs : is_add_subgroup s) (h : a s) :
a + b s b s
theorem is_subgroup.mul_mem_cancel_left {G : Type u_1} {a b : G} [group G] {s : set G} (hs : is_subgroup s) (h : a s) :
a * b s b s
structure is_normal_add_subgroup {A : Type u_3} [add_group A] (s : set A) :
Prop

is_normal_add_subgroup (s : set A) expresses the fact that s is a normal additive subgroup of the additive group A. Important: the preferred way to say this in Lean is via bundled subgroups S : add_subgroup A and hs : S.normal, and not via this structure.

structure is_normal_subgroup {G : Type u_1} [group G] (s : set G) :
Prop

is_normal_subgroup (s : set G) expresses the fact that s is a normal subgroup of the group G. Important: the preferred way to say this in Lean is via bundled subgroups S : subgroup G and not via this structure.

theorem is_normal_subgroup_of_comm_group {G : Type u_1} [comm_group G] {s : set G} (hs : is_subgroup s) :
theorem is_subgroup.mem_norm_comm {G : Type u_1} [group G] {s : set G} (hs : is_normal_subgroup s) {a b : G} (hab : a * b s) :
b * a s
theorem is_add_subgroup.mem_norm_comm {G : Type u_1} [add_group G] {s : set G} (hs : is_normal_add_subgroup s) {a b : G} (hab : a + b s) :
b + a s
theorem is_add_subgroup.mem_norm_comm_iff {G : Type u_1} [add_group G] {s : set G} (hs : is_normal_add_subgroup s) {a b : G} :
a + b s b + a s
theorem is_subgroup.mem_norm_comm_iff {G : Type u_1} [group G] {s : set G} (hs : is_normal_subgroup s) {a b : G} :
a * b s b * a s
def is_add_subgroup.trivial (G : Type u_1) [add_group G] :
set G

the trivial additive subgroup

def is_subgroup.trivial (G : Type u_1) [group G] :
set G

The trivial subgroup

Equations
@[simp]
theorem is_add_subgroup.mem_trivial {G : Type u_1} [add_group G] {g : G} :
@[simp]
theorem is_subgroup.mem_trivial {G : Type u_1} [group G] {g : G} :
theorem is_add_subgroup.eq_trivial_iff {G : Type u_1} [add_group G] {s : set G} (hs : is_add_subgroup s) :
s = is_add_subgroup.trivial G ∀ (x : G), x sx = 0
theorem is_subgroup.eq_trivial_iff {G : Type u_1} [group G] {s : set G} (hs : is_subgroup s) :
s = is_subgroup.trivial G ∀ (x : G), x sx = 1
def is_add_subgroup.add_center (G : Type u_1) [add_group G] :
set G

The underlying set of the center of an additive group.

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

The underlying set of the center of a group.

Equations
theorem is_add_subgroup.mem_add_center {G : Type u_1} [add_group G] {a : G} :
a is_add_subgroup.add_center G ∀ (g : G), g + a = a + g
theorem is_subgroup.mem_center {G : Type u_1} [group G] {a : G} :
a is_subgroup.center G ∀ (g : G), g * a = a * g
def is_add_subgroup.add_normalizer {G : Type u_1} [add_group G] (s : set G) :
set G

The underlying set of the normalizer of a subset S : set A of an additive group A. That is, the elements a : A such that a + S - a = S.

def is_subgroup.normalizer {G : Type u_1} [group G] (s : set G) :
set G

The underlying set of the normalizer of a subset S : set G of a group G. That is, the elements g : G such that g * S * g⁻¹ = S.

Equations
theorem is_subgroup.subset_normalizer {G : Type u_1} [group G] {s : set G} (hs : is_subgroup s) :
def is_group_hom.ker {G : Type u_1} {H : Type u_2} [group H] (f : G → H) :
set G

ker f : set G is the underlying subset of the kernel of a map G → H.

Equations
def is_add_group_hom.ker {G : Type u_1} {H : Type u_2} [add_group H] (f : G → H) :
set G

ker f : set A is the underlying subset of the kernel of a map A → B

theorem is_group_hom.mem_ker {G : Type u_1} {H : Type u_2} [group H] (f : G → H) {x : G} :
theorem is_add_group_hom.mem_ker {G : Type u_1} {H : Type u_2} [add_group H] (f : G → H) {x : G} :
theorem is_add_group_hom.zero_ker_neg {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) {a b : G} (h : f (a + -b) = 0) :
f a = f b
theorem is_group_hom.one_ker_inv {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {a b : G} (h : f (a * b⁻¹) = 1) :
f a = f b
theorem is_add_group_hom.zero_ker_neg' {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) {a b : G} (h : f (-a + b) = 0) :
f a = f b
theorem is_group_hom.one_ker_inv' {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {a b : G} (h : f (a⁻¹ * b) = 1) :
f a = f b
theorem is_add_group_hom.neg_ker_zero {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) {a b : G} (h : f a = f b) :
f (a + -b) = 0
theorem is_group_hom.inv_ker_one {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {a b : G} (h : f a = f b) :
f (a * b⁻¹) = 1
theorem is_add_group_hom.neg_ker_zero' {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) {a b : G} (h : f a = f b) :
f (-a + b) = 0
theorem is_group_hom.inv_ker_one' {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {a b : G} (h : f a = f b) :
f (a⁻¹ * b) = 1
theorem is_add_group_hom.zero_iff_ker_neg {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) (a b : G) :
f a = f b f (a + -b) = 0
theorem is_group_hom.one_iff_ker_inv {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (a b : G) :
f a = f b f (a * b⁻¹) = 1
theorem is_group_hom.one_iff_ker_inv' {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (a b : G) :
f a = f b f (a⁻¹ * b) = 1
theorem is_add_group_hom.zero_iff_ker_neg' {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) (a b : G) :
f a = f b f (-a + b) = 0
theorem is_add_group_hom.neg_iff_ker {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) (a b : G) :
theorem is_group_hom.inv_iff_ker {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (a b : G) :
theorem is_add_group_hom.neg_iff_ker' {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) (a b : G) :
theorem is_group_hom.inv_iff_ker' {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (a b : G) :
theorem is_add_group_hom.image_add_subgroup {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) {s : set G} (hs : is_add_subgroup s) :
theorem is_group_hom.image_subgroup {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {s : set G} (hs : is_subgroup s) :
theorem is_add_group_hom.range_add_subgroup {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) :
theorem is_group_hom.range_subgroup {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) :
theorem is_group_hom.preimage {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {s : set H} (hs : is_subgroup s) :
theorem is_add_group_hom.preimage {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) {s : set H} (hs : is_add_subgroup s) :
theorem is_add_group_hom.preimage_normal {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) {s : set H} (hs : is_normal_add_subgroup s) :
theorem is_group_hom.preimage_normal {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {s : set H} (hs : is_normal_subgroup s) :
theorem is_add_group_hom.is_normal_add_subgroup_ker {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) :
theorem is_group_hom.is_normal_subgroup_ker {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) :
theorem is_group_hom.injective_of_trivial_ker {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (h : is_group_hom.ker f = is_subgroup.trivial G) :
theorem is_group_hom.trivial_ker_of_injective {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (h : function.injective f) :
theorem is_group_hom.injective_iff_trivial_ker {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) :
theorem is_add_group_hom.trivial_ker_iff_eq_zero {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) :
is_add_group_hom.ker f = is_add_subgroup.trivial G ∀ (x : G), f x = 0x = 0
theorem is_group_hom.trivial_ker_iff_eq_one {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) :
is_group_hom.ker f = is_subgroup.trivial G ∀ (x : G), f x = 1x = 1
inductive add_group.in_closure {A : Type u_3} [add_group A] (s : set A) :
A → Prop

If A is an additive group and s : set A, then in_closure s : set A is the underlying subset of the subgroup generated by s.

inductive group.in_closure {G : Type u_1} [group G] (s : set G) :
G → Prop

If G is a group and s : set G, then in_closure s : set G is the underlying subset of the subgroup generated by s.

def add_group.closure {G : Type u_1} [add_group G] (s : set G) :
set G

add_group.closure s is the additive subgroup generated by s, i.e., the smallest additive subgroup containing s.

def group.closure {G : Type u_1} [group G] (s : set G) :
set G

group.closure s is the subgroup generated by s, i.e. the smallest subgroup containg s.

Equations
theorem add_group.mem_closure {G : Type u_1} [add_group G] {s : set G} {a : G} :
theorem group.mem_closure {G : Type u_1} [group G] {s : set G} {a : G} :
a sa group.closure s
theorem group.closure.is_subgroup {G : Type u_1} [group G] (s : set G) :
theorem group.subset_closure {G : Type u_1} [group G] {s : set G} :
theorem add_group.subset_closure {G : Type u_1} [add_group G] {s : set G} :
theorem add_group.closure_subset {G : Type u_1} [add_group G] {s t : set G} (ht : is_add_subgroup t) (h : s t) :
theorem group.closure_subset {G : Type u_1} [group G] {s t : set G} (ht : is_subgroup t) (h : s t) :
theorem add_group.closure_subset_iff {G : Type u_1} [add_group G] {s t : set G} (ht : is_add_subgroup t) :
theorem group.closure_subset_iff {G : Type u_1} [group G] {s t : set G} (ht : is_subgroup t) :
theorem add_group.closure_mono {G : Type u_1} [add_group G] {s t : set G} (h : s t) :
theorem group.closure_mono {G : Type u_1} [group G] {s t : set G} (h : s t) :
@[simp]
theorem add_group.closure_add_subgroup {G : Type u_1} [add_group G] {s : set G} (hs : is_add_subgroup s) :
@[simp]
theorem group.closure_subgroup {G : Type u_1} [group G] {s : set G} (hs : is_subgroup s) :
theorem group.exists_list_of_mem_closure {G : Type u_1} [group G] {s : set G} {a : G} (h : a group.closure s) :
∃ (l : list G), (∀ (x : G), x lx s x⁻¹ s) l.prod = a
theorem add_group.exists_list_of_mem_closure {G : Type u_1} [add_group G] {s : set G} {a : G} (h : a add_group.closure s) :
∃ (l : list G), (∀ (x : G), x lx s -x s) l.sum = a
theorem add_group.image_closure {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) (s : set G) :
theorem group.image_closure {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (s : set G) :
theorem group.mclosure_subset {G : Type u_1} [group G] {s : set G} :
theorem add_group.mem_closure_union_iff {G : Type u_1} [add_comm_group G] {s t : set G} {x : G} :
x add_group.closure (s t) ∃ (y : G) (H : y add_group.closure s) (z : G) (H : z add_group.closure t), y + z = x
theorem group.mem_closure_union_iff {G : Type u_1} [comm_group G] {s t : set G} {x : G} :
x group.closure (s t) ∃ (y : G) (H : y group.closure s) (z : G) (H : z group.closure t), y * z = x
theorem group.conjugates_of_subset {G : Type u_1} [group G] {t : set G} (ht : is_normal_subgroup t) {a : G} (h : a t) :
theorem group.conjugates_of_set_subset' {G : Type u_1} [group G] {s t : set G} (ht : is_normal_subgroup t) (h : s t) :
def group.normal_closure {G : Type u_1} [group G] (s : set G) :
set 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 group.subset_normal_closure {G : Type u_1} {s : set G} [group G] :
theorem group.normal_closure.is_subgroup {G : Type u_1} [group G] (s : set G) :

The normal closure of a set is a subgroup.

The normal closure of s is a normal subgroup.

theorem group.normal_closure_subset {G : Type u_1} [group G] {s t : set G} (ht : is_normal_subgroup t) (h : s t) :

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

theorem group.normal_closure_subset_iff {G : Type u_1} [group G] {s t : set G} (ht : is_normal_subgroup t) :
theorem group.normal_closure_mono {G : Type u_1} [group G] {s t : set G} :
def subgroup.of {G : Type u_1} [group G] {s : set G} (h : is_subgroup s) :

Create a bundled subgroup from a set s and [is_subgroup s].

Equations
def add_subgroup.of {G : Type u_1} [add_group G] {s : set G} (h : is_add_subgroup s) :

Create a bundled additive subgroup from a set s and [is_add_subgroup s].

theorem subgroup.is_subgroup {G : Type u_1} [group G] (K : subgroup G) :
theorem subgroup.of_normal {G : Type u_1} [group G] (s : set G) (h : is_subgroup s) (n : is_normal_subgroup s) :
theorem add_subgroup.of_normal {G : Type u_1} [add_group G] (s : set G) (h : is_add_subgroup s) (n : is_normal_add_subgroup s) :