mathlib documentation

group_theory.coset

Cosets #

This file develops the basic theory of left and right cosets.

Main definitions #

Notation #

TODO #

Add to_additive to preimage_mk_equiv_subgroup_times_set.

source
def left_add_coset {α : Type u_1} [has_add α] (a : α) (s : set α) :
set α

The left coset a+s for an element a : α and a subset s : set α

Equations
  • a +l s = (λ (x : α), a + x) '' s
source
def left_coset {α : Type u_1} [has_mul α] (a : α) (s : set α) :
set α

The left coset a * s for an element a : α and a subset s : set α

Equations
  • a *l s = (λ (x : α), a * x) '' s
source
def right_coset {α : Type u_1} [has_mul α] (s : set α) (a : α) :
set α

The right coset s * a for an element a : α and a subset s : set α

Equations
  • s *r a = (λ (x : α), x * a) '' s
source
def right_add_coset {α : Type u_1} [has_add α] (s : set α) (a : α) :
set α

The right coset s+a for an element a : α and a subset s : set α

Equations
  • s +r a = (λ (x : α), x + a) '' s
source
theorem mem_left_coset {α : Type u_1} [has_mul α] {s : set α} {x : α} (a : α) (hxS : x ∈ s) :
a * x ∈ a *l s
source
theorem mem_left_add_coset {α : Type u_1} [has_add α] {s : set α} {x : α} (a : α) (hxS : x ∈ s) :
a + x ∈ a +l s
source
theorem mem_right_coset {α : Type u_1} [has_mul α] {s : set α} {x : α} (a : α) (hxS : x ∈ s) :
x * a ∈ s *r a
source
theorem mem_right_add_coset {α : Type u_1} [has_add α] {s : set α} {x : α} (a : α) (hxS : x ∈ s) :
x + a ∈ s +r a
source
def left_coset_equivalence {α : Type u_1} [has_mul α] (s : set α) (a b : α) :
Prop

Equality of two left cosets a * s and b * s.

Equations
source
def left_add_coset_equivalence {α : Type u_1} [has_add α] (s : set α) (a b : α) :
Prop

Equality of two left cosets a + s and b + s.

Equations
source
theorem left_add_coset_equivalence_rel {α : Type u_1} [has_add α] (s : set α) :
equivalence (left_add_coset_equivalence s)
source
theorem left_coset_equivalence_rel {α : Type u_1} [has_mul α] (s : set α) :
equivalence (left_coset_equivalence s)
source
def right_coset_equivalence {α : Type u_1} [has_mul α] (s : set α) (a b : α) :
Prop

Equality of two right cosets s * a and s * b.

Equations
source
def right_add_coset_equivalence {α : Type u_1} [has_add α] (s : set α) (a b : α) :
Prop

Equality of two right cosets s + a and s + b.

