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:
G Nare groupsAis an add_groupH Kare subgroups ofGor add_subgroups ofAxis an element of typeGor typeAf g : N →* Gare group homomorphismss kare sets of elements of typeG
Definitions in the file:
subgroup G: the type of subgroups of a groupGadd_subgroup A: the type of subgroups of an additive groupAcomplete_lattice (subgroup G): the subgroups ofGform a complete latticeclosure k: the minimal subgroup that includes the setksubtype: the natural group homomorphism from a subgroup of groupGtoGgi:closureforms a Galois insertion with the coercion to setcomap H f: the preimage of a subgroupHalong the group homomorphismfis also a subgroupmap f H: the image of a subgroupHalong the group homomorphismfis also a subgroupprod H K: the product of subgroupsH,Kof groupsG,Nrespectively,H × Kis a subgroup ofG × Nmonoid_hom.range f: the range of the group homomorphismfis a subgroupmonoid_hom.ker f: the kernel of a group homomorphismfis the subgroup of elementsx : Gsuch thatf x = 1monoid_hom.eq_locus f g: given group homomorphismsf,g, the elements ofGsuch thatf x = g xform a subgroup ofG
Implementation notes
Subgroup inclusion is denoted ≤ rather than ⊆, although ∈ is defined as
membership of a subgroup's underlying set.
Tags
subgroup, subgroups
Reinterpret an add_subgroup as an add_submonoid.
Map from subgroups of group G to add_subgroups of additive G.
Equations
- H.to_add_subgroup = {carrier := H.to_submonoid.to_add_submonoid.carrier, zero_mem' := _, add_mem' := _, neg_mem' := _}
Map from add_subgroups of additive G to subgroups of G.
Equations
- subgroup.of_add_subgroup H = {carrier := (submonoid.of_add_submonoid H.to_add_submonoid).carrier, one_mem' := _, mul_mem' := _, inv_mem' := _}
Map from add_subgroups of add_group G to subgroups of multiplicative G.
Equations
- H.to_subgroup = {carrier := H.to_add_submonoid.to_submonoid.carrier, one_mem' := _, mul_mem' := _, inv_mem' := _}
Map from subgroups of multiplicative G to add_subgroups of add_group G.
Equations
- add_subgroup.of_subgroup H = {carrier := (add_submonoid.of_submonoid H.to_submonoid).carrier, zero_mem' := _, add_mem' := _, neg_mem' := _}
Subgroups of group G are isomorphic to additive subgroups of additive G.
Equations
- subgroup.add_subgroup_equiv G = {to_fun := subgroup.to_add_subgroup _inst_3, inv_fun := subgroup.of_add_subgroup _inst_3, left_inv := _, right_inv := _}
Equations
- subgroup.has_coe = {coe := subgroup.carrier _inst_1}
Equations
- subgroup.has_coe_to_sort = {S := has_coe_to_sort.S (subgroup G) coe_sort_trans, coe := λ (G_1 : subgroup G), ↥G_1}
Copy of an additive subgroup with a new carrier equal to the old one.
Useful to fix definitional equalities
Two add_groups are equal if the underlying subsets are equal.
Two add_subgroups are equal if and only if the underlying subsets are equal.
Two add_subgroups are equal if they have the same elements.
An add_subgroup contains the group's 0.
A subgroup contains the group's 1.
An add_subgroup is closed under addition.
An add_subgroup is closed under inverse.
Sum of a list of elements in an add_subgroup is in the add_subgroup.
Sum of a multiset of elements in an add_subgroup of an add_comm_group
is in the add_subgroup.
Product of a multiset of elements in a subgroup of a comm_group is in the subgroup.
Sum of elements in an add_subgroup of an add_comm_group indexed by a finset
is in the add_subgroup.
Product of elements of a subgroup of a comm_group indexed by a finset is in the
subgroup.
Construct a subgroup from a nonempty set that is closed under division.
An add_subgroup of an add_group inherits an addition.
A subgroup of a group inherits a multiplication.
Equations
- H.has_mul = H.to_submonoid.has_mul
An add_subgroup of an add_group inherits a zero.
A add_subgroup of a add_group inherits an inverse.
A subgroup of a group inherits a group structure.
Equations
- H.to_group = {mul := monoid.mul H.to_submonoid.to_monoid, mul_assoc := _, one := monoid.one H.to_submonoid.to_monoid, one_mul := _, mul_one := _, inv := has_inv.inv H.has_inv, mul_left_inv := _}
An add_subgroup of an add_group inherits an add_group structure.
A subgroup of a comm_group is a comm_group.
An add_subgroup of an add_comm_group is an add_comm_group.
The natural group hom from an add_subgroup of add_group G to G.
Equations
- subgroup.partial_order = {le := has_le.le subgroup.has_le, lt := partial_order.lt (partial_order.lift coe subgroup.partial_order._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
The add_subgroup G of the add_group G.
The trivial add_subgroup {0} of an add_group G.
Equations
- subgroup.inhabited = {default := ⊥}
The inf of two subgroups is their intersection.
Equations
- subgroup.has_inf = {inf := λ (H₁ H₂ : subgroup G), {carrier := (H₁.to_submonoid ⊓ H₂.to_submonoid).carrier, one_mem' := _, mul_mem' := _, inv_mem' := _}}
The inf of two add_subgroupss is their intersection.
Subgroups of a group form a complete lattice.
Equations
- subgroup.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf subgroup.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, top := ⊤, le_top := _, bot := ⊥, bot_le := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), Inf := complete_lattice.Inf (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
The add_subgroups of an add_group form a complete lattice.
The subgroup generated by a set.
Equations
- subgroup.closure k = has_Inf.Inf {K : subgroup G | k ⊆ ↑K}
The add_subgroup generated by a set
The add_subgroup generated by a set includes the set.
The subgroup generated by a set includes the set.
An additive subgroup K includes closure k if and only if it includes k
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.
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.
closure forms a Galois insertion with the coercion to set.
closure forms a Galois insertion with the coercion to set.
Equations
- subgroup.gi G = {choice := λ (s : set G) (_x : ↑(subgroup.closure s) ≤ s), subgroup.closure s, gc := _, le_l_u := _, choice_eq := _}
Additive subgroup closure of a set is monotone in its argument: if h ⊆ k,
then closure h ≤ closure k
Subgroup closure of a set is monotone in its argument: if h ⊆ k,
then closure h ≤ closure k.
Closure of a subgroup K equals K.
Additive closure of an additive subgroup K equals K
The subgroup generated by an element of a group equals the set of integer number powers of the element.
The preimage of an add_subgroup along an add_monoid homomorphism
is an add_subgroup.
The image of an add_subgroup along an add_monoid homomorphism
is an add_subgroup.
Given subgroups H, K of groups G, N respectively, H × K as a subgroup of G × N.
Given add_subgroups H, K of add_groups A, B respectively, H × K
as an add_subgroup of A × B.
Product of additive subgroups is isomorphic to their product as additive groups
Product of subgroups is isomorphic to their product as groups.
A subgroup is normal if whenever n ∈ H, then g * n * g⁻¹ ∈ H for every g : G
An add_subgroup is normal if whenever n ∈ H, then g + n - g ∈ H for every g : G
The center of a group G is the set of elements that commute with everything in G
The normalizer of H is the smallest subgroup of G inside which H is normal.
The set_normalizer of S is the subgroup of G whose elements satisfy g*S*g⁻¹=S
The set_normalizer of S is the subgroup of G whose elements satisfy g+S-g=S.
Given an element a, conjugates a is the set of conjugates.
Equations
- group.conjugates a = {b : G | is_conj a b}
Given a set s, conjugates_of_set s is the set of all conjugates of
the elements of s.
Equations
- group.conjugates_of_set s = ⋃ (a : G) (H : a ∈ s), group.conjugates a
The set of conjugates of s is closed under conjugation.
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 s is a normal subgroup.
The normal closure of s is the smallest normal subgroup containing s.
The add_subgroup generated by an element of an add_group equals the set of
natural number multiples of the element.
The range of an add_monoid_hom from an add_group is an add_subgroup.
The range of a surjective add_monoid homomorphism is the whole of the codomain.
The range of a surjective monoid homomorphism is the whole of the codomain.
The additive kernel of an add_monoid homomorphism is the add_subgroup of elements
such that f x = 0
The multiplicative kernel of a monoid homomorphism is the subgroup of elements x : G such that
f x = 1
Equations
- f.ker = subgroup.comap f ⊥
The additive subgroup of elements x : G such that f x = g x
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.
The image under a monoid homomorphism of the subgroup generated by a set equals the subgroup generated by the image of the set.
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₃satisfieshg : f.ker ≤ g.ker.
See lift_of_surjective_eq for the uniqueness lemma.
G₁.
| \
f | \ g
| \
v \⌟
G₂----> G₃
∃!φ
Equations
- f.lift_of_surjective hf g hg = {to_fun := λ (b : G₂), ⇑g (classical.some _), map_one' := _, map_mul' := _}
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₃satisfieshg : f.ker ≤ g.ker.
See lift_of_surjective_eq for the uniqueness lemma.
G₁.
| \
f | \ g
| \
v \⌟
G₂----> G₃
∃!φ
The subgroup generated by an element.
Equations
- subgroup.gpowers g = (⇑(gpowers_hom G) g).range.copy (set.range (has_pow.pow g)) _
The subgroup generated by an element.
Equations
- add_subgroup.gmultiples a = (⇑(gmultiples_hom A) a).range.copy (set.range (λ (_x : ℤ), _x •ℤ a)) _
Makes the identity isomorphism from a proof two subgroups of a multiplicative group are equal.
Equations
- mul_equiv.subgroup_congr h = {to_fun := (equiv.set_congr _).to_fun, inv_fun := (equiv.set_congr _).inv_fun, left_inv := _, right_inv := _, map_mul' := _}
Makes the identity additive isomorphism from a proof two subgroups of an additive group are equal.