mathlib docs: group_theory.coset

source

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 α

source

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

left_coset a s = (λ (x : α), a * x) '' s

source

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 α

source

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

right_coset s a = (λ (x : α), x * a) '' s

source

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

x ∈ s → a * x ∈ left_coset a s

source

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

x ∈ s → a + x ∈ left_add_coset a s

source

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

x ∈ s → x + a ∈ right_add_coset s a

source

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

x ∈ s → x * a ∈ right_coset s a

source

def left_coset_equiv {α : Type u_1} [has_mul α] :

set α → α → α → Prop

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

Equations

left_coset_equiv s a b = (left_coset a s = left_coset b s)

source

def left_add_coset_equiv {α : Type u_1} [has_add α] :

set α → α → α → Prop

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

source

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

equivalence (left_coset_equiv s)

source

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

equivalence (left_add_coset_equiv s)

source

@[simp]

theorem left_coset_assoc {α : Type u_1} [semigroup α] (s : set α) (a b : α) :

left_coset a (left_coset b s) = left_coset (a * b) s

source

@[simp]

theorem right_coset_assoc {α : Type u_1} [semigroup α] (s : set α) (a b : α) :

right_coset (right_coset s a) b = right_coset s (a * b)

source

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

right_coset (left_coset a s) b = left_coset a (right_coset s b)

source

theorem left_add_coset_right_add_coset {α : Type u_1} [add_semigroup α] (s : set α) (a b : α) :

right_add_coset (left_add_coset a s) b = left_add_coset a (right_add_coset s b)

source

@[simp]

theorem one_left_coset {α : Type u_1} [monoid α] (s : set α) :

left_coset 1 s = s

source

@[simp]

theorem right_coset_one {α : Type u_1} [monoid α] (s : set α) :

right_coset s 1 = s

source

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

a ∈ left_coset a ↑s

source

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

a ∈ left_add_coset a ↑s

source

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

a ∈ right_add_coset ↑s a

source

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

a ∈ right_coset ↑s a

source

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

left_add_coset a ↑s = ↑s → a ∈ s

source

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

left_coset a ↑s = ↑s → a ∈ s

source

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

right_coset ↑s a = ↑s → a ∈ s

source

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

right_add_coset ↑s a = ↑s → a ∈ s

source

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

x ∈ left_coset a s ↔ a⁻¹ * x ∈ s

source

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

x ∈ left_add_coset a s ↔ -a + x ∈ s

source

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

x ∈ right_add_coset s a ↔ x + -a ∈ s

source

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

x ∈ right_coset s a ↔ x * a⁻¹ ∈ s

source

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

a ∈ s → left_coset a ↑s = ↑s

source

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

a ∈ s → left_add_coset a ↑s = ↑s

source

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

a ∈ s → right_add_coset ↑s a = ↑s

source

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

a ∈ s → right_coset ↑s a = ↑s

source

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

left_coset g ↑s = right_coset ↑s g

source

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

left_add_coset g ↑s = right_add_coset ↑s g

source

theorem eq_add_cosets_of_normal {α : Type u_1} [add_group α] (s : add_subgroup α) :

(∀ (g : α), left_add_coset g ↑s = right_add_coset ↑s g) → s.normal

source

theorem eq_cosets_of_normal {α : Type u_1} [group α] (s : subgroup α) :

(∀ (g : α), left_coset g ↑s = right_coset ↑s g) → s.normal

source

theorem normal_iff_eq_cosets {α : Type u_1} [group α] (s : subgroup α) :

s.normal ↔ ∀ (g : α), left_coset g ↑s = right_coset ↑s g

source

theorem normal_iff_eq_add_cosets {α : Type u_1} [add_group α] (s : add_subgroup α) :

s.normal ↔ ∀ (g : α), left_add_coset g ↑s = right_add_coset ↑s g

source

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

quotient_group.left_rel s = {r := λ (x y : α), x⁻¹ * y ∈ s, iseqv := _}

source

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

add_subgroup α → setoid α

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

source

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

quotient_group.quotient s = quotient (quotient_group.left_rel s)

source

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

quotient_add_group.quotient s = quotient (quotient_add_group.left_rel s)

source

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

α → quotient_group.quotient s

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

Equations

quotient_group.mk a = quotient.mk' a

source

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

α → quotient_add_group.quotient s

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

source

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

source

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

source

@[instance]

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

has_coe_t α (quotient_group.quotient s)

Equations

quotient_group.has_coe_t = {coe := quotient_group.mk s}

source

@[instance]

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

has_coe_t α (quotient_add_group.quotient s)

source

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

source

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

source

@[instance]

def quotient_add_group.inhabited {α : Type u_1} [add_group α] (s : add_subgroup α) :

inhabited (quotient_add_group.quotient s)

source

@[instance]

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

inhabited (quotient_group.quotient s)

Equations

quotient_group.inhabited s = {default := ↑1}

source

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

↑a = ↑b ↔ -a + b ∈ s

source

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

↑a = ↑b ↔ a⁻¹ * b ∈ s

source

theorem quotient_add_group.eq_class_eq_left_coset {α : Type u_1} [add_group α] (s : add_subgroup α) (g : α) :

{x : α | ↑x = ↑g} = left_add_coset g ↑s

source

theorem quotient_group.eq_class_eq_left_coset {α : Type u_1} [group α] (s : subgroup α) (g : α) :

{x : α | ↑x = ↑g} = left_coset g ↑s

source

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

↥(left_add_coset g ↑s) ≃ ↥s

The natural bijection between the cosets g+s and s

source

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

↥(left_coset g ↑s) ≃ ↥s

The natural bijection between the cosets g*s and s

Equations

subgroup.left_coset_equiv_subgroup g = {to_fun := λ (x : ↥(left_coset g ↑s)), ⟨g⁻¹ * x.val, _⟩, inv_fun := λ (x : ↥s), ⟨g * x.val, _⟩, left_inv := _, right_inv := _}

source

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

α ≃ quotient_group.quotient s × ↥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)

source

def add_subgroup.add_group_equiv_quotient_times_add_subgroup {α : Type u_1} [add_group α] {s : add_subgroup α} :

α ≃ quotient_add_group.quotient s × ↥s

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

source

def quotient_group.preimage_mk_equiv_subgroup_times_set {α : Type u_1} [group α] (s : subgroup α) (t : set (quotient_group.quotient 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

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, _⟩

mathlib documentation

group_theory.coset

General documentation

Additional documentation

Library

mathlib documentation

group_theory.​coset

General documentation

Additional documentation

Library

group_theory.coset