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

• 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_leftCoset {α : Type u_1} [Mul α] {s : Set α} {x : α} (a : α) (hxS : x ∈ s) : a * x ∈ a • s

theorem mem_leftAddCoset {α : Type u_1} [Add α] {s : Set α} {x : α} (a : α) (hxS : x ∈ s) : a + x ∈ a +ᵥ s

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

theorem mem_rightAddCoset {α : Type u_1} [Add α] {s : Set α} {x : α} (a : α) (hxS : x ∈ s) : x + a ∈ AddOpposite.op a +ᵥ s

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem leftAddCoset_assoc {α : Type u_1} [AddSemigroup α] (s : Set α) (a b : α) : a +ᵥ b +ᵥ s = (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 rightAddCoset_assoc {α : Type u_1} [AddSemigroup α] (s : Set α) (a b : α) : AddOpposite.op b +ᵥ AddOpposite.op a +ᵥ s = AddOpposite.op (a + b) +ᵥ s

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

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

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

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

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

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

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

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

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

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

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

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

theorem mem_rightCoset_rightCoset {α : Type u_1} [Monoid α] (s : Submonoid α) {a : α} (ha : MulOpposite.op 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_leftCoset_iff {α : Type u_1} [Group α] {s : Set α} {x : α} (a : α) : x ∈ a • s ↔ a⁻¹ * x ∈ s

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

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

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

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

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

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

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

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

theorem orbit_addSubgroup_eq_rightCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) : AddAction.orbit (↥s) a = AddOpposite.op 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_eq_self_of_mem {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {a : α} (ha : a ∈ s) : AddAction.orbit (↥s) a = ↑s

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

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

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

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

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

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

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

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

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

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

theorem rightCoset_eq_iff {α : Type u_1} [Group α] (s : Subgroup α) {x y : α} : MulOpposite.op x • ↑s = MulOpposite.op y • ↑s ↔ y * x⁻¹ ∈ 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 QuotientGroup.leftRel_r_eq_leftCosetEquivalence {α : Type u_1} [Group α] (s : Subgroup α) : ⇑(leftRel s) = LeftCosetEquivalence ↑s

theorem QuotientGroup.leftRel_prod {α : Type u_1} [Group α] (s : Subgroup α) {β : Type u_2} [Group β] (s' : Subgroup β) : leftRel (s.prod s') = (leftRel s).prod (leftRel s')

theorem QuotientAddGroup.leftRel_prod {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {β : Type u_2} [AddGroup β] (s' : AddSubgroup β) : leftRel (s.prod s') = (leftRel s).prod (leftRel s')

@[deprecated QuotientAddGroup.leftRel_prod (since := "2025-03-11")]

theorem QuotientAddGroup.leftRel_sum {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {β : Type u_2} [AddGroup β] (s' : AddSubgroup β) : leftRel (s.prod s') = (leftRel s).prod (leftRel s')

Alias of QuotientAddGroup.leftRel_prod.

theorem QuotientGroup.leftRel_pi {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Group (β i)] (s' : (i : ι) → Subgroup (β i)) : leftRel (Subgroup.pi Set.univ s') = piSetoid

theorem QuotientAddGroup.leftRel_pi {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → AddGroup (β i)] (s' : (i : ι) → AddSubgroup (β i)) : leftRel (AddSubgroup.pi Set.univ s') = piSetoid

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

theorem QuotientGroup.rightRel_prod {α : Type u_1} [Group α] (s : Subgroup α) {β : Type u_2} [Group β] (s' : Subgroup β) : rightRel (s.prod s') = (rightRel s).prod (rightRel s')

theorem QuotientAddGroup.rightRel_prod {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {β : Type u_2} [AddGroup β] (s' : AddSubgroup β) : rightRel (s.prod s') = (rightRel s).prod (rightRel s')

@[deprecated QuotientAddGroup.rightRel_prod (since := "2025-03-11")]

theorem QuotientAddGroup.rightRel_sum {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {β : Type u_2} [AddGroup β] (s' : AddSubgroup β) : rightRel (s.prod s') = (rightRel s).prod (rightRel s')

Alias of QuotientAddGroup.rightRel_prod.

theorem QuotientGroup.rightRel_pi {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Group (β i)] (s' : (i : ι) → Subgroup (β i)) : rightRel (Subgroup.pi Set.univ s') = piSetoid

theorem QuotientAddGroup.rightRel_pi {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → AddGroup (β i)] (s' : (i : ι) → AddSubgroup (β i)) : rightRel (AddSubgroup.pi Set.univ s') = piSetoid

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

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

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

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

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

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

theorem QuotientGroup.strictMono_comap_prod_image {α : Type u_1} [Group α] (s : Subgroup α) : StrictMono fun (t : Subgroup α) => (Subgroup.comap s.subtype t, mk '' ↑t)

Given a subgroup s, the function that sends a subgroup t to the pair consisting of its intersection with s and its image in the quotient α ⧸ s is strictly monotone, even though it is not injective in general.

theorem QuotientAddGroup.strictMono_comap_prod_image {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : StrictMono fun (t : AddSubgroup α) => (AddSubgroup.comap s.subtype t, mk '' ↑t)

Given an additive subgroup s, the function that sends an additive subgroup t to the pair consisting of its intersection with s and its image in the quotient α ⧸ s is strictly monotone, even though it is not injective in general.

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

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

theorem QuotientGroup.orbit_mk_eq_smul {α : Type u_1} [Group α] {s : Subgroup α} (x : α) : MulAction.orbitRel.Quotient.orbit ↑x = x • ↑s

theorem QuotientAddGroup.orbit_mk_eq_vadd {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (x : α) : AddAction.orbitRel.Quotient.orbit ↑x = x +ᵥ ↑s

theorem QuotientGroup.orbit_eq_out_smul {α : Type u_1} [Group α] {s : Subgroup α} (x : α ⧸ s) : MulAction.orbitRel.Quotient.orbit x = Quotient.out x • ↑s

theorem QuotientAddGroup.orbit_eq_out_vadd {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (x : α ⧸ s) : AddAction.orbitRel.Quotient.orbit x = Quotient.out 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.

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

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

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.

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.

noncomputable def Subgroup.groupEquivQuotientProdSubgroup {α : Type u_1} [Group α] {s : Subgroup α} : α ≃ (α ⧸ s) × ↥s

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

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

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

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

@[simp]

theorem Subgroup.quotientEquivProdOfLE'_symm_apply {α : Type u_1} [Group α] {s t : Subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientGroup.mk) (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) : (quotientEquivProdOfLE' h_le f hf).symm a = Quotient.map' (fun (b : ↥t) => f a.1 * ↑b) ⋯ a.2

@[simp]

theorem AddSubgroup.quotientEquivProdOfLE'_symm_apply {α : Type u_1} [AddGroup α] {s t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : (α ⧸ t) × ↥t ⧸ s.addSubgroupOf t) : (quotientEquivProdOfLE' 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 t : Subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientGroup.mk) (a : α ⧸ s) : (quotientEquivProdOfLE' h_le f hf) a = (Quotient.map' id ⋯ a, Quotient.map' (fun (g : α) => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a)

@[simp]

theorem AddSubgroup.quotientEquivProdOfLE'_apply {α : Type u_1} [AddGroup α] {s t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : α ⧸ s) : (quotientEquivProdOfLE' h_le f hf) a = (Quotient.map' id ⋯ a, Quotient.map' (fun (g : α) => ⟨-f (Quotient.mk'' g) + g, ⋯⟩) ⋯ a)

@[deprecated AddSubgroup.quotientEquivProdOfLE' (since := "2025-03-11")]

def Subgroup.AddSubgroup.quotientEquivSumOfLE' {α : Type u_1} [AddGroup α] {s t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) : α ⧸ s ≃ (α ⧸ t) × ↥t ⧸ s.addSubgroupOf t

Alias of AddSubgroup.quotientEquivProdOfLE'.

---

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

@[deprecated AddSubgroup.quotientEquivProdOfLE'_apply (since := "2025-03-11")]

theorem Subgroup.AddSubgroup.quotientEquivSumOfLE'_apply {α : Type u_1} [AddGroup α] {s t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : α ⧸ s) : (AddSubgroup.quotientEquivProdOfLE' h_le f hf) a = (Quotient.map' id ⋯ a, Quotient.map' (fun (g : α) => ⟨-f (Quotient.mk'' g) + g, ⋯⟩) ⋯ a)

Alias of AddSubgroup.quotientEquivProdOfLE'_apply.

@[deprecated AddSubgroup.quotientEquivProdOfLE'_symm_apply (since := "2025-03-11")]

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

Alias of AddSubgroup.quotientEquivProdOfLE'_symm_apply.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[deprecated AddSubgroup.quotientEquivProdOfLE (since := "2025-03-11")]

def Subgroup.AddSubgroup.quotientEquivSumOfLE {α : Type u_1} [AddGroup α] {s t : AddSubgroup α} (h_le : s ≤ t) : α ⧸ s ≃ (α ⧸ t) × ↥t ⧸ s.addSubgroupOf t

Alias of AddSubgroup.quotientEquivProdOfLE.

---

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

@[deprecated AddSubgroup.quotientEquivProdOfLE_apply (since := "2025-03-11")]

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

Alias of AddSubgroup.quotientEquivProdOfLE_apply.

@[deprecated AddSubgroup.quotientEquivProdOfLE_symm_apply (since := "2025-03-11")]

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

Alias of AddSubgroup.quotientEquivProdOfLE_symm_apply.

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

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.

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.

@[simp]

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

@[simp]

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

@[simp]

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

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.

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def MonoidHom.fiberEquivKer {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) : ↑(⇑f ⁻¹' {f a}) ≃ ↥f.ker

An equivalence between any non-empty fiber of a MonoidHom and its kernel.

def AddMonoidHom.fiberEquivKer {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) : ↑(⇑f ⁻¹' {f a}) ≃ ↥f.ker

An equivalence between any non-empty fiber of an AddMonoidHom and its kernel.

@[simp]

theorem MonoidHom.fiberEquivKer_apply {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) (g : ↑(⇑f ⁻¹' {f a})) : ↑((f.fiberEquivKer a) g) = a⁻¹ * ↑g

@[simp]

theorem AddMonoidHom.fiberEquivKer_apply {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) (g : ↑(⇑f ⁻¹' {f a})) : ↑((f.fiberEquivKer a) g) = -a + ↑g

@[simp]

theorem MonoidHom.fiberEquivKer_symm_apply {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) (g : ↥f.ker) : ↑((f.fiberEquivKer a).symm g) = a * ↑g

@[simp]

theorem AddMonoidHom.fiberEquivKer_symm_apply {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) (g : ↥f.ker) : ↑((f.fiberEquivKer a).symm g) = a + ↑g

noncomputable def MonoidHom.fiberEquivKerOfSurjective {α : Type u_1} [Group α] {H : Type u_2} [Group H] {f : α →* H} (hf : Function.Surjective ⇑f) (h : H) : ↑(⇑f ⁻¹' {h}) ≃ ↥f.ker

An equivalence between any fiber of a surjective MonoidHom and its kernel.

noncomputable def AddMonoidHom.fiberEquivKerOfSurjective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] {f : α →+ H} (hf : Function.Surjective ⇑f) (h : H) : ↑(⇑f ⁻¹' {h}) ≃ ↥f.ker

An equivalence between any fiber of a surjective AddMonoidHom and its kernel.

def MonoidHom.fiberEquiv {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a b : α) : ↑(⇑f ⁻¹' {f a}) ≃ ↑(⇑f ⁻¹' {f b})

An equivalence between any two non-empty fibers of a MonoidHom.

def AddMonoidHom.fiberEquiv {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a b : α) : ↑(⇑f ⁻¹' {f a}) ≃ ↑(⇑f ⁻¹' {f b})

An equivalence between any two non-empty fibers of an AddMonoidHom.

@[simp]

theorem MonoidHom.fiberEquiv_apply {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a b : α) (g : ↑(⇑f ⁻¹' {f a})) : ↑((f.fiberEquiv a b) g) = b * (a⁻¹ * ↑g)

@[simp]

theorem AddMonoidHom.fiberEquiv_apply {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a b : α) (g : ↑(⇑f ⁻¹' {f a})) : ↑((f.fiberEquiv a b) g) = b + (-a + ↑g)

@[simp]

theorem MonoidHom.fiberEquiv_symm_apply {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a b : α) (g : ↑(⇑f ⁻¹' {f b})) : ↑((f.fiberEquiv a b).symm g) = a * (b⁻¹ * ↑g)

@[simp]

theorem AddMonoidHom.fiberEquiv_symm_apply {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a b : α) (g : ↑(⇑f ⁻¹' {f b})) : ↑((f.fiberEquiv a b).symm g) = a + (-b + ↑g)

noncomputable def MonoidHom.fiberEquivOfSurjective {α : Type u_1} [Group α] {H : Type u_2} [Group H] {f : α →* H} (hf : Function.Surjective ⇑f) (h h' : H) : ↑(⇑f ⁻¹' {h}) ≃ ↑(⇑f ⁻¹' {h'})

An equivalence between any two fibers of a surjective MonoidHom.

noncomputable def AddMonoidHom.fiberEquivOfSurjective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] {f : α →+ H} (hf : Function.Surjective ⇑f) (h h' : H) : ↑(⇑f ⁻¹' {h}) ≃ ↑(⇑f ⁻¹' {h'})

An equivalence between any two fibers of a surjective AddMonoidHom.

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

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

theorem QuotientGroup.univ_eq_iUnion_smul {α : Type u_1} [Group α] (H : Subgroup α) : Set.univ = ⋃ (x : α ⧸ H), Quotient.out x • ↑H

A group is made up of a disjoint union of cosets of a subgroup.

theorem QuotientAddGroup.univ_eq_iUnion_vadd {α : Type u_1} [AddGroup α] (H : AddSubgroup α) : Set.univ = ⋃ (x : α ⧸ H), Quotient.out x +ᵥ ↑H

An additive group is made up of a disjoint union of cosets of an additive subgroup.

def QuotientGroup.quotientEquivSelf (α : Type u_1) [Group α] : α ⧸ ⊥ ≃ α

α ⧸ ⊥ is in bijection with α. See QuotientGroup.quotientBot for a multiplicative version.

def QuotientAddGroup.quotientEquivSelf (α : Type u_1) [AddGroup α] : α ⧸ ⊥ ≃ α

α ⧸ ⊥ is in bijection with α. See QuotientAddGroup.quotientBot for an additive version.