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 anAddGroup
-
H K
areSubgroup
s ofG
orAddSubgroup
s ofA
-
x
is an element of typeG
or typeA
-
f g : N →* G→* 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
-
AddSubgroup A
: the type of subgroups of an additive groupA
-
CompleteLattice (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× K
is a subgroup ofG × N× N
-
MonoidHom.range f
: the range of the group homomorphismf
is a subgroup -
MonoidHom.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
SubgroupClass S G
states S
is a type of subsets s ⊆ G⊆ G
that are subgroups of G
.
Instances
AddSubgroupClass S G
states S
is a type of subsets s ⊆ G⊆ G
that are
additive subgroups of G
.
Instances
Equations
- zsmul_mem.match_1 motive x h_1 h_2 = Int.casesOn x (fun a => h_1 a) fun a => h_2 a
An additive subgroup of a add_group
inherits an inverse.
A subgroup of a group inherits an inverse.
An additive subgroup of an add_group
inherits a subtraction.
A subgroup of a group inherits a division
An additive subgroup of an add_group
inherits an integer scaling.
A subgroup of a group inherits an integer power.
Equations
- (_ : ZeroMemClass S G) = (_ : ZeroMemClass S G)
Equations
- (_ : AddSubmonoidClass S G) = (_ : AddSubmonoidClass S G)
An additive subgroup of an AddGroup
inherits an AddGroup
structure.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
A subgroup of a group inherits a group structure.
Equations
- One or more equations did not get rendered due to their size.
An additive subgroup of an AddCommGroup
is an AddCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : AddSubmonoidClass S G) = (_ : AddSubmonoidClass S G)
Equations
- (_ : ZeroMemClass S G) = (_ : ZeroMemClass S G)
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
Equations
- (_ : AddSubmonoidClass S G) = (_ : AddSubmonoidClass S G)
An additive subgroup of an AddOrderedCommGroup
is an AddOrderedCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
Equations
- (_ : ZeroMemClass S G) = (_ : ZeroMemClass S G)
A subgroup of an OrderedCommGroup
is an OrderedCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
An additive subgroup of a LinearOrderedAddCommGroup
is a
LinearOrderedAddCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : AddSubmonoidClass S G) = (_ : AddSubmonoidClass S G)
Equations
- (_ : ZeroMemClass S G) = (_ : ZeroMemClass S G)
A subgroup of a LinearOrderedCommGroup
is a LinearOrderedCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The natural group hom from an additive subgroup of AddGroup
G
to G
.
Equations
- One or more equations did not get rendered due to their size.
The natural group hom from a subgroup of group G
to G
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The inclusion homomorphism from a additive subgroup H
contained in K
to K
.
Equations
- One or more equations did not get rendered due to their size.
The inclusion homomorphism from a subgroup H
contained in K
to K
.
Equations
- One or more equations did not get rendered due to their size.
G
is closed under inverses
A subgroup of a group G
is a subset containing 1, closed under multiplication
and closed under multiplicative inverse.
Instances For
G
is closed under negation
An additive subgroup of an additive group G
is a subset containing 0, closed
under addition and additive inverse.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : AddSubgroupClass (AddSubgroup G) G) = (_ : AddSubgroupClass (AddSubgroup G) G)
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.
Additive subgroup of an additive group Additive G
are isomorphic to subgroup of G
.
Equations
- AddSubgroup.toSubgroup' = OrderIso.symm Subgroup.toAddSubgroup
Additive supgroups 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.
Subgroups of an additive group Multiplicative A
are isomorphic to additive subgroups of A
.
Equations
- Subgroup.toAddSubgroup' = OrderIso.symm AddSubgroup.toSubgroup
Equations
- One or more equations did not get rendered due to their size.
Copy of an additive subgroup with a new carrier
equal to the old one.
Useful to fix definitional equalities
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- AddSubgroup.ofSub.match_1 s motive hsn h_1 = Exists.casesOn hsn fun w h => h_1 w h
Construct a subgroup from a nonempty set that is closed under subtraction
Equations
- One or more equations did not get rendered due to their size.
An AddSubgroup
of an AddGroup
inherits an addition.
Equations
- AddSubgroup.add H = AddSubmonoid.add H.toAddSubmonoid
A subgroup of a group inherits a multiplication.
Equations
- Subgroup.mul H = Submonoid.mul H.toSubmonoid
An AddSubgroup
of an AddGroup
inherits a zero.
Equations
- AddSubgroup.zero H = AddSubmonoid.zero H.toAddSubmonoid
A subgroup of a group inherits a 1.
Equations
- Subgroup.one H = Submonoid.one H.toSubmonoid
A AddSubgroup
of a AddGroup
inherits an inverse.
Equations
- AddSubgroup.neg H = { neg := fun a => { val := -↑a, property := (_ : -↑a ∈ H) } }
An AddSubgroup
of an AddGroup
inherits a subtraction.
Equations
- AddSubgroup.sub H = { sub := fun a b => { val := ↑a - ↑b, property := (_ : ↑a - ↑b ∈ H) } }
An AddSubgroup
of an AddGroup
inherits a natural scaling.
An AddSubgroup
of an AddGroup
inherits an integer scaling.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
An AddSubgroup
of an AddGroup
inherits an AddGroup
structure.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
An AddSubgroup
of an AddCommGroup
is an AddCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
An AddSubgroup
of an AddOrderedCommGroup
is an AddOrderedCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
A subgroup of an OrderedCommGroup
is an OrderedCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
An AddSubgroup
of a LinearOrderedAddCommGroup
is a
LinearOrderedAddCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
A subgroup of a LinearOrderedCommGroup
is a LinearOrderedCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The natural group hom from an AddSubgroup
of AddGroup
G
to G
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The inclusion homomorphism from a additive subgroup H
contained in K
to K
.
Equations
- One or more equations did not get rendered due to their size.
The AddSubgroup G
of the AddGroup G
.
Equations
- One or more equations did not get rendered due to their size.
The top additive subgroup is isomorphic to the additive group.
This is the additive group version of AddSubmonoid.topEquiv
.
Equations
- AddSubgroup.topEquiv = AddSubmonoid.topEquiv
The top subgroup is isomorphic to the group.
This is the group version of Submonoid.topEquiv
.
Equations
- Subgroup.topEquiv = Submonoid.topEquiv
The trivial AddSubgroup
{0}
of an AddGroup
G
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddSubgroup.coe_eq_singleton.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h
A subgroup is either the trivial subgroup or nontrivial.
The inf of two add_subgroups
s is their intersection.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : (Set.interᵢ fun S => Set.interᵢ fun h => ↑S) = ↑(⨅ i, ⨅ h, i.toAddSubmonoid)) = (_ : (Set.interᵢ fun S => Set.interᵢ fun h => ↑S) = ↑(⨅ i, ⨅ h, i.toAddSubmonoid))
Equations
- (_ : -x ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x) = (_ : -x ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (s : Set (AddSubgroup G)) (a : AddSubgroup G), a ∈ s → a ≤ supₛ s) = (_ : ∀ (