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
- to_is_add_submonoid : is_add_submonoid s
- neg_mem : ∀ {a : A}, a ∈ s → -a ∈ s
s is an additive subgroup: a set containing 0 and closed under addition and negation.
- to_is_submonoid : is_submonoid s
- inv_mem : ∀ {a : G}, a ∈ s → a⁻¹ ∈ s
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) :
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) :
theorem
multiplicative.is_subgroup
{A : Type u_3}
[add_group A]
{s : set A}
(hs : is_add_subgroup 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)) :
is_subgroup (set.Inter s)
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) :
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) :
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) :
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) :
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) :
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.
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_add_subgroup_of_add_comm_group
{G : Type u_1}
[add_comm_group G]
{s : set G}
(hs : is_add_subgroup s) :
theorem
is_normal_subgroup_of_comm_group
{G : Type u_1}
[comm_group G]
{s : set G}
(hs : is_subgroup s) :
theorem
additive.is_normal_add_subgroup
{G : Type u_1}
[group G]
{s : set G}
(hs : is_normal_subgroup s) :
theorem
multiplicative.is_normal_subgroup
{A : Type u_3}
[add_group A]
{s : set A}
(hs : is_normal_add_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) :
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) :
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} :
theorem
is_subgroup.mem_norm_comm_iff
{G : Type u_1}
[group G]
{s : set G}
(hs : is_normal_subgroup s)
{a b : G} :
the trivial additive subgroup
Equations
- is_add_subgroup.trivial G = {0}
The trivial subgroup
Equations
- is_subgroup.trivial G = {1}
@[simp]
theorem
is_add_subgroup.mem_trivial
{G : Type u_1}
[add_group G]
{g : G} :
g ∈ is_add_subgroup.trivial G ↔ g = 0
@[simp]
theorem
is_subgroup.mem_trivial
{G : Type u_1}
[group G]
{g : G} :
g ∈ is_subgroup.trivial G ↔ g = 1
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 ∈ s → x = 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 ∈ s → x = 1
The underlying set of the center of an additive group.
Equations
- is_add_subgroup.add_center G = {z : G | ∀ (g : G), g + z = z + g}
The underlying set of the center of a group.
Equations
- is_subgroup.center G = {z : G | ∀ (g : G), g * z = z * 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.
theorem
is_add_subgroup.subset_add_normalizer
{G : Type u_1}
[add_group G]
{s : set G}
(hs : is_add_subgroup s) :
ker f : set G is the underlying subset of the kernel of a map G → H.
Equations
ker f : set A is the underlying subset of the kernel of a map A → B
Equations
theorem
is_group_hom.mem_ker
{G : Type u_1}
{H : Type u_2}
[group H]
(f : G → H)
{x : G} :
x ∈ is_group_hom.ker f ↔ f x = 1
theorem
is_add_group_hom.mem_ker
{G : Type u_1}
{H : Type u_2}
[add_group H]
(f : G → H)
{x : G} :
x ∈ is_add_group_hom.ker f ↔ f x = 0
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
is_add_subgroup (f '' 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) :
is_subgroup (f '' 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) :
is_subgroup (set.range 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) :
is_subgroup (f ⁻¹' 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) :
is_add_subgroup (f ⁻¹' 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) :
is_normal_add_subgroup (f ⁻¹' 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) :
is_normal_subgroup (f ⁻¹' 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_add_group_hom.injective_of_trivial_ker
{G : Type u_1}
{H : Type u_2}
[add_group G]
[add_group H]
{f : G → H}
(hf : is_add_group_hom f)
(h : is_add_group_hom.ker f = is_add_subgroup.trivial G) :
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_add_group_hom.trivial_ker_of_injective
{G : Type u_1}
{H : Type u_2}
[add_group G]
[add_group H]
{f : G → H}
(hf : is_add_group_hom f)
(h : function.injective f) :
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_add_group_hom.injective_iff_trivial_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.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 = 0 → x = 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 = 1 → x = 1
- basic : ∀ {A : Type u_3} [_inst_1 : add_group A] {s : set A} {a : A}, a ∈ s → add_group.in_closure s a
- zero : ∀ {A : Type u_3} [_inst_1 : add_group A] {s : set A}, add_group.in_closure s 0
- neg : ∀ {A : Type u_3} [_inst_1 : add_group A] {s : set A} {a : A}, add_group.in_closure s a → add_group.in_closure s (-a)
- add : ∀ {A : Type u_3} [_inst_1 : add_group A] {s : set A} {a b : A}, add_group.in_closure s a → add_group.in_closure s b → add_group.in_closure s (a + b)
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.
- basic : ∀ {G : Type u_1} [_inst_1 : group G] {s : set G} {a : G}, a ∈ s → group.in_closure s a
- one : ∀ {G : Type u_1} [_inst_1 : group G] {s : set G}, group.in_closure s 1
- inv : ∀ {G : Type u_1} [_inst_1 : group G] {s : set G} {a : G}, group.in_closure s a → group.in_closure s a⁻¹
- mul : ∀ {G : Type u_1} [_inst_1 : group G] {s : set G} {a b : G}, group.in_closure s a → group.in_closure s b → group.in_closure s (a * b)
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.
add_group.closure s is the additive subgroup generated by s, i.e., the
smallest additive subgroup containing s.
Equations
- add_group.closure s = {a : G | add_group.in_closure s a}
group.closure s is the subgroup generated by s, i.e. the smallest subgroup containg s.
Equations
- group.closure s = {a : G | group.in_closure s a}
theorem
add_group.mem_closure
{G : Type u_1}
[add_group G]
{s : set G}
{a : G} :
a ∈ s → a ∈ add_group.closure s
theorem
group.mem_closure
{G : Type u_1}
[group G]
{s : set G}
{a : G} :
a ∈ s → a ∈ group.closure s
theorem
add_group.closure_subset
{G : Type u_1}
[add_group G]
{s t : set G}
(ht : is_add_subgroup t)
(h : s ⊆ t) :
add_group.closure s ⊆ t
theorem
group.closure_subset
{G : Type u_1}
[group G]
{s t : set G}
(ht : is_subgroup t)
(h : s ⊆ t) :
group.closure s ⊆ t
theorem
add_group.closure_subset_iff
{G : Type u_1}
[add_group G]
{s t : set G}
(ht : is_add_subgroup t) :
add_group.closure s ⊆ t ↔ s ⊆ t
theorem
group.closure_subset_iff
{G : Type u_1}
[group G]
{s t : set G}
(ht : is_subgroup t) :
group.closure s ⊆ t ↔ s ⊆ t
@[simp]
theorem
add_group.closure_add_subgroup
{G : Type u_1}
[add_group G]
{s : set G}
(hs : is_add_subgroup s) :
add_group.closure s = s
@[simp]
theorem
group.closure_subgroup
{G : Type u_1}
[group G]
{s : set G}
(hs : is_subgroup s) :
group.closure s = s
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) :
f '' add_group.closure s = add_group.closure (f '' s)
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) :
f '' group.closure s = group.closure (f '' s)
theorem
add_group.closure_eq_mclosure
{G : Type u_1}
[add_group G]
{s : set G} :
add_group.closure s = add_monoid.closure (s ∪ has_neg.neg ⁻¹' s)
theorem
group.closure_eq_mclosure
{G : Type u_1}
[group G]
{s : set G} :
group.closure s = monoid.closure (s ∪ has_inv.inv ⁻¹' s)
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) :
conjugates_of 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) :
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
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) :
s ⊆ t ↔ group.normal_closure s ⊆ t
theorem
group.normal_closure_mono
{G : Type u_1}
[group G]
{s t : set G} :
s ⊆ t → group.normal_closure s ⊆ group.normal_closure t
Create a bundled subgroup from a set s and [is_subgroup s].
Create a bundled additive subgroup from a set s and [is_add_subgroup s].
theorem
subgroup.of_normal
{G : Type u_1}
[group G]
(s : set G)
(h : is_subgroup s)
(n : is_normal_subgroup s) :
(subgroup.of h).normal
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) :