Unbundled subgroups (deprecated) #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.
This file defines unbundled multiplicative and additive subgroups. Instead of using this file,
please use subgroup G and add_subgroup A, defined in group_theory.subgroup.basic.
Main definitions #
is_add_subgroup (S : set A) : the predicate that S is the underlying subset of an additive
subgroup of A. The bundled variant add_subgroup A 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
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.neg_mem_iff
{G : Type u_1}
{a : G}
[add_group G]
{s : set G}
(hs : is_add_subgroup 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) :
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) :
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.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) :