Cosets #
This file develops the basic theory of left and right cosets.
Main definitions #
leftCoset a s
: the left coseta * s
for an elementa : α
and a subsets ⊆ α
, for anAddGroup
this isleftAddCoset a s
.rightCoset s a
: the right cosets * a
for an elementa : α
and a subsets ⊆ α
, for anAddGroup
this isrightAddCoset s a
.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
.Subgroup.leftCosetEquivSubgroup
: the natural bijection between a left coset and the subgroup, for anAddGroup
this isAddSubgroup.leftCosetEquivAddSubgroup
.
Notation #
-
a *l s
: forleftCoset a s
. -
a +l s
: forleftAddCoset a s
. -
s *r a
: forrightCoset s a
. -
s +r a
: forrightAddCoset s a
. -
G ⧸ H
is the quotient of the (additive) groupG
by the (additive) subgroupH
The left coset a * s
for an element a : α
and a subset s : Set α
Instances For
The left coset a+s
for an element a : α
and a subset s : set α
Instances For
The right coset s * a
for an element a : α
and a subset s : Set α
Instances For
The right coset s+a
for an element a : α
and a subset s : set α
Instances For
Instances For
Instances For
Instances For
Instances For
The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.
Instances For
α ⧸ s
is the quotient type representing the left cosets of s
. If s
is a normal
subgroup, α ⧸ s
is a group
α ⧸ s
is the quotient type representing the left cosets of s
.
If s
is a normal subgroup, α ⧸ s
is a group
The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.
Instances For
Right cosets are in bijection with left cosets.
Instances For
Right cosets are in bijection with left cosets.
Instances For
The canonical map from an AddGroup
α
to the quotient α ⧸ s
.
Instances For
Instances For
Instances For
The natural bijection between the cosets g + s
and s
.
Instances For
Instances For
Instances For
The natural bijection between the cosets s + g
and s
.
Instances For
The natural bijection between a right coset s * g
and s
.
Instances For
A (non-canonical) bijection between an add_group α
and the product (α/s) × s
Instances For
If two subgroups M
and N
of G
are equal, their quotients are in bijection.
Instances For
If H ≤ K
, then G/H ≃ G/K × K/H
constructively, using the provided right inverse
of the quotient map G → G/K
. The classical version is AddSubgroup.quotientEquivSumOfLE
.
Instances For
If H ≤ K
, then G/H ≃ G/K × K/H
constructively, using the provided right inverse
of the quotient map G → G/K
. The classical version is Subgroup.quotientEquivProdOfLE
.
Instances For
If H ≤ K
, then G/H ≃ G/K × K/H
nonconstructively. The
constructive version is quotientEquivProdOfLE'
.
Instances For
If H ≤ K
, then G/H ≃ G/K × K/H
nonconstructively.
The constructive version is quotientEquivProdOfLE'
.
Instances For
If s ≤ t
, then there is an embedding
s ⧸ H.addSubgroupOf s ↪ t ⧸ H.addSubgroupOf t
.
Instances For
If s ≤ t
, then there is an embedding s ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t
.
Instances For
If s ≤ t
, then there is a map H ⧸ s.addSubgroupOf H → H ⧸ t.addSubgroupOf H
.
Instances For
If s ≤ t
, then there is a map H ⧸ s.subgroupOf H → H ⧸ t.subgroupOf H
.
Instances For
If s ≤ t
, then there is a map α ⧸ s → α ⧸ t
.
Instances For
The natural embedding
H ⧸ (⨅ i, f i).addSubgroupOf H) ↪ Π i, H ⧸ (f i).addSubgroupOf H
.
Instances For
The natural embedding H ⧸ (⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H
.
Instances For
The natural embedding α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i
.
Instances For
Lagrange's Theorem: The order of an additive subgroup divides the order of its ambient additive group.
Lagrange's Theorem: The order of a subgroup divides the order of its ambient group.
Instances For
If s
is a subgroup of the additive group α
, and t
is a subset of α ⧸ s
, then
there is a (typically non-canonical) bijection between the preimage of t
in α
and the product
s × t
.
Instances For
Instances For
If s
is a subgroup of the group α
, and t
is a subset of α ⧸ s
, then there is a
(typically non-canonical) bijection between the preimage of t
in α
and the product s × t
.