mathlib documentation

group_theory.coset

def left_add_coset {α : Type u_1} [has_add α] :
α → set αset α

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

def left_coset {α : Type u_1} [has_mul α] :
α → set αset α

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

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

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

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

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

theorem mem_left_coset {α : Type u_1} [has_mul α] {s : set α} {x : α} (a : α) :
x sa * x a *l s

theorem mem_left_add_coset {α : Type u_1} [has_add α] {s : set α} {x : α} (a : α) :
x sa + x a +l s

theorem mem_right_coset {α : Type u_1} [has_mul α] {s : set α} {x : α} (a : α) :
x sx * a s *r a

theorem mem_right_add_coset {α : Type u_1} [has_add α] {s : set α} {x : α} (a : α) :
x sx + a s +r a

def left_coset_equiv {α : Type u_1} [has_mul α] :
set αα → α → Prop

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

Equations
def left_add_coset_equiv {α : Type u_1} [has_add α] :
set αα → α → Prop

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

theorem left_coset_equiv_rel {α : Type u_1} [has_mul α] (s : set α) :

theorem left_add_coset_equiv_rel {α : Type u_1} [has_add α] (s : set α) :

@[simp]
theorem left_coset_assoc {α : Type u_1} [semigroup α] (s : set α) (a b : α) :
a *l (b *l s) = a * b *l s

@[simp]
theorem right_coset_assoc {α : Type u_1} [semigroup α] (s : set α) (a b : α) :
s *r a *r b = s *r a * b

theorem left_coset_right_coset {α : Type u_1} [semigroup α] (s : set α) (a b : α) :
a *l s *r b = a *l (s *r b)

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)

@[simp]
theorem one_left_coset {α : Type u_1} [monoid α] (s : set α) :
1 *l s = s

@[simp]
theorem right_coset_one {α : Type u_1} [monoid α] (s : set α) :
s *r 1 = s

theorem mem_own_left_coset {α : Type u_1} [monoid α] (s : submonoid α) (a : α) :
a a *l s

theorem mem_own_left_add_coset {α : Type u_1} [add_monoid α] (s : add_submonoid α) (a : α) :
a a +l s

theorem mem_own_right_coset {α : Type u_1} [monoid α] (s : submonoid α) (a : α) :
a s *r a

theorem mem_own_right_add_coset {α : Type u_1} [add_monoid α] (s : add_submonoid α) (a : α) :
a s +r a

theorem mem_left_add_coset_left_add_coset {α : Type u_1} [add_monoid α] (s : add_submonoid α) {a : α} :
a +l s = sa s

theorem mem_left_coset_left_coset {α : Type u_1} [monoid α] (s : submonoid α) {a : α} :
a *l s = sa s

theorem mem_right_coset_right_coset {α : Type u_1} [monoid α] (s : submonoid α) {a : α} :
s *r a = sa s

theorem mem_right_add_coset_right_add_coset {α : Type u_1} [add_monoid α] (s : add_submonoid α) {a : α} :
s +r a = sa s

theorem mem_left_add_coset_iff {α : Type u_1} [add_group α] {s : set α} {x : α} (a : α) :
x a +l s -a + x s

theorem mem_left_coset_iff {α : Type u_1} [group α] {s : set α} {x : α} (a : α) :
x a *l s a⁻¹ * x s

theorem mem_right_coset_iff {α : Type u_1} [group α] {s : set α} {x : α} (a : α) :
x s *r a x * a⁻¹ s

theorem mem_right_add_coset_iff {α : Type u_1} [add_group α] {s : set α} {x : α} (a : α) :
x s +r a x + -a s

theorem left_coset_mem_left_coset {α : Type u_1} [group α] (s : subgroup α) {a : α} :
a sa *l s = s

theorem left_add_coset_mem_left_add_coset {α : Type u_1} [add_group α] (s : add_subgroup α) {a : α} :
a sa +l s = s

theorem right_coset_mem_right_coset {α : Type u_1} [group α] (s : subgroup α) {a : α} :
a ss *r a = s

theorem right_add_coset_mem_right_add_coset {α : Type u_1} [add_group α] (s : add_subgroup α) {a : α} :
a ss +r a = s

theorem normal_of_eq_cosets {α : Type u_1} [group α] (s : subgroup α) (N : s.normal) (g : α) :
g *l s = s *r g

theorem normal_of_eq_add_cosets {α : Type u_1} [add_group α] (s : add_subgroup α) (N : s.normal) (g : α) :
g +l s = s +r g

theorem eq_cosets_of_normal {α : Type u_1} [group α] (s : subgroup α) :
(∀ (g : α), g *l s = s *r g) → s.normal

theorem eq_add_cosets_of_normal {α : Type u_1} [add_group α] (s : add_subgroup α) :
(∀ (g : α), g +l s = s +r g) → s.normal

theorem normal_iff_eq_add_cosets {α : Type u_1} [add_group α] (s : add_subgroup α) :
s.normal ∀ (g : α), g +l s = s +r g

theorem normal_iff_eq_cosets {α : Type u_1} [group α] (s : subgroup α) :
s.normal ∀ (g : α), g *l s = s *r g

def quotient_add_group.left_rel {α : Type u_1} [add_group α] :

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

def quotient_group.left_rel {α : Type u_1} [group α] :
subgroup αsetoid α

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

Equations
def quotient_group.quotient {α : Type u_1} [group α] :
subgroup αType u_1

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

Equations
def quotient_add_group.quotient {α : Type u_1} [add_group α] :
add_subgroup αType u_1

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

Equations
def quotient_add_group.mk {α : Type u_1} [add_group α] {s : add_subgroup α} :

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

def quotient_group.mk {α : Type u_1} [group α] {s : subgroup α} :

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

Equations
theorem quotient_group.induction_on {α : Type u_1} [group α] {s : subgroup α} {C : quotient_group.quotient s → Prop} (x : quotient_group.quotient s) :
(∀ (z : α), C (quotient_group.mk z))C x

theorem quotient_add_group.induction_on {α : Type u_1} [add_group α] {s : add_subgroup α} {C : quotient_add_group.quotient s → Prop} (x : quotient_add_group.quotient s) :
(∀ (z : α), C (quotient_add_group.mk z))C x

@[instance]
def quotient_group.has_coe_t {α : Type u_1} [group α] {s : subgroup α} :

Equations
@[instance]

theorem quotient_add_group.induction_on' {α : Type u_1} [add_group α] {s : add_subgroup α} {C : quotient_add_group.quotient s → Prop} (x : quotient_add_group.quotient s) :
(∀ (z : α), C z)C x

theorem quotient_group.induction_on' {α : Type u_1} [group α] {s : subgroup α} {C : quotient_group.quotient s → Prop} (x : quotient_group.quotient s) :
(∀ (z : α), C z)C x

@[instance]
def quotient_group.inhabited {α : Type u_1} [group α] (s : subgroup α) :

Equations
theorem quotient_add_group.eq {α : Type u_1} [add_group α] {s : add_subgroup α} {a b : α} :
a = b -a + b s

theorem quotient_group.eq {α : Type u_1} [group α] {s : subgroup α} {a b : α} :
a = b a⁻¹ * b s

theorem quotient_group.eq_class_eq_left_coset {α : Type u_1} [group α] (s : subgroup α) (g : α) :
{x : α | x = g} = g *l s

theorem quotient_add_group.eq_class_eq_left_coset {α : Type u_1} [add_group α] (s : add_subgroup α) (g : α) :
{x : α | x = g} = g +l s

theorem quotient_group.preimage_image_coe {α : Type u_1} [group α] (N : subgroup α) (s : set α) :
coe ⁻¹' (coe '' s) = ⋃ (x : N), (λ (y : α), y * x) '' s

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

def subgroup.left_coset_equiv_subgroup {α : Type u_1} [group α] {s : subgroup α} (g : α) :

The natural bijection between the cosets g*s and s

Equations
def add_subgroup.left_coset_equiv_add_subgroup {α : Type u_1} [add_group α] {s : add_subgroup α} (g : α) :

The natural bijection between the cosets g+s and 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