# 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.
• Subgroup.leftCosetEquivSubgroup: the natural bijection between a left coset and the subgroup, for an AddGroup this is AddSubgroup.leftCosetEquivAddSubgroup.

## 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.

theorem mem_leftAddCoset {α : Type u_1} [Add α] {s : Set α} {x : α} (a : α) (hxS : x s) :
a + x a +ᵥ s
theorem mem_leftCoset {α : Type u_1} [Mul α] {s : Set α} {x : α} (a : α) (hxS : x s) :
a * x a s
theorem mem_rightAddCoset {α : Type u_1} [Add α] {s : Set α} {x : α} (a : α) (hxS : x s) :
x + a
theorem mem_rightCoset {α : Type u_1} [Mul α] {s : Set α} {x : α} (a : α) (hxS : x s) :
x * a
def LeftAddCosetEquivalence {α : Type u_1} [Add α] (s : Set α) (a : α) (b : α) :

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

Equations
Instances For
def LeftCosetEquivalence {α : Type u_1} [Mul α] (s : Set α) (a : α) (b : α) :

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

Equations
Instances For
theorem leftAddCosetEquivalence_rel {α : Type u_1} [Add α] (s : Set α) :
theorem leftCosetEquivalence_rel {α : Type u_1} [Mul α] (s : Set α) :
def RightAddCosetEquivalence {α : Type u_1} [Add α] (s : Set α) (a : α) (b : α) :

Equality of two right cosets s + a and s + b.

Equations
Instances For
def RightCosetEquivalence {α : Type u_1} [Mul α] (s : Set α) (a : α) (b : α) :

Equality of two right cosets s * a and s * b.

Equations
Instances For
theorem rightAddCosetEquivalence_rel {α : Type u_1} [Add α] (s : Set α) :
theorem rightCosetEquivalence_rel {α : Type u_1} [Mul α] (s : Set α) :
theorem leftAddCoset_assoc {α : Type u_1} [] (s : Set α) (a : α) (b : α) :
a +ᵥ (b +ᵥ s) = a + b +ᵥ s
theorem leftCoset_assoc {α : Type u_1} [] (s : Set α) (a : α) (b : α) :
a b s = (a * b) s
theorem rightAddCoset_assoc {α : Type u_1} [] (s : Set α) (a : α) (b : α) :
+ᵥ () = AddOpposite.op (a + b) +ᵥ s
theorem rightCoset_assoc {α : Type u_1} [] (s : Set α) (a : α) (b : α) :
theorem leftAddCoset_rightAddCoset {α : Type u_1} [] (s : Set α) (a : α) (b : α) :
+ᵥ (a +ᵥ s) = a +ᵥ ()
theorem leftCoset_rightCoset {α : Type u_1} [] (s : Set α) (a : α) (b : α) :
a s = a
theorem zero_leftAddCoset {α : Type u_1} [] (s : Set α) :
0 +ᵥ s = s
theorem one_leftCoset {α : Type u_1} [] (s : Set α) :
1 s = s
theorem rightAddCoset_zero {α : Type u_1} [] (s : Set α) :
= s
theorem rightCoset_one {α : Type u_1} [] (s : Set α) :
= s
theorem mem_own_leftAddCoset {α : Type u_1} [] (s : ) (a : α) :
a a +ᵥ s
theorem mem_own_leftCoset {α : Type u_1} [] (s : ) (a : α) :
a a s
theorem mem_own_rightAddCoset {α : Type u_1} [] (s : ) (a : α) :
a +ᵥ s
theorem mem_own_rightCoset {α : Type u_1} [] (s : ) (a : α) :
a s
theorem mem_leftAddCoset_leftAddCoset {α : Type u_1} [] (s : ) {a : α} (ha : a +ᵥ s = s) :
a s
theorem mem_leftCoset_leftCoset {α : Type u_1} [] (s : ) {a : α} (ha : a s = s) :
a s
theorem mem_rightAddCoset_rightAddCoset {α : Type u_1} [] (s : ) {a : α} (ha : +ᵥ s = s) :
a s
theorem mem_rightCoset_rightCoset {α : Type u_1} [] (s : ) {a : α} (ha : s = s) :
a s
abbrev mem_leftAddCoset_iff.match_1 {α : Type u_1} [] {s : Set α} {x : α} (a : α) (motive : x a +ᵥ sProp) :
∀ (x_1 : x a +ᵥ s), (∀ (b : α) (hb : b s) (Eq : (fun (x : α) => a +ᵥ x) b = x), motive )motive x_1
Equations
• =
Instances For
theorem mem_leftAddCoset_iff {α : Type u_1} [] {s : Set α} {x : α} (a : α) :
x a +ᵥ s -a + x s
theorem mem_leftCoset_iff {α : Type u_1} [] {s : Set α} {x : α} (a : α) :
x a s a⁻¹ * x s
theorem mem_rightAddCoset_iff {α : Type u_1} [] {s : Set α} {x : α} (a : α) :
x x + -a s
abbrev mem_rightAddCoset_iff.match_1 {α : Type u_1} [] {s : Set α} {x : α} (a : α) (motive : x Prop) :
∀ (x_1 : x ), (∀ (b : α) (hb : b s) (Eq : (fun (x : α) => ) b = x), motive )motive x_1
Equations
• =
Instances For
theorem mem_rightCoset_iff {α : Type u_1} [] {s : Set α} {x : α} (a : α) :
x x * a⁻¹ s
theorem leftAddCoset_mem_leftAddCoset {α : Type u_1} [] (s : ) {a : α} (ha : a s) :
a +ᵥ s = s
theorem leftCoset_mem_leftCoset {α : Type u_1} [] (s : ) {a : α} (ha : a s) :
a s = s
theorem rightAddCoset_mem_rightAddCoset {α : Type u_1} [] (s : ) {a : α} (ha : a s) :
+ᵥ s = s
theorem rightCoset_mem_rightCoset {α : Type u_1} [] (s : ) {a : α} (ha : a s) :
s = s
abbrev orbit_addSubgroup_eq_rightCoset.match_1 {α : Type u_1} [] (s : ) (a : α) (_b : α) (motive : _b AddAction.orbit (s) aProp) :
∀ (x : _b AddAction.orbit (s) a), (∀ (c : s) (d : (fun (m : s) => m +ᵥ a) c = _b), motive )motive x
Equations
• =
Instances For
theorem orbit_addSubgroup_eq_rightCoset {α : Type u_1} [] (s : ) (a : α) :
AddAction.orbit (s) a = +ᵥ s
abbrev orbit_addSubgroup_eq_rightCoset.match_2 {α : Type u_1} [] (s : ) (a : α) (_b : α) (motive : _b +ᵥ sProp) :
∀ (x : _b +ᵥ s), (∀ (c : α) (d : c s) (e : (fun (x : α) => ) c = _b), motive )motive x
Equations
• =
Instances For
theorem orbit_subgroup_eq_rightCoset {α : Type u_1} [] (s : ) (a : α) :
MulAction.orbit (s) a = s
theorem orbit_addSubgroup_eq_self_of_mem {α : Type u_1} [] (s : ) {a : α} (ha : a s) :
theorem orbit_subgroup_eq_self_of_mem {α : Type u_1} [] (s : ) {a : α} (ha : a s) :
MulAction.orbit (s) a = s
theorem orbit_addSubgroup_zero_eq_self {α : Type u_1} [] (s : ) :
theorem orbit_subgroup_one_eq_self {α : Type u_1} [] (s : ) :
MulAction.orbit (s) 1 = s
theorem eq_addCosets_of_normal {α : Type u_1} [] (s : ) (N : s.Normal) (g : α) :
g +ᵥ s = +ᵥ s
theorem eq_cosets_of_normal {α : Type u_1} [] (s : ) (N : s.Normal) (g : α) :
g s = s
theorem normal_of_eq_addCosets {α : Type u_1} [] (s : ) (h : ∀ (g : α), g +ᵥ s = +ᵥ s) :
s.Normal
theorem normal_of_eq_cosets {α : Type u_1} [] (s : ) (h : ∀ (g : α), g s = s) :
s.Normal
theorem normal_iff_eq_addCosets {α : Type u_1} [] (s : ) :
s.Normal ∀ (g : α), g +ᵥ s = +ᵥ s
theorem normal_iff_eq_cosets {α : Type u_1} [] (s : ) :
s.Normal ∀ (g : α), g s = s
theorem leftAddCoset_eq_iff {α : Type u_1} [] (s : ) {x : α} {y : α} :
x +ᵥ s = y +ᵥ s -x + y s
theorem leftCoset_eq_iff {α : Type u_1} [] (s : ) {x : α} {y : α} :
x s = y s x⁻¹ * y s
theorem rightAddCoset_eq_iff {α : Type u_1} [] (s : ) {x : α} {y : α} :
+ᵥ s = +ᵥ s y + -x s
theorem rightCoset_eq_iff {α : Type u_1} [] (s : ) {x : α} {y : α} :
s = s y * x⁻¹ s
def QuotientAddGroup.leftRel {α : Type u_1} [] (s : ) :

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

Equations
Instances For
def QuotientGroup.leftRel {α : Type u_1} [] (s : ) :

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

Equations
Instances For
theorem QuotientAddGroup.leftRel_apply {α : Type u_1} [] {s : } {x : α} {y : α} :
Setoid.r x y -x + y s
theorem QuotientGroup.leftRel_apply {α : Type u_1} [] {s : } {x : α} {y : α} :
theorem QuotientAddGroup.leftRel_eq {α : Type u_1} [] (s : ) :
Setoid.r = fun (x y : α) => -x + y s
theorem QuotientGroup.leftRel_eq {α : Type u_1} [] (s : ) :
Setoid.r = fun (x y : α) => x⁻¹ * y s
theorem QuotientGroup.leftRel_r_eq_leftCosetEquivalence {α : Type u_1} [] (s : ) :
Setoid.r =
theorem QuotientAddGroup.leftRelDecidable.proof_1 {α : Type u_1} [] (s : ) (x : α) (y : α) :
Decidable (Setoid.r x y) = Decidable ((fun (x y : α) => -x + y s) x y)
instance QuotientAddGroup.leftRelDecidable {α : Type u_1} [] (s : ) [DecidablePred fun (x : α) => x s] :
DecidableRel Setoid.r
Equations
• = .mpr (inst (-x + y))
instance QuotientGroup.leftRelDecidable {α : Type u_1} [] (s : ) [DecidablePred fun (x : α) => x s] :
DecidableRel Setoid.r
Equations

α ⧸ 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 : ) => }

α ⧸ 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 : ) => }
def QuotientAddGroup.rightRel {α : Type u_1} [] (s : ) :

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

Equations
Instances For
def QuotientGroup.rightRel {α : Type u_1} [] (s : ) :

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

Equations
Instances For
theorem QuotientAddGroup.rightRel_apply {α : Type u_1} [] {s : } {x : α} {y : α} :
Setoid.r x y y + -x s
theorem QuotientGroup.rightRel_apply {α : Type u_1} [] {s : } {x : α} {y : α} :
theorem QuotientAddGroup.rightRel_eq {α : Type u_1} [] (s : ) :
Setoid.r = fun (x y : α) => y + -x s
theorem QuotientGroup.rightRel_eq {α : Type u_1} [] (s : ) :
Setoid.r = fun (x y : α) => y * x⁻¹ s
theorem QuotientGroup.rightRel_r_eq_rightCosetEquivalence {α : Type u_1} [] (s : ) :
Setoid.r =
theorem QuotientAddGroup.rightRelDecidable.proof_1 {α : Type u_1} [] (s : ) (x : α) (y : α) :
Decidable (Setoid.r x y) = Decidable ((fun (x y : α) => y + -x s) x y)
instance QuotientAddGroup.rightRelDecidable {α : Type u_1} [] (s : ) [DecidablePred fun (x : α) => x s] :
DecidableRel Setoid.r
Equations
• = .mpr (inst (y + -x))
instance QuotientGroup.rightRelDecidable {α : Type u_1} [] (s : ) [DecidablePred fun (x : α) => x s] :
DecidableRel Setoid.r
Equations
theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_2 {α : Type u_1} [] (s : ) (a : α) (b : α) :
Setoid.r a bSetoid.r ((fun (g : α) => -g) a) ((fun (g : α) => -g) b)
theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_3 {α : Type u_1} [] (s : ) (g : ) :
Quotient.map' (fun (g : α) => -g) (Quotient.map' (fun (g : α) => -g) g) = g
theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_1 {α : Type u_1} [] (s : ) (a : α) (b : α) :
Setoid.r a bSetoid.r ((fun (g : α) => -g) a) ((fun (g : α) => -g) b)

Right cosets are in bijection with left cosets.

Equations
Instances For
theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_4 {α : Type u_1} [] (s : ) (g : α s) :
Quotient.map' (fun (g : α) => -g) (Quotient.map' (fun (g : α) => -g) g) = g

Right cosets are in bijection with left cosets.

Equations
Instances For
instance QuotientAddGroup.fintypeQuotientRightRel {α : Type u_1} [] (s : ) [Fintype (α s)] :
Equations
instance QuotientGroup.fintypeQuotientRightRel {α : Type u_1} [] (s : ) [Fintype (α s)] :
Equations
theorem QuotientAddGroup.card_quotient_rightRel {α : Type u_1} [] (s : ) [Fintype (α s)] :
theorem QuotientGroup.card_quotient_rightRel {α : Type u_1} [] (s : ) [Fintype (α s)] :
instance QuotientAddGroup.fintype {α : Type u_1} [] [] (s : ) [DecidableRel Setoid.r] :
Fintype (α s)
Equations
instance QuotientGroup.fintype {α : Type u_1} [] [] (s : ) [DecidableRel Setoid.r] :
Fintype (α s)
Equations
abbrev QuotientAddGroup.mk {α : Type u_1} [] {s : } (a : α) :
α s

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

Equations
• a =
Instances For
@[reducible, inline]
abbrev QuotientGroup.mk {α : Type u_1} [] {s : } (a : α) :
α s

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

Equations
• a =
Instances For
theorem QuotientAddGroup.mk_surjective {α : Type u_1} [] {s : } :
theorem QuotientGroup.mk_surjective {α : Type u_1} [] {s : } :
Function.Surjective QuotientGroup.mk
@[simp]
theorem QuotientAddGroup.range_mk {α : Type u_1} [] {s : } :
@[simp]
theorem QuotientGroup.range_mk {α : Type u_1} [] {s : } :
Set.range QuotientGroup.mk = Set.univ
theorem QuotientAddGroup.induction_on {α : Type u_1} [] {s : } {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
C x
theorem QuotientGroup.induction_on {α : Type u_1} [] {s : } {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
C x
Coe α (α s)
Equations
instance QuotientGroup.instCoeQuotientSubgroup {α : Type u_1} [] {s : } :
Coe α (α s)
Equations
• QuotientGroup.instCoeQuotientSubgroup = { coe := QuotientGroup.mk }
theorem QuotientAddGroup.induction_on' {α : Type u_1} [] {s : } {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
C x
theorem QuotientGroup.induction_on' {α : Type u_1} [] {s : } {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
C x
@[simp]
theorem QuotientAddGroup.quotient_liftOn_mk {α : Type u_1} [] {s : } {β : Sort u_2} (f : αβ) (h : ∀ (a b : α), Setoid.r a bf a = f b) (x : α) :
Quotient.liftOn' (x) f h = f x
@[simp]
theorem QuotientGroup.quotient_liftOn_mk {α : Type u_1} [] {s : } {β : Sort u_2} (f : αβ) (h : ∀ (a b : α), Setoid.r a bf a = f b) (x : α) :
Quotient.liftOn' (x) f h = f x
theorem QuotientAddGroup.forall_mk {α : Type u_1} [] {s : } {C : α sProp} :
(∀ (x : α s), C x) ∀ (x : α), C x
theorem QuotientGroup.forall_mk {α : Type u_1} [] {s : } {C : α sProp} :
(∀ (x : α s), C x) ∀ (x : α), C x
theorem QuotientAddGroup.exists_mk {α : Type u_1} [] {s : } {C : α sProp} :
(∃ (x : α s), C x) ∃ (x : α), C x
theorem QuotientGroup.exists_mk {α : Type u_1} [] {s : } {C : α sProp} :
(∃ (x : α s), C x) ∃ (x : α), C x
Equations
• = { default := 0 }
instance QuotientGroup.instInhabitedQuotientSubgroup {α : Type u_1} [] (s : ) :
Inhabited (α s)
Equations
• = { default := 1 }
theorem QuotientAddGroup.eq {α : Type u_1} [] {s : } {a : α} {b : α} :
a = b -a + b s
theorem QuotientGroup.eq {α : Type u_1} [] {s : } {a : α} {b : α} :
a = b a⁻¹ * b s
theorem QuotientAddGroup.eq' {α : Type u_1} [] {s : } {a : α} {b : α} :
a = b -a + b s
theorem QuotientGroup.eq' {α : Type u_1} [] {s : } {a : α} {b : α} :
a = b a⁻¹ * b s
theorem QuotientAddGroup.out_eq' {α : Type u_1} [] {s : } (a : α s) :
() = a
theorem QuotientGroup.out_eq' {α : Type u_1} [] {s : } (a : α s) :
() = a
theorem QuotientAddGroup.mk_out'_eq_mul {α : Type u_1} [] (s : ) (g : α) :
∃ (h : s), = g + h
theorem QuotientGroup.mk_out'_eq_mul {α : Type u_1} [] (s : ) (g : α) :
∃ (h : s), = g * h
@[simp]
theorem QuotientAddGroup.mk_add_of_mem {α : Type u_1} [] {s : } {b : α} (a : α) (hb : b s) :
(a + b) = a
@[simp]
theorem QuotientGroup.mk_mul_of_mem {α : Type u_1} [] {s : } {b : α} (a : α) (hb : b s) :
(a * b) = a
theorem QuotientAddGroup.eq_class_eq_leftCoset {α : Type u_1} [] (s : ) (g : α) :
{x : α | x = g} = g +ᵥ s
theorem QuotientGroup.eq_class_eq_leftCoset {α : Type u_1} [] (s : ) (g : α) :
{x : α | x = g} = g s
theorem QuotientAddGroup.preimage_image_mk {α : Type u_1} [] (N : ) (s : Set α) :
QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 + x) ⁻¹' s
abbrev QuotientAddGroup.preimage_image_mk.match_1 {α : Type u_1} [] (N : ) (s : Set α) (x : α) (motive : (x_1s, -x_1 + x N)Prop) :
∀ (x_1 : x_1s, -x_1 + x N), (∀ (y : α) (hs : y s) (hN : -y + x N), motive )motive x_1
Equations
• =
Instances For
abbrev QuotientAddGroup.preimage_image_mk.match_2 {α : Type u_1} [] (N : ) (s : Set α) (x : α) (motive : (x_1N, x + x_1 s)Prop) :
∀ (x_1 : x_1N, x + x_1 s), (∀ (z : α) (hz : z N) (hxz : x + z s), motive )motive x_1
Equations
• =
Instances For
theorem QuotientGroup.preimage_image_mk {α : Type u_1} [] (N : ) (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} [] (N : ) (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} [] (N : ) (s : Set α) :
QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 * x) '' s
theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_3 {α : Type u_1} [] {s : } (g : α) :
∀ (x : (g +ᵥ s)), (fun (x : s) => g + x, ) ((fun (x : (g +ᵥ s)) => -g + x, ) x) = x
abbrev AddSubgroup.leftCosetEquivAddSubgroup.match_1 {α : Type u_1} [] {s : } (g : α) (motive : (g +ᵥ s)Prop) :
∀ (x : (g +ᵥ s)), (∀ (x : α) (hx : x g +ᵥ s), motive x, hx)motive x
Equations
• =
Instances For
abbrev AddSubgroup.leftCosetEquivAddSubgroup.match_2 {α : Type u_1} [] {s : } (motive : sProp) :
∀ (x : s), (∀ (g : α) (hg : g s), motive g, hg)motive x
Equations
• =
Instances For
theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_2 {α : Type u_1} [] {s : } (g : α) (x : s) :
as, (fun (x : α) => g +ᵥ x) a = g + x
theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_4 {α : Type u_1} [] {s : } (g : α) :
∀ (x : s), (fun (x : (g +ᵥ s)) => -g + x, ) ((fun (x : s) => g + x, ) x) = x
def AddSubgroup.leftCosetEquivAddSubgroup {α : Type u_1} [] {s : } (g : α) :
(g +ᵥ s) s

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

Equations
• = { toFun := fun (x : (g +ᵥ s)) => -g + x, , invFun := fun (x : s) => g + x, , left_inv := , right_inv := }
Instances For
theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_1 {α : Type u_1} [] {s : } (g : α) (x : (g +ᵥ s)) :
-g + x s
def Subgroup.leftCosetEquivSubgroup {α : Type u_1} [] {s : } (g : α) :
(g s) s

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

Equations
• = { toFun := fun (x : (g s)) => g⁻¹ * x, , invFun := fun (x : s) => g * x, , left_inv := , right_inv := }
Instances For
theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_3 {α : Type u_1} [] {s : } (g : α) :
∀ (x : ( +ᵥ s)), (fun (x : s) => x + g, ) ((fun (x : ( +ᵥ s)) => x + -g, ) x) = x
def AddSubgroup.rightCosetEquivAddSubgroup {α : Type u_1} [] {s : } (g : α) :
( +ᵥ s) s

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

Equations
• = { toFun := fun (x : ( +ᵥ s)) => x + -g, , invFun := fun (x : s) => x + g, , left_inv := , right_inv := }
Instances For
theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_2 {α : Type u_1} [] {s : } (g : α) (x : s) :
as, (fun (x : α) => ) a = x + g
theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_1 {α : Type u_1} [] {s : } (g : α) (x : ( +ᵥ s)) :
x + -g s
abbrev AddSubgroup.rightCosetEquivAddSubgroup.match_1 {α : Type u_1} [] {s : } (g : α) (motive : ( +ᵥ s)Prop) :
∀ (x : ( +ᵥ s)), (∀ (x : α) (hx : x +ᵥ s), motive x, hx)motive x
Equations
• =
Instances For
theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_4 {α : Type u_1} [] {s : } (g : α) :
∀ (x : s), (fun (x : ( +ᵥ s)) => x + -g, ) ((fun (x : s) => x + g, ) x) = x
def Subgroup.rightCosetEquivSubgroup {α : Type u_1} [] {s : } (g : α) :
( s) s

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

Equations
• = { toFun := fun (x : ( s)) => x * g⁻¹, , invFun := fun (x : s) => x * g, , left_inv := , right_inv := }
Instances For
({ x : α // x = L } ( +ᵥ s)) = ({ x : α // x = L } {x : α | x = ()})
({ x : α // } { x : α // }) = ({ x : α // } { x : α // })
α (α s) × s

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def Subgroup.groupEquivQuotientProdSubgroup {α : Type u_1} [] {s : } :
α (α s) × s

A (non-canonical) bijection between a group α and the product (α/s) × s

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddSubgroup.quotientEquivOfEq.proof_2 {α : Type u_1} [] {s : } {t : } (h : s = t) (_a : α) (_b : α) (h' : Setoid.r _a _b) :
Setoid.r (id _a) (id _b)
theorem AddSubgroup.quotientEquivOfEq.proof_3 {α : Type u_1} [] {s : } {t : } (h : s = t) (q : α s) :
Quotient.map' id (Quotient.map' id q) = q
theorem AddSubgroup.quotientEquivOfEq.proof_1 {α : Type u_1} [] {s : } {t : } (h : s = t) (_a : α) (_b : α) (h' : Setoid.r _a _b) :
Setoid.r (id _a) (id _b)
def AddSubgroup.quotientEquivOfEq {α : Type u_1} [] {s : } {t : } (h : s = t) :
α s α t

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

Equations
• = { toFun := , invFun := , left_inv := , right_inv := }
Instances For
theorem AddSubgroup.quotientEquivOfEq.proof_4 {α : Type u_1} [] {s : } {t : } (h : s = t) (q : α t) :
Quotient.map' id (Quotient.map' id q) = q
def Subgroup.quotientEquivOfEq {α : Type u_1} [] {s : } {t : } (h : s = t) :
α s α t

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

Equations
• = { toFun := , invFun := , left_inv := , right_inv := }
Instances For
theorem Subgroup.quotientEquivOfEq_mk {α : Type u_1} [] {s : } {t : } (h : s = t) (a : α) :
= a
theorem AddSubgroup.quotientEquivSumOfLE'.proof_2 {α : Type u_1} [] {t : } (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (g : α) :
-f () + g t
theorem AddSubgroup.quotientEquivSumOfLE'.proof_1 {α : Type u_1} [] {s : } {t : } (h_le : s t) (b : α) (c : α) (h : Setoid.r b c) :
Setoid.r (id b) (id c)
theorem AddSubgroup.quotientEquivSumOfLE'.proof_3 {α : Type u_1} [] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (b : α) (c : α) (h : Setoid.r b c) :
Setoid.r ((fun (g : α) => -f () + g, ) b) ((fun (g : α) => -f () + g, ) c)
def AddSubgroup.quotientEquivSumOfLE' {α : Type u_1} [] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) :
α s (α t) × t s.addSubgroupOf 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 AddSubgroup.quotientEquivSumOfLE.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddSubgroup.quotientEquivSumOfLE'.proof_5 {α : Type u_1} [] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (q : ) :
(fun (a : (α t) × t s.addSubgroupOf t) => Quotient.map' (fun (b : t) => f a.1 + b) a.2) ((fun (a : α s) => (Quotient.map' id a, Quotient.map' (fun (g : α) => -f () + g, ) a)) q) = q
theorem AddSubgroup.quotientEquivSumOfLE'.proof_6 {α : Type u_1} [] {s : } {t : } (h_le : s t✝) (f : α t✝α) (hf : Function.RightInverse f QuotientAddGroup.mk) (t : (α t✝) × t✝ s.addSubgroupOf t✝) :
(fun (a : α s) => (Quotient.map' id a, Quotient.map' (fun (g : α) => -f () + g, ) a)) ((fun (a : (α t✝) × t✝ s.addSubgroupOf t✝) => Quotient.map' (fun (b : t✝) => f a.1 + b) a.2) t) = t
theorem AddSubgroup.quotientEquivSumOfLE'.proof_4 {α : Type u_1} [] {s : } {t : } (f : α tα) (a : (α t) × t s.addSubgroupOf t) (b : t) (c : t) (h : Setoid.r b c) :
Setoid.r ((fun (b : t) => f a.1 + b) b) ((fun (b : t) => f a.1 + b) c)
@[simp]
theorem Subgroup.quotientEquivProdOfLE'_symm_apply {α : Type u_1} [] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) (a : (α t) × t s.subgroupOf t) :
().symm a = Quotient.map' (fun (b : t) => f a.1 * b) a.2
@[simp]
theorem AddSubgroup.quotientEquivSumOfLE'_apply {α : Type u_1} [] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : α s) :
() a = (Quotient.map' id a, Quotient.map' (fun (g : α) => -f () + g, ) a)
@[simp]
theorem AddSubgroup.quotientEquivSumOfLE'_symm_apply {α : Type u_1} [] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : (α t) × t s.addSubgroupOf t) :
().symm a = Quotient.map' (fun (b : t) => f a.1 + b) a.2
@[simp]
theorem Subgroup.quotientEquivProdOfLE'_apply {α : Type u_1} [] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) (a : α s) :
() a = (Quotient.map' id a, Quotient.map' (fun (g : α) => (f ())⁻¹ * g, ) a)
def Subgroup.quotientEquivProdOfLE' {α : Type u_1} [] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) :
α s (α t) × t s.subgroupOf 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 Subgroup.quotientEquivProdOfLE.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def AddSubgroup.quotientEquivSumOfLE {α : Type u_1} [] {s : } {t : } (h_le : s t) :
α s (α t) × t s.addSubgroupOf t

If H ≤ K, then G/H ≃ G/K × K/H nonconstructively. The constructive version is quotientEquivProdOfLE'.

Equations
Instances For
theorem AddSubgroup.quotientEquivSumOfLE.proof_1 {α : Type u_1} [] {t : } (q : ) :
Quotient.mk'' q.out' = q
@[simp]
theorem AddSubgroup.quotientEquivSumOfLE_symm_apply {α : Type u_1} [] {s : } {t : } (h_le : s t) (a : (α t) × t s.addSubgroupOf t) :
.symm a = Quotient.map' (fun (b : t) => + b) a.2
@[simp]
theorem Subgroup.quotientEquivProdOfLE_apply {α : Type u_1} [] {s : } {t : } (h_le : s t) (a : α s) :
a = (Quotient.map' id a, Quotient.map' (fun (g : α) => ().out'⁻¹ * g, ) a)
@[simp]
theorem Subgroup.quotientEquivProdOfLE_symm_apply {α : Type u_1} [] {s : } {t : } (h_le : s t) (a : (α t) × t s.subgroupOf t) :
.symm a = Quotient.map' (fun (b : t) => * b) a.2
@[simp]
theorem AddSubgroup.quotientEquivSumOfLE_apply {α : Type u_1} [] {s : } {t : } (h_le : s t) (a : α s) :
a = (Quotient.map' id a, Quotient.map' (fun (g : α) => -().out' + g, ) a)
noncomputable def Subgroup.quotientEquivProdOfLE {α : Type u_1} [] {s : } {t : } (h_le : s t) :
α s (α t) × t s.subgroupOf t

If H ≤ K, then G/H ≃ G/K × K/H nonconstructively. The constructive version is quotientEquivProdOfLE'.

Equations
Instances For
def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE {α : Type u_1} [] {s : } {t : } (H : ) (h : s t) :

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

Equations
• = { toFun := , inj' := }
Instances For
= q₁ = q₂
theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE.proof_1 {α : Type u_1} [] {s : } {t : } (H : ) (h : s t) (a : s) (b : s) :
Setoid.r a bSetoid.r () ()
def Subgroup.quotientSubgroupOfEmbeddingOfLE {α : Type u_1} [] {s : } {t : } (H : ) (h : s t) :
s H.subgroupOf s t H.subgroupOf t

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

Equations
• = { toFun := , inj' := }
Instances For
@[simp]
theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE_apply_mk {α : Type u_1} [] {s : } {t : } (H : ) (h : s t) (g : s) :
= ()
@[simp]
theorem Subgroup.quotientSubgroupOfEmbeddingOfLE_apply_mk {α : Type u_1} [] {s : } {t : } (H : ) (h : s t) (g : s) :
= ( g)
def AddSubgroup.quotientAddSubgroupOfMapOfLE {α : Type u_1} [] {s : } {t : } (H : ) (h : s t) :

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

Equations
Instances For
theorem AddSubgroup.quotientAddSubgroupOfMapOfLE.proof_1 {α : Type u_1} [] {s : } {t : } (H : ) (h : s t) (a : H) (b : H) :
Setoid.r a bSetoid.r (id a) (id b)
def Subgroup.quotientSubgroupOfMapOfLE {α : Type u_1} [] {s : } {t : } (H : ) (h : s t) :
H s.subgroupOf HH t.subgroupOf H

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

Equations
Instances For
@[simp]
theorem AddSubgroup.quotientAddSubgroupOfMapOfLE_apply_mk {α : Type u_1} [] {s : } {t : } (H : ) (h : s t) (g : H) :
@[simp]
theorem Subgroup.quotientSubgroupOfMapOfLE_apply_mk {α : Type u_1} [] {s : } {t : } (H : ) (h : s t) (g : H) :
= g
def AddSubgroup.quotientMapOfLE {α : Type u_1} [] {s : } {t : } (h : s t) :
α sα t

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

Equations
Instances For
theorem AddSubgroup.quotientMapOfLE.proof_1 {α : Type u_1} [] {s : } {t : } (h : s t) (a : α) (b : α) :
Setoid.r a bSetoid.r (id a) (id b)
def Subgroup.quotientMapOfLE {α : Type u_1} [] {s : } {t : } (h : s t) :
α sα t

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

Equations
Instances For
@[simp]
theorem AddSubgroup.quotientMapOfLE_apply_mk {α : Type u_1} [] {s : } {t : } (h : s t) (g : α) :
= g
@[simp]
theorem Subgroup.quotientMapOfLE_apply_mk {α : Type u_1} [] {s : } {t : } (h : s t) (g : α) :
= g
theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding.proof_2 {α : Type u_1} [] {ι : Type u_2} (f : ι) (H : ) (q₁ : Quotient (QuotientAddGroup.leftRel ((⨅ (i : ι), f i).addSubgroupOf H))) (q₂ : Quotient (QuotientAddGroup.leftRel ((⨅ (i : ι), f i).addSubgroupOf H))) :
(fun (q : H (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) => ) q₁ = (fun (q : H (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) => ) q₂q₁ = q₂
def AddSubgroup.quotientiInfAddSubgroupOfEmbedding {α : Type u_1} [] {ι : Type u_2} (f : ι) (H : ) :
H (⨅ (i : ι), f i).addSubgroupOf H (i : ι) → H (f i).addSubgroupOf H

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

Equations
• = { toFun := fun (q : H (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) => , inj' := }
Instances For
theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding.proof_1 {α : Type u_1} [] {ι : Type u_2} (f : ι) (i : ι) :
iInf f f i
@[simp]
theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply {α : Type u_1} [] {ι : Type u_2} (f : ι) (H : ) (q : H (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) :
@[simp]
theorem Subgroup.quotientiInfSubgroupOfEmbedding_apply {α : Type u_1} [] {ι : Type u_2} (f : ι) (H : ) (q : H (⨅ (i : ι), f i).subgroupOf H) (i : ι) :
def Subgroup.quotientiInfSubgroupOfEmbedding {α : Type u_1} [] {ι : Type u_2} (f : ι) (H : ) :
H (⨅ (i : ι), f i).subgroupOf H (i : ι) → H (f i).subgroupOf H

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

Equations
• = { toFun := fun (q : H (⨅ (i : ι), f i).subgroupOf H) (i : ι) => , inj' := }
Instances For
@[simp]
theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply_mk {α : Type u_1} [] {ι : Type u_2} (f : ι) (H : ) (g : H) (i : ι) :
= g
@[simp]
theorem Subgroup.quotientiInfSubgroupOfEmbedding_apply_mk {α : Type u_1} [] {ι : Type u_2} (f : ι) (H : ) (g : H) (i : ι) :
(g) i = g
theorem AddSubgroup.quotientiInfEmbedding.proof_2 {α : Type u_1} [] {ι : Type u_2} (f : ι) (q₁ : Quotient (QuotientAddGroup.leftRel (⨅ (i : ι), f i))) (q₂ : Quotient (QuotientAddGroup.leftRel (⨅ (i : ι), f i))) :
(fun (q : α ⨅ (i : ι), f i) (i : ι) => ) q₁ = (fun (q : α ⨅ (i : ι), f i) (i : ι) => ) q₂q₁ = q₂
theorem AddSubgroup.quotientiInfEmbedding.proof_1 {α : Type u_1} [] {ι : Type u_2} (f : ι) (i : ι) :
iInf f f i
def AddSubgroup.quotientiInfEmbedding {α : Type u_1} [] {ι : Type u_2} (f : ι) :
α ⨅ (i : ι), f i (i : ι) → α f i

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

Equations
• = { toFun := fun (q : α ⨅ (i : ι), f i) (i : ι) => , inj' := }
Instances For
@[simp]
theorem AddSubgroup.quotientiInfEmbedding_apply {α : Type u_1} [] {ι : Type u_2} (f : ι) (q : α ⨅ (i : ι), f i) (i : ι) :
@[simp]
theorem Subgroup.quotientiInfEmbedding_apply {α : Type u_1} [] {ι : Type u_2} (f : ι) (q : α ⨅ (i : ι), f i) (i : ι) :
def Subgroup.quotientiInfEmbedding {α : Type u_1} [] {ι : Type u_2} (f : ι) :
α ⨅ (i : ι), f i (i : ι) → α f i

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

Equations
• = { toFun := fun (q : α ⨅ (i : ι), f i) (i : ι) => , inj' := }
Instances For
@[simp]
theorem AddSubgroup.quotientiInfEmbedding_apply_mk {α : Type u_1} [] {ι : Type u_2} (f : ι) (g : α) (i : ι) :
(g) i = g
@[simp]
theorem Subgroup.quotientiInfEmbedding_apply_mk {α : Type u_1} [] {ι : Type u_2} (f : ι) (g : α) (i : ι) :
(g) i = g

Lagrange's Theorem: The order of an additive subgroup divides the order of its ambient additive group.

theorem Subgroup.card_subgroup_dvd_card {α : Type u_1} [] (s : ) :

Lagrange's Theorem: The order of a subgroup divides the order of its ambient group.

theorem AddSubgroup.card_quotient_dvd_card {α : Type u_1} [] (s : ) :
Nat.card (α s)
theorem Subgroup.card_quotient_dvd_card {α : Type u_1} [] (s : ) :
Nat.card (α s)
theorem AddSubgroup.card_dvd_of_injective {α : Type u_1} [] {H : Type u_2} [] (f : α →+ H) (hf : ) :
theorem Subgroup.card_dvd_of_injective {α : Type u_1} [] {H : Type u_2} [] (f : α →* H) (hf : ) :
theorem AddSubgroup.card_dvd_of_le {α : Type u_1} [] {H : } {K : } (hHK : H K) :
theorem Subgroup.card_dvd_of_le {α : Type u_1} [] {H : } {K : } (hHK : H K) :
theorem AddSubgroup.card_comap_dvd_of_injective {α : Type u_1} [] {H : Type u_2} [] (K : ) (f : α →+ H) (hf : ) :
Nat.card () Nat.card K
theorem Subgroup.card_comap_dvd_of_injective {α : Type u_1} [] {H : Type u_2} [] (K : ) (f : α →* H) (hf : ) :
Nat.card () Nat.card K
theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_4 {α : Type u_1} [] (s : ) (t : Set (α s)) :
∀ (x : (QuotientAddGroup.mk ⁻¹' t)), (fun (a : s × t) => Quotient.out' a.2 + a.1, ) ((fun (a : (QuotientAddGroup.mk ⁻¹' t)) => (- + a, , a, )) x) = x
abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_1 {α : Type u_1} [] (s : ) (t : Set (α s)) (motive : (QuotientAddGroup.mk ⁻¹' t)Prop) :
∀ (x : (QuotientAddGroup.mk ⁻¹' t)), (∀ (a : α) (ha : a QuotientAddGroup.mk ⁻¹' t), motive a, ha)motive x
Equations
• =
Instances For
theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_1 {α : Type u_1} [] (s : ) (t : Set (α s)) (a : (QuotientAddGroup.mk ⁻¹' t)) :
- + a s
noncomputable def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet {α : Type u_1} [] (s : ) (t : Set (α s)) :
(QuotientAddGroup.mk ⁻¹' t) s × t

If s is a subgroup of the additive 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
• One or more equations did not get rendered due to their size.
Instances For
abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_2 {α : Type u_1} [] (s : ) (t : Set (α s)) (motive : s × tProp) :
∀ (x : s × t), (∀ (a : α) (ha : a s) (x : α s) (hx : x t), motive (a, ha, x, hx))motive x
Equations
• =
Instances For
theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_3 {α : Type u_1} [] (s : ) (t : Set (α s)) (a : s × t) :
(Quotient.out' a.2 + a.1) t
theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_5 {α : Type u_1} [] (s : ) (t : Set (α s)) :
∀ (x : s × t), (fun (a : (QuotientAddGroup.mk ⁻¹' t)) => (- + a, , a, )) ((fun (a : s × t) => Quotient.out' a.2 + a.1, ) x) = x
theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_2 {α : Type u_1} [] (s : ) (t : Set (α s)) (a : (QuotientAddGroup.mk ⁻¹' 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.