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.

Equations

• LeftCosetEquivalence s a b = (a • s = b • 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)

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.

Equations

• RightCosetEquivalence s a b = (MulOpposite.op a • s = MulOpposite.op b • 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)

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 α) : ⇑(QuotientGroup.leftRel s) = LeftCosetEquivalence ↑s

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations

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

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

Equations

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

theorem QuotientGroup.strictMono_comap_prod_image {α : Type u_1} [Group α] (s : Subgroup α) : StrictMono fun (t : Subgroup α) => (Subgroup.comap s.subtype t, QuotientGroup.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, QuotientAddGroup.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.

Equations

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

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 := ⋯ }

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 := ⋯ }

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 := ⋯ }

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.

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.

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.

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.

@[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)

@[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'_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 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)

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' ⋯

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' ⋯

@[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)

@[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_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

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' := ⋯ }

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' := ⋯ }

@[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)

@[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)

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 ⋯

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 ⋯

@[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

@[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

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 ⋯

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 ⋯

@[simp]

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

@[simp]

theorem AddSubgroup.quotientMapOfLE_apply_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s ≤ t) (g : α) : AddSubgroup.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.

Equations

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

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' := ⋯ }

@[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

@[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

@[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

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' := ⋯ }

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

@[simp]

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

@[simp]

theorem AddSubgroup.quotientiInfEmbedding_apply_mk {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (g : α) (i : ι) : (AddSubgroup.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.

Equations

• f.fiberEquivKer a = (Equiv.setCongr ⋯).trans (Subgroup.leftCosetEquivSubgroup a)

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.

Equations

• f.fiberEquivKer a = (Equiv.setCongr ⋯).trans (AddSubgroup.leftCosetEquivAddSubgroup a)

@[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.

Equations

• MonoidHom.fiberEquivKerOfSurjective hf h = ⋯ ▸ f.fiberEquivKer ⋯.choose

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.

Equations

• AddMonoidHom.fiberEquivKerOfSurjective hf h = ⋯ ▸ f.fiberEquivKer ⋯.choose

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.

Equations

• f.fiberEquiv a b = (f.fiberEquivKer a).trans (f.fiberEquivKer b).symm

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.

Equations

• f.fiberEquiv a b = (f.fiberEquivKer a).trans (f.fiberEquivKer b).symm

@[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' : H) : ↑(⇑f ⁻¹' {h}) ≃ ↑(⇑f ⁻¹' {h'})

An equivalence between any two fibers of a surjective MonoidHom.

Equations

• MonoidHom.fiberEquivOfSurjective hf h h' = (MonoidHom.fiberEquivKerOfSurjective hf h).trans (MonoidHom.fiberEquivKerOfSurjective hf h').symm

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

An equivalence between any two fibers of a surjective AddMonoidHom.

Equations

• AddMonoidHom.fiberEquivOfSurjective hf h h' = (AddMonoidHom.fiberEquivKerOfSurjective hf h).trans (AddMonoidHom.fiberEquivKerOfSurjective hf h').symm

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.

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.

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.