Double cosets #
This file defines double cosets for two subgroups H K
of a group G
and the quotient of G
by
the double coset relation, i.e. H \ G / K
. We also prove that G
can be written as a disjoint
union of the double cosets and that if one of H
or K
is the trivial group (i.e. ⊥
) then
this is the usual left or right quotient of a group by a subgroup.
Main definitions #
rel
: The double coset relation defined by two subgroupsH K
ofG
.Doset.quotient
: The quotient ofG
by the double coset relation, i.e,H \ G / K
.
theorem
Doset.doset_eq_image2
{α : Type u_2}
[Mul α]
(a : α)
(s : Set α)
(t : Set α)
:
Doset.doset a s t = Set.image2 (fun (x1 x2 : α) => x1 * a * x2) s t
theorem
Doset.mem_doset_self
{G : Type u_1}
[Group G]
(H : Subgroup G)
(K : Subgroup G)
(a : G)
:
a ∈ Doset.doset a ↑H ↑K
theorem
Doset.doset_eq_of_mem
{G : Type u_1}
[Group G]
{H : Subgroup G}
{K : Subgroup G}
{a : G}
{b : G}
(hb : b ∈ Doset.doset a ↑H ↑K)
:
Doset.doset b ↑H ↑K = Doset.doset a ↑H ↑K
theorem
Doset.mem_doset_of_not_disjoint
{G : Type u_1}
[Group G]
{H : Subgroup G}
{K : Subgroup G}
{a : G}
{b : G}
(h : ¬Disjoint (Doset.doset a ↑H ↑K) (Doset.doset b ↑H ↑K))
:
b ∈ Doset.doset a ↑H ↑K
theorem
Doset.eq_of_not_disjoint
{G : Type u_1}
[Group G]
{H : Subgroup G}
{K : Subgroup G}
{a : G}
{b : G}
(h : ¬Disjoint (Doset.doset a ↑H ↑K) (Doset.doset b ↑H ↑K))
:
Doset.doset a ↑H ↑K = Doset.doset b ↑H ↑K
The setoid defined by the double_coset relation
Equations
- Doset.setoid H K = Setoid.ker fun (x : G) => Doset.doset x H K
Instances For
Quotient of G
by the double coset relation, i.e. H \ G / K
Equations
- Doset.Quotient H K = Quotient (Doset.setoid H K)
Instances For
theorem
Doset.bot_rel_eq_leftRel
{G : Type u_1}
[Group G]
(H : Subgroup G)
:
(Doset.setoid ↑⊥ ↑H).Rel = (QuotientGroup.leftRel H).Rel
theorem
Doset.rel_bot_eq_right_group_rel
{G : Type u_1}
[Group G]
(H : Subgroup G)
:
(Doset.setoid ↑H ↑⊥).Rel = (QuotientGroup.rightRel H).Rel
def
Doset.quotToDoset
{G : Type u_1}
[Group G]
(H : Subgroup G)
(K : Subgroup G)
(q : Doset.Quotient ↑H ↑K)
:
Set G
Create a doset out of an element of H \ G / K
Equations
- Doset.quotToDoset H K q = Doset.doset (Quotient.out' q) ↑H ↑K
Instances For
@[reducible, inline]
abbrev
Doset.mk
{G : Type u_1}
[Group G]
(H : Subgroup G)
(K : Subgroup G)
(a : G)
:
Doset.Quotient ↑H ↑K
Map from G
to H \ G / K
Equations
- Doset.mk H K a = Quotient.mk'' a
Instances For
instance
Doset.instInhabitedQuotientCoeSubgroup
{G : Type u_1}
[Group G]
(H : Subgroup G)
(K : Subgroup G)
:
Inhabited (Doset.Quotient ↑H ↑K)
Equations
- Doset.instInhabitedQuotientCoeSubgroup H K = { default := Doset.mk H K 1 }
theorem
Doset.out_eq'
{G : Type u_1}
[Group G]
(H : Subgroup G)
(K : Subgroup G)
(q : Doset.Quotient ↑H ↑K)
:
Doset.mk H K (Quotient.out' q) = q
theorem
Doset.mk_eq_of_doset_eq
{G : Type u_1}
[Group G]
{H : Subgroup G}
{K : Subgroup G}
{a : G}
{b : G}
(h : Doset.doset a ↑H ↑K = Doset.doset b ↑H ↑K)
:
theorem
Doset.disjoint_out'
{G : Type u_1}
[Group G]
{H : Subgroup G}
{K : Subgroup G}
{a : Doset.Quotient ↑H ↑K}
{b : Doset.Quotient ↑H ↑K}
:
a ≠ b → Disjoint (Doset.doset (Quotient.out' a) ↑H ↑K) (Doset.doset (Quotient.out' b) ↑H ↑K)
theorem
Doset.union_quotToDoset
{G : Type u_1}
[Group G]
(H : Subgroup G)
(K : Subgroup G)
:
⋃ (q : Doset.Quotient ↑H ↑K), Doset.quotToDoset H K q = Set.univ
theorem
Doset.doset_union_rightCoset
{G : Type u_1}
[Group G]
(H : Subgroup G)
(K : Subgroup G)
(a : G)
:
⋃ (k : ↥K), MulOpposite.op (a * ↑k) • ↑H = Doset.doset a ↑H ↑K
theorem
Doset.doset_union_leftCoset
{G : Type u_1}
[Group G]
(H : Subgroup G)
(K : Subgroup G)
(a : G)
:
⋃ (h : ↥H), (↑h * a) • ↑K = Doset.doset a ↑H ↑K
theorem
Doset.left_bot_eq_left_quot
{G : Type u_1}
[Group G]
(H : Subgroup G)
:
Doset.Quotient ↑⊥ ↑H = (G ⧸ H)
theorem
Doset.right_bot_eq_right_quot
{G : Type u_1}
[Group G]
(H : Subgroup G)
:
Doset.Quotient ↑H ↑⊥ = Quotient (QuotientGroup.rightRel H)