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 ∈ AddOpposite.op a +ᵥ s

theorem mem_rightCoset {α : Type u_1} [Mul α] {s : Set α} {x : α} (a : α) (hxS : x ∈ s) : x * a ∈ MulOpposite.op a • s

def LeftAddCosetEquivalence {α : Type u_1} [Add α] (s : Set α) (a : α) (b : α) : Prop

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

Equations

• LeftAddCosetEquivalence s a b = (a +ᵥ s = b +ᵥ s)

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

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

Equations

• LeftCosetEquivalence s a b = (a • s = b • s)

theorem leftAddCosetEquivalence_rel {α : Type u_1} [Add α] (s : Set α) : Equivalence (LeftAddCosetEquivalence s)

theorem leftCosetEquivalence_rel {α : Type u_1} [Mul α] (s : Set α) : Equivalence (LeftCosetEquivalence s)

def RightAddCosetEquivalence {α : Type u_1} [Add α] (s : Set α) (a : α) (b : α) : Prop

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

Equations

• RightAddCosetEquivalence s a b = (AddOpposite.op a +ᵥ s = AddOpposite.op b +ᵥ s)

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

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

Equations

• RightCosetEquivalence s a b = (MulOpposite.op a • s = MulOpposite.op b • s)

theorem rightAddCosetEquivalence_rel {α : Type u_1} [Add α] (s : Set α) : Equivalence (RightAddCosetEquivalence s)

theorem rightCosetEquivalence_rel {α : Type u_1} [Mul α] (s : Set α) : Equivalence (RightCosetEquivalence s)

theorem leftAddCoset_assoc {α : Type u_1} [AddSemigroup α] (s : Set α) (a : α) (b : α) : a +ᵥ (b +ᵥ s) = a + b +ᵥ s

theorem leftCoset_assoc {α : Type u_1} [Semigroup α] (s : Set α) (a : α) (b : α) : a • b • s = (a * b) • s

theorem rightAddCoset_assoc {α : Type u_1} [AddSemigroup α] (s : Set α) (a : α) (b : α) : AddOpposite.op b +ᵥ (AddOpposite.op a +ᵥ s) = AddOpposite.op (a + b) +ᵥ s

theorem rightCoset_assoc {α : Type u_1} [Semigroup α] (s : Set α) (a : α) (b : α) : MulOpposite.op b • MulOpposite.op a • s = MulOpposite.op (a * b) • s

theorem leftAddCoset_rightAddCoset {α : Type u_1} [AddSemigroup α] (s : Set α) (a : α) (b : α) : AddOpposite.op b +ᵥ (a +ᵥ s) = a +ᵥ (AddOpposite.op b +ᵥ s)

theorem leftCoset_rightCoset {α : Type u_1} [Semigroup α] (s : Set α) (a : α) (b : α) : MulOpposite.op b • a • s = a • MulOpposite.op b • s

theorem zero_leftAddCoset {α : Type u_1} [AddMonoid α] (s : Set α) : 0 +ᵥ s = s

theorem one_leftCoset {α : Type u_1} [Monoid α] (s : Set α) : 1 • s = s

theorem rightAddCoset_zero {α : Type u_1} [AddMonoid α] (s : Set α) : AddOpposite.op 0 +ᵥ s = s

theorem rightCoset_one {α : Type u_1} [Monoid α] (s : Set α) : MulOpposite.op 1 • s = s

theorem mem_own_leftAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) (a : α) : a ∈ a +ᵥ ↑s

theorem mem_own_leftCoset {α : Type u_1} [Monoid α] (s : Submonoid α) (a : α) : a ∈ a • ↑s

theorem mem_own_rightAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) (a : α) : a ∈ AddOpposite.op a +ᵥ ↑s

theorem mem_own_rightCoset {α : Type u_1} [Monoid α] (s : Submonoid α) (a : α) : a ∈ MulOpposite.op a • ↑s

theorem mem_leftAddCoset_leftAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) {a : α} (ha : a +ᵥ ↑s = ↑s) : a ∈ s

theorem mem_leftCoset_leftCoset {α : Type u_1} [Monoid α] (s : Submonoid α) {a : α} (ha : a • ↑s = ↑s) : a ∈ s

theorem mem_rightAddCoset_rightAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) {a : α} (ha : AddOpposite.op a +ᵥ ↑s = ↑s) : a ∈ s

theorem mem_rightCoset_rightCoset {α : Type u_1} [Monoid α] (s : Submonoid α) {a : α} (ha : MulOpposite.op a • ↑s = ↑s) : a ∈ s

abbrev mem_leftAddCoset_iff.match_1 {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) (motive : x ∈ a +ᵥ s → Prop) : ∀ (x_1 : x ∈ a +ᵥ s), (∀ (b : α) (hb : b ∈ s) (Eq : (fun (x : α) => a +ᵥ x) b = x), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

theorem mem_leftAddCoset_iff {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) : x ∈ a +ᵥ s ↔ -a + x ∈ s

theorem mem_leftCoset_iff {α : Type u_1} [Group α] {s : Set α} {x : α} (a : α) : x ∈ a • s ↔ a⁻¹ * x ∈ s

theorem mem_rightAddCoset_iff {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) : x ∈ AddOpposite.op a +ᵥ s ↔ x + -a ∈ s

abbrev mem_rightAddCoset_iff.match_1 {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) (motive : x ∈ AddOpposite.op a +ᵥ s → Prop) : ∀ (x_1 : x ∈ AddOpposite.op a +ᵥ s), (∀ (b : α) (hb : b ∈ s) (Eq : (fun (x : α) => AddOpposite.op a +ᵥ x) b = x), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

theorem mem_rightCoset_iff {α : Type u_1} [Group α] {s : Set α} {x : α} (a : α) : x ∈ MulOpposite.op a • s ↔ x * a⁻¹ ∈ s

theorem leftAddCoset_mem_leftAddCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {a : α} (ha : a ∈ s) : a +ᵥ ↑s = ↑s

theorem leftCoset_mem_leftCoset {α : Type u_1} [Group α] (s : Subgroup α) {a : α} (ha : a ∈ s) : a • ↑s = ↑s

theorem rightAddCoset_mem_rightAddCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {a : α} (ha : a ∈ s) : AddOpposite.op a +ᵥ ↑s = ↑s

theorem rightCoset_mem_rightCoset {α : Type u_1} [Group α] (s : Subgroup α) {a : α} (ha : a ∈ s) : MulOpposite.op a • ↑s = ↑s

abbrev orbit_addSubgroup_eq_rightCoset.match_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (_b : α) (motive : _b ∈ AddAction.orbit (↥s) a → Prop) : ∀ (x : _b ∈ AddAction.orbit (↥s) a), (∀ (c : ↥s) (d : (fun (m : ↥s) => m +ᵥ a) c = _b), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem orbit_addSubgroup_eq_rightCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) : AddAction.orbit (↥s) a = AddOpposite.op a +ᵥ ↑s

abbrev orbit_addSubgroup_eq_rightCoset.match_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (_b : α) (motive : _b ∈ AddOpposite.op a +ᵥ ↑s → Prop) : ∀ (x : _b ∈ AddOpposite.op a +ᵥ ↑s), (∀ (c : α) (d : c ∈ ↑s) (e : (fun (x : α) => AddOpposite.op a +ᵥ x) c = _b), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem orbit_subgroup_eq_rightCoset {α : Type u_1} [Group α] (s : Subgroup α) (a : α) : MulAction.orbit (↥s) a = MulOpposite.op a • ↑s

theorem orbit_addSubgroup_eq_self_of_mem {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {a : α} (ha : a ∈ s) : AddAction.orbit (↥s) a = ↑s

theorem orbit_subgroup_eq_self_of_mem {α : Type u_1} [Group α] (s : Subgroup α) {a : α} (ha : a ∈ s) : MulAction.orbit (↥s) a = ↑s

theorem orbit_addSubgroup_zero_eq_self {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : AddAction.orbit (↥s) 0 = ↑s

theorem orbit_subgroup_one_eq_self {α : Type u_1} [Group α] (s : Subgroup α) : MulAction.orbit (↥s) 1 = ↑s

theorem eq_addCosets_of_normal {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (N : s.Normal) (g : α) : g +ᵥ ↑s = AddOpposite.op g +ᵥ ↑s

theorem eq_cosets_of_normal {α : Type u_1} [Group α] (s : Subgroup α) (N : s.Normal) (g : α) : g • ↑s = MulOpposite.op g • ↑s

theorem normal_of_eq_addCosets {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (h : ∀ (g : α), g +ᵥ ↑s = AddOpposite.op g +ᵥ ↑s) : s.Normal

theorem normal_of_eq_cosets {α : Type u_1} [Group α] (s : Subgroup α) (h : ∀ (g : α), g • ↑s = MulOpposite.op g • ↑s) : s.Normal

theorem normal_iff_eq_addCosets {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : s.Normal ↔ ∀ (g : α), g +ᵥ ↑s = AddOpposite.op g +ᵥ ↑s

theorem normal_iff_eq_cosets {α : Type u_1} [Group α] (s : Subgroup α) : s.Normal ↔ ∀ (g : α), g • ↑s = MulOpposite.op g • ↑s

theorem leftAddCoset_eq_iff {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {x : α} {y : α} : x +ᵥ ↑s = y +ᵥ ↑s ↔ -x + y ∈ s

theorem leftCoset_eq_iff {α : Type u_1} [Group α] (s : Subgroup α) {x : α} {y : α} : x • ↑s = y • ↑s ↔ x⁻¹ * y ∈ s

theorem rightAddCoset_eq_iff {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {x : α} {y : α} : AddOpposite.op x +ᵥ ↑s = AddOpposite.op y +ᵥ ↑s ↔ y + -x ∈ s

theorem rightCoset_eq_iff {α : Type u_1} [Group α] (s : Subgroup α) {x : α} {y : α} : MulOpposite.op x • ↑s = MulOpposite.op y • ↑s ↔ y * x⁻¹ ∈ s

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

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

Equations

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

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

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

Equations

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

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

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

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

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

theorem QuotientGroup.leftRel_r_eq_leftCosetEquivalence {α : Type u_1} [Group α] (s : Subgroup α) : Setoid.r = LeftCosetEquivalence ↑s

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

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

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

theorem QuotientGroup.rightRel_r_eq_rightCosetEquivalence {α : Type u_1} [Group α] (s : Subgroup α) : Setoid.r = RightCosetEquivalence ↑s

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

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

Equations

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

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

Equations

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

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

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

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

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

Right cosets are in bijection with left cosets.

Equations

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

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

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

Right cosets are in bijection with left cosets.

Equations

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

instance QuotientAddGroup.fintypeQuotientRightRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [Fintype (α ⧸ s)] : Fintype (Quotient (QuotientAddGroup.rightRel s))

Equations

• QuotientAddGroup.fintypeQuotientRightRel s = Fintype.ofEquiv (α ⧸ s) (QuotientAddGroup.quotientRightRelEquivQuotientLeftRel s).symm

instance QuotientGroup.fintypeQuotientRightRel {α : Type u_1} [Group α] (s : Subgroup α) [Fintype (α ⧸ s)] : Fintype (Quotient (QuotientGroup.rightRel s))

Equations

• QuotientGroup.fintypeQuotientRightRel s = Fintype.ofEquiv (α ⧸ s) (QuotientGroup.quotientRightRelEquivQuotientLeftRel s).symm

theorem QuotientAddGroup.card_quotient_rightRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [Fintype (α ⧸ s)] : Fintype.card (Quotient (QuotientAddGroup.rightRel s)) = Fintype.card (α ⧸ s)

theorem QuotientGroup.card_quotient_rightRel {α : Type u_1} [Group α] (s : Subgroup α) [Fintype (α ⧸ s)] : Fintype.card (Quotient (QuotientGroup.rightRel s)) = Fintype.card (α ⧸ s)

instance QuotientAddGroup.fintype {α : Type u_1} [AddGroup α] [Fintype α] (s : AddSubgroup α) [DecidableRel Setoid.r] : Fintype (α ⧸ s)

Equations

• QuotientAddGroup.fintype s = Quotient.fintype (QuotientAddGroup.leftRel s)

instance QuotientGroup.fintype {α : Type u_1} [Group α] [Fintype α] (s : Subgroup α) [DecidableRel Setoid.r] : Fintype (α ⧸ s)

Equations

• QuotientGroup.fintype s = Quotient.fintype (QuotientGroup.leftRel s)

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

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

Equations

• ↑a = Quotient.mk'' a

@[reducible, inline]

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

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

Equations

• ↑a = Quotient.mk'' a

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

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

@[simp]

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

@[simp]

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

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

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

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

Equations

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

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

Equations

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

theorem QuotientAddGroup.eq_class_eq_leftCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : α) : {x : α | ↑x = ↑g} = g +ᵥ ↑s

theorem QuotientGroup.eq_class_eq_leftCoset {α : Type u_1} [Group α] (s : Subgroup α) (g : α) : {x : α | ↑x = ↑g} = g • ↑s

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

abbrev QuotientAddGroup.preimage_image_mk.match_1 {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) (x : α) (motive : (∃ x_1 ∈ s, -x_1 + x ∈ N) → Prop) : ∀ (x_1 : ∃ x_1 ∈ s, -x_1 + x ∈ N), (∀ (y : α) (hs : y ∈ s) (hN : -y + x ∈ N), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

abbrev QuotientAddGroup.preimage_image_mk.match_2 {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) (x : α) (motive : (∃ x_1 ∈ N, x + x_1 ∈ s) → Prop) : ∀ (x_1 : ∃ x_1 ∈ N, x + x_1 ∈ s), (∀ (z : α) (hz : z ∈ N) (hxz : x + z ∈ s), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

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

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

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

theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (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} [AddGroup α] {s : AddSubgroup α} (g : α) (motive : ↑(g +ᵥ ↑s) → Prop) : ∀ (x : ↑(g +ᵥ ↑s)), (∀ (x : α) (hx : x ∈ g +ᵥ ↑s), motive ⟨x, hx⟩) → motive x

Equations

• ⋯ = ⋯

abbrev AddSubgroup.leftCosetEquivAddSubgroup.match_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (motive : ↥s → Prop) : ∀ (x : ↥s), (∀ (g : α) (hg : g ∈ s), motive ⟨g, hg⟩) → motive x

Equations

• ⋯ = ⋯

theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : ↥s) : ∃ a ∈ ↑s, (fun (x : α) => g +ᵥ x) a = g + ↑x

theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : ∀ (x : ↥s), (fun (x : ↑(g +ᵥ ↑s)) => ⟨-g + ↑x, ⋯⟩) ((fun (x : ↥s) => ⟨g + ↑x, ⋯⟩) x) = x

def AddSubgroup.leftCosetEquivAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : ↑(g +ᵥ ↑s) ≃ ↥s

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

Equations

• AddSubgroup.leftCosetEquivAddSubgroup g = { toFun := fun (x : ↑(g +ᵥ ↑s)) => ⟨-g + ↑x, ⋯⟩, invFun := fun (x : ↥s) => ⟨g + ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : ↑(g +ᵥ ↑s)) : -g + ↑x ∈ ↑s

def Subgroup.leftCosetEquivSubgroup {α : Type u_1} [Group α] {s : Subgroup α} (g : α) : ↑(g • ↑s) ≃ ↥s

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

Equations

• Subgroup.leftCosetEquivSubgroup g = { toFun := fun (x : ↑(g • ↑s)) => ⟨g⁻¹ * ↑x, ⋯⟩, invFun := fun (x : ↥s) => ⟨g * ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : ∀ (x : ↑(AddOpposite.op g +ᵥ ↑s)), (fun (x : ↥s) => ⟨↑x + g, ⋯⟩) ((fun (x : ↑(AddOpposite.op g +ᵥ ↑s)) => ⟨↑x + -g, ⋯⟩) x) = x

def AddSubgroup.rightCosetEquivAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : ↑(AddOpposite.op g +ᵥ ↑s) ≃ ↥s

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

Equations

• AddSubgroup.rightCosetEquivAddSubgroup g = { toFun := fun (x : ↑(AddOpposite.op g +ᵥ ↑s)) => ⟨↑x + -g, ⋯⟩, invFun := fun (x : ↥s) => ⟨↑x + g, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : ↥s) : ∃ a ∈ ↑s, (fun (x : α) => AddOpposite.op g +ᵥ x) a = ↑x + g

theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : ↑(AddOpposite.op g +ᵥ ↑s)) : ↑x + -g ∈ ↑s

abbrev AddSubgroup.rightCosetEquivAddSubgroup.match_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (motive : ↑(AddOpposite.op g +ᵥ ↑s) → Prop) : ∀ (x : ↑(AddOpposite.op g +ᵥ ↑s)), (∀ (x : α) (hx : x ∈ AddOpposite.op g +ᵥ ↑s), motive ⟨x, hx⟩) → motive x

Equations

• ⋯ = ⋯

theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : ∀ (x : ↥s), (fun (x : ↑(AddOpposite.op g +ᵥ ↑s)) => ⟨↑x + -g, ⋯⟩) ((fun (x : ↥s) => ⟨↑x + g, ⋯⟩) x) = x

def Subgroup.rightCosetEquivSubgroup {α : Type u_1} [Group α] {s : Subgroup α} (g : α) : ↑(MulOpposite.op g • ↑s) ≃ ↥s

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

Equations

• Subgroup.rightCosetEquivSubgroup g = { toFun := fun (x : ↑(MulOpposite.op g • ↑s)) => ⟨↑x * g⁻¹, ⋯⟩, invFun := fun (x : ↥s) => ⟨↑x * g, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem AddSubgroup.addGroupEquivQuotientProdAddSubgroup.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (L : α ⧸ s) : ({ x : α // ↑x = L } ≃ ↑(Quotient.out' L +ᵥ ↑s)) = ({ x : α // ↑x = L } ≃ ↑{x : α | ↑x = ↑(Quotient.out' L)})

theorem AddSubgroup.addGroupEquivQuotientProdAddSubgroup.proof_2 {α : Type u_1} [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 })

noncomputable def AddSubgroup.addGroupEquivQuotientProdAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} : α ≃ (α ⧸ 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.

noncomputable def Subgroup.groupEquivQuotientProdSubgroup {α : Type u_1} [Group α] {s : Subgroup α} : α ≃ (α ⧸ 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.

theorem AddSubgroup.quotientEquivOfEq.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (_a : α) (_b : α) (h' : Setoid.r _a _b) : Setoid.r (id _a) (id _b)

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

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

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

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

Equations

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

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

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

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

Equations

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

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

theorem AddSubgroup.quotientEquivSumOfLE'.proof_2 {α : Type u_1} [AddGroup α] {t : AddSubgroup α} (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) (g : α) : -f (Quotient.mk'' g) + g ∈ t

theorem AddSubgroup.quotientEquivSumOfLE'.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (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} [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 : α) => ⟨-f (Quotient.mk'' g) + g, ⋯⟩) b) ((fun (g : α) => ⟨-f (Quotient.mk'' g) + g, ⋯⟩) c)

def AddSubgroup.quotientEquivSumOfLE' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (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.

theorem AddSubgroup.quotientEquivSumOfLE'.proof_5 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) (q : Quotient (QuotientAddGroup.leftRel s)) : (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 (Quotient.mk'' g) + g, ⋯⟩) ⋯ a)) q) = q

theorem AddSubgroup.quotientEquivSumOfLE'.proof_6 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (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 (Quotient.mk'' g) + 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} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (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} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientGroup.mk) (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) : (Subgroup.quotientEquivProdOfLE' h_le f hf).symm a = Quotient.map' (fun (b : ↥t) => f a.1 * ↑b) ⋯ a.2

@[simp]

theorem AddSubgroup.quotientEquivSumOfLE'_apply {α : Type u_1} [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 ⋯ a, Quotient.map' (fun (g : α) => ⟨-f (Quotient.mk'' g) + g, ⋯⟩) ⋯ a)

@[simp]

theorem AddSubgroup.quotientEquivSumOfLE'_symm_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : (α ⧸ t) × ↥t ⧸ s.addSubgroupOf t) : (AddSubgroup.quotientEquivSumOfLE' h_le f hf).symm a = Quotient.map' (fun (b : ↥t) => f a.1 + ↑b) ⋯ a.2

@[simp]

theorem Subgroup.quotientEquivProdOfLE'_apply {α : Type u_1} [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 ⋯ a, Quotient.map' (fun (g : α) => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a)

def Subgroup.quotientEquivProdOfLE' {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (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.

noncomputable def AddSubgroup.quotientEquivSumOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (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

• AddSubgroup.quotientEquivSumOfLE h_le = AddSubgroup.quotientEquivSumOfLE' h_le Quotient.out' ⋯

theorem AddSubgroup.quotientEquivSumOfLE.proof_1 {α : Type u_1} [AddGroup α] {t : AddSubgroup α} (q : Quotient (QuotientAddGroup.leftRel t)) : Quotient.mk'' q.out' = q

@[simp]

theorem AddSubgroup.quotientEquivSumOfLE_symm_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (a : (α ⧸ t) × ↥t ⧸ s.addSubgroupOf t) : (AddSubgroup.quotientEquivSumOfLE h_le).symm a = Quotient.map' (fun (b : ↥t) => Quotient.out' a.1 + ↑b) ⋯ a.2

@[simp]

theorem Subgroup.quotientEquivProdOfLE_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s ≤ t) (a : α ⧸ s) : (Subgroup.quotientEquivProdOfLE h_le) a = (Quotient.map' id ⋯ a, Quotient.map' (fun (g : α) => ⟨(Quotient.mk'' g).out'⁻¹ * g, ⋯⟩) ⋯ a)

@[simp]

theorem Subgroup.quotientEquivProdOfLE_symm_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s ≤ t) (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) : (Subgroup.quotientEquivProdOfLE h_le).symm a = Quotient.map' (fun (b : ↥t) => Quotient.out' a.1 * ↑b) ⋯ a.2

@[simp]

theorem AddSubgroup.quotientEquivSumOfLE_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (a : α ⧸ s) : (AddSubgroup.quotientEquivSumOfLE h_le) a = (Quotient.map' id ⋯ a, Quotient.map' (fun (g : α) => ⟨-(Quotient.mk'' g).out' + g, ⋯⟩) ⋯ a)

noncomputable def Subgroup.quotientEquivProdOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (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

• Subgroup.quotientEquivProdOfLE h_le = Subgroup.quotientEquivProdOfLE' h_le Quotient.out' ⋯

def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) : ↥s ⧸ H.addSubgroupOf s ↪ ↥t ⧸ H.addSubgroupOf t

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

Equations

• AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE H h = { toFun := Quotient.map' ⇑(AddSubgroup.inclusion h) ⋯, inj' := ⋯ }

theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) (q₁ : Quotient (QuotientAddGroup.leftRel (H.addSubgroupOf s))) (q₂ : Quotient (QuotientAddGroup.leftRel (H.addSubgroupOf s))) : Quotient.map' ⇑(AddSubgroup.inclusion h) ⋯ q₁ = Quotient.map' ⇑(AddSubgroup.inclusion h) ⋯ q₂ → q₁ = q₂

theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) (a : ↥s) (b : ↥s) : Setoid.r a b → Setoid.r ((AddSubgroup.inclusion h) a) ((AddSubgroup.inclusion h) b)

def Subgroup.quotientSubgroupOfEmbeddingOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (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

• Subgroup.quotientSubgroupOfEmbeddingOfLE H h = { toFun := Quotient.map' ⇑(Subgroup.inclusion h) ⋯, inj' := ⋯ }

@[simp]

theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE_apply_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) (g : ↥s) : (AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE H h) ↑g = ↑((AddSubgroup.inclusion h) g)

@[simp]

theorem Subgroup.quotientSubgroupOfEmbeddingOfLE_apply_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s ≤ t) (g : ↥s) : (Subgroup.quotientSubgroupOfEmbeddingOfLE H h) ↑g = ↑((Subgroup.inclusion h) g)

def AddSubgroup.quotientAddSubgroupOfMapOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) : ↥H ⧸ s.addSubgroupOf H → ↥H ⧸ t.addSubgroupOf H

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

Equations

• AddSubgroup.quotientAddSubgroupOfMapOfLE H h = Quotient.map' id ⋯

theorem AddSubgroup.quotientAddSubgroupOfMapOfLE.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) (a : ↥H) (b : ↥H) : Setoid.r a b → Setoid.r (id a) (id b)

def Subgroup.quotientSubgroupOfMapOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s ≤ t) : ↥H ⧸ s.subgroupOf H → ↥H ⧸ t.subgroupOf H

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

Equations

• Subgroup.quotientSubgroupOfMapOfLE H h = Quotient.map' id ⋯

@[simp]

theorem AddSubgroup.quotientAddSubgroupOfMapOfLE_apply_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) (g : ↥H) : AddSubgroup.quotientAddSubgroupOfMapOfLE H h ↑g = ↑g

@[simp]

theorem Subgroup.quotientSubgroupOfMapOfLE_apply_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s ≤ t) (g : ↥H) : Subgroup.quotientSubgroupOfMapOfLE H h ↑g = ↑g

def AddSubgroup.quotientMapOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s ≤ t) : α ⧸ s → α ⧸ t

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

Equations

• AddSubgroup.quotientMapOfLE h = Quotient.map' id ⋯

theorem AddSubgroup.quotientMapOfLE.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s ≤ t) (a : α) (b : α) : Setoid.r a b → Setoid.r (id a) (id b)

def Subgroup.quotientMapOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s ≤ t) : α ⧸ s → α ⧸ t

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

Equations

• Subgroup.quotientMapOfLE h = Quotient.map' id ⋯

@[simp]

theorem AddSubgroup.quotientMapOfLE_apply_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s ≤ t) (g : α) : AddSubgroup.quotientMapOfLE h ↑g = ↑g

@[simp]

theorem Subgroup.quotientMapOfLE_apply_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s ≤ t) (g : α) : Subgroup.quotientMapOfLE h ↑g = ↑g

theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding.proof_2 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (H : AddSubgroup α) (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 : ι) => AddSubgroup.quotientAddSubgroupOfMapOfLE H ⋯ q) q₁ = (fun (q : ↥H ⧸ (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) => AddSubgroup.quotientAddSubgroupOfMapOfLE H ⋯ q) q₂ → q₁ = q₂

def AddSubgroup.quotientiInfAddSubgroupOfEmbedding {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (H : AddSubgroup α) : ↥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

• AddSubgroup.quotientiInfAddSubgroupOfEmbedding f H = { toFun := fun (q : ↥H ⧸ (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) => AddSubgroup.quotientAddSubgroupOfMapOfLE H ⋯ q, inj' := ⋯ }

theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding.proof_1 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (i : ι) : iInf f ≤ f i

@[simp]

theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (H : AddSubgroup α) (q : ↥H ⧸ (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) : (AddSubgroup.quotientiInfAddSubgroupOfEmbedding f H) q i = AddSubgroup.quotientAddSubgroupOfMapOfLE H ⋯ q

@[simp]

theorem Subgroup.quotientiInfSubgroupOfEmbedding_apply {α : Type u_1} [Group α] {ι : Type u_2} (f : ι → Subgroup α) (H : Subgroup α) (q : ↥H ⧸ (⨅ (i : ι), f i).subgroupOf H) (i : ι) : (Subgroup.quotientiInfSubgroupOfEmbedding f H) q i = Subgroup.quotientSubgroupOfMapOfLE H ⋯ q

def Subgroup.quotientiInfSubgroupOfEmbedding {α : Type u_1} [Group α] {ι : Type u_2} (f : ι → Subgroup α) (H : Subgroup α) : ↥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

• Subgroup.quotientiInfSubgroupOfEmbedding f H = { toFun := fun (q : ↥H ⧸ (⨅ (i : ι), f i).subgroupOf H) (i : ι) => Subgroup.quotientSubgroupOfMapOfLE H ⋯ q, inj' := ⋯ }

@[simp]

theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply_mk {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (H : AddSubgroup α) (g : ↥H) (i : ι) : (AddSubgroup.quotientiInfAddSubgroupOfEmbedding f H) (↑g) i = ↑g

@[simp]

theorem Subgroup.quotientiInfSubgroupOfEmbedding_apply_mk {α : Type u_1} [Group α] {ι : Type u_2} (f : ι → Subgroup α) (H : Subgroup α) (g : ↥H) (i : ι) : (Subgroup.quotientiInfSubgroupOfEmbedding f H) (↑g) i = ↑g

theorem AddSubgroup.quotientiInfEmbedding.proof_2 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (q₁ : Quotient (QuotientAddGroup.leftRel (⨅ (i : ι), f i))) (q₂ : Quotient (QuotientAddGroup.leftRel (⨅ (i : ι), f i))) : (fun (q : α ⧸ ⨅ (i : ι), f i) (i : ι) => AddSubgroup.quotientMapOfLE ⋯ q) q₁ = (fun (q : α ⧸ ⨅ (i : ι), f i) (i : ι) => AddSubgroup.quotientMapOfLE ⋯ q) q₂ → q₁ = q₂

theorem AddSubgroup.quotientiInfEmbedding.proof_1 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (i : ι) : iInf f ≤ f i

def AddSubgroup.quotientiInfEmbedding {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) : α ⧸ ⨅ (i : ι), f i ↪ (i : ι) → α ⧸ f i

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

Equations

• AddSubgroup.quotientiInfEmbedding f = { toFun := fun (q : α ⧸ ⨅ (i : ι), f i) (i : ι) => AddSubgroup.quotientMapOfLE ⋯ q, inj' := ⋯ }

@[simp]

theorem AddSubgroup.quotientiInfEmbedding_apply {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (q : α ⧸ ⨅ (i : ι), f i) (i : ι) : (AddSubgroup.quotientiInfEmbedding f) q i = AddSubgroup.quotientMapOfLE ⋯ q

@[simp]

theorem Subgroup.quotientiInfEmbedding_apply {α : Type u_1} [Group α] {ι : Type u_2} (f : ι → Subgroup α) (q : α ⧸ ⨅ (i : ι), f i) (i : ι) : (Subgroup.quotientiInfEmbedding f) q i = Subgroup.quotientMapOfLE ⋯ q

def Subgroup.quotientiInfEmbedding {α : Type u_1} [Group α] {ι : Type u_2} (f : ι → Subgroup α) : α ⧸ ⨅ (i : ι), f i ↪ (i : ι) → α ⧸ f i

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

Equations

• Subgroup.quotientiInfEmbedding f = { toFun := fun (q : α ⧸ ⨅ (i : ι), f i) (i : ι) => Subgroup.quotientMapOfLE ⋯ q, inj' := ⋯ }

@[simp]

theorem AddSubgroup.quotientiInfEmbedding_apply_mk {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (g : α) (i : ι) : (AddSubgroup.quotientiInfEmbedding f) (↑g) i = ↑g

@[simp]

theorem Subgroup.quotientiInfEmbedding_apply_mk {α : Type u_1} [Group α] {ι : Type u_2} (f : ι → Subgroup α) (g : α) (i : ι) : (Subgroup.quotientiInfEmbedding f) (↑g) i = ↑g

theorem AddSubgroup.card_eq_card_quotient_mul_card_addSubgroup {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s

theorem Subgroup.card_eq_card_quotient_mul_card_subgroup {α : Type u_1} [Group α] (s : Subgroup α) : Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s

theorem AddSubgroup.card_addSubgroup_dvd_card {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Nat.card ↥s ∣ Nat.card α

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} [Group α] (s : Subgroup α) : Nat.card ↥s ∣ Nat.card α

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

theorem AddSubgroup.card_quotient_dvd_card {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Nat.card (α ⧸ s) ∣ Nat.card α

theorem Subgroup.card_quotient_dvd_card {α : Type u_1} [Group α] (s : Subgroup α) : Nat.card (α ⧸ s) ∣ Nat.card α

theorem AddSubgroup.card_dvd_of_injective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (hf : Function.Injective ⇑f) : Nat.card α ∣ Nat.card H

theorem Subgroup.card_dvd_of_injective {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (hf : Function.Injective ⇑f) : Nat.card α ∣ Nat.card H

theorem AddSubgroup.card_dvd_of_le {α : Type u_1} [AddGroup α] {H : AddSubgroup α} {K : AddSubgroup α} (hHK : H ≤ K) : Nat.card ↥H ∣ Nat.card ↥K

theorem Subgroup.card_dvd_of_le {α : Type u_1} [Group α] {H : Subgroup α} {K : Subgroup α} (hHK : H ≤ K) : Nat.card ↥H ∣ Nat.card ↥K

theorem AddSubgroup.card_comap_dvd_of_injective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (K : AddSubgroup H) (f : α →+ H) (hf : Function.Injective ⇑f) : Nat.card ↥(AddSubgroup.comap f K) ∣ Nat.card ↥K

theorem Subgroup.card_comap_dvd_of_injective {α : Type u_1} [Group α] {H : Type u_2} [Group H] (K : Subgroup H) (f : α →* H) (hf : Function.Injective ⇑f) : Nat.card ↥(Subgroup.comap f K) ∣ Nat.card ↥K

theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_4 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) : ∀ (x : ↑(QuotientAddGroup.mk ⁻¹' t)), (fun (a : ↥s × ↑t) => ⟨Quotient.out' ↑a.2 + ↑a.1, ⋯⟩) ((fun (a : ↑(QuotientAddGroup.mk ⁻¹' t)) => (⟨-Quotient.out' ↑↑a + ↑a, ⋯⟩, ⟨↑↑a, ⋯⟩)) x) = x

abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) (motive : ↑(QuotientAddGroup.mk ⁻¹' t) → Prop) : ∀ (x : ↑(QuotientAddGroup.mk ⁻¹' t)), (∀ (a : α) (ha : a ∈ QuotientAddGroup.mk ⁻¹' t), motive ⟨a, ha⟩) → motive x

Equations

• ⋯ = ⋯

theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) (a : ↑(QuotientAddGroup.mk ⁻¹' t)) : -Quotient.out' ↑↑a + ↑a ∈ s

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

abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) (motive : ↥s × ↑t → Prop) : ∀ (x : ↥s × ↑t), (∀ (a : α) (ha : a ∈ s) (x : α ⧸ s) (hx : x ∈ t), motive (⟨a, ha⟩, ⟨x, hx⟩)) → motive x

Equations

• ⋯ = ⋯

theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_3 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) (a : ↥s × ↑t) : ↑(Quotient.out' ↑a.2 + ↑a.1) ∈ t

theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_5 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) : ∀ (x : ↥s × ↑t), (fun (a : ↑(QuotientAddGroup.mk ⁻¹' t)) => (⟨-Quotient.out' ↑↑a + ↑a, ⋯⟩, ⟨↑↑a, ⋯⟩)) ((fun (a : ↥s × ↑t) => ⟨Quotient.out' ↑a.2 + ↑a.1, ⋯⟩) x) = x

theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) (a : ↑(QuotientAddGroup.mk ⁻¹' t)) : ↑a ∈ QuotientAddGroup.mk ⁻¹' t

noncomputable def QuotientGroup.preimageMkEquivSubgroupProdSet {α : Type u_1} [Group α] (s : Subgroup α) (t : Set (α ⧸ s)) : ↑(QuotientGroup.mk ⁻¹' t) ≃ ↥s × ↑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.

Equations

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