group_theory.coset - mathlib docs

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

left_add_coset a 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

left_coset a 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

right_coset s 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

right_add_coset s a = (λ (x : α), x + a) '' s

source

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

a * x ∈ left_coset a s

source

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

a + x ∈ left_add_coset a s

source

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

x * a ∈ right_coset s a

source

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

x + a ∈ right_add_coset s 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

left_coset_equivalence s a b = (left_coset a s = left_coset b s)

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

left_add_coset_equivalence s a b = (left_add_coset a s = left_add_coset b s)

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

right_coset_equivalence s a b = (right_coset s a = right_coset s b)

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

right_add_coset_equivalence s a b = (right_add_coset s a = right_add_coset s b)

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 : α) :

left_add_coset a (left_add_coset b s) = left_add_coset (a + b) 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

@[simp]

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

right_add_coset (right_add_coset s a) b = right_add_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 zero_left_add_coset {α : Type u_1} [add_monoid α] (s : set α) :

left_add_coset 0 s = s

source

@[simp]

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

left_coset 1 s = s

source

@[simp]

theorem right_add_coset_zero {α : Type u_1} [add_monoid α] (s : set α) :

right_add_coset s 0 = 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_coset {α : Type u_1} [monoid α] (s : submonoid α) (a : α) :

a ∈ right_coset ↑s a

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_left_add_coset_left_add_coset {α : Type u_1} [add_monoid α] (s : add_submonoid α) {a : α} (ha : left_add_coset a ↑s = ↑s) :

a ∈ s

source

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

a ∈ s

source

theorem mem_right_coset_right_coset {α : Type u_1} [monoid α] (s : submonoid α) {a : α} (ha : 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 : α} (ha : right_add_coset ↑s a = ↑s) :

a ∈ 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_left_coset_iff {α : Type u_1} [group α] {s : set α} {x : α} (a : α) :

x ∈ left_coset a s ↔ a⁻¹ * x ∈ 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 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 left_coset_mem_left_coset {α : Type u_1} [group α] (s : subgroup α) {a : α} (ha : 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 : α} (ha : a ∈ s) :

left_add_coset a ↑s = ↑s

source

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

right_coset ↑s a = ↑s

source

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

right_add_coset ↑s a = ↑s

source

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

add_action.orbit ↥s a = right_add_coset ↑s a

source

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

mul_action.orbit ↥s a = right_coset ↑s a

source

theorem orbit_add_subgroup_eq_self_of_mem {α : Type u_1} [add_group α] (s : add_subgroup α) {a : α} (ha : a ∈ s) :

add_action.orbit ↥s a = ↑s

source

theorem orbit_subgroup_eq_self_of_mem {α : Type u_1} [group α] (s : subgroup α) {a : α} (ha : a ∈ s) :

mul_action.orbit ↥s a = ↑s

source

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

add_action.orbit ↥s 0 = ↑s

source

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

mul_action.orbit ↥s 1 = ↑s

source

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

left_coset g ↑s = right_coset ↑s g

source

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

left_add_coset g ↑s = right_add_coset ↑s g

source

theorem normal_of_eq_cosets {α : Type u_1} [group α] (s : subgroup α) (h : ∀ (g : α), left_coset g ↑s = right_coset ↑s g) :

s.normal

source

theorem normal_of_eq_add_cosets {α : Type u_1} [add_group α] (s : add_subgroup α) (h : ∀ (g : α), left_add_coset g ↑s = right_add_coset ↑s g) :

s.normal

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

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

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

source

theorem left_add_coset_eq_iff {α : Type u_1} [add_group α] (s : add_subgroup α) {x y : α} :

left_add_coset x ↑s = left_add_coset y ↑s ↔ -x + y ∈ s

source

theorem left_coset_eq_iff {α : Type u_1} [group α] (s : subgroup α) {x y : α} :

left_coset x ↑s = left_coset y ↑s ↔ x⁻¹ * y ∈ s

source

theorem right_coset_eq_iff {α : Type u_1} [group α] (s : subgroup α) {x y : α} :

right_coset ↑s x = right_coset ↑s y ↔ y * x⁻¹ ∈ s

source

theorem right_add_coset_eq_iff {α : Type u_1} [add_group α] (s : add_subgroup α) {x y : α} :

right_add_coset ↑s x = right_add_coset ↑s 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

quotient_add_group.left_rel s = add_action.orbit_rel ↥(⇑add_subgroup.opposite s) α

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

quotient_group.left_rel s = mul_action.orbit_rel ↥(⇑subgroup.opposite s) α

source

theorem quotient_group.left_rel_apply {α : Type u_1} [group α] {s : subgroup α} {x y : α} :

setoid.r x y ↔ x⁻¹ * y ∈ s

source

theorem quotient_add_group.left_rel_apply {α : Type u_1} [add_group α] {s : add_subgroup α} {x y : α} :

setoid.r x y ↔ -x + y ∈ s

source

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

setoid.r = λ (x y : α), -x + y ∈ s

source

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

setoid.r = λ (x y : α), x⁻¹ * y ∈ s

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

quotient_group.left_rel_decidable s = λ (x y : α), _.mpr (_inst_2 (x⁻¹ * y))

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

quotient_add_group.left_rel_decidable s = λ (x y : α), _.mpr (_inst_2 (-x + y))

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

quotient_add_group.subgroup.has_quotient = {quotient' := λ (s : add_subgroup α), quotient (quotient_add_group.left_rel s)}

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

quotient_group.subgroup.has_quotient = {quotient' := λ (s : subgroup α), quotient (quotient_group.left_rel s)}

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

quotient_group.right_rel s = mul_action.orbit_rel ↥s α

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

quotient_add_group.right_rel s = add_action.orbit_rel ↥s α

source

theorem quotient_group.right_rel_apply {α : Type u_1} [group α] {s : subgroup α} {x y : α} :

setoid.r x y ↔ y * x⁻¹ ∈ s

source

theorem quotient_add_group.right_rel_apply {α : Type u_1} [add_group α] {s : add_subgroup α} {x y : α} :

setoid.r x y ↔ y + -x ∈ s

source

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

setoid.r = λ (x y : α), y + -x ∈ s

source

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

setoid.r = λ (x y : α), y * x⁻¹ ∈ s

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

quotient_group.right_rel_decidable s = λ (x y : α), _.mpr (_inst_2 (y * x⁻¹))

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

quotient_add_group.right_rel_decidable s = λ (x y : α), _.mpr (_inst_2 (y + -x))

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

quotient_group.quotient_right_rel_equiv_quotient_left_rel s = {to_fun := quotient.map' (λ (g : α), g⁻¹) _, inv_fun := quotient.map' (λ (g : α), g⁻¹) _, left_inv := _, right_inv := _}

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

quotient_add_group.quotient_right_rel_equiv_quotient_left_rel s = {to_fun := quotient.map' (λ (g : α), -g) _, inv_fun := quotient.map' (λ (g : α), -g) _, left_inv := _, right_inv := _}

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

quotient_group.fintype_quotient_right_rel s = fintype.of_equiv (α ⧸ s) (quotient_group.quotient_right_rel_equiv_quotient_left_rel s).symm

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

quotient_add_group.fintype_quotient_right_rel s = fintype.of_equiv (α ⧸ s) (quotient_add_group.quotient_right_rel_equiv_quotient_left_rel s).symm

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

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

source

@[protected, instance]

def quotient_add_group.fintype {α : Type u_1} [add_group α] [fintype α] (s : add_subgroup α) [decidable_rel setoid.r] :

fintype (α ⧸ s)

Equations

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

source

@[reducible]

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

@[reducible]

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

quotient_add_group.has_quotient.quotient.has_coe_t = {coe := quotient_add_group.mk s}

source

@[protected, instance]

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

has_coe_t α (α ⧸ s)

Equations

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

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

quotient_add_group.has_quotient.quotient.inhabited s = {default := ↑0}

source

@[protected, instance]

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

inhabited (α ⧸ s)

Equations

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

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} = left_coset g ↑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.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 : α) :

↥(left_coset g ↑s) ≃ ↥s

The natural bijection between a left coset 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 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.

Equations

add_subgroup.left_coset_equiv_add_subgroup g = {to_fun := λ (x : ↥(left_add_coset g ↑s)), ⟨-g + x.val, _⟩, inv_fun := λ (x : ↥s), ⟨g + x.val, _⟩, left_inv := _, right_inv := _}

source

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

↥(right_coset ↑s g) ≃ ↥s

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

Equations

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

source

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

↥(right_add_coset ↑s g) ≃ ↥s

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

Equations

add_subgroup.right_coset_equiv_add_subgroup g = {to_fun := λ (x : ↥(right_add_coset ↑s g)), ⟨x.val + -g, _⟩, inv_fun := λ (x : ↥s), ⟨x.val + g, _⟩, left_inv := _, right_inv := _}

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

subgroup.group_equiv_quotient_times_subgroup = (((equiv.sigma_fiber_equiv quotient_group.mk).symm.trans (equiv.sigma_congr_right (λ (L : α ⧸ s), _.mpr (id (_.mpr (equiv.refl {x // quotient.mk' x = L})))))).trans (equiv.sigma_congr_right (λ (L : α ⧸ s), subgroup.left_coset_equiv_subgroup (quotient.out' L)))).trans (equiv.sigma_equiv_prod (α ⧸ s) ↥s)

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

add_subgroup.add_group_equiv_quotient_times_add_subgroup = (((equiv.sigma_fiber_equiv quotient_add_group.mk).symm.trans (equiv.sigma_congr_right (λ (L : α ⧸ s), _.mpr (id (_.mpr (equiv.refl {x // quotient.mk' x = L})))))).trans (equiv.sigma_congr_right (λ (L : α ⧸ s), add_subgroup.left_coset_equiv_add_subgroup (quotient.out' L)))).trans (equiv.sigma_equiv_prod (α ⧸ s) ↥s)

source

def add_subgroup.quotient_equiv_of_eq {α : Type u_1} [add_group α] {s t : add_subgroup α} (h : s = t) :

α ⧸ s ≃ α ⧸ t

If two subgroups M and N of G are equal, their quotients are in bijection.

Equations

add_subgroup.quotient_equiv_of_eq h = {to_fun := quotient.map' id _, inv_fun := quotient.map' id _, left_inv := _, right_inv := _}

source

def subgroup.quotient_equiv_of_eq {α : Type u_1} [group α] {s t : subgroup α} (h : s = t) :

α ⧸ s ≃ α ⧸ t

If two subgroups M and N of G are equal, their quotients are in bijection.

Equations

subgroup.quotient_equiv_of_eq h = {to_fun := quotient.map' id _, inv_fun := quotient.map' id _, left_inv := _, right_inv := _}

source

theorem subgroup.quotient_equiv_of_eq_mk {α : Type u_1} [group α] {s t : subgroup α} (h : s = t) (a : α) :

⇑(subgroup.quotient_equiv_of_eq h) (quotient_group.mk a) = quotient_group.mk a

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

subgroup.quotient_equiv_prod_of_le' h_le f hf = {to_fun := λ (a : α ⧸ s), (quotient.map' id _ a, quotient.map' (λ (g : α), ⟨(f (quotient.mk' g))⁻¹ * g, _⟩) _ a), inv_fun := λ (a : (α ⧸ t) × ↥t ⧸ s.subgroup_of t), quotient.map' (λ (b : ↥t), f a.fst * ↑b) _ a.snd, left_inv := _, right_inv := _}

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

add_subgroup.quotient_equiv_sum_of_le' h_le f hf = {to_fun := λ (a : α ⧸ s), (quotient.map' id _ a, quotient.map' (λ (g : α), ⟨-f (quotient.mk' g) + g, _⟩) _ a), inv_fun := λ (a : (α ⧸ t) × ↥t ⧸ s.add_subgroup_of t), quotient.map' (λ (b : ↥t), f a.fst + ↑b) _ a.snd, left_inv := _, right_inv := _}

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

add_subgroup.quotient_equiv_sum_of_le h_le = add_subgroup.quotient_equiv_sum_of_le' h_le quotient.out' add_subgroup.quotient_equiv_sum_of_le._proof_1

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

subgroup.quotient_equiv_prod_of_le h_le = subgroup.quotient_equiv_prod_of_le' h_le quotient.out' subgroup.quotient_equiv_prod_of_le._proof_1

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 α] {s t : add_subgroup α} (H : add_subgroup α) (h : s ≤ t) :

↥s ⧸ H.add_subgroup_of s ↪ ↥t ⧸ H.add_subgroup_of t

If s ≤ t, then there is an embedding s ⧸ H.add_subgroup_of s ↪ t ⧸ H.add_subgroup_of t.

Equations

H.quotient_add_subgroup_of_embedding_of_le h = {to_fun := quotient.map' ⇑(add_subgroup.inclusion h) _, inj' := _}

source

def subgroup.quotient_subgroup_of_embedding_of_le {α : Type u_1} [group α] {s t : subgroup α} (H : subgroup α) (h : s ≤ t) :

↥s ⧸ H.subgroup_of s ↪ ↥t ⧸ H.subgroup_of t

If s ≤ t, then there is an embedding s ⧸ H.subgroup_of s ↪ t ⧸ H.subgroup_of t.

Equations

H.quotient_subgroup_of_embedding_of_le h = {to_fun := quotient.map' ⇑(subgroup.inclusion h) _, inj' := _}

source

@[simp]

theorem subgroup.quotient_subgroup_of_embedding_of_le_apply_mk {α : Type u_1} [group α] {s t : subgroup α} (H : subgroup α) (h : s ≤ t) (g : ↥s) :

⇑(H.quotient_subgroup_of_embedding_of_le h) (quotient_group.mk g) = quotient_group.mk (⇑(subgroup.inclusion h) g)

source

@[simp]

theorem add_subgroup.quotient_add_subgroup_of_embedding_of_le_apply_mk {α : Type u_1} [add_group α] {s t : add_subgroup α} (H : add_subgroup α) (h : s ≤ t) (g : ↥s) :

⇑(H.quotient_add_subgroup_of_embedding_of_le h) (quotient_add_group.mk g) = quotient_add_group.mk (⇑(add_subgroup.inclusion h) g)

source

def add_subgroup.quotient_add_subgroup_of_map_of_le {α : Type u_1} [add_group α] {s t : add_subgroup α} (H : add_subgroup α) (h : s ≤ t) :

↥H ⧸ s.add_subgroup_of H → ↥H ⧸ t.add_subgroup_of H

If s ≤ t, then there is an map H ⧸ s.add_subgroup_of H → H ⧸ t.add_subgroup_of H.

Equations

H.quotient_add_subgroup_of_map_of_le h = quotient.map' id _

source

def subgroup.quotient_subgroup_of_map_of_le {α : Type u_1} [group α] {s t : subgroup α} (H : subgroup α) (h : s ≤ t) :

↥H ⧸ s.subgroup_of H → ↥H ⧸ t.subgroup_of H

If s ≤ t, then there is a map H ⧸ s.subgroup_of H → H ⧸ t.subgroup_of H.

Equations

H.quotient_subgroup_of_map_of_le h = quotient.map' id _

source

@[simp]

theorem add_subgroup.quotient_add_subgroup_of_map_of_le_apply_mk {α : Type u_1} [add_group α] {s t : add_subgroup α} (H : add_subgroup α) (h : s ≤ t) (g : ↥H) :

H.quotient_add_subgroup_of_map_of_le h (quotient_add_group.mk g) = quotient_add_group.mk g

source

@[simp]

theorem subgroup.quotient_subgroup_of_map_of_le_apply_mk {α : Type u_1} [group α] {s t : subgroup α} (H : subgroup α) (h : s ≤ t) (g : ↥H) :

H.quotient_subgroup_of_map_of_le h (quotient_group.mk g) = quotient_group.mk g

source

def subgroup.quotient_infi_embedding {α : Type u_1} [group α] {ι : Type u_2} (f : ι → subgroup α) (H : subgroup α) :

↥H ⧸ (⨅ (i : ι), f i).subgroup_of H ↪ Π (i : ι), ↥H ⧸ (f i).subgroup_of H

The natural embedding H ⧸ (⨅ i, f i).subgroup_of H ↪ Π i, H ⧸ (f i).subgroup_of H.

Equations

subgroup.quotient_infi_embedding f H = {to_fun := λ (q : ↥H ⧸ (⨅ (i : ι), f i).subgroup_of H) (i : ι), H.quotient_subgroup_of_map_of_le _ q, inj' := _}

source

def add_subgroup.quotient_infi_embedding {α : Type u_1} [add_group α] {ι : Type u_2} (f : ι → add_subgroup α) (H : add_subgroup α) :

↥H ⧸ (⨅ (i : ι), f i).add_subgroup_of H ↪ Π (i : ι), ↥H ⧸ (f i).add_subgroup_of H

There is an embedding H ⧸ (⨅ i, f i).add_subgroup_of H) ↪ Π i, H ⧸ (f i).add_subgroup_of H.

Equations

add_subgroup.quotient_infi_embedding f H = {to_fun := λ (q : ↥H ⧸ (⨅ (i : ι), f i).add_subgroup_of H) (i : ι), H.quotient_add_subgroup_of_map_of_le _ q, inj' := _}

source

@[simp]

theorem subgroup.quotient_infi_embedding_apply_mk {α : Type u_1} [group α] {ι : Type u_2} (f : ι → subgroup α) (H : subgroup α) (g : ↥H) (i : ι) :

⇑(subgroup.quotient_infi_embedding f H) (quotient_group.mk g) i = quotient_group.mk g

source

@[simp]

theorem add_subgroup.quotient_infi_embedding_apply_mk {α : Type u_1} [add_group α] {ι : Type u_2} (f : ι → add_subgroup α) (H : add_subgroup α) (g : ↥H) (i : ι) :

⇑(add_subgroup.quotient_infi_embedding f H) (quotient_add_group.mk g) i = quotient_add_group.mk g

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

quotient_group.preimage_mk_equiv_subgroup_times_set s t = have h : ∀ {x : α ⧸ 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, _⟩

source

def library_note.use has_coe_t :

unit

We use the class has_coe_t instead of has_coe if the first argument is a variable, or if the second argument is a variable not occurring in the first. Using has_coe would cause looping of type-class inference. See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/remove.20all.20instances.20with.20variable.20domain

mathlib documentation

Cosets #

Main definitions #

Notation #

TODO #