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 N
aregroup
s -
A
is anadd_group
-
H K
aresubgroup
s ofG
oradd_subgroup
s ofA
-
x
is an element of typeG
or typeA
-
f g : N →* G
are group homomorphisms -
s k
are sets of elements of typeG
Definitions in the file:
-
subgroup G
: the type of subgroups of a groupG
-
add_subgroup A
: the type of subgroups of an additive groupA
-
complete_lattice (subgroup G)
: the subgroups ofG
form a complete lattice -
subgroup.closure k
: the minimal subgroup that includes the setk
-
subgroup.subtype
: the natural group homomorphism from a subgroup of groupG
toG
-
subgroup.gi
:closure
forms a Galois insertion with the coercion to set -
subgroup.comap H f
: the preimage of a subgroupH
along the group homomorphismf
is also a subgroup -
subgroup.map f H
: the image of a subgroupH
along the group homomorphismf
is also a subgroup -
subgroup.prod H K
: the product of subgroupsH
,K
of groupsG
,N
respectively,H × K
is a subgroup ofG × N
-
monoid_hom.range f
: the range of the group homomorphismf
is a subgroup -
monoid_hom.ker f
: the kernel of a group homomorphismf
is the subgroup of elementsx : G
such thatf x = 1
-
monoid_hom.eq_locus f g
: given group homomorphismsf
,g
, the elements ofG
such thatf x = g x
form a subgroup ofG
-
is_simple_group G
: a class indicating that a group has exactly two normal subgroups
Implementation notes #
Subgroup inclusion is denoted ≤
rather than ⊆
, although ∈
is defined as
membership of a subgroup's underlying set.
Tags #
subgroup, subgroups
inv_mem_class S G
states S
is a type of subsets s ⊆ G
closed under inverses.
Instances of this typeclass
Instances of other typeclasses for inv_mem_class
- inv_mem_class.has_sizeof_inst
neg_mem_class S G
states S
is a type of subsets s ⊆ G
closed under negation.
Instances of this typeclass
Instances of other typeclasses for neg_mem_class
- neg_mem_class.has_sizeof_inst
- to_submonoid_class : submonoid_class S G
- inv_mem : ∀ {s : S} {x : G}, x ∈ s → x⁻¹ ∈ s
subgroup_class S G
states S
is a type of subsets s ⊆ G
that are subgroups of G
.
Instances of this typeclass
Instances of other typeclasses for subgroup_class
- subgroup_class.has_sizeof_inst
- to_add_submonoid_class : add_submonoid_class S G
- neg_mem : ∀ {s : S} {x : G}, x ∈ s → -x ∈ s
add_subgroup_class S G
states S
is a type of subsets s ⊆ G
that are
additive subgroups of G
.
Instances of this typeclass
Instances of other typeclasses for add_subgroup_class
- add_subgroup_class.has_sizeof_inst
Equations
- add_subgroup_class.to_neg_mem_class M S = {neg_mem := _}
Equations
- subgroup_class.to_inv_mem_class M S = {inv_mem := _}
A subgroup is closed under division.
An additive subgroup is closed under subtraction.
An additive subgroup of a add_group
inherits an inverse.
A subgroup of a group inherits an inverse.
A subgroup of a group inherits a division
An additive subgroup of an add_group
inherits a subtraction.
An additive subgroup of an add_group
inherits an integer scaling.
A subgroup of a group inherits an integer power.
A subgroup of a group inherits a group structure.
Equations
- subgroup_class.to_group H = function.injective.group coe _ _ _ _ _ _ _
An additive subgroup of an add_group
inherits an add_group
structure.
Equations
- add_subgroup_class.to_add_group H = function.injective.add_group coe _ _ _ _ _ _ _
A subgroup of a comm_group
is a comm_group
.
Equations
- subgroup_class.to_comm_group H = function.injective.comm_group coe _ _ _ _ _ _ _
An additive subgroup of an add_comm_group
is an add_comm_group
.
Equations
- add_subgroup_class.to_add_comm_group H = function.injective.add_comm_group coe _ _ _ _ _ _ _
An additive subgroup of an add_ordered_comm_group
is an add_ordered_comm_group
.
Equations
A subgroup of an ordered_comm_group
is an ordered_comm_group
.
Equations
An additive subgroup of a linear_ordered_add_comm_group
is a
linear_ordered_add_comm_group
.
Equations
A subgroup of a linear_ordered_comm_group
is a linear_ordered_comm_group
.
Equations
The natural group hom from an additive subgroup of add_group
G
to G
.
Equations
- add_subgroup_class.subtype H = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}
The natural group hom from a subgroup of group G
to G
.
Equations
- subgroup_class.subtype H = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _}
The inclusion homomorphism from a additive subgroup H
contained in K
to K
.
Equations
- add_subgroup_class.inclusion h = add_monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _
The inclusion homomorphism from a subgroup H
contained in K
to K
.
Equations
- subgroup_class.inclusion h = monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _
- carrier : set G
- mul_mem' : ∀ {a b : G}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
- one_mem' : 1 ∈ self.carrier
- inv_mem' : ∀ {x : G}, x ∈ self.carrier → x⁻¹ ∈ self.carrier
A subgroup of a group G
is a subset containing 1, closed under multiplication
and closed under multiplicative inverse.
Instances for subgroup
- subgroup.has_sizeof_inst
- subgroup.set_like
- subgroup.subgroup_class
- subgroup.has_top
- subgroup.has_bot
- subgroup.inhabited
- subgroup.has_inf
- subgroup.has_Inf
- subgroup.complete_lattice
- subgroup.unique
- subgroup.nontrivial
- subgroup.is_modular_lattice
- is_simple_group.subgroup.is_simple_order
- quotient_group.subgroup.has_quotient
- subgroup.pointwise_central_scalar
- subgroup.commutator
- open_subgroup.has_coe_subgroup
- sylow.subgroup.has_coe
- carrier : set G
- add_mem' : ∀ {a b : G}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
- zero_mem' : 0 ∈ self.carrier
- neg_mem' : ∀ {x : G}, x ∈ self.carrier → -x ∈ self.carrier
An additive subgroup of an additive group G
is a subset containing 0, closed
under addition and additive inverse.
Instances for add_subgroup
- add_subgroup.has_sizeof_inst
- add_subgroup.set_like
- add_subgroup.add_subgroup_class
- add_subgroup.has_top
- add_subgroup.has_bot
- add_subgroup.inhabited
- add_subgroup.has_inf
- add_subgroup.has_Inf
- add_subgroup.complete_lattice
- add_subgroup.unique
- add_subgroup.nontrivial
- add_subgroup.is_modular_lattice
- is_simple_add_group.subgroup.is_simple_order
- quotient_add_group.subgroup.has_quotient
- add_subgroup.pointwise_central_scalar
- open_add_subgroup.has_coe_add_subgroup
Reinterpret an add_subgroup
as an add_submonoid
.
Equations
- subgroup.set_like = {coe := subgroup.carrier _inst_1, coe_injective' := _}
Equations
- add_subgroup.set_like = {coe := add_subgroup.carrier _inst_1, coe_injective' := _}
Equations
- add_subgroup.add_subgroup_class = {to_add_submonoid_class := {to_add_mem_class := {add_mem := _}, zero_mem := _}, neg_mem := _}
Equations
- subgroup.subgroup_class = {to_submonoid_class := {to_mul_mem_class := {mul_mem := _}, one_mem := _}, inv_mem := _}
See Note [custom simps projection]
Equations
- subgroup.simps.coe S = ↑S
See Note [custom simps projection]
Equations
Equations
- K.fintype = show fintype {g // g ∈ K}, from infer_instance
Equations
- K.fintype = show fintype {g // g ∈ K}, from infer_instance
Conversion to/from additive
/multiplicative
#
Supgroups of a group G
are isomorphic to additive subgroups of additive G
.
Equations
- subgroup.to_add_subgroup = {to_equiv := {to_fun := λ (S : subgroup G), {carrier := (⇑submonoid.to_add_submonoid S.to_submonoid).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}, inv_fun := λ (S : add_subgroup (additive G)), {carrier := (⇑add_submonoid.to_submonoid' S.to_add_submonoid).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}, left_inv := _, right_inv := _}, map_rel_iff' := _}
Additive subgroup of an additive group additive G
are isomorphic to subgroup of G
.
Additive supgroups of an additive group A
are isomorphic to subgroups of multiplicative A
.
Equations
- add_subgroup.to_subgroup = {to_equiv := {to_fun := λ (S : add_subgroup A), {carrier := (⇑add_submonoid.to_submonoid S.to_add_submonoid).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}, inv_fun := λ (S : subgroup (multiplicative A)), {carrier := (⇑submonoid.to_add_submonoid' S.to_submonoid).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}, left_inv := _, right_inv := _}, map_rel_iff' := _}
Subgroups of an additive group multiplicative A
are isomorphic to additive subgroups of A
.
Copy of a subgroup with a new carrier
equal to the old one. Useful to fix definitional
equalities.
Copy of an additive subgroup with a new carrier
equal to the old one.
Useful to fix definitional equalities
Two add_subgroup
s are equal if they have the same elements.
A subgroup contains the group's 1.
An add_subgroup
contains the group's 0.
An add_subgroup
is closed under addition.
An add_subgroup
is closed under inverse.
An add_subgroup
is closed under subtraction.
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.
A subgroup of a group inherits a multiplication.
Equations
- H.has_mul = H.to_submonoid.has_mul
A subgroup of a group inherits a 1.
Equations
- H.has_one = H.to_submonoid.has_one
An add_subgroup
of an add_group
inherits a natural scaling.
An add_subgroup
of an add_group
inherits an integer scaling.
A subgroup of a group inherits a group structure.
Equations
- H.to_group = function.injective.group coe _ _ _ _ _ _ _
An add_subgroup
of an add_group
inherits an add_group
structure.
Equations
- H.to_add_group = function.injective.add_group coe _ _ _ _ _ _ _
An add_subgroup
of an add_comm_group
is an add_comm_group
.
Equations
- H.to_add_comm_group = function.injective.add_comm_group coe _ _ _ _ _ _ _
A subgroup of a comm_group
is a comm_group
.
Equations
- H.to_comm_group = function.injective.comm_group coe _ _ _ _ _ _ _
An add_subgroup
of an add_ordered_comm_group
is an add_ordered_comm_group
.
Equations
- H.to_ordered_add_comm_group = function.injective.ordered_add_comm_group coe _ _ _ _ _ _ _
A subgroup of an ordered_comm_group
is an ordered_comm_group
.
Equations
- H.to_ordered_comm_group = function.injective.ordered_comm_group coe _ _ _ _ _ _ _
A subgroup of a linear_ordered_comm_group
is a linear_ordered_comm_group
.
Equations
- H.to_linear_ordered_comm_group = function.injective.linear_ordered_comm_group coe _ _ _ _ _ _ _
An add_subgroup
of a linear_ordered_add_comm_group
is a
linear_ordered_add_comm_group
.
Equations
The natural group hom from an add_subgroup
of add_group
G
to G
.
The inclusion homomorphism from a additive subgroup H
contained in K
to K
.
Equations
- add_subgroup.inclusion h = add_monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _
The inclusion homomorphism from a subgroup H
contained in K
to K
.
Equations
- subgroup.inclusion h = monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _
The add_subgroup G
of the add_group G
.
The top subgroup is isomorphic to the group.
This is the group version of submonoid.top_equiv
.
Equations
The top additive subgroup is isomorphic to the additive group.
This is the additive group version of add_submonoid.top_equiv
.
Equations
The trivial add_subgroup
{0}
of an add_group
G
.
Equations
Equations
- subgroup.inhabited = {default := ⊥}
Equations
- add_subgroup.has_bot.bot.unique = {to_inhabited := {default := 0}, uniq := _}
Equations
- subgroup.has_bot.bot.unique = {to_inhabited := {default := 1}, uniq := _}
A subgroup is either the trivial subgroup or nontrivial.
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, mul_mem' := _, one_mem' := _, inv_mem' := _}}
The inf of two add_subgroups
s is their intersection.
Equations
- add_subgroup.has_inf = {inf := λ (H₁ H₂ : add_subgroup G), {carrier := (H₁.to_add_submonoid ⊓ H₂.to_add_submonoid).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}}
Equations
- add_subgroup.has_Inf = {Inf := λ (s : set (add_subgroup G)), {carrier := ((⨅ (S : add_subgroup G) (H : S ∈ s), S.to_add_submonoid).copy (⋂ (S : add_subgroup G) (H : S ∈ s), ↑S) _).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}}
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 := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}
The add_subgroup
s of an add_group
form a complete lattice.
Equations
- add_subgroup.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (add_subgroup G) add_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 add_subgroup.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}
Equations
- add_subgroup.unique = {to_inhabited := {default := ⊥}, uniq := _}
Equations
- subgroup.unique = {to_inhabited := {default := ⊥}, uniq := _}
The add_subgroup
generated by a set
Equations
- add_subgroup.closure k = has_Inf.Inf {K : add_subgroup G | k ⊆ ↑K}
The subgroup
generated by a set.
Equations
- subgroup.closure k = has_Inf.Inf {K : subgroup G | k ⊆ ↑K}
The subgroup generated by a set includes the set.
The add_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 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
.
An induction principle for additive closure membership. If p
holds for 0
and all elements of k
, and is preserved under addition and inverses, then p
holds
for all elements of the additive closure of k
.
A dependent version of subgroup.closure_induction
.
A dependent version of add_subgroup.closure_induction
.
An induction principle for additive closure membership, for predicates with two arguments.
An induction principle for closure membership for predicates with two arguments.
If all the elements of a set s
commute, then closure s
is a commutative group.
Equations
- subgroup.closure_comm_group_of_comm hcomm = {mul := group.mul (subgroup.closure k).to_group, mul_assoc := _, one := group.one (subgroup.closure k).to_group, one_mul := _, mul_one := _, npow := group.npow (subgroup.closure k).to_group, npow_zero' := _, npow_succ' := _, inv := group.inv (subgroup.closure k).to_group, div := group.div (subgroup.closure k).to_group, div_eq_mul_inv := _, zpow := group.zpow (subgroup.closure k).to_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
If all the elements of a set s
commute, then closure s
is an additive
commutative group.
Equations
- add_subgroup.closure_add_comm_group_of_comm hcomm = {add := add_group.add (add_subgroup.closure k).to_add_group, add_assoc := _, zero := add_group.zero (add_subgroup.closure k).to_add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul (add_subgroup.closure k).to_add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (add_subgroup.closure k).to_add_group, sub := add_group.sub (add_subgroup.closure k).to_add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul (add_subgroup.closure k).to_add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
closure
forms a Galois insertion with the coercion to set.
Equations
- add_subgroup.gi G = {choice := λ (s : set G) (_x : ↑(add_subgroup.closure s) ≤ s), add_subgroup.closure s, gc := _, le_l_u := _, choice_eq := _}
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 := _}
Closure of a subgroup K
equals K
.
Additive closure of an additive subgroup K
equals K
The add_subgroup
generated by an element of an add_group
equals the set of
natural number multiples of the element.
The subgroup generated by an element of a group equals the set of integer number powers of the element.
An induction principle for closure membership. If p
holds for 1
and all elements of
k
and their inverse, and is preserved under multiplication, then p
holds for all elements of
the closure of k
.