Equations
source
theorem right_add_coset_equivalence_rel {α : Type u_1} [has_add α] (s : set α) :
equivalence (right_add_coset_equivalence s)
source
theorem right_coset_equivalence_rel {α : Type u_1} [has_mul α] (s : set α) :
equivalence (right_coset_equivalence s)
source
@[simp]
theorem left_add_coset_assoc {α : Type u_1} [add_semigroup α] (s : set α) (a b : α) :
a +l (b +l s) = (a + b) +l s
source
@[simp]
theorem left_coset_assoc {α : Type u_1} [semigroup α] (s : set α) (a b : α) :
a *l (b *l s) = a * b *l s
source
@[simp]
theorem right_coset_assoc {α : Type u_1} [semigroup α] (s : set α) (a b : α) :
s *r a *r b = s *r a * b
source
@[simp]
theorem right_add_coset_assoc {α : Type u_1} [add_semigroup α] (s : set α) (a b : α) :
s +r a +r b = s +r (a + b)
source
theorem left_coset_right_coset {α : Type u_1} [semigroup α] (s : set α) (a b : α) :
a *l s *r b = a *l (s *r b)
source
theorem left_add_coset_right_add_coset {α : Type u_1} [add_semigroup α] (s : set α) (a b : α) :
a +l s +r b = a +l (s +r b)
source
@[simp]
theorem zero_left_add_coset {α : Type u_1} [add_monoid α] (s : set α) :
0 +l s = s
source
@[simp]
theorem one_left_coset {α : Type u_1} [monoid α] (s : set α) :
1 *l s = s
source
@[simp]
theorem right_add_coset_zero {α : Type u_1} [add_monoid α] (s : set α) :
s +r 0 = s
source
@[simp]
theorem right_coset_one {α : Type u_1} [monoid α] (s : set α) :
s *r 1 = s
source
theorem mem_own_left_coset {α : Type u_1} [monoid α] (s : submonoid α) (a : α) :
a ∈ a *l ↑s
source
theorem mem_own_left_add_coset {α : Type u_1} [add_monoid α] (s : add_submonoid α) (a : α) :
a ∈ a +l ↑s
source
theorem mem_own_right_coset {α : Type u_1} [monoid α] (s : submonoid α) (a : α) :
a ∈ ↑s *r a
source
theorem mem_own_right_add_coset {α : Type u_1} [add_monoid α] (s : add_submonoid α) (a : α) :
a ∈ ↑s +r a
source
theorem mem_left_add_coset_left_add_coset {α : Type u_1} [add_monoid α] (s : add_submonoid α) {a : α} (ha : a +l ↑s = ↑s) :
a ∈ s
source
theorem mem_left_coset_left_coset {α : Type u_1} [monoid α] (s : submonoid α) {a : α} (ha : a *l ↑s = ↑s) :
a ∈ s
source
theorem mem_right_coset_right_coset {α : Type u_1} [monoid α] (s : submonoid α) {a : α} (ha : ↑s *r a = ↑s) :
a ∈ s
source
theorem mem_right_add_coset_right_add_coset {α : Type u_1} [add_monoid α] (s : add_submonoid α) {a : α} (ha : ↑s +r a = ↑s) :
a ∈ s
source
theorem mem_left_add_coset_iff {α : Type u_1} [add_group α] {s : set α} {x : α} (a : α) :
x ∈ a +l s ↔ -a + x ∈ s
source
theorem mem_left_coset_iff {α : Type u_1} [group α] {s : set α} {x : α} (a : α) :
x ∈ a *l s ↔ a⁻¹ * x ∈ s
source
theorem mem_right_coset_iff {α : Type u_1} [group α] {s : set α} {x : α} (a : α) :
x ∈ s *r a ↔ x * a⁻¹ ∈ s
source
theorem mem_right_add_coset_iff {α : Type u_1} [add_group α] {s : set α} {x : α} (a : α) :
x ∈ s +r a ↔ x + -a ∈ s
source
theorem left_coset_mem_left_coset {α : Type u_1} [group α] (s : subgroup α) {a : α} (ha : a ∈ s) :
a *l ↑s = ↑s
source
theorem left_add_coset_mem_left_add_coset {α : Type u_1} [add_group α] (s : add_subgroup α) {a : α} (ha : a ∈ s) :
a +l ↑s = ↑s
source
theorem right_coset_mem_right_coset {α : Type u_1} [group α] (s : subgroup α) {a : α} (ha : a ∈ s) :
↑s *r a = ↑s
source
theorem right_add_coset_mem_right_add_coset {α : Type u_1} [add_group α] (s : add_subgroup α) {a : α} (ha : a ∈ s) :
↑s +r a = ↑s
source
theorem eq_cosets_of_normal {α : Type u_1} [group α] (s : subgroup α) (N : s.normal) (g : α) :
g *l ↑s = ↑s *r g
source
theorem eq_add_cosets_of_normal {α : Type u_1} [add_group α] (s : add_subgroup α) (N : s.normal) (g : α) :
g +l ↑s = ↑s +r g
source
theorem normal_of_eq_cosets {α : Type u_1} [group α] (s : subgroup α) (h : ∀ (g : α), g *l ↑s = ↑s *r g) :
s.normal
source
theorem normal_of_eq_add_cosets {α : Type u_1} [add_group α] (s : add_subgroup α) (h : ∀ (g : α), g +l ↑s = ↑s +r g) :
s.normal
source
theorem normal_iff_eq_add_cosets {α : Type u_1} [add_group α] (s : add_subgroup α) :
s.normal ↔ ∀ (g : α), g +l ↑s = ↑s +r g
source
theorem normal_iff_eq_cosets {α : Type u_1} [group α] (s : subgroup α) :
s.normal ↔ ∀ (g : α), g *l ↑s = ↑s *r g
source
theorem left_add_coset_eq_iff {α : Type u_1} [add_group α] (s : add_subgroup α) {x y : α} :
x +l ↑s = y +l ↑s ↔ -x + y ∈ s
source
theorem left_coset_eq_iff {α : Type u_1} [group α] (s : subgroup α) {x y : α} :
x *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ s
source
theorem right_coset_eq_iff {α : Type u_1} [group α] (s : subgroup α) {x y : α} :
↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ s
source
theorem right_add_coset_eq_iff {α : Type u_1} [add_group α] (s : add_subgroup α) {x y : α} :
↑s +r x = ↑s +r y ↔ y + -x ∈ s
source
def quotient_add_group.left_rel {α : Type u_1} [add_group α] (s : add_subgroup α) :
setoid α

