Cosets #
This file develops the basic theory of left and right cosets.
When G
is a group and a : G
, s : Set G
, with open scoped Pointwise
we can write:
- the left coset of
s
bya
asa • s
- the right coset of
s
bya
asMulOpposite.op a • s
(orop a • s
withopen MulOpposite
)
If instead G
is an additive group, we can write (with open scoped Pointwise
still)
- the left coset of
s
bya
asa +ᵥ s
- the right coset of
s
bya
asAddOpposite.op a +ᵥ s
(orop a • s
withopen AddOpposite
)
Main definitions #
QuotientGroup.quotient s
: the quotient type representing the left cosets with respect to a subgroups
, for anAddGroup
this isQuotientAddGroup.quotient s
.QuotientGroup.mk
: the canonical map fromα
toα/s
for a subgroups
ofα
, for anAddGroup
this isQuotientAddGroup.mk
.
Notation #
G ⧸ H
is the quotient of the (additive) groupG
by the (additive) subgroupH
TODO #
Properly merge with pointwise actions on sets, by renaming and deduplicating lemmas as appropriate.
The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.
Equations
Instances For
Equations
Equations
α ⧸ s
is the quotient type representing the left cosets of s
.
If s
is a normal subgroup, α ⧸ s
is a group
Equations
α ⧸ s
is the quotient type representing the left cosets of s
. If s
is a normal
subgroup, α ⧸ s
is a group
Equations
Equations
Equations
The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.
Equations
Instances For
Equations
Equations
Right cosets are in bijection with left cosets.
Equations
Instances For
The canonical map from an AddGroup
α
to the quotient α ⧸ s
.
Equations
Instances For
Equations
Alias of QuotientGroup.induction_on
.
Equations
If two subgroups M
and N
of G
are equal, their quotients are in bijection.