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, or s <• a with open scoped Pointwise RightActions)

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, or s <+ᵥ a with open scoped Pointwise RightActions)

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.

@[implicit_reducible]

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.

@[implicit_reducible]

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.

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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.

@[implicit_reducible]

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.

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

Right cosets are in bijection with left cosets.

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

Right cosets are in bijection with left cosets.

@[reducible, inline]

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

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

@[reducible, inline]

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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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.

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.

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