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
sA
is anAddGroup
H K
areSubgroup
s ofG
orAddSubgroup
s ofA
x
is an element of typeG
or typeA
f g : N →* G
are group homomorphismss k
are sets of elements of typeG
Definitions in the file:
Subgroup G
: the type of subgroups of a groupG
AddSubgroup A
: the type of subgroups of an additive groupA
CompleteLattice (Subgroup G)
: the subgroups ofG
form a complete latticeSubgroup.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 setSubgroup.comap H f
: the preimage of a subgroupH
along the group homomorphismf
is also a subgroupSubgroup.map f H
: the image of a subgroupH
along the group homomorphismf
is also a subgroupSubgroup.prod H K
: the product of subgroupsH
,K
of groupsG
,N
respectively,H × K
is a subgroup ofG × N
MonoidHom.range f
: the range of the group homomorphismf
is a subgroupMonoidHom.ker f
: the kernel of a group homomorphismf
is the subgroup of elementsx : G
such thatf x = 1
MonoidHom.eq_locus f g
: given group homomorphismsf
,g
, the elements ofG
such thatf x = g x
form 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
s
is closed under inverses
s
is closed under negation
SubgroupClass S G
states S
is a type of subsets s ⊆ G
that are subgroups of G
.
Instances
AddSubgroupClass S G
states S
is a type of subsets s ⊆ G
that are
additive subgroups of G
.
Instances
Alias of InvMemClass.coe_inv
.
An additive subgroup of an AddGroup
inherits a subtraction.
A subgroup of a group inherits a division
An additive subgroup of an AddGroup
inherits an integer scaling.
A subgroup of a group inherits an integer power.
An additive subgroup of an AddGroup
inherits an AddGroup
structure.
Equations
- AddSubgroupClass.toAddGroup H = Function.Injective.addGroup (fun (a : { x : G // x ∈ H }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
A subgroup of a group inherits a group structure.
Equations
- SubgroupClass.toGroup H = Function.Injective.group (fun (a : { x : G // x ∈ H }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
An additive subgroup of an AddCommGroup
is an AddCommGroup
.
Equations
- AddSubgroupClass.toAddCommGroup H = Function.Injective.addCommGroup (fun (a : { x : G // x ∈ H }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
A subgroup of a CommGroup
is a CommGroup
.
Equations
- SubgroupClass.toCommGroup H = Function.Injective.commGroup (fun (a : { x : G // x ∈ H }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The natural group hom from a subgroup of group G
to G
.
Equations
- ↑H = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The inclusion homomorphism from an additive subgroup H
contained in K
to K
.
Equations
- AddSubgroupClass.inclusion h = AddMonoidHom.mk' (fun (x : { x : G // x ∈ H }) => ⟨↑x, ⋯⟩) ⋯
Instances For
The inclusion homomorphism from a subgroup H
contained in K
to K
.
Equations
- SubgroupClass.inclusion h = MonoidHom.mk' (fun (x : { x : G // x ∈ H }) => ⟨↑x, ⋯⟩) ⋯
Instances For
A subgroup of a group G
is a subset containing 1, closed under multiplication
and closed under multiplicative inverse.
Instances For
An additive subgroup of an additive group G
is a subset containing 0, closed
under addition and additive inverse.
Instances For
G
is closed under negation
Equations
- AddSubgroup.instSetLike = { coe := fun (s : AddSubgroup G) => s.carrier, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Conversion to/from Additive
/Multiplicative
#
Subgroups of a group G
are isomorphic to additive subgroups of Additive G
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Additive subgroups of an additive group A
are isomorphic to subgroups of Multiplicative A
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Subgroups of an additive group Multiplicative A
are isomorphic to additive subgroups of A
.
Equations
- Subgroup.toAddSubgroup' = AddSubgroup.toSubgroup.symm
Instances For
Copy of an additive subgroup with a new carrier
equal to the old one.
Useful to fix definitional equalities
Equations
- K.copy s hs = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
Two AddSubgroup
s are equal if they have the same elements.
An AddSubgroup
contains the group's 0.
An AddSubgroup
is closed under addition.
An AddSubgroup
is closed under inverse.
An AddSubgroup
is closed under subtraction.
Construct a subgroup from a nonempty set that is closed under subtraction
Equations
- AddSubgroup.ofSub s hsn hs = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
Construct a subgroup from a nonempty set that is closed under division.
Equations
- Subgroup.ofDiv s hsn hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
An AddSubgroup
of an AddGroup
inherits an addition.
Equations
- H.add = H.add
An AddSubgroup
of an AddGroup
inherits a zero.
Equations
- H.zero = H.zero
An AddSubgroup
of an AddGroup
inherits an inverse.
An AddSubgroup
of an AddGroup
inherits a subtraction.
An AddSubgroup
of an AddGroup
inherits a natural scaling.
An AddSubgroup
of an AddGroup
inherits an integer scaling.
An AddSubgroup
of an AddGroup
inherits an AddGroup
structure.
Equations
- H.toAddGroup = Function.Injective.addGroup (fun (a : { x : G // x ∈ H }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
A subgroup of a group inherits a group structure.
Equations
- H.toGroup = Function.Injective.group (fun (a : { x : G // x ∈ H }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
An AddSubgroup
of an AddCommGroup
is an AddCommGroup
.
Equations
- H.toAddCommGroup = Function.Injective.addCommGroup (fun (a : { x : G // x ∈ H }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The natural group hom from an AddSubgroup
of AddGroup
G
to G
.
Equations
- H.subtype = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The inclusion homomorphism from an additive subgroup H
contained in K
to K
.
Equations
- AddSubgroup.inclusion h = AddMonoidHom.mk' (fun (x : { x : G // x ∈ H }) => ⟨↑x, ⋯⟩) ⋯
Instances For
The inclusion homomorphism from a subgroup H
contained in K
to K
.
Equations
- Subgroup.inclusion h = MonoidHom.mk' (fun (x : { x : G // x ∈ H }) => ⟨↑x, ⋯⟩) ⋯
Instances For
The AddSubgroup G
of the AddGroup G
.
The top additive subgroup is isomorphic to the additive group.
This is the additive group version of AddSubmonoid.topEquiv
.
Equations
- AddSubgroup.topEquiv = AddSubmonoid.topEquiv
Instances For
The top subgroup is isomorphic to the group.
This is the group version of Submonoid.topEquiv
.
Equations
- Subgroup.topEquiv = Submonoid.topEquiv
Instances For
The trivial AddSubgroup
{0}
of an AddGroup
G
.
A subgroup is either the trivial subgroup or nontrivial.
A subgroup is either the trivial subgroup or nontrivial.
A subgroup is either the trivial subgroup or contains a nonzero element.
The inf of two AddSubgroup
s is their intersection.
Equations
- AddSubgroup.instInf = { inf := fun (H₁ H₂ : AddSubgroup G) => let __src := H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid; { toAddSubmonoid := __src, neg_mem' := ⋯ } }
Equations
- AddSubgroup.instInfSet = { sInf := fun (s : Set (AddSubgroup G)) => let __src := (⨅ S ∈ s, S.toAddSubmonoid).copy (⋂ S ∈ s, ↑S) ⋯; { toAddSubmonoid := __src, neg_mem' := ⋯ } }
The AddSubgroup
s of an AddGroup
form a complete lattice.
Equations
- AddSubgroup.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Subgroups of a group form a complete lattice.
Equations
- Subgroup.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The AddSubgroup
generated by a set
Equations
- AddSubgroup.closure k = sInf {K : AddSubgroup G | k ⊆ ↑K}
Instances For
The AddSubgroup
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 inverses, then p
holds for all elements of the additive closure of k
.
See also AddSubgroup.closure_induction_left
and AddSubgroup.closure_induction_left
for
versions that only require showing p
is preserved by addition by elements in 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
.
See also Subgroup.closure_induction_left
and Subgroup.closure_induction_right
for versions that
only require showing p
is preserved by multiplication by elements in k
.
A dependent version of AddSubgroup.closure_induction
.
A dependent version of 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 an additive
commutative group.
Equations
Instances For
closure
forms a Galois insertion with the coercion to set.
Equations
- AddSubgroup.gi G = { choice := fun (s : Set G) (x : ↑(AddSubgroup.closure s) ≤ s) => AddSubgroup.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
Instances For
closure
forms a Galois insertion with the coercion to set.
Equations
- Subgroup.gi G = { choice := fun (s : Set G) (x : ↑(Subgroup.closure s) ≤ s) => Subgroup.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
Instances For
Additive closure of an additive subgroup K
equals K
Closure of a subgroup K
equals K
.
The AddSubgroup
generated by an element of an AddGroup
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.