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

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

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

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

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

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

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

Equations

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

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

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

Equations

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

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.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) }

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

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

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

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

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

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

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

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

Equations

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

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

Equations

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

theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (b : α) : (QuotientAddGroup.leftRel s) a b → (QuotientAddGroup.rightRel s) ((fun (g : α) => -g) a) ((fun (g : α) => -g) b)

theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_4 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : α ⧸ s) : Quotient.map' (fun (g : α) => -g) ⋯ (Quotient.map' (fun (g : α) => -g) ⋯ g) = g

theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_3 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : Quotient (QuotientAddGroup.rightRel s)) : Quotient.map' (fun (g : α) => -g) ⋯ (Quotient.map' (fun (g : α) => -g) ⋯ g) = g

theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (b : α) : (QuotientAddGroup.rightRel s) a b → (QuotientAddGroup.leftRel s) ((fun (g : α) => -g) a) ((fun (g : α) => -g) b)

def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Quotient (QuotientAddGroup.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 := ⋯ }

def QuotientGroup.quotientRightRelEquivQuotientLeftRel {α : Type u_1} [Group α] (s : Subgroup α) : Quotient (QuotientGroup.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 := ⋯ }

@[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

@[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

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

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

@[simp]

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

@[simp]

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

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

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

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

Equations

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

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

Equations

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

@[deprecated]

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.

@[deprecated]

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

@[simp]

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

@[simp]

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

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

theorem QuotientGroup.forall_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

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

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

Equations

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

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

Equations

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

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

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

@[deprecated]

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

Alias of QuotientGroup.eq.

@[deprecated]

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem AddSubgroup.quotientEquivOfEq.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (_a : α) (_b : α) (h' : (QuotientAddGroup.leftRel s) _a _b) : (QuotientAddGroup.leftRel t) (id _a) (id _b)

def AddSubgroup.quotientEquivOfEq {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {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 AddSubgroup.quotientEquivOfEq.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (_a : α) (_b : α) (h' : (QuotientAddGroup.leftRel t) _a _b) : (QuotientAddGroup.leftRel s) (id _a) (id _b)

theorem AddSubgroup.quotientEquivOfEq.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (q : α ⧸ t) : Quotient.map' id ⋯ (Quotient.map' id ⋯ q) = q

theorem AddSubgroup.quotientEquivOfEq.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (q : α ⧸ s) : Quotient.map' id ⋯ (Quotient.map' id ⋯ q) = q

def Subgroup.quotientEquivOfEq {α : Type u_1} [Group α] {s : Subgroup α} {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 := ⋯ }

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