The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.

Equations
source
def quotient_group.left_rel {α : Type u_1} [group α] (s : subgroup α) :
setoid α

The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.

Equations
source
theorem quotient_group.left_rel_r_eq_left_coset_equivalence {α : Type u_1} [group α] (s : subgroup α) :
setoid.r = left_coset_equivalence ↑s
source
@[protected, instance]
def quotient_group.left_rel_decidable {α : Type u_1} [group α] (s : subgroup α) [decidable_pred (λ (_x : α), _x ∈ s)] :
decidable_rel setoid.r
Equations
source
@[protected, instance]
def quotient_add_group.left_rel_decidable {α : Type u_1} [add_group α] (s : add_subgroup α) [decidable_pred (λ (_x : α), _x ∈ s)] :
decidable_rel setoid.r
Equations
source
@[protected, instance]
def quotient_add_group.subgroup.has_quotient {α : Type u_1} [add_group α] :
has_quotient α (add_subgroup α)

α ⧸ s is the quotient type representing the left cosets of s. If s is a normal subgroup, α ⧸ s is a group

Equations
source
@[protected, instance]
def quotient_group.subgroup.has_quotient {α : Type u_1} [group α] :
has_quotient α (subgroup α)

α ⧸ s is the quotient type representing the left cosets of s. If s is a normal subgroup, α ⧸ s is a group

Equations
source
def quotient_group.right_rel {α : Type u_1} [group α] (s : subgroup α) :
setoid α

The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.

Equations
source
def quotient_add_group.right_rel {α : Type u_1} [add_group α] (s : add_subgroup α) :
setoid α

The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.

Equations
source
theorem quotient_group.right_rel_r_eq_right_coset_equivalence {α : Type u_1} [group α] (s : subgroup α) :
setoid.r = right_coset_equivalence ↑s
source
@[protected, instance]
def quotient_group.right_rel_decidable {α : Type u_1} [group α] (s : subgroup α) [decidable_pred (λ (_x : α), _x ∈ s)] :
decidable_rel setoid.r
Equations
source
@[protected, instance]
def quotient_add_group.right_rel_decidable {α : Type u_1} [add_group α] (s : add_subgroup α) [decidable_pred (λ (_x : α), _x ∈ s)] :
decidable_rel setoid.r
Equations
source
def quotient_group.quotient_right_rel_equiv_quotient_left_rel {α : Type u_1} [group α] (s : subgroup α) :
quotient (quotient_group.right_rel s) ≃ α ⧸ s

Right cosets are in bijection with left cosets.

Equations
source
def quotient_add_group.quotient_right_rel_equiv_quotient_left_rel {α : Type u_1} [add_group α] (s : add_subgroup α) :
quotient (quotient_add_group.right_rel s) ≃ α ⧸ s

Right cosets are in bijection with left cosets.

Equations
source
@[protected, instance]
def quotient_group.fintype_quotient_right_rel {α : Type u_1} [group α] (s : subgroup α) [fintype (α ⧸ s)] :
fintype (quotient (quotient_group.right_rel s))
Equations
source
@[protected, instance]
def quotient_add_group.fintype_quotient_right_rel {α : Type u_1} [add_group α] (s : add_subgroup α) [fintype (α ⧸ s)] :
fintype (quotient (quotient_add_group.right_rel s))
Equations
source
theorem quotient_group.card_quotient_right_rel {α : Type u_1} [group α] (s : subgroup α) [fintype (α ⧸ s)] :
fintype.card (quotient (quotient_group.right_rel s)) = fintype.card (α ⧸ s)
source
theorem quotient_add_group.card_quotient_right_rel {α : Type u_1} [add_group α] (s : add_subgroup α) [fintype (α ⧸ s)] :
fintype.card (quotient (quotient_add_group.right_rel s)) = fintype.card (α ⧸ s)
source
@[protected, instance]
def quotient_group.fintype {α : Type u_1} [group α] [fintype α] (s : subgroup α) [decidable_rel setoid.r] :
fintype (α ⧸ s)
Equations
source
@[protected, instance]
def quotient_add_group.fintype {α : Type u_1} [add_group α] [fintype α] (s : add_subgroup α) [decidable_rel setoid.r] :
fintype (α ⧸ s)
Equations
source
def quotient_add_group.mk {α : Type u_1} [add_group α] {s : add_subgroup α} (a : α) :
α ⧸ s

The canonical map from an add_group α to the quotient α ⧸ s.

source
def quotient_group.mk {α : Type u_1} [group α] {s : subgroup α} (a : α) :
α ⧸ s

The canonical map from a group α to the quotient α ⧸ s.

source
theorem quotient_add_group.mk_surjective {α : Type u_1} [add_group α] {s : add_subgroup α} :
function.surjective quotient_add_group.mk
source
theorem quotient_group.mk_surjective {α : Type u_1} [group α] {s : subgroup α} :
function.surjective quotient_group.mk
source
theorem quotient_group.induction_on {α : Type u_1} [group α] {s : subgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ (z : α), C (quotient_group.mk z)) :
C x
source
theorem quotient_add_group.induction_on {α : Type u_1} [add_group α] {s : add_subgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ (z : α), C (quotient_add_group.mk z)) :
C x
source
@[protected, instance]
def quotient_add_group.has_quotient.quotient.has_coe_t {α : Type u_1} [add_group α] {s : add_subgroup α} :
has_coe_t α (α ⧸ s)
Equations
source
@[protected, instance]
def quotient_group.has_quotient.quotient.has_coe_t {α : Type u_1} [group α] {s : subgroup α} :
has_coe_t α (α ⧸ s)
Equations
source
theorem quotient_add_group.induction_on' {α : Type u_1} [add_group α] {s : add_subgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ (z : α), C ↑z) :
C x
source
theorem quotient_group.induction_on' {α : Type u_1} [group α] {s : subgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ (z : α), C ↑z) :
C x
source
@[simp]
theorem quotient_add_group.quotient_lift_on_coe {α : Type u_1} [add_group α] {s : add_subgroup α} {β : Sort u_2} (f : α → β) (h : ∀ (a b : α), setoid.r a b → f a = f b) (x : α) :
quotient.lift_on' ↑x f h = f x
source
@[simp]
theorem quotient_group.quotient_lift_on_coe {α : Type u_1} [group α] {s : subgroup α} {β : Sort u_2} (f : α → β) (h : ∀ (a b : α), setoid.r a b → f a = f b) (x : α) :
quotient.lift_on' ↑x f h = f x
source
theorem quotient_add_group.forall_coe {α : Type u_1} [add_group α] {s : add_subgroup α} {C : α ⧸ s → Prop} :
(∀ (x : α ⧸ s), C x) ↔ ∀ (x : α), C ↑x
source
theorem quotient_group.forall_coe {α : Type u_1} [group α] {s : subgroup α} {C : α ⧸ s → Prop} :
(∀ (x : α ⧸ s), C x) ↔ ∀ (x : α), C ↑x
source
@[protected, instance]
def quotient_add_group.has_quotient.quotient.inhabited {α : Type u_1} [add_group α] (s : add_subgroup α) :
inhabited (α ⧸ s)
Equations
source
@[protected, instance]
def quotient_group.has_quotient.quotient.inhabited {α : Type u_1} [group α] (s : subgroup α) :
inhabited (α ⧸ s)
Equations
source
@[protected]
theorem quotient_add_group.eq {α : Type u_1} [add_group α] {s : add_subgroup α} {a b : α} :
↑a = ↑b ↔ -a + b ∈ s
source
@[protected]
theorem quotient_group.eq {α : Type u_1} [group α] {s : subgroup α} {a b : α} :
↑a = ↑b ↔ a⁻¹ * b ∈ s
source
theorem quotient_add_group.eq' {α : Type u_1} [add_group α] {s : add_subgroup α} {a b : α} :
quotient_add_group.mk a = quotient_add_group.mk b ↔ -a + b ∈ s
source
theorem quotient_group.eq' {α : Type u_1} [group α] {s : subgroup α} {a b : α} :
quotient_group.mk a = quotient_group.mk b ↔ a⁻¹ * b ∈ s
source
theorem quotient_group.out_eq' {α : Type u_1} [group α] {s : subgroup α} (a : α ⧸ s) :
quotient_group.mk (quotient.out' a) = a
source
theorem quotient_add_group.out_eq' {α : Type u_1} [add_group α] {s : add_subgroup α} (a : α ⧸ s) :
quotient_add_group.mk (quotient.out' a) = a
source
theorem quotient_add_group.mk_out'_eq_mul {α : Type u_1} [add_group α] (s : add_subgroup α) (g : α) :
∃ (h : ↥s), quotient.out' (quotient_add_group.mk g) = g + ↑h
source
theorem quotient_group.mk_out'_eq_mul {α : Type u_1} [group α] (s : subgroup α) (g : α) :
∃ (h : ↥s), quotient.out' (quotient_group.mk g) = g * ↑h
source
theorem quotient_add_group.mk_mul_of_mem {α : Type u_1} [add_group α] {s : add_subgroup α} (g₁ g₂ : α) (hg₂ : g₂ ∈ s) :
quotient_add_group.mk (g₁ + g₂) = quotient_add_group.mk g₁
source
theorem quotient_group.mk_mul_of_mem {α : Type u_1} [group α] {s : subgroup α} (g₁ g₂ : α) (hg₂ : g₂ ∈ s) :
quotient_group.mk (g₁ * g₂) = quotient_group.mk g₁
source
theorem quotient_group.eq_class_eq_left_coset {α : Type u_1} [group α] (s : subgroup α) (g : α) :
{x : α | ↑x = ↑g} = g *l ↑s
source
theorem quotient_add_group.eq_class_eq_left_coset {α : Type u_1} [add_group α] (s : add_subgroup α) (g : α) :
{x : α | ↑x = ↑g} = g +l ↑s
source
theorem quotient_group.preimage_image_coe {α : Type u_1} [group α] (N : subgroup α) (s : set α) :
coe ⁻¹' (coe '' s) = ⋃ (x : ↥N), (λ (y : α), y * ↑x) ⁻¹' s
source
theorem quotient_add_group.preimage_image_coe {α : Type u_1} [add_group α] (N : add_subgroup α) (s : set α) :
coe ⁻¹' (coe '' s) = ⋃ (x : ↥N), (λ (y : α), y + ↑x) ⁻¹' s
source
def subgroup.left_coset_equiv_subgroup {α : Type u_1} [group α] {s : subgroup α} (g : α) :
↥(g *l ↑s) ≃ ↥s

The natural bijection between a left coset g * s and s.

Equations
source
def add_subgroup.left_coset_equiv_add_subgroup {α : Type u_1} [add_group α] {s : add_subgroup α} (g : α) :
↥(g +l ↑s) ≃ ↥s

The natural bijection between the cosets g + s and s.

Equations
source
def subgroup.right_coset_equiv_subgroup {α : Type u_1} [group α] {s : subgroup α} (g : α) :
↥(↑s *r g) ≃ ↥s

The natural bijection between a right coset s * g and s.

Equations
source
def add_subgroup.right_coset_equiv_add_subgroup {α : Type u_1} [add_group α] {s : add_subgroup α} (g : α) :
↥(↑s +r g) ≃ ↥s

The natural bijection between the cosets s + g and s.

Equations
source
noncomputable def subgroup.group_equiv_quotient_times_subgroup {α : Type u_1} [group α] {s : subgroup α} :
α ≃ (α ⧸ s) × ↥s

A (non-canonical) bijection between a group α and the product (α/s) × s

Equations
source
noncomputable def add_subgroup.add_group_equiv_quotient_times_add_subgroup {α : Type u_1} [add_group α] {s : add_subgroup α} :
α ≃ (α ⧸ s) × ↥s

A (non-canonical) bijection between an add_group α and the product (α/s) × s

Equations
source
@[simp]
theorem subgroup.quotient_equiv_prod_of_le'_symm_apply {α : Type u_1} [group α] {s t : subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : function.right_inverse f quotient_group.mk) (a : (α ⧸ t) × ↥t ⧸ s.subgroup_of t) :
⇑((subgroup.quotient_equiv_prod_of_le' h_le f hf).symm) a = quotient.map' (λ (b : ↥t), (f a.fst) * ↑b) _ a.snd
source
def subgroup.quotient_equiv_prod_of_le' {α : Type u_1} [group α] {s t : subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : function.right_inverse f quotient_group.mk) :
α ⧸ s ≃ (α ⧸ t) × ↥t ⧸ s.subgroup_of t

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 quotient_equiv_prod_of_le.

Equations
source
@[simp]
theorem add_subgroup.quotient_equiv_sum_of_le'_symm_apply {α : Type u_1} [add_group α] {s t : add_subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : function.right_inverse f quotient_add_group.mk) (a : (α ⧸ t) × ↥t ⧸ s.add_subgroup_of t) :
⇑((add_subgroup.quotient_equiv_sum_of_le' h_le f hf).symm) a = quotient.map' (λ (b : ↥t), f a.fst + ↑b) _ a.snd
source
@[simp]
theorem add_subgroup.quotient_equiv_sum_of_le'_apply {α : Type u_1} [add_group α] {s t : add_subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : function.right_inverse f quotient_add_group.mk) (a : α ⧸ s) :
⇑(add_subgroup.quotient_equiv_sum_of_le' h_le f hf) a = (quotient.map' id _ a, quotient.map' (λ (g : α), ⟨-f (quotient.mk' g) + g, _⟩) _ a)
source
def add_subgroup.quotient_equiv_sum_of_le' {α : Type u_1} [add_group α] {s t : add_subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : function.right_inverse f quotient_add_group.mk) :
α ⧸ s ≃ (α ⧸ t) × ↥t ⧸ s.add_subgroup_of t

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 quotient_equiv_prod_of_le.

Equations
source
@[simp]
theorem subgroup.quotient_equiv_prod_of_le'_apply {α : Type u_1} [group α] {s t : subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : function.right_inverse f quotient_group.mk) (a : α ⧸ s) :
⇑(subgroup.quotient_equiv_prod_of_le' h_le f hf) a = (quotient.map' id _ a, quotient.map' (λ (g : α), ⟨(f (quotient.mk' g))⁻¹ * g, _⟩) _ a)
source
@[simp]
theorem subgroup.quotient_equiv_prod_of_le_symm_apply {α : Type u_1} [group α] {s t : subgroup α} (h_le : s ≤ t) (a : (α ⧸ t) × ↥t ⧸ s.subgroup_of t) :
⇑((subgroup.quotient_equiv_prod_of_le h_le).symm) a = quotient.map' (λ (b : ↥t), (quotient.out' a.fst) * ↑b) _ a.snd
source
noncomputable def add_subgroup.quotient_equiv_sum_of_le {α : Type u_1} [add_group α] {s t : add_subgroup α} (h_le : s ≤ t) :
α ⧸ s ≃ (α ⧸ t) × ↥t ⧸ s.add_subgroup_of t

If H ≤ K, then G/H ≃ G/K × K/H nonconstructively. The constructive version is quotient_equiv_prod_of_le'.

Equations
source
@[simp]
theorem add_subgroup.quotient_equiv_sum_of_le_apply {α : Type u_1} [add_group α] {s t : add_subgroup α} (h_le : s ≤ t) (a : α ⧸ s) :
⇑(add_subgroup.quotient_equiv_sum_of_le h_le) a = (quotient.map' id _ a, quotient.map' (λ (g : α), ⟨-(quotient.mk' g).out' + g, _⟩) _ a)
source
@[simp]
theorem add_subgroup.quotient_equiv_sum_of_le_symm_apply {α : Type u_1} [add_group α] {s t : add_subgroup α} (h_le : s ≤ t) (a : (α ⧸ t) × ↥t ⧸ s.add_subgroup_of t) :
⇑((add_subgroup.quotient_equiv_sum_of_le h_le).symm) a = quotient.map' (λ (b : ↥t), quotient.out' a.fst + ↑b) _ a.snd
source
noncomputable def subgroup.quotient_equiv_prod_of_le {α : Type u_1} [group α] {s t : subgroup α} (h_le : s ≤ t) :
α ⧸ s ≃ (α ⧸ t) × ↥t ⧸ s.subgroup_of t

If H ≤ K, then G/H ≃ G/K × K/H nonconstructively. The constructive version is quotient_equiv_prod_of_le'.

Equations
source
@[simp]
theorem subgroup.quotient_equiv_prod_of_le_apply {α : Type u_1} [group α] {s t : subgroup α} (h_le : s ≤ t) (a : α ⧸ s) :
⇑(subgroup.quotient_equiv_prod_of_le h_le) a = (quotient.map' id _ a, quotient.map' (λ (g : α), ⟨((quotient.mk' g).out')⁻¹ * g, _⟩) _ a)
source
def add_subgroup.quotient_add_subgroup_of_embedding_of_le {α : Type u_1} [add_group α] (H : add_subgroup α) {K L : add_subgroup α} (h : K ≤ L) :
↥K ⧸ H.add_subgroup_of K ↪ ↥L ⧸ H.add_subgroup_of L

If K ≤ L, then there is an embedding K ⧸ (H.add_subgroup_of K) ↪ L ⧸ (H.add_subgroup_of L).

Equations
source
def subgroup.quotient_subgroup_of_embedding_of_le {α : Type u_1} [group α] (H : subgroup α) {K L : subgroup α} (h : K ≤ L) :
↥K ⧸ H.subgroup_of K ↪ ↥L ⧸ H.subgroup_of L

If K ≤ L, then there is an embedding K ⧸ (H.subgroup_of K) ↪ L ⧸ (H.subgroup_of L).

Equations
source
theorem add_subgroup.card_eq_card_quotient_add_card_add_subgroup {α : Type u_1} [add_group α] [fintype α] (s : add_subgroup α) [fintype ↥s] [decidable_pred (λ (a : α), a ∈ s)] :
fintype.card α = (fintype.card (α ⧸ s)) * fintype.card ↥s
source
theorem subgroup.card_eq_card_quotient_mul_card_subgroup {α : Type u_1} [group α] [fintype α] (s : subgroup α) [fintype ↥s] [decidable_pred (λ (a : α), a ∈ s)] :
fintype.card α = (fintype.card (α ⧸ s)) * fintype.card ↥s
source
theorem add_subgroup.card_add_subgroup_dvd_card {α : Type u_1} [add_group α] [fintype α] (s : add_subgroup α) [fintype ↥s] :
fintype.card ↥s ∣ fintype.card α
source
theorem subgroup.card_subgroup_dvd_card {α : Type u_1} [group α] [fintype α] (s : subgroup α) [fintype ↥s] :
fintype.card ↥s ∣ fintype.card α

Lagrange's Theorem: The order of a subgroup divides the order of its ambient group.

source
theorem subgroup.card_quotient_dvd_card {α : Type u_1} [group α] [fintype α] (s : subgroup α) [decidable_pred (λ (a : α), a ∈ s)] [fintype ↥s] :
fintype.card (α ⧸ s) ∣ fintype.card α
source
theorem add_subgroup.card_quotient_dvd_card {α : Type u_1} [add_group α] [fintype α] (s : add_subgroup α) [decidable_pred (λ (a : α), a ∈ s)] [fintype ↥s] :
fintype.card (α ⧸ s) ∣ fintype.card α
source
theorem add_subgroup.card_dvd_of_injective {α : Type u_1} [add_group α] {H : Type u_2} [add_group H] [fintype α] [fintype H] (f : α →+ H) (hf : function.injective ⇑f) :
fintype.card α ∣ fintype.card H
source
theorem subgroup.card_dvd_of_injective {α : Type u_1} [group α] {H : Type u_2} [group H] [fintype α] [fintype H] (f : α →* H) (hf : function.injective ⇑f) :
fintype.card α ∣ fintype.card H
source
theorem subgroup.card_dvd_of_le {α : Type u_1} [group α] {H K : subgroup α} [fintype ↥H] [fintype ↥K] (hHK : H ≤ K) :
fintype.card ↥H ∣ fintype.card ↥K
source
theorem add_subgroup.card_dvd_of_le {α : Type u_1} [add_group α] {H K : add_subgroup α} [fintype ↥H] [fintype ↥K] (hHK : H ≤ K) :
fintype.card ↥H ∣ fintype.card ↥K
source
theorem subgroup.card_comap_dvd_of_injective {α : Type u_1} [group α] {H : Type u_2} [group H] (K : subgroup H) [fintype ↥K] (f : α →* H) [fintype ↥(subgroup.comap f K)] (hf : function.injective ⇑f) :
fintype.card ↥(subgroup.comap f K) ∣ fintype.card ↥K
source
theorem add_subgroup.card_comap_dvd_of_injective {α : Type u_1} [add_group α] {H : Type u_2} [add_group H] (K : add_subgroup H) [fintype ↥K] (f : α →+ H) [fintype ↥(add_subgroup.comap f K)] (hf : function.injective ⇑f) :
fintype.card ↥(add_subgroup.comap f K) ∣ fintype.card ↥K
source
noncomputable def quotient_group.preimage_mk_equiv_subgroup_times_set {α : Type u_1} [group α] (s : subgroup α) (t : set (α ⧸ s)) :
↥(quotient_group.mk ⁻¹' t) ≃ ↥s × ↥t

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