Documentation

Mathlib.GroupTheory.Coset

Cosets #

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

Main definitions #

Notation #

def leftAddCoset {α : Type u_1} [inst : Add α] (a : α) (s : Set α) :
Set α

The left coset a+s for an element a : α and a subset s : set α

Equations
def leftCoset {α : Type u_1} [inst : Mul α] (a : α) (s : Set α) :
Set α

The left coset a * s for an element a : α and a subset s : set α

Equations
def rightAddCoset {α : Type u_1} [inst : Add α] (s : Set α) (a : α) :
Set α

The right coset s+a for an element a : α and a subset s : set α

Equations
def rightCoset {α : Type u_1} [inst : Mul α] (s : Set α) (a : α) :
Set α

The right coset s * a for an element a : α and a subset s : set α

Equations

The left coset a * s for an element a : α and a subset s : set α

Equations

The left coset a+s for an element a : α and a subset s : set α

Equations

The right coset s * a for an element a : α and a subset s : set α

Equations

The right coset s+a for an element a : α and a subset s : set α

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

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

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

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

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

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

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

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

Equations
@[simp]
theorem leftAddCoset_assoc {α : Type u_1} [inst : AddSemigroup α] (s : Set α) (a : α) (b : α) :
@[simp]
theorem leftCoset_assoc {α : Type u_1} [inst : Semigroup α] (s : Set α) (a : α) (b : α) :
leftCoset a (leftCoset b s) = leftCoset (a * b) s
@[simp]
theorem rightAddCoset_assoc {α : Type u_1} [inst : AddSemigroup α] (s : Set α) (a : α) (b : α) :
@[simp]
theorem rightCoset_assoc {α : Type u_1} [inst : Semigroup α] (s : Set α) (a : α) (b : α) :
theorem leftAddCoset_rightAddCoset {α : Type u_1} [inst : AddSemigroup α] (s : Set α) (a : α) (b : α) :
theorem leftCoset_rightCoset {α : Type u_1} [inst : Semigroup α] (s : Set α) (a : α) (b : α) :
@[simp]
theorem zero_leftAddCoset {α : Type u_1} [inst : AddMonoid α] (s : Set α) :
@[simp]
theorem one_leftCoset {α : Type u_1} [inst : Monoid α] (s : Set α) :
leftCoset 1 s = s
@[simp]
theorem rightAddCoset_zero {α : Type u_1} [inst : AddMonoid α] (s : Set α) :
@[simp]
theorem rightCoset_one {α : Type u_1} [inst : Monoid α] (s : Set α) :
theorem mem_own_leftAddCoset {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) (a : α) :
a leftAddCoset a s
theorem mem_own_leftCoset {α : Type u_1} [inst : Monoid α] (s : Submonoid α) (a : α) :
a leftCoset a s
theorem mem_own_rightAddCoset {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) (a : α) :
a rightAddCoset (s) a
theorem mem_own_rightCoset {α : Type u_1} [inst : Monoid α] (s : Submonoid α) (a : α) :
a rightCoset (s) a
theorem mem_leftAddCoset_leftAddCoset {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) {a : α} (ha : leftAddCoset a s = s) :
a s
theorem mem_leftCoset_leftCoset {α : Type u_1} [inst : Monoid α] (s : Submonoid α) {a : α} (ha : leftCoset a s = s) :
a s
theorem mem_rightAddCoset_rightAddCoset {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) {a : α} (ha : rightAddCoset (s) a = s) :
a s
theorem mem_rightCoset_rightCoset {α : Type u_1} [inst : Monoid α] (s : Submonoid α) {a : α} (ha : rightCoset (s) a = s) :
a s
abbrev mem_leftAddCoset_iff.match_1 {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α) (motive : x leftAddCoset a sProp) :
(x : x leftAddCoset a s) → ((b : α) → (hb : b s) → (Eq : (fun x => a + x) b = x) → motive (_ : a, a s (fun x => a + x) a = x)) → motive x
Equations
theorem mem_leftAddCoset_iff {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α) :
x leftAddCoset a s -a + x s
theorem mem_leftCoset_iff {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α) :
x leftCoset a s a⁻¹ * x s
abbrev mem_rightAddCoset_iff.match_1 {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α) (motive : x rightAddCoset s aProp) :
(x : x rightAddCoset s a) → ((b : α) → (hb : b s) → (Eq : (fun x => x + a) b = x) → motive (_ : a, a s (fun x => x + a) a = x)) → motive x
Equations
theorem mem_rightAddCoset_iff {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α) :
x rightAddCoset s a x + -a s
theorem mem_rightCoset_iff {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α) :
theorem leftAddCoset_mem_leftAddCoset {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {a : α} (ha : a s) :
leftAddCoset a s = s
theorem leftCoset_mem_leftCoset {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α} (ha : a s) :
leftCoset a s = s
theorem rightAddCoset_mem_rightAddCoset {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {a : α} (ha : a s) :
rightAddCoset (s) a = s
theorem rightCoset_mem_rightCoset {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α} (ha : a s) :
rightCoset (s) a = s
abbrev orbit_addSubgroup_eq_rightCoset.match_2 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (a : α) (_b : α) (motive : _b rightAddCoset (s) aProp) :
(x : _b rightAddCoset (s) a) → ((c : α) → (d : c s) → (e : (fun x => x + a) c = _b) → motive (_ : a, a s (fun x => x + a) a = _b)) → motive x
Equations
abbrev orbit_addSubgroup_eq_rightCoset.match_1 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (a : α) (_b : α) (motive : _b AddAction.orbit { x // x s } aProp) :
(x : _b AddAction.orbit { x // x s } a) → ((c : { x // x s }) → (d : (fun x => x +ᵥ a) c = _b) → motive (_ : y, (fun x => x +ᵥ a) y = _b)) → motive x
Equations
theorem orbit_addSubgroup_eq_rightCoset {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (a : α) :
AddAction.orbit { x // x s } a = rightAddCoset (s) a
theorem orbit_subgroup_eq_rightCoset {α : Type u_1} [inst : Group α] (s : Subgroup α) (a : α) :
MulAction.orbit { x // x s } a = rightCoset (s) a
theorem orbit_addSubgroup_eq_self_of_mem {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {a : α} (ha : a s) :
AddAction.orbit { x // x s } a = s
theorem orbit_subgroup_eq_self_of_mem {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α} (ha : a s) :
MulAction.orbit { x // x s } a = s
theorem orbit_addSubgroup_zero_eq_self {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) :
AddAction.orbit { x // x s } 0 = s
theorem orbit_subgroup_one_eq_self {α : Type u_1} [inst : Group α] (s : Subgroup α) :
MulAction.orbit { x // x s } 1 = s
theorem eq_addCosets_of_normal {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (N : AddSubgroup.Normal s) (g : α) :
leftAddCoset g s = rightAddCoset (s) g
theorem eq_cosets_of_normal {α : Type u_1} [inst : Group α] (s : Subgroup α) (N : Subgroup.Normal s) (g : α) :
leftCoset g s = rightCoset (s) g
theorem normal_of_eq_addCosets {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (h : ∀ (g : α), leftAddCoset g s = rightAddCoset (s) g) :
theorem normal_of_eq_cosets {α : Type u_1} [inst : Group α] (s : Subgroup α) (h : ∀ (g : α), leftCoset g s = rightCoset (s) g) :
theorem normal_iff_eq_addCosets {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) :
AddSubgroup.Normal s ∀ (g : α), leftAddCoset g s = rightAddCoset (s) g
theorem normal_iff_eq_cosets {α : Type u_1} [inst : Group α] (s : Subgroup α) :
Subgroup.Normal s ∀ (g : α), leftCoset g s = rightCoset (s) g
theorem leftAddCoset_eq_iff {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {x : α} {y : α} :
leftAddCoset x s = leftAddCoset y s -x + y s
theorem leftCoset_eq_iff {α : Type u_1} [inst : Group α] (s : Subgroup α) {x : α} {y : α} :
leftCoset x s = leftCoset y s x⁻¹ * y s
theorem rightAddCoset_eq_iff {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {x : α} {y : α} :
rightAddCoset (s) x = rightAddCoset (s) y y + -x s
theorem rightCoset_eq_iff {α : Type u_1} [inst : Group α] (s : Subgroup α) {x : α} {y : α} :
rightCoset (s) x = rightCoset (s) y y * x⁻¹ s
def QuotientAddGroup.leftRel {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) :

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

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

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

Equations
theorem QuotientAddGroup.leftRel_apply {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {x : α} {y : α} :
Setoid.r x y -x + y s
theorem QuotientGroup.leftRel_apply {α : Type u_1} [inst : Group α] {s : Subgroup α} {x : α} {y : α} :
theorem QuotientAddGroup.leftRel_eq {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) :
Setoid.r = fun x y => -x + y s
theorem QuotientGroup.leftRel_eq {α : Type u_1} [inst : Group α] (s : Subgroup α) :
Setoid.r = fun x y => x⁻¹ * y s
def QuotientAddGroup.leftRelDecidable.proof_1 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (x : α) (y : α) :
Decidable (Setoid.r x y) = Decidable ((fun x y => -x + y s) x y)
Equations
instance QuotientAddGroup.leftRelDecidable {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) [inst : DecidablePred fun x => x s] :
DecidableRel Setoid.r
Equations
instance QuotientGroup.leftRelDecidable {α : Type u_1} [inst : Group α] (s : Subgroup α) [inst : DecidablePred fun x => x s] :
DecidableRel Setoid.r
Equations

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

Equations
instance QuotientGroup.instHasQuotientSubgroup {α : Type u_1} [inst : Group α] :

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

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

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

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

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

Equations
theorem QuotientAddGroup.rightRel_apply {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {x : α} {y : α} :
Setoid.r x y y + -x s
theorem QuotientGroup.rightRel_apply {α : Type u_1} [inst : Group α] {s : Subgroup α} {x : α} {y : α} :
theorem QuotientAddGroup.rightRel_eq {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) :
Setoid.r = fun x y => y + -x s
theorem QuotientGroup.rightRel_eq {α : Type u_1} [inst : Group α] (s : Subgroup α) :
Setoid.r = fun x y => y * x⁻¹ s
instance QuotientAddGroup.rightRelDecidable {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) [inst : DecidablePred fun x => x s] :
DecidableRel Setoid.r
Equations
def QuotientAddGroup.rightRelDecidable.proof_1 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (x : α) (y : α) :
Decidable (Setoid.r x y) = Decidable ((fun x y => y + -x s) x y)
Equations
instance QuotientGroup.rightRelDecidable {α : Type u_1} [inst : Group α] (s : Subgroup α) [inst : DecidablePred fun x => x s] :
DecidableRel Setoid.r
Equations
def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_3 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (g : Quotient (QuotientAddGroup.rightRel s)) :
Quotient.map' (fun g => -g) (_ : ∀ (a b : α), Setoid.r a bSetoid.r ((fun g => -g) a) ((fun g => -g) b)) (Quotient.map' (fun g => -g) (_ : ∀ (a b : α), Setoid.r a bSetoid.r ((fun g => -g) a) ((fun g => -g) b)) g) = g
Equations
  • One or more equations did not get rendered due to their size.

Right cosets are in bijection with left cosets.

Equations
  • One or more equations did not get rendered due to their size.
def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_2 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (a : α) (b : α) :
Setoid.r a bSetoid.r ((fun g => -g) a) ((fun g => -g) b)
Equations
def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_1 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (a : α) (b : α) :
Setoid.r a bSetoid.r ((fun g => -g) a) ((fun g => -g) b)
Equations
def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_4 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (g : α s) :
Quotient.map' (fun g => -g) (_ : ∀ (a b : α), Setoid.r a bSetoid.r ((fun g => -g) a) ((fun g => -g) b)) (Quotient.map' (fun g => -g) (_ : ∀ (a b : α), Setoid.r a bSetoid.r ((fun g => -g) a) ((fun g => -g) b)) g) = g
Equations
  • One or more equations did not get rendered due to their size.

Right cosets are in bijection with left cosets.

Equations
  • One or more equations did not get rendered due to their size.
instance QuotientAddGroup.fintype {α : Type u_1} [inst : AddGroup α] [inst : Fintype α] (s : AddSubgroup α) [inst : DecidableRel Setoid.r] :
Fintype (α s)
Equations
instance QuotientGroup.fintype {α : Type u_1} [inst : Group α] [inst : Fintype α] (s : Subgroup α) [inst : DecidableRel Setoid.r] :
Fintype (α s)
Equations
abbrev QuotientAddGroup.mk {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (a : α) :
α s

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

Equations
@[inline]
abbrev QuotientGroup.mk {α : Type u_1} [inst : Group α] {s : Subgroup α} (a : α) :
α s

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

Equations
theorem QuotientAddGroup.mk_surjective {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} :
Function.Surjective QuotientAddGroup.mk
theorem QuotientGroup.mk_surjective {α : Type u_1} [inst : Group α] {s : Subgroup α} :
Function.Surjective QuotientGroup.mk
theorem QuotientAddGroup.induction_on {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {C : α sProp} (x : α s) (H : (z : α) → C z) :
C x
theorem QuotientGroup.induction_on {α : Type u_1} [inst : Group α] {s : Subgroup α} {C : α sProp} (x : α s) (H : (z : α) → C z) :
C x
Equations
  • QuotientAddGroup.instCoeTCQuotientAddSubgroupInstHasQuotientAddSubgroup = { coe := QuotientAddGroup.mk }
Equations
  • QuotientGroup.instCoeTCQuotientSubgroupInstHasQuotientSubgroup = { coe := QuotientGroup.mk }
theorem QuotientAddGroup.induction_on' {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {C : α sProp} (x : α s) (H : (z : α) → C z) :
C x
theorem QuotientGroup.induction_on' {α : Type u_1} [inst : Group α] {s : Subgroup α} {C : α sProp} (x : α s) (H : (z : α) → C z) :
C x
@[simp]
theorem QuotientAddGroup.quotient_liftOn_mk {α : Type u_2} [inst : AddGroup α] {s : AddSubgroup α} {β : Sort u_1} (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_2} [inst : Group α] {s : Subgroup α} {β : Sort u_1} (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} [inst : AddGroup α] {s : AddSubgroup α} {C : α sProp} :
((x : α s) → C x) (x : α) → C x
theorem QuotientGroup.forall_mk {α : Type u_1} [inst : Group α] {s : Subgroup α} {C : α sProp} :
((x : α s) → C x) (x : α) → C x
theorem QuotientAddGroup.exists_mk {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {C : α sProp} :
(x, C x) x, C x
theorem QuotientGroup.exists_mk {α : Type u_1} [inst : Group α] {s : Subgroup α} {C : α sProp} :
(x, C x) x, C x
theorem QuotientAddGroup.eq {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {a : α} {b : α} :
a = b -a + b s
theorem QuotientGroup.eq {α : Type u_1} [inst : Group α] {s : Subgroup α} {a : α} {b : α} :
a = b a⁻¹ * b s
theorem QuotientAddGroup.eq' {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {a : α} {b : α} :
a = b -a + b s
theorem QuotientGroup.eq' {α : Type u_1} [inst : Group α] {s : Subgroup α} {a : α} {b : α} :
a = b a⁻¹ * b s
theorem QuotientAddGroup.out_eq' {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (a : α s) :
↑(Quotient.out' a) = a
theorem QuotientGroup.out_eq' {α : Type u_1} [inst : Group α] {s : Subgroup α} (a : α s) :
↑(Quotient.out' a) = a
theorem QuotientAddGroup.mk_out'_eq_mul {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (g : α) :
h, Quotient.out' g = g + h
theorem QuotientGroup.mk_out'_eq_mul {α : Type u_1} [inst : Group α] (s : Subgroup α) (g : α) :
h, Quotient.out' g = g * h
@[simp]
theorem QuotientAddGroup.mk_add_of_mem {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {b : α} (a : α) (hb : b s) :
↑(a + b) = a
@[simp]
theorem QuotientGroup.mk_mul_of_mem {α : Type u_1} [inst : Group α] {s : Subgroup α} {b : α} (a : α) (hb : b s) :
↑(a * b) = a
theorem QuotientAddGroup.eq_class_eq_leftCoset {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (g : α) :
{ x | x = g } = leftAddCoset g s
theorem QuotientGroup.eq_class_eq_leftCoset {α : Type u_1} [inst : Group α] (s : Subgroup α) (g : α) :
{ x | x = g } = leftCoset g s
abbrev QuotientAddGroup.preimage_image_mk.match_1 {α : Type u_1} [inst : AddGroup α] (N : AddSubgroup α) (s : Set α) (x : α) (motive : (x, x s -x + x N) → Prop) :
(x : x, x s -x + x N) → ((y : α) → (hs : y s) → (hN : -y + x N) → motive (_ : x, x s -x + x N)) → motive x
Equations
theorem QuotientAddGroup.preimage_image_mk {α : Type u_1} [inst : AddGroup α] (N : AddSubgroup α) (s : Set α) :
QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = Set.unionᵢ fun x => (fun y => y + x) ⁻¹' s
abbrev QuotientAddGroup.preimage_image_mk.match_2 {α : Type u_1} [inst : AddGroup α] (N : AddSubgroup α) (s : Set α) (x : α) (motive : (x, x N x + x s) → Prop) :
(x : x, x N x + x s) → ((z : α) → (hz : z N) → (hxz : x + z s) → motive (_ : x, x N x + x s)) → motive x
Equations
theorem QuotientGroup.preimage_image_mk {α : Type u_1} [inst : Group α] (N : Subgroup α) (s : Set α) :
QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = Set.unionᵢ fun x => (fun y => y * x) ⁻¹' s
def AddSubgroup.leftCosetEquivAddSubgroup.proof_4 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α) :
∀ (x : { x // x s }), (fun x => { val := -g + x, property := (_ : -g + x s) }) ((fun x => { val := g + x, property := (_ : a, a s (fun x => g + x) a = g + x) }) x) = x
Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.leftCosetEquivAddSubgroup.proof_3 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α) :
∀ (x : ↑(leftAddCoset g s)), (fun x => { val := g + x, property := (_ : a, a s (fun x => g + x) a = g + x) }) ((fun x => { val := -g + x, property := (_ : -g + x s) }) x) = x
Equations
  • One or more equations did not get rendered due to their size.
abbrev AddSubgroup.leftCosetEquivAddSubgroup.match_2 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (motive : { x // x s }Prop) :
(x : { x // x s }) → ((g : α) → (hg : g s) → motive { val := g, property := hg }) → motive x
Equations
abbrev AddSubgroup.leftCosetEquivAddSubgroup.match_1 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α) (motive : ↑(leftAddCoset g s)Prop) :
(x : ↑(leftAddCoset g s)) → ((x : α) → (hx : x leftAddCoset g s) → motive { val := x, property := hx }) → motive x
Equations
def AddSubgroup.leftCosetEquivAddSubgroup.proof_2 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α) (x : { x // x s }) :
a, a s (fun x => g + x) a = g + x
Equations
  • (_ : a, a s (fun x => g + x) a = g + x) = (_ : a, a s (fun x => g + x) a = g + x)
def AddSubgroup.leftCosetEquivAddSubgroup.proof_1 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α) (x : ↑(leftAddCoset g s)) :
-g + x s
Equations
def AddSubgroup.leftCosetEquivAddSubgroup {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α) :
↑(leftAddCoset g s) { x // x s }

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

Equations
  • One or more equations did not get rendered due to their size.
def Subgroup.leftCosetEquivSubgroup {α : Type u_1} [inst : Group α] {s : Subgroup α} (g : α) :
↑(leftCoset g s) { x // x s }

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

Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.rightCosetEquivAddSubgroup {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α) :
↑(rightAddCoset (s) g) { x // x s }

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

Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.rightCosetEquivAddSubgroup.proof_2 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α) (x : { x // x s }) :
a, a s (fun x => x + g) a = x + g
Equations
  • (_ : a, a s (fun x => x + g) a = x + g) = (_ : a, a s (fun x => x + g) a = x + g)
abbrev AddSubgroup.rightCosetEquivAddSubgroup.match_1 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α) (motive : ↑(rightAddCoset (s) g)Prop) :
(x : ↑(rightAddCoset (s) g)) → ((x : α) → (hx : x rightAddCoset (s) g) → motive { val := x, property := hx }) → motive x
Equations
def AddSubgroup.rightCosetEquivAddSubgroup.proof_1 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α) (x : ↑(rightAddCoset (s) g)) :
x + -g s
Equations
def AddSubgroup.rightCosetEquivAddSubgroup.proof_3 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α) :
∀ (x : ↑(rightAddCoset (s) g)), (fun x => { val := x + g, property := (_ : a, a s (fun x => x + g) a = x + g) }) ((fun x => { val := x + -g, property := (_ : x + -g s) }) x) = x
Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.rightCosetEquivAddSubgroup.proof_4 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (g : α) :
∀ (x : { x // x s }), (fun x => { val := x + -g, property := (_ : x + -g s) }) ((fun x => { val := x + g, property := (_ : a, a s (fun x => x + g) a = x + g) }) x) = x
Equations
  • One or more equations did not get rendered due to their size.
def Subgroup.rightCosetEquivSubgroup {α : Type u_1} [inst : Group α] {s : Subgroup α} (g : α) :
↑(rightCoset (s) g) { x // x s }

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

Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.addGroupEquivQuotientProdAddSubgroup.proof_1 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (L : α s) :
({ x // x = L } ↑(leftAddCoset (Quotient.out' L) s)) = ({ x // x = L } { x | x = ↑(Quotient.out' L) })
Equations
  • One or more equations did not get rendered due to their size.
noncomputable def AddSubgroup.addGroupEquivQuotientProdAddSubgroup {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} :
α (α s) × { x // x s }

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

Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.addGroupEquivQuotientProdAddSubgroup.proof_2 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (L : α s) :
({ x // Quotient.mk'' x = L } { x // Quotient.mk'' x = Quotient.mk'' (Quotient.out' L) }) = ({ x // Quotient.mk'' x = L } { x // Quotient.mk'' x = L })
Equations
  • One or more equations did not get rendered due to their size.
noncomputable def Subgroup.groupEquivQuotientProdSubgroup {α : Type u_1} [inst : Group α] {s : Subgroup α} :
α (α s) × { x // x s }

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

Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivOfEq.proof_4 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (q : α t) :
Quotient.map' id (_ : ∀ (_a _b : α), Setoid.r _a _bSetoid.r (id _a) (id _b)) (Quotient.map' id (_ : ∀ (_a _b : α), Setoid.r _a _bSetoid.r (id _a) (id _b)) q) = q
Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivOfEq.proof_3 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (q : α s) :
Quotient.map' id (_ : ∀ (_a _b : α), Setoid.r _a _bSetoid.r (id _a) (id _b)) (Quotient.map' id (_ : ∀ (_a _b : α), Setoid.r _a _bSetoid.r (id _a) (id _b)) q) = q
Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivOfEq {α : Type u_1} [inst : 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
  • One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivOfEq.proof_2 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (_a : α) (_b : α) (h' : Setoid.r _a _b) :
Setoid.r (id _a) (id _b)
Equations
def AddSubgroup.quotientEquivOfEq.proof_1 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (_a : α) (_b : α) (h' : Setoid.r _a _b) :
Setoid.r (id _a) (id _b)
Equations
def Subgroup.quotientEquivOfEq {α : Type u_1} [inst : 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
  • One or more equations did not get rendered due to their size.
theorem Subgroup.quotientEquivOfEq_mk {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (h : s = t) (a : α) :
↑(Subgroup.quotientEquivOfEq h) a = a
def AddSubgroup.quotientEquivSumOfLe'.proof_1 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (b : α) (c : α) (h : Setoid.r b c) :
Setoid.r (id b) (id c)
Equations
def AddSubgroup.quotientEquivSumOfLe' {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) :
α s (α t) × { x // x t } AddSubgroup.addSubgroupOf s t

If H ≤ K≤ K, then G/H ≃ G/K × K/H≃ G/K × K/H× K/H constructively, using the provided right inverse of the quotient map G → G/K→ G/K. The classical version is addQuotientEquivProdOfLe.

Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivSumOfLe'.proof_4 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (f : α tα) (a : (α t) × { x // x t } AddSubgroup.addSubgroupOf s t) (b : { x // x t }) (c : { x // x t }) (h : Setoid.r b c) :
Setoid.r ((fun b => f a.fst + b) b) ((fun b => f a.fst + b) c)
Equations
  • (_ : Setoid.r ((fun b => f a.fst + b) b) ((fun b => f a.fst + b) c)) = (_ : Setoid.r ((fun b => f a.fst + b) b) ((fun b => f a.fst + b) c))
def AddSubgroup.quotientEquivSumOfLe'.proof_6 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (t : (α t) × { x // x t } AddSubgroup.addSubgroupOf s t) :
(fun a => (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b cSetoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g t) }) (_ : ∀ (b c : α), Setoid.r b cSetoid.r ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g t) }) b) ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g t) }) c)) a)) ((fun a => Quotient.map' (fun b => f a.fst + b) (_ : ∀ (b c : { x // x t }), Setoid.r b cSetoid.r ((fun b => f a.fst + b) b) ((fun b => f a.fst + b) c)) a.snd) t) = t
Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivSumOfLe'.proof_3 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (b : α) (c : α) (h : Setoid.r b c) :
Setoid.r ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g t) }) b) ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g t) }) c)
Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivSumOfLe'.proof_2 {α : Type u_1} [inst : AddGroup α] {t : AddSubgroup α} (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (g : α) :
-f (Quotient.mk'' g) + g t
Equations
def AddSubgroup.quotientEquivSumOfLe'.proof_5 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (q : Quotient (QuotientAddGroup.leftRel s)) :
(fun a => Quotient.map' (fun b => f a.fst + b) (_ : ∀ (b c : { x // x t }), Setoid.r b cSetoid.r ((fun b => f a.fst + b) b) ((fun b => f a.fst + b) c)) a.snd) ((fun a => (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b cSetoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g t) }) (_ : ∀ (b c : α), Setoid.r b cSetoid.r ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g t) }) b) ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g t) }) c)) a)) q) = q
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubgroup.quotientEquivSumOfLe'_symm_apply {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : (α t) × { x // x t } AddSubgroup.addSubgroupOf s t) :
↑(Equiv.symm (AddSubgroup.quotientEquivSumOfLe' h_le f hf)) a = Quotient.map' (fun b => f a.fst + b) (_ : ∀ (b c : { x // x t }), Setoid.r b cSetoid.r ((fun b => f a.fst + b) b) ((fun b => f a.fst + b) c)) a.snd
@[simp]
theorem Subgroup.quotientEquivProdOfLe'_symm_apply {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) (a : (α t) × { x // x t } Subgroup.subgroupOf s t) :
↑(Equiv.symm (Subgroup.quotientEquivProdOfLe' h_le f hf)) a = Quotient.map' (fun b => f a.fst * b) (_ : ∀ (b c : { x // x t }), Setoid.r b cSetoid.r ((fun b => f a.fst * b) b) ((fun b => f a.fst * b) c)) a.snd
@[simp]
theorem AddSubgroup.quotientEquivSumOfLe'_apply {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : α s) :
↑(AddSubgroup.quotientEquivSumOfLe' h_le f hf) a = (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b cSetoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g t) }) (_ : ∀ (b c : α), Setoid.r b cSetoid.r ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g t) }) b) ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g t) }) c)) a)
@[simp]
theorem Subgroup.quotientEquivProdOfLe'_apply {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) (a : α s) :
↑(Subgroup.quotientEquivProdOfLe' h_le f hf) a = (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b cSetoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g t) }) (_ : ∀ (b c : α), Setoid.r b cSetoid.r ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g t) }) b) ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g t) }) c)) a)
def Subgroup.quotientEquivProdOfLe' {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) :
α s (α t) × { x // x t } Subgroup.subgroupOf s t

If H ≤ K≤ K, then G/H ≃ G/K × K/H≃ G/K × K/H× K/H constructively, using the provided right inverse of the quotient map G → G/K→ G/K. The classical version is quotientEquivProdOfLe.

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

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

Equations
@[simp]
theorem Subgroup.quotientEquivProdOfLe_symm_apply {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (a : (α t) × { x // x t } Subgroup.subgroupOf s t) :
↑(Equiv.symm (Subgroup.quotientEquivProdOfLe h_le)) a = Quotient.map' (fun b => Quotient.out' a.fst * b) (_ : ∀ (b c : { x // x t }), Setoid.r b cSetoid.r ((fun b => Quotient.out' a.fst * b) b) ((fun b => Quotient.out' a.fst * b) c)) a.snd
@[simp]
theorem AddSubgroup.quotientEquivSumOfLe_symm_apply {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (a : (α t) × { x // x t } AddSubgroup.addSubgroupOf s t) :
↑(Equiv.symm (AddSubgroup.quotientEquivSumOfLe h_le)) a = Quotient.map' (fun b => Quotient.out' a.fst + b) (_ : ∀ (b c : { x // x t }), Setoid.r b cSetoid.r ((fun b => Quotient.out' a.fst + b) b) ((fun b => Quotient.out' a.fst + b) c)) a.snd
@[simp]
theorem Subgroup.quotientEquivProdOfLe_apply {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (a : α s) :
↑(Subgroup.quotientEquivProdOfLe h_le) a = (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b cSetoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := (Quotient.out' (Quotient.mk'' g))⁻¹ * g, property := (_ : (Quotient.out' (Quotient.mk'' g))⁻¹ * g t) }) (_ : ∀ (b c : α), Setoid.r b cSetoid.r ((fun g => { val := (Quotient.out' (Quotient.mk'' g))⁻¹ * g, property := (_ : (Quotient.out' (Quotient.mk'' g))⁻¹ * g t) }) b) ((fun g => { val := (Quotient.out' (Quotient.mk'' g))⁻¹ * g, property := (_ : (Quotient.out' (Quotient.mk'' g))⁻¹ * g t) }) c)) a)
@[simp]
theorem AddSubgroup.quotientEquivSumOfLe_apply {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (a : α s) :
↑(AddSubgroup.quotientEquivSumOfLe h_le) a = (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b cSetoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := -Quotient.out' (Quotient.mk'' g) + g, property := (_ : -Quotient.out' (Quotient.mk'' g) + g t) }) (_ : ∀ (b c : α), Setoid.r b cSetoid.r ((fun g => { val := -Quotient.out' (Quotient.mk'' g) + g, property := (_ : -Quotient.out' (Quotient.mk'' g) + g t) }) b) ((fun g => { val := -Quotient.out' (Quotient.mk'' g) + g, property := (_ : -Quotient.out' (Quotient.mk'' g) + g t) }) c)) a)
noncomputable def Subgroup.quotientEquivProdOfLe {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) :
α s (α t) × { x // x t } Subgroup.subgroupOf s t

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

Equations
def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLe.proof_1 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) (a : { x // x s }) (b : { x // x s }) :
Equations
def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLe {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) :

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

Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLe.proof_2 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) (q₁ : Quotient (QuotientAddGroup.leftRel (AddSubgroup.addSubgroupOf H s))) (q₂ : Quotient (QuotientAddGroup.leftRel (AddSubgroup.addSubgroupOf H s))) :
Quotient.map' ↑(AddSubgroup.inclusion h) (_ : ∀ (a b : { x // x s }), Setoid.r a bSetoid.r (↑(AddSubgroup.inclusion h) a) (↑(AddSubgroup.inclusion h) b)) q₁ = Quotient.map' ↑(AddSubgroup.inclusion h) (_ : ∀ (a b : { x // x s }), Setoid.r a bSetoid.r (↑(AddSubgroup.inclusion h) a) (↑(AddSubgroup.inclusion h) b)) q₂q₁ = q₂
Equations
  • One or more equations did not get rendered due to their size.
def Subgroup.quotientSubgroupOfEmbeddingOfLe {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s t) :
{ x // x s } Subgroup.subgroupOf H s { x // x t } Subgroup.subgroupOf H t

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLe_apply_mk {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) (g : { x // x s }) :
@[simp]
theorem Subgroup.quotientSubgroupOfEmbeddingOfLe_apply_mk {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s t) (g : { x // x s }) :
def AddSubgroup.quotientAddSubgroupOfMapOfLe.proof_1 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) (a : { x // x H }) (b : { x // x H }) :
Setoid.r a bSetoid.r (id a) (id b)
Equations
def AddSubgroup.quotientAddSubgroupOfMapOfLe {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) :
{ x // x H } AddSubgroup.addSubgroupOf s H{ x // x H } AddSubgroup.addSubgroupOf t H

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

Equations
def Subgroup.quotientSubgroupOfMapOfLe {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s t) :
{ x // x H } Subgroup.subgroupOf s H{ x // x H } Subgroup.subgroupOf t H

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

Equations
@[simp]
theorem AddSubgroup.quotientAddSubgroupOfMapOfLe_apply_mk {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) (g : { x // x H }) :
@[simp]
theorem Subgroup.quotientSubgroupOfMapOfLe_apply_mk {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s t) (g : { x // x H }) :
def AddSubgroup.quotientMapOfLe.proof_1 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s t) (a : α) (b : α) :
Setoid.r a bSetoid.r (id a) (id b)
Equations
def AddSubgroup.quotientMapOfLe {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s t) :
α sα t

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

Equations
def Subgroup.quotientMapOfLe {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (h : s t) :
α sα t

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

Equations
@[simp]
theorem AddSubgroup.quotientMapOfLe_apply_mk {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s t) (g : α) :
@[simp]
theorem Subgroup.quotientMapOfLe_apply_mk {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (h : s t) (g : α) :
def AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding.proof_1 {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (i : ι) :
infᵢ f f i
Equations
def AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding.proof_2 {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (H : AddSubgroup α) (q₁ : Quotient (QuotientAddGroup.leftRel (AddSubgroup.addSubgroupOf (i, f i) H))) (q₂ : Quotient (QuotientAddGroup.leftRel (AddSubgroup.addSubgroupOf (i, f i) H))) :
(fun q i => AddSubgroup.quotientAddSubgroupOfMapOfLe H (_ : infᵢ f f i) q) q₁ = (fun q i => AddSubgroup.quotientAddSubgroupOfMapOfLe H (_ : infᵢ f f i) q) q₂q₁ = q₂
Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (H : AddSubgroup α) :
{ x // x H } AddSubgroup.addSubgroupOf (i, f i) H (i : ι) → { x // x H } AddSubgroup.addSubgroupOf (f i) H

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Subgroup.quotientInfᵢSubgroupOfEmbedding_apply {α : Type u_1} [inst : Group α] {ι : Type u_2} (f : ιSubgroup α) (H : Subgroup α) (q : { x // x H } Subgroup.subgroupOf (i, f i) H) (i : ι) :
@[simp]
theorem AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding_apply {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (H : AddSubgroup α) (q : { x // x H } AddSubgroup.addSubgroupOf (i, f i) H) (i : ι) :
def Subgroup.quotientInfᵢSubgroupOfEmbedding {α : Type u_1} [inst : Group α] {ι : Type u_2} (f : ιSubgroup α) (H : Subgroup α) :
{ x // x H } Subgroup.subgroupOf (i, f i) H (i : ι) → { x // x H } Subgroup.subgroupOf (f i) H

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding_apply_mk {α : Type u_2} [inst : AddGroup α] {ι : Type u_1} (f : ιAddSubgroup α) (H : AddSubgroup α) (g : { x // x H }) (i : ι) :
@[simp]
theorem Subgroup.quotientInfᵢSubgroupOfEmbedding_apply_mk {α : Type u_2} [inst : Group α] {ι : Type u_1} (f : ιSubgroup α) (H : Subgroup α) (g : { x // x H }) (i : ι) :
def AddSubgroup.quotientInfᵢEmbedding.proof_2 {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (q₁ : Quotient (QuotientAddGroup.leftRel (i, f i))) (q₂ : Quotient (QuotientAddGroup.leftRel (i, f i))) :
(fun q i => AddSubgroup.quotientMapOfLe (_ : infᵢ f f i) q) q₁ = (fun q i => AddSubgroup.quotientMapOfLe (_ : infᵢ f f i) q) q₂q₁ = q₂
Equations
  • One or more equations did not get rendered due to their size.
def AddSubgroup.quotientInfᵢEmbedding.proof_1 {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (i : ι) :
infᵢ f f i
Equations
def AddSubgroup.quotientInfᵢEmbedding {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) :
(α i, f i) (i : ι) → α f i

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubgroup.quotientInfᵢEmbedding_apply {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (q : α i, f i) (i : ι) :
@[simp]
theorem Subgroup.quotientInfᵢEmbedding_apply {α : Type u_1} [inst : Group α] {ι : Type u_2} (f : ιSubgroup α) (q : α i, f i) (i : ι) :
def Subgroup.quotientInfᵢEmbedding {α : Type u_1} [inst : Group α] {ι : Type u_2} (f : ιSubgroup α) :
(α i, f i) (i : ι) → α f i

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubgroup.quotientInfᵢEmbedding_apply_mk {α : Type u_2} [inst : AddGroup α] {ι : Type u_1} (f : ιAddSubgroup α) (g : α) (i : ι) :
@[simp]
theorem Subgroup.quotientInfᵢEmbedding_apply_mk {α : Type u_2} [inst : Group α] {ι : Type u_1} (f : ιSubgroup α) (g : α) (i : ι) :
↑(Subgroup.quotientInfᵢEmbedding f) (g) i = g
theorem AddSubgroup.card_eq_card_quotient_add_card_addSubgroup {α : Type u_1} [inst : AddGroup α] [inst : Fintype α] (s : AddSubgroup α) [inst : Fintype { x // x s }] [inst : DecidablePred fun a => a s] :
theorem Subgroup.card_eq_card_quotient_mul_card_subgroup {α : Type u_1} [inst : Group α] [inst : Fintype α] (s : Subgroup α) [inst : Fintype { x // x s }] [inst : DecidablePred fun a => a s] :
theorem AddSubgroup.card_addSubgroup_dvd_card {α : Type u_1} [inst : AddGroup α] [inst : Fintype α] (s : AddSubgroup α) [inst : Fintype { x // x s }] :

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} [inst : Group α] [inst : Fintype α] (s : Subgroup α) [inst : Fintype { x // x 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} [inst : AddGroup α] [inst : Fintype α] (s : AddSubgroup α) [inst : DecidablePred fun x => x s] :
theorem Subgroup.card_quotient_dvd_card {α : Type u_1} [inst : Group α] [inst : Fintype α] (s : Subgroup α) [inst : DecidablePred fun x => x s] :
theorem AddSubgroup.card_dvd_of_injective {α : Type u_1} [inst : AddGroup α] {H : Type u_2} [inst : AddGroup H] [inst : Fintype α] [inst : Fintype H] (f : α →+ H) (hf : Function.Injective f) :
theorem Subgroup.card_dvd_of_injective {α : Type u_1} [inst : Group α] {H : Type u_2} [inst : Group H] [inst : Fintype α] [inst : Fintype H] (f : α →* H) (hf : Function.Injective f) :
theorem AddSubgroup.card_dvd_of_le {α : Type u_1} [inst : AddGroup α] {H : AddSubgroup α} {K : AddSubgroup α} [inst : Fintype { x // x H }] [inst : Fintype { x // x K }] (hHK : H K) :
Fintype.card { x // x H } Fintype.card { x // x K }
theorem Subgroup.card_dvd_of_le {α : Type u_1} [inst : Group α] {H : Subgroup α} {K : Subgroup α} [inst : Fintype { x // x H }] [inst : Fintype { x // x K }] (hHK : H K) :
Fintype.card { x // x H } Fintype.card { x // x K }
theorem AddSubgroup.card_comap_dvd_of_injective {α : Type u_2} [inst : AddGroup α] {H : Type u_1} [inst : AddGroup H] (K : AddSubgroup H) [inst : Fintype { x // x K }] (f : α →+ H) [inst : Fintype { x // x AddSubgroup.comap f K }] (hf : Function.Injective f) :
theorem Subgroup.card_comap_dvd_of_injective {α : Type u_2} [inst : Group α] {H : Type u_1} [inst : Group H] (K : Subgroup H) [inst : Fintype { x // x K }] (f : α →* H) [inst : Fintype { x // x Subgroup.comap f K }] (hf : Function.Injective f) :
Fintype.card { x // x Subgroup.comap f K } Fintype.card { x // x K }
abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_2 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (motive : { x // x s } × tProp) :
(x : { x // x s } × t) → ((a : α) → (ha : a s) → (x : α s) → (hx : x t) → motive ({ val := a, property := ha }, { val := x, property := hx })) → motive x
Equations
  • One or more equations did not get rendered due to their size.
noncomputable def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (t : Set (α s)) :
↑(QuotientAddGroup.mk ⁻¹' t) { x // x s } × t

If s is a subgroup of the additive group α, and t is a subset of α ⧸ s⧸ s, then there is a (typically non-canonical) bijection between the preimage of t in α and the product s × t× t.

Equations
  • One or more equations did not get rendered due to their size.
def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_5 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (t : Set (α s)) :
∀ (x : { x // x s } × t), (fun a => ({ val := -Quotient.out' a + a, property := (_ : -Quotient.out' a + a s) }, { val := a, property := (_ : a QuotientAddGroup.mk ⁻¹' t) })) ((fun a => { val := Quotient.out' a.snd + a.fst, property := (_ : ↑(Quotient.out' a.snd + a.fst) t) }) x) = x
Equations
  • One or more equations did not get rendered due to their size.
def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_4 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (t : Set (α s)) :
∀ (x : ↑(QuotientAddGroup.mk ⁻¹' t)), (fun a => { val := Quotient.out' a.snd + a.fst, property := (_ : ↑(Quotient.out' a.snd + a.fst) t) }) ((fun a => ({ val := -Quotient.out' a + a, property := (_ : -Quotient.out' a + a s) }, { val := a, property := (_ : a QuotientAddGroup.mk ⁻¹' t) })) x) = x
Equations
  • One or more equations did not get rendered due to their size.
def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_1 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (a : ↑(QuotientAddGroup.mk ⁻¹' t)) :
-Quotient.out' a + a s
Equations
def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_3 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (a : { x // x s } × t) :
↑(Quotient.out' a.snd + a.fst) t
Equations
def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_2 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (a : ↑(QuotientAddGroup.mk ⁻¹' t)) :
a QuotientAddGroup.mk ⁻¹' t
Equations
abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_1 {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (motive : ↑(QuotientAddGroup.mk ⁻¹' t)Prop) :
(x : ↑(QuotientAddGroup.mk ⁻¹' t)) → ((a : α) → (ha : a QuotientAddGroup.mk ⁻¹' t) → motive { val := a, property := ha }) → motive x
Equations
noncomputable def QuotientGroup.preimageMkEquivSubgroupProdSet {α : Type u_1} [inst : Group α] (s : Subgroup α) (t : Set (α s)) :
↑(QuotientGroup.mk ⁻¹' t) { x // x s } × t

If s is a subgroup of the group α, and t is a subset of α ⧸ s⧸ s, then there is a (typically non-canonical) bijection between the preimage of t in α and the product s × t× t.

Equations
  • One or more equations did not get rendered due to their size.