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
.Subgroup.leftCosetEquivSubgroup
: the natural bijection between a left coset and the subgroup, for anAddGroup
this isAddSubgroup.leftCosetEquivAddSubgroup
.
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.
Equality of two right cosets s + a
and s + b
.
Equations
- RightAddCosetEquivalence s a b = (AddOpposite.op a +ᵥ s = AddOpposite.op b +ᵥ s)
Instances For
Equality of two right cosets s * a
and s * b
.
Equations
- RightCosetEquivalence s a b = (MulOpposite.op a • s = MulOpposite.op b • s)
Instances For
The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.
Equations
- QuotientAddGroup.leftRel s = AddAction.orbitRel (↥s.op) α
Instances For
The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.
Equations
- QuotientGroup.leftRel s = MulAction.orbitRel (↥s.op) α
Instances For
Equations
- QuotientAddGroup.leftRelDecidable s x y = ⋯.mpr (inst (-x + y))
Equations
- QuotientGroup.leftRelDecidable s x y = ⋯.mpr (inst (x⁻¹ * y))
α ⧸ s
is the quotient type representing the left cosets of s
. If s
is a normal
subgroup, α ⧸ s
is a group
Equations
- QuotientAddGroup.instHasQuotientAddSubgroup = { quotient' := fun (s : AddSubgroup α) => Quotient (QuotientAddGroup.leftRel s) }
α ⧸ s
is the quotient type representing the left cosets of s
.
If s
is a normal subgroup, α ⧸ s
is a group
Equations
- QuotientGroup.instHasQuotientSubgroup = { quotient' := fun (s : Subgroup α) => Quotient (QuotientGroup.leftRel s) }
The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.
Equations
- QuotientAddGroup.rightRel s = AddAction.orbitRel (↥s) α
Instances For
The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.
Equations
- QuotientGroup.rightRel s = MulAction.orbitRel (↥s) α
Instances For
Equations
- QuotientAddGroup.rightRelDecidable s x y = ⋯.mpr (inst (y + -x))
Equations
- QuotientGroup.rightRelDecidable s x y = ⋯.mpr (inst (y * x⁻¹))
Right cosets are in bijection with left cosets.
Equations
- QuotientAddGroup.quotientRightRelEquivQuotientLeftRel s = { toFun := Quotient.map' (fun (g : α) => -g) ⋯, invFun := Quotient.map' (fun (g : α) => -g) ⋯, left_inv := ⋯, right_inv := ⋯ }
Instances For
Right cosets are in bijection with left cosets.
Equations
- QuotientGroup.quotientRightRelEquivQuotientLeftRel s = { toFun := Quotient.map' (fun (g : α) => g⁻¹) ⋯, invFun := Quotient.map' (fun (g : α) => g⁻¹) ⋯, left_inv := ⋯, right_inv := ⋯ }
Instances For
Equations
Equations
Equations
The canonical map from an AddGroup
α
to the quotient α ⧸ s
.
Equations
- ↑a = Quotient.mk'' a
Instances For
The canonical map from a group α
to the quotient α ⧸ s
.
Equations
- ↑a = Quotient.mk'' a
Instances For
Equations
- QuotientAddGroup.instCoeQuotientAddSubgroup = { coe := QuotientAddGroup.mk }
Alias of QuotientGroup.induction_on
.
Equations
- QuotientAddGroup.instInhabitedQuotientAddSubgroup s = { default := ↑0 }
Equations
- QuotientGroup.instInhabitedQuotientSubgroup s = { default := ↑1 }
Given an additive subgroup s
,
the function that sends an additive subgroup t
to the pair consisting of
its intersection with s
and its image in the quotient α ⧸ s
is strictly monotone, even though it is not injective in general.
Given a subgroup s
, the function that sends a subgroup t
to the pair consisting of
its intersection with s
and its image in the quotient α ⧸ s
is strictly monotone, even though
it is not injective in general.
The natural bijection between the cosets g + s
and s
.
Equations
Instances For
The natural bijection between a left coset g * s
and s
.
Equations
Instances For
The natural bijection between the cosets s + g
and s
.
Equations
- AddSubgroup.rightCosetEquivAddSubgroup g = { toFun := fun (x : ↑(AddOpposite.op g +ᵥ ↑s)) => ⟨↑x + -g, ⋯⟩, invFun := fun (x : ↥s) => ⟨↑x + g, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
Instances For
The natural bijection between a right coset s * g
and s
.
Equations
- Subgroup.rightCosetEquivSubgroup g = { toFun := fun (x : ↑(MulOpposite.op g • ↑s)) => ⟨↑x * g⁻¹, ⋯⟩, invFun := fun (x : ↥s) => ⟨↑x * g, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
Instances For
A (non-canonical) bijection between an add_group α
and the product (α/s) × s
Equations
- One or more equations did not get rendered due to their size.
Instances For
If two subgroups M
and N
of G
are equal, their quotients are in bijection.
Equations
- AddSubgroup.quotientEquivOfEq h = { toFun := Quotient.map' id ⋯, invFun := Quotient.map' id ⋯, left_inv := ⋯, right_inv := ⋯ }
Instances For
If two subgroups M
and N
of G
are equal, their quotients are in bijection.
Equations
- Subgroup.quotientEquivOfEq h = { toFun := Quotient.map' id ⋯, invFun := Quotient.map' id ⋯, left_inv := ⋯, right_inv := ⋯ }
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
.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If H ≤ K
, then G/H ≃ G/K × K/H
nonconstructively. The
constructive version is quotientEquivProdOfLE'
.
Equations
- AddSubgroup.quotientEquivSumOfLE h_le = AddSubgroup.quotientEquivSumOfLE' h_le Quotient.out' ⋯
Instances For
If H ≤ K
, then G/H ≃ G/K × K/H
nonconstructively.
The constructive version is quotientEquivProdOfLE'
.
Equations
- Subgroup.quotientEquivProdOfLE h_le = Subgroup.quotientEquivProdOfLE' h_le Quotient.out' ⋯
Instances For
If s ≤ t
, then there is an embedding
s ⧸ H.addSubgroupOf s ↪ t ⧸ H.addSubgroupOf t
.
Equations
- AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE H h = { toFun := Quotient.map' ⇑(AddSubgroup.inclusion h) ⋯, inj' := ⋯ }
Instances For
If s ≤ t
, then there is an embedding s ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t
.
Equations
- Subgroup.quotientSubgroupOfEmbeddingOfLE H h = { toFun := Quotient.map' ⇑(Subgroup.inclusion h) ⋯, inj' := ⋯ }
Instances For
If s ≤ t
, then there is a map H ⧸ s.addSubgroupOf H → H ⧸ t.addSubgroupOf H
.
Equations
Instances For
If s ≤ t
, then there is a map α ⧸ s → α ⧸ t
.
Equations
Instances For
The natural embedding
H ⧸ (⨅ i, f i).addSubgroupOf H) ↪ Π i, H ⧸ (f i).addSubgroupOf H
.
Equations
- AddSubgroup.quotientiInfAddSubgroupOfEmbedding f H = { toFun := fun (q : ↥H ⧸ (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) => AddSubgroup.quotientAddSubgroupOfMapOfLE H ⋯ q, inj' := ⋯ }
Instances For
The natural embedding H ⧸ (⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H
.
Equations
- Subgroup.quotientiInfSubgroupOfEmbedding f H = { toFun := fun (q : ↥H ⧸ (⨅ (i : ι), f i).subgroupOf H) (i : ι) => Subgroup.quotientSubgroupOfMapOfLE H ⋯ q, inj' := ⋯ }
Instances For
The natural embedding α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i
.
Equations
- AddSubgroup.quotientiInfEmbedding f = { toFun := fun (q : α ⧸ ⨅ (i : ι), f i) (i : ι) => AddSubgroup.quotientMapOfLE ⋯ q, inj' := ⋯ }
Instances For
The natural embedding α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i
.
Equations
- Subgroup.quotientiInfEmbedding f = { toFun := fun (q : α ⧸ ⨅ (i : ι), f i) (i : ι) => Subgroup.quotientMapOfLE ⋯ q, inj' := ⋯ }
Instances For
An equivalence between any non-empty fiber of an AddMonoidHom
and its kernel.
Equations
- f.fiberEquivKer a = (Equiv.setCongr ⋯).trans (AddSubgroup.leftCosetEquivAddSubgroup a)
Instances For
An equivalence between any non-empty fiber of a MonoidHom
and its kernel.
Equations
- f.fiberEquivKer a = (Equiv.setCongr ⋯).trans (Subgroup.leftCosetEquivSubgroup a)
Instances For
An equivalence between any fiber of a surjective AddMonoidHom
and its kernel.
Equations
- AddMonoidHom.fiberEquivKerOfSurjective hf h = ⋯ ▸ f.fiberEquivKer ⋯.choose
Instances For
An equivalence between any fiber of a surjective MonoidHom
and its kernel.
Equations
- MonoidHom.fiberEquivKerOfSurjective hf h = ⋯ ▸ f.fiberEquivKer ⋯.choose
Instances For
An equivalence between any two non-empty fibers of an AddMonoidHom
.
Equations
- f.fiberEquiv a b = (f.fiberEquivKer a).trans (f.fiberEquivKer b).symm
Instances For
An equivalence between any two fibers of a surjective AddMonoidHom
.
Equations
- AddMonoidHom.fiberEquivOfSurjective hf h h' = (AddMonoidHom.fiberEquivKerOfSurjective hf h).trans (AddMonoidHom.fiberEquivKerOfSurjective hf h').symm
Instances For
An equivalence between any two fibers of a surjective MonoidHom
.
Equations
- MonoidHom.fiberEquivOfSurjective hf h h' = (MonoidHom.fiberEquivKerOfSurjective hf h).trans (MonoidHom.fiberEquivKerOfSurjective hf h').symm
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
.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- One or more equations did not get rendered due to their size.