Cosets #
This file develops the basic theory of left and right cosets.
Main definitions #
left_coset a s
: the left coseta * s
for an elementa : α
and a subsets ⊆ α
, for anadd_group
this isleft_add_coset a s
.right_coset s a
: the right cosets * a
for an elementa : α
and a subsets ⊆ α
, for anadd_group
this isright_add_coset s a
.quotient_group.quotient s
: the quotient type representing the left cosets with respect to a subgroups
, for anadd_group
this isquotient_add_group.quotient s
.quotient_group.mk
: the canonical map fromα
toα/s
for a subgroups
ofα
, for anadd_group
this isquotient_add_group.mk
.subgroup.left_coset_equiv_subgroup
: the natural bijection between a left coset and the subgroup, for anadd_group
this isadd_subgroup.left_coset_equiv_add_subgroup
.
Notation #
a *l s
: forleft_coset a s
.a +l s
: forleft_add_coset a s
.s *r a
: forright_coset s a
.s +r a
: forright_add_coset s a
.
TODO #
Add to_additive
to preimage_mk_equiv_subgroup_times_set
.
Equality of two left cosets a * s
and b * s
.
Equations
- left_coset_equivalence s a b = (a *l s = b *l s)
Equality of two left cosets a + s
and b + s
.
Equality of two right cosets s * a
and s * b
.
Equations
- right_coset_equivalence s a b = (s *r a = s *r b)
Equality of two right cosets s + a
and s + b
.
The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.
Equations
- quotient_group.left_rel_decidable s = λ (_x _x_1 : α), d (_x⁻¹ * _x_1)
The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.
Equations
- quotient_group.right_rel_decidable s = λ (_x _x_1 : α), d (_x⁻¹ * _x_1)
Equations
The canonical map from an add_group
α
to the quotient α/s
.
The canonical map from a group α
to the quotient α/s
.
Equations
Equations
The natural bijection between a left coset g * s
and s
.
The natural bijection between the cosets g + s
and s
.
The natural bijection between a right coset s * g
and s
.
The natural bijection between the cosets s + g
and s
.
A (non-canonical) bijection between a group α
and the product (α/s) × s
Equations
- subgroup.group_equiv_quotient_times_subgroup = (((equiv.sigma_preimage_equiv quotient_group.mk).symm.trans (equiv.sigma_congr_right (λ (L : quotient_group.quotient s), _.mpr (id (_.mpr (equiv.refl {x // quotient.mk' x = L})))))).trans (equiv.sigma_congr_right (λ (L : quotient_group.quotient s), subgroup.left_coset_equiv_subgroup (quotient.out' L)))).trans (equiv.sigma_equiv_prod (quotient_group.quotient s) ↥s)
A (non-canonical) bijection between an add_group α
and the product (α/s) × s
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
- quotient_group.preimage_mk_equiv_subgroup_times_set s t = have h : ∀ {x : quotient_group.quotient s} {a : α}, x ∈ t → a ∈ s → quotient.mk' ((quotient.out' x) * a) = quotient.mk' (quotient.out' x), from _, {to_fun := λ (_x : ↥(quotient_group.mk ⁻¹' t)), quotient_group.preimage_mk_equiv_subgroup_times_set._match_1 s t _x, inv_fun := λ (_x : ↥s × ↥t), quotient_group.preimage_mk_equiv_subgroup_times_set._match_2 s t h _x, left_inv := _, right_inv := _}
- quotient_group.preimage_mk_equiv_subgroup_times_set._match_1 s t ⟨a, ha⟩ = (⟨((quotient.mk' a).out')⁻¹ * a, _⟩, ⟨quotient.mk' a, ha⟩)
- quotient_group.preimage_mk_equiv_subgroup_times_set._match_2 s t h (⟨a, ha⟩, ⟨x, hx⟩) = ⟨(quotient.out' x) * a, _⟩