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⧸ 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 α
Equations
- Coset.«term_*l_» = Lean.ParserDescr.trailingNode `Coset.term_*l_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *l ") (Lean.ParserDescr.cat `term 71))
The left coset a+s
for an element a : α
and a subset s : set α
Equations
- Coset.«term_+l_» = Lean.ParserDescr.trailingNode `Coset.term_+l_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " +l ") (Lean.ParserDescr.cat `term 71))
The right coset s * a
for an element a : α
and a subset s : set α
Equations
- Coset.«term_*r_» = Lean.ParserDescr.trailingNode `Coset.term_*r_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *r ") (Lean.ParserDescr.cat `term 71))
The right coset s+a
for an element a : α
and a subset s : set α
Equations
- Coset.«term_+r_» = Lean.ParserDescr.trailingNode `Coset.term_+r_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " +r ") (Lean.ParserDescr.cat `term 71))
Equality of two left cosets a + s
and b + s
.
Equations
- LeftAddCosetEquivalence s a b = (leftAddCoset a s = leftAddCoset b s)
Equality of two right cosets s + a
and s + b
.
Equations
- RightAddCosetEquivalence s a b = (rightAddCoset s a = rightAddCoset s b)
Equality of two right cosets s * a
and s * b
.
Equations
- RightCosetEquivalence s a b = (rightCoset s a = rightCoset s b)
Equations
- mem_leftAddCoset_iff.match_1 a motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right
Equations
- mem_rightAddCoset_iff.match_1 a motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right
Equations
- orbit_addSubgroup_eq_rightCoset.match_2 s a _b motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right
Equations
- orbit_addSubgroup_eq_rightCoset.match_1 s a _b motive x h_1 = Exists.casesOn x fun w h => h_1 w h
The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.
Equations
- QuotientAddGroup.leftRel s = AddAction.orbitRel { x // x ∈ ↑AddSubgroup.opposite s } α
The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.
Equations
- QuotientGroup.leftRel s = MulAction.orbitRel { x // x ∈ ↑Subgroup.opposite s } α
α ⧸ s⧸ s
is the quotient type representing the left cosets of s
. If s
is a normal
subgroup, α ⧸ s⧸ s
is a group
Equations
- QuotientAddGroup.instHasQuotientAddSubgroup = { quotient' := fun s => Quotient (QuotientAddGroup.leftRel s) }
α ⧸ s⧸ s
is the quotient type representing the left cosets of s
.
If s
is a normal subgroup, α ⧸ s⧸ s
is a group
Equations
- QuotientGroup.instHasQuotientSubgroup = { quotient' := fun s => 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 { x // x ∈ s } α
The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.
Equations
- QuotientGroup.rightRel s = MulAction.orbitRel { x // x ∈ s } α
Equations
- One or more equations did not get rendered due to their size.
Right cosets are in bijection with left cosets.
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.
Right cosets are in bijection with left cosets.
Equations
- One or more equations did not get rendered due to their size.
Equations
Equations
The canonical map from an AddGroup
α
to the quotient α ⧸ s⧸ s
.
Equations
- ↑a = Quotient.mk'' a
Equations
- QuotientAddGroup.instCoeTCQuotientAddSubgroupInstHasQuotientAddSubgroup = { coe := QuotientAddGroup.mk }
Equations
- QuotientAddGroup.instInhabitedQuotientAddSubgroupInstHasQuotientAddSubgroup s = { default := ↑0 }
Equations
- QuotientGroup.instInhabitedQuotientSubgroupInstHasQuotientSubgroup s = { default := ↑1 }
Equations
- QuotientAddGroup.preimage_image_mk.match_1 N s x motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right
Equations
- QuotientAddGroup.preimage_image_mk.match_2 N s x motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right
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
- AddSubgroup.leftCosetEquivAddSubgroup.match_2 motive x h_1 = Subtype.casesOn x fun val property => h_1 val property
Equations
- AddSubgroup.leftCosetEquivAddSubgroup.match_1 g motive x h_1 = Subtype.casesOn x fun val property => h_1 val property
The natural bijection between the cosets g + s
and s
.
Equations
- One or more equations did not get rendered due to their size.
The natural bijection between the cosets s + g
and s
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddSubgroup.rightCosetEquivAddSubgroup.match_1 g motive x h_1 = Subtype.casesOn x fun val property => h_1 val property
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 bijection between a right coset s * g
and s
.
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.
A (non-canonical) bijection between an add_group α
and the product (α/s) × s× s
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.
If two subgroups M
and N
of G
are equal, their quotients are in bijection.
Equations
- One or more equations did not get rendered due to their size.
If H ≤ K≤ K
, then G/H ≃ G/K × K/H≃ G/K × K/H× K/H
constructively, using the provided right inverse
of the quotient map G → G/K→ G/K
. The classical version is addQuotientEquivProdOfLe
.
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
- (_ : -f (Quotient.mk'' g) + g ∈ t) = (_ : -f (Quotient.mk'' g) + g ∈ t)
Equations
- One or more equations did not get rendered due to their size.
If H ≤ K≤ K
, then G/H ≃ G/K × K/H≃ G/K × K/H× K/H
constructively, using the provided right inverse
of the quotient map G → G/K→ G/K
. The classical version is quotientEquivProdOfLe
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (q : Quotient (QuotientAddGroup.leftRel t)), Quotient.mk'' (Quotient.out' q) = q) = (_ : ∀ (q : Quotient (QuotientAddGroup.leftRel t)), Quotient.mk'' (Quotient.out' q) = q)
If H ≤ K≤ K
, then G/H ≃ G/K × K/H≃ G/K × K/H× K/H
nonconstructively. The
constructive version is quotientEquivProdOfLe'
.
Equations
- AddSubgroup.quotientEquivSumOfLe h_le = AddSubgroup.quotientEquivSumOfLe' h_le Quotient.out' (_ : ∀ (q : Quotient (QuotientAddGroup.leftRel t)), Quotient.mk'' (Quotient.out' q) = q)
If H ≤ K≤ K
, then G/H ≃ G/K × K/H≃ G/K × K/H× K/H
nonconstructively.
The constructive version is quotientEquivProdOfLe'
.
Equations
- Subgroup.quotientEquivProdOfLe h_le = Subgroup.quotientEquivProdOfLe' h_le Quotient.out' (_ : ∀ (q : Quotient (QuotientGroup.leftRel t)), Quotient.mk'' (Quotient.out' q) = q)
Equations
- (_ : Setoid.r a b → Setoid.r (↑(AddSubgroup.inclusion h) a) (↑(AddSubgroup.inclusion h) b)) = (_ : Setoid.r a b → Setoid.r (↑(AddSubgroup.inclusion h) a) (↑(AddSubgroup.inclusion h) b))
If s ≤ t≤ t
, then there is an embedding
s ⧸ H.addSubgroupOf s ↪ t ⧸ H.addSubgroupOf t⧸ H.addSubgroupOf s ↪ t ⧸ H.addSubgroupOf t↪ t ⧸ H.addSubgroupOf t⧸ H.addSubgroupOf t
.
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.
If s ≤ t≤ t
, then there is an embedding s ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t↪ t ⧸ H.subgroupOf t⧸ H.subgroupOf t
.
Equations
- One or more equations did not get rendered due to their size.
If s ≤ t≤ t
, then there is an map H ⧸ s.addSubgroupOf H → H ⧸ t.addSubgroupOf H⧸ s.addSubgroupOf H → H ⧸ t.addSubgroupOf H→ H ⧸ t.addSubgroupOf H⧸ t.addSubgroupOf H
.
Equations
- AddSubgroup.quotientAddSubgroupOfMapOfLe H h = Quotient.map' id (_ : ∀ (a b : { x // x ∈ H }), Setoid.r a b → Setoid.r (id a) (id b))
If s ≤ t≤ t
, then there is a map H ⧸ s.subgroupOf H → H ⧸ t.subgroupOf H⧸ s.subgroupOf H → H ⧸ t.subgroupOf H→ H ⧸ t.subgroupOf H⧸ t.subgroupOf H
.
Equations
- Subgroup.quotientSubgroupOfMapOfLe H h = Quotient.map' id (_ : ∀ (a b : { x // x ∈ H }), Setoid.r a b → Setoid.r (id a) (id b))
If s ≤ t≤ t
, then there is an map α ⧸ s → α ⧸ t⧸ s → α ⧸ t→ α ⧸ t⧸ t
.
Equations
- AddSubgroup.quotientMapOfLe h = Quotient.map' id (_ : ∀ (a b : α), Setoid.r a b → Setoid.r (id a) (id b))
If s ≤ t≤ t
, then there is a map α ⧸ s → α ⧸ t⧸ s → α ⧸ t→ α ⧸ t⧸ t
.
Equations
- Subgroup.quotientMapOfLe h = Quotient.map' id (_ : ∀ (a b : α), Setoid.r a b → Setoid.r (id a) (id b))
Equations
- One or more equations did not get rendered due to their size.
The natural embedding
H ⧸ (⨅ i, f i).addSubgroupOf H) ↪ Π i, H ⧸ (f i).addSubgroupOf H⧸ (⨅ i, f i).addSubgroupOf H) ↪ Π i, H ⧸ (f i).addSubgroupOf H⨅ i, f i).addSubgroupOf H) ↪ Π i, H ⧸ (f i).addSubgroupOf H↪ Π i, H ⧸ (f i).addSubgroupOf H⧸ (f i).addSubgroupOf H
.
Equations
- One or more equations did not get rendered due to their size.
The natural embedding H ⧸ (⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H⧸ (⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H↪ Π i, H ⧸ (f i).subgroupOf H⧸ (f i).subgroupOf H
.
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 embedding α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i⨅ i, f i) ↪ Π i, α ⧸ f i↪ Π i, α ⧸ f i⧸ f i
.
Equations
- One or more equations did not get rendered due to their size.
The natural embedding α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i⨅ i, f i) ↪ Π i, α ⧸ f i↪ Π i, α ⧸ f i⧸ f i
.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
If s
is a subgroup of the additive group α
, and t
is a subset of α ⧸ s⧸ s
, then
there is a (typically non-canonical) bijection between the preimage of t
in α
and the product
s × t× t
.
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
- (_ : -Quotient.out' ↑↑a + ↑a ∈ s) = (_ : -Quotient.out' ↑↑a + ↑a ∈ s)
Equations
- (_ : ↑(Quotient.out' ↑a.snd + ↑a.fst) ∈ t) = (_ : ↑(Quotient.out' ↑a.snd + ↑a.fst) ∈ t)
Equations
- QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_1 s t motive x h_1 = Subtype.casesOn x fun val property => h_1 val property
If s
is a subgroup of the group α
, and t
is a subset of α ⧸ s⧸ s
, then there is a
(typically non-canonical) bijection between the preimage of t
in α
and the product s × t× t
.
Equations
- One or more equations did not get rendered due to their size.