Cosets

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

When G is a group and a : G, s : Set G, with open scoped Pointwise we can write:

• the left coset of s by a as a • s
• the right coset of s by a as MulOpposite.op a • s (or op a • s with open MulOpposite)

If instead G is an additive group, we can write (with open scoped Pointwise still)

• the left coset of s by a as a +ᵥ s
• the right coset of s by a as AddOpposite.op a +ᵥ s (or op a • s with open AddOpposite)

Main definitions

• QuotientGroup.quotient s: the quotient type representing the left cosets with respect to a subgroup s, for an AddGroup this is QuotientAddGroup.quotient s.
• QuotientGroup.mk: the canonical map from α to α/s for a subgroup s of α, for an AddGroup this is QuotientAddGroup.mk.

Notation

• G ⧸ H is the quotient of the (additive) group G by the (additive) subgroup H

TODO

Properly merge with pointwise actions on sets, by renaming and deduplicating lemmas as appropriate.

def QuotientGroup.leftRel {α : Type u_1} [Group α] (s : Subgroup α) : Setoid α

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

Equations

• QuotientGroup.leftRel s = MulAction.orbitRel (↥s.op) α

def QuotientAddGroup.leftRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Setoid α

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

Equations

• QuotientAddGroup.leftRel s = AddAction.orbitRel (↥s.op) α

theorem QuotientGroup.leftRel_apply {α : Type u_1} [Group α] {s : Subgroup α} {x y : α} : (leftRel s) x y ↔ x⁻¹ * y ∈ s

theorem QuotientAddGroup.leftRel_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {x y : α} : (leftRel s) x y ↔ -x + y ∈ s

theorem QuotientGroup.leftRel_eq {α : Type u_1} [Group α] (s : Subgroup α) : ⇑(leftRel s) = fun (x y : α) => x⁻¹ * y ∈ s

theorem QuotientAddGroup.leftRel_eq {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : ⇑(leftRel s) = fun (x y : α) => -x + y ∈ s

instance QuotientGroup.leftRelDecidable {α : Type u_1} [Group α] (s : Subgroup α) [DecidablePred fun (x : α) => x ∈ s] : DecidableRel ⇑(leftRel s)

Equations

• QuotientGroup.leftRelDecidable s x y = ⋯.mpr (inst✝ (x⁻¹ * y))

instance QuotientAddGroup.leftRelDecidable {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [DecidablePred fun (x : α) => x ∈ s] : DecidableRel ⇑(leftRel s)

Equations

• QuotientAddGroup.leftRelDecidable s x y = ⋯.mpr (inst✝ (-x + y))

instance QuotientGroup.instHasQuotientSubgroup {α : Type u_1} [Group α] : HasQuotient α (Subgroup α)

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

Equations

• QuotientGroup.instHasQuotientSubgroup = { quotient' := fun (s : Subgroup α) => Quotient (QuotientGroup.leftRel s) }

instance QuotientAddGroup.instHasQuotientAddSubgroup {α : Type u_1} [AddGroup α] : HasQuotient α (AddSubgroup α)

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

Equations

• QuotientAddGroup.instHasQuotientAddSubgroup = { quotient' := fun (s : AddSubgroup α) => Quotient (QuotientAddGroup.leftRel s) }

instance QuotientGroup.instDecidableEqQuotientSubgroupOfDecidablePredMem {α : Type u_1} [Group α] (s : Subgroup α) [DecidablePred fun (x : α) => x ∈ s] : DecidableEq (α ⧸ s)

Equations

• QuotientGroup.instDecidableEqQuotientSubgroupOfDecidablePredMem s = Quotient.decidableEq

instance QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [DecidablePred fun (x : α) => x ∈ s] : DecidableEq (α ⧸ s)

Equations

• QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem s = Quotient.decidableEq

def QuotientGroup.rightRel {α : Type u_1} [Group α] (s : Subgroup α) : Setoid α

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

Equations

• QuotientGroup.rightRel s = MulAction.orbitRel (↥s) α

def QuotientAddGroup.rightRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Setoid α

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

Equations

• QuotientAddGroup.rightRel s = AddAction.orbitRel (↥s) α

theorem QuotientGroup.rightRel_apply {α : Type u_1} [Group α] {s : Subgroup α} {x y : α} : (rightRel s) x y ↔ y * x⁻¹ ∈ s

theorem QuotientAddGroup.rightRel_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {x y : α} : (rightRel s) x y ↔ y + -x ∈ s

theorem QuotientGroup.rightRel_eq {α : Type u_1} [Group α] (s : Subgroup α) : ⇑(rightRel s) = fun (x y : α) => y * x⁻¹ ∈ s

theorem QuotientAddGroup.rightRel_eq {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : ⇑(rightRel s) = fun (x y : α) => y + -x ∈ s

instance QuotientGroup.rightRelDecidable {α : Type u_1} [Group α] (s : Subgroup α) [DecidablePred fun (x : α) => x ∈ s] : DecidableRel ⇑(rightRel s)

Equations

• QuotientGroup.rightRelDecidable s x y = ⋯.mpr (inst✝ (y * x⁻¹))

instance QuotientAddGroup.rightRelDecidable {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [DecidablePred fun (x : α) => x ∈ s] : DecidableRel ⇑(rightRel s)

Equations

• QuotientAddGroup.rightRelDecidable s x y = ⋯.mpr (inst✝ (y + -x))

def QuotientGroup.quotientRightRelEquivQuotientLeftRel {α : Type u_1} [Group α] (s : Subgroup α) : Quotient (rightRel s) ≃ α ⧸ s

Right cosets are in bijection with left cosets.

Equations

• QuotientGroup.quotientRightRelEquivQuotientLeftRel s = { toFun := Quotient.map' (fun (g : α) => g⁻¹) ⋯, invFun := Quotient.map' (fun (g : α) => g⁻¹) ⋯, left_inv := ⋯, right_inv := ⋯ }

def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Quotient (rightRel s) ≃ α ⧸ s

Right cosets are in bijection with left cosets.

Equations

• QuotientAddGroup.quotientRightRelEquivQuotientLeftRel s = { toFun := Quotient.map' (fun (g : α) => -g) ⋯, invFun := Quotient.map' (fun (g : α) => -g) ⋯, left_inv := ⋯, right_inv := ⋯ }

@[reducible, inline]

abbrev QuotientGroup.mk {α : Type u_1} [Group α] {s : Subgroup α} (a : α) : α ⧸ s

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

Equations

• ↑a = Quotient.mk'' a

@[reducible, inline]

abbrev QuotientAddGroup.mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (a : α) : α ⧸ s

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

Equations

• ↑a = Quotient.mk'' a

theorem QuotientGroup.mk_surjective {α : Type u_1} [Group α] {s : Subgroup α} : Function.Surjective mk

theorem QuotientAddGroup.mk_surjective {α : Type u_1} [AddGroup α] {s : AddSubgroup α} : Function.Surjective mk

@[simp]

theorem QuotientGroup.range_mk {α : Type u_1} [Group α] {s : Subgroup α} : Set.range mk = Set.univ

@[simp]

theorem QuotientAddGroup.range_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} : Set.range mk = Set.univ

theorem QuotientGroup.induction_on {α : Type u_1} [Group α] {s : Subgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ (z : α), C ↑z) : C x

theorem QuotientAddGroup.induction_on {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ (z : α), C ↑z) : C x

instance QuotientGroup.instCoeQuotientSubgroup {α : Type u_1} [Group α] {s : Subgroup α} : Coe α (α ⧸ s)

Equations

• QuotientGroup.instCoeQuotientSubgroup = { coe := QuotientGroup.mk }

instance QuotientAddGroup.instCoeQuotientAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} : Coe α (α ⧸ s)

Equations

• QuotientAddGroup.instCoeQuotientAddSubgroup = { coe := QuotientAddGroup.mk }

theorem QuotientGroup.induction_on' {α : Type u_1} [Group α] {s : Subgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ (z : α), C ↑z) : C x

Alias of QuotientGroup.induction_on.

theorem QuotientAddGroup.induction_on' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ (z : α), C ↑z) : C x

@[simp]

theorem QuotientGroup.quotient_liftOn_mk {α : Type u_1} [Group α] {s : Subgroup α} {β : Sort u_2} (f : α → β) (h : ∀ (a b : α), (leftRel s) a b → f a = f b) (x : α) : Quotient.liftOn' (↑x) f h = f x

@[simp]

theorem QuotientAddGroup.quotient_liftOn_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {β : Sort u_2} (f : α → β) (h : ∀ (a b : α), (leftRel s) a b → f a = f b) (x : α) : Quotient.liftOn' (↑x) f h = f x

theorem QuotientGroup.forall_mk {α : Type u_1} [Group α] {s : Subgroup α} {C : α ⧸ s → Prop} : (∀ (x : α ⧸ s), C x) ↔ ∀ (x : α), C ↑x

theorem QuotientAddGroup.forall_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop} : (∀ (x : α ⧸ s), C x) ↔ ∀ (x : α), C ↑x

theorem QuotientGroup.exists_mk {α : Type u_1} [Group α] {s : Subgroup α} {C : α ⧸ s → Prop} : (∃ (x : α ⧸ s), C x) ↔ ∃ (x : α), C ↑x

theorem QuotientAddGroup.exists_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop} : (∃ (x : α ⧸ s), C x) ↔ ∃ (x : α), C ↑x

instance QuotientGroup.instInhabitedQuotientSubgroup {α : Type u_1} [Group α] (s : Subgroup α) : Inhabited (α ⧸ s)

Equations

• QuotientGroup.instInhabitedQuotientSubgroup s = { default := ↑1 }

instance QuotientAddGroup.instInhabitedQuotientAddSubgroup {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Inhabited (α ⧸ s)

Equations

• QuotientAddGroup.instInhabitedQuotientAddSubgroup s = { default := ↑0 }

theorem QuotientGroup.eq {α : Type u_1} [Group α] {s : Subgroup α} {a b : α} : ↑a = ↑b ↔ a⁻¹ * b ∈ s

theorem QuotientAddGroup.eq {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {a b : α} : ↑a = ↑b ↔ -a + b ∈ s

theorem QuotientGroup.out_eq' {α : Type u_1} [Group α] {s : Subgroup α} (a : α ⧸ s) : ↑(Quotient.out a) = a

theorem QuotientAddGroup.out_eq' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (a : α ⧸ s) : ↑(Quotient.out a) = a

theorem QuotientGroup.mk_out_eq_mul {α : Type u_1} [Group α] (s : Subgroup α) (g : α) : ∃ (h : ↥s), Quotient.out ↑g = g * ↑h

theorem QuotientAddGroup.mk_out_eq_mul {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : α) : ∃ (h : ↥s), Quotient.out ↑g = g + ↑h

@[simp]

theorem QuotientGroup.mk_mul_of_mem {α : Type u_1} [Group α] {s : Subgroup α} {b : α} (a : α) (hb : b ∈ s) : ↑(a * b) = ↑a

@[simp]

theorem QuotientAddGroup.mk_add_of_mem {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {b : α} (a : α) (hb : b ∈ s) : ↑(a + b) = ↑a

theorem QuotientGroup.preimage_image_mk {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) : mk ⁻¹' (mk '' s) = ⋃ (x : ↥N), (fun (x_1 : α) => x_1 * ↑x) ⁻¹' s

theorem QuotientAddGroup.preimage_image_mk {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) : mk ⁻¹' (mk '' s) = ⋃ (x : ↥N), (fun (x_1 : α) => x_1 + ↑x) ⁻¹' s

theorem QuotientGroup.preimage_image_mk_eq_iUnion_image {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) : mk ⁻¹' (mk '' s) = ⋃ (x : ↥N), (fun (x_1 : α) => x_1 * ↑x) '' s

theorem QuotientAddGroup.preimage_image_mk_eq_iUnion_image {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) : mk ⁻¹' (mk '' s) = ⋃ (x : ↥N), (fun (x_1 : α) => x_1 + ↑x) '' s

theorem QuotientGroup.preimage_image_mk_eq_mul {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) : mk ⁻¹' (mk '' s) = s * ↑N

theorem QuotientAddGroup.preimage_image_mk_eq_add {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) : mk ⁻¹' (mk '' s) = s + ↑N

theorem QuotientGroup.preimage_mk_one {α : Type u_1} [Group α] (N : Subgroup α) : mk ⁻¹' {↑1} = ↑N

theorem QuotientAddGroup.preimage_mk_zero {α : Type u_1} [AddGroup α] (N : AddSubgroup α) : mk ⁻¹' {↑0} = ↑N

def Subgroup.quotientEquivOfEq {α : 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.quotientEquivOfEq h = { toFun := Quotient.map' id ⋯, invFun := Quotient.map' id ⋯, left_inv := ⋯, right_inv := ⋯ }

def AddSubgroup.quotientEquivOfEq {α : Type u_1} [AddGroup α] {s t : AddSubgroup α} (h : s = t) : α ⧸ s ≃ α ⧸ t

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

Equations

• AddSubgroup.quotientEquivOfEq h = { toFun := Quotient.map' id ⋯, invFun := Quotient.map' id ⋯, left_inv := ⋯, right_inv := ⋯ }

theorem Subgroup.quotientEquivOfEq_mk {α : Type u_1} [Group α] {s t : Subgroup α} (h : s = t) (a : α) : (quotientEquivOfEq h) ↑a = ↑a