Mathlib.GroupTheory.Coset.Defs

Module docstring

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

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. "}

QuotientGroup.leftRel definition

: Setoid α

Full source

/-- The equivalence relation corresponding to the partition of a group by left cosets
of a subgroup. -/
@[to_additive "The equivalence relation corresponding to the partition of a group by left cosets
 of a subgroup."]
def leftRel : Setoid α :=
  MulAction.orbitRel s.op α

Left coset equivalence relation

Informal description

The equivalence relation on a group $\alpha$ induced by left cosets of a subgroup $s$, where two elements $x$ and $y$ are related if and only if $x^{-1} y \in s$. This relation partitions the group into left cosets of $s$.

QuotientGroup.leftRel_apply theorem

{x y : α} : leftRel s x y ↔ x⁻¹ * y ∈ s

Full source

@[to_additive]
theorem leftRel_apply {x y : α} : leftRelleftRel s x y ↔ x⁻¹ * y ∈ s :=
  calc
    (∃ a : s.op, y * MulOpposite.unop a = x) ↔ ∃ a : s, y * a = x :=
      s.equivOp.symm.exists_congr_left
    _ ↔ ∃ a : s, x⁻¹ * y = a⁻¹calc
    (∃ a : s.op, y * MulOpposite.unop a = x) ↔ ∃ a : s, y * a = x :=
      s.equivOp.symm.exists_congr_left
    _ ↔ ∃ a : s, x⁻¹ * y = a⁻¹ := by
      simp only [inv_mul_eq_iff_eq_mul, Subgroup.coe_inv, eq_mul_inv_iff_mul_eq]
    _ ↔ x⁻¹ * y ∈ s := by simp [exists_inv_mem_iff_exists_mem]

Characterization of Left Coset Equivalence Relation: $x \sim y \leftrightarrow x^{-1}y \in s$

Informal description

For any elements $x$ and $y$ in a group $\alpha$ and a subgroup $s$ of $\alpha$, the relation $\text{leftRel}\, s\, x\, y$ holds if and only if $x^{-1} y \in s$.

QuotientGroup.leftRel_eq theorem

: ⇑(leftRel s) = fun x y => x⁻¹ * y ∈ s

Full source

@[to_additive]
theorem leftRel_eq : ⇑(leftRel s) = fun x y => x⁻¹x⁻¹ * y ∈ s :=
  funext₂ <| by
    simp only [eq_iff_iff]
    apply leftRel_apply

Characterization of Left Coset Equivalence Relation as $x^{-1}y \in s$

Informal description

The left coset equivalence relation $\text{leftRel}\, s$ on a group $\alpha$ with respect to a subgroup $s$ is equal to the relation defined by $(x, y) \mapsto x^{-1} y \in s$. In other words, two elements $x$ and $y$ are related under $\text{leftRel}\, s$ if and only if $x^{-1} y$ is an element of the subgroup $s$.

QuotientGroup.leftRelDecidable instance

[DecidablePred (· ∈ s)] : DecidableRel (leftRel s).r

Full source

@[to_additive]
instance leftRelDecidable [DecidablePred (· ∈ s)] : DecidableRel (leftRel s).r := fun x y => by
  rw [leftRel_eq]
  exact ‹DecidablePred (· ∈ s)› _

Decidability of Left Coset Equivalence Relation

Informal description

For any subgroup $s$ of a group $\alpha$ with a decidable membership predicate for $s$, the equivalence relation induced by left cosets of $s$ is decidable. That is, given two elements $x, y \in \alpha$, it is decidable whether $x^{-1}y \in s$.

QuotientGroup.instHasQuotientSubgroup instance

: HasQuotient α (Subgroup α)

Full source

/-- `α ⧸ s` is the quotient type representing the left cosets of `s`.
  If `s` is a normal subgroup, `α ⧸ s` is a group -/
@[to_additive "`α ⧸ s` is the quotient type representing the left cosets of `s`. If `s` is a normal
 subgroup, `α ⧸ s` is a group"]
instance instHasQuotientSubgroup : HasQuotient α (Subgroup α) :=
  ⟨fun s => Quotient (leftRel s)⟩

Quotient Group by Subgroup

Informal description

For any group $\alpha$ and subgroup $s$ of $\alpha$, the quotient $\alpha ⧸ s$ is defined as the type of left cosets of $s$ in $\alpha$. When $s$ is a normal subgroup, $\alpha ⧸ s$ inherits a group structure.

QuotientGroup.instDecidableEqQuotientSubgroupOfDecidablePredMem instance

[DecidablePred (· ∈ s)] : DecidableEq (α ⧸ s)

Full source

@[to_additive]
instance [DecidablePred (· ∈ s)] : DecidableEq (α ⧸ s) :=
  @Quotient.decidableEq _ _ (leftRelDecidable _)

Decidability of Equality in Quotient Groups

Informal description

For any group $\alpha$ and subgroup $s$ of $\alpha$ with a decidable membership predicate, the quotient group $\alpha ⧸ s$ has decidable equality.

QuotientGroup.rightRel definition

: Setoid α

Full source

/-- The equivalence relation corresponding to the partition of a group by right cosets of a
subgroup. -/
@[to_additive "The equivalence relation corresponding to the partition of a group by right cosets
 of a subgroup."]
def rightRel : Setoid α :=
  MulAction.orbitRel s α

Right coset equivalence relation

Informal description

The equivalence relation on a group $\alpha$ corresponding to the partition by right cosets of a subgroup $s$, where two elements $x$ and $y$ are related if and only if $y * x^{-1} \in s$.

QuotientGroup.rightRel_apply theorem

{x y : α} : rightRel s x y ↔ y * x⁻¹ ∈ s

Full source

@[to_additive]
theorem rightRel_apply {x y : α} : rightRelrightRel s x y ↔ y * x⁻¹ ∈ s :=
  calc
    (∃ a : s, (a : α) * y = x) ↔ ∃ a : s, y * x⁻¹ = a⁻¹ := by
      simp only [mul_inv_eq_iff_eq_mul, Subgroup.coe_inv, eq_inv_mul_iff_mul_eq]
    _ ↔ y * x⁻¹ ∈ s := by simp [exists_inv_mem_iff_exists_mem]

Characterization of Right Coset Equivalence Relation

Informal description

For any elements $x$ and $y$ in a group $\alpha$ and a subgroup $s$ of $\alpha$, the relation $\text{rightRel}\, s\, x\, y$ holds if and only if $y * x^{-1} \in s$.

QuotientGroup.rightRel_eq theorem

: ⇑(rightRel s) = fun x y => y * x⁻¹ ∈ s

Full source

@[to_additive]
theorem rightRel_eq : ⇑(rightRel s) = fun x y => y * x⁻¹ ∈ s :=
  funext₂ <| by
    simp only [eq_iff_iff]
    apply rightRel_apply

Characterization of Right Coset Equivalence Relation as $y * x^{-1} \in s$

Informal description

The right coset equivalence relation `rightRel s` on a group $\alpha$ with respect to a subgroup $s$ is equal to the relation defined by $(x, y) \mapsto y * x^{-1} \in s$.

QuotientGroup.rightRelDecidable instance

[DecidablePred (· ∈ s)] : DecidableRel (rightRel s).r

Full source

@[to_additive]
instance rightRelDecidable [DecidablePred (· ∈ s)] : DecidableRel (rightRel s).r := fun x y => by
  rw [rightRel_eq]
  exact ‹DecidablePred (· ∈ s)› _

Decidability of Right Coset Equivalence Relation

Informal description

For any subgroup $s$ of a group $\alpha$, if membership in $s$ is decidable, then the equivalence relation defining right cosets (where $x \sim y$ if $y * x^{-1} \in s$) is decidable.

QuotientGroup.quotientRightRelEquivQuotientLeftRel definition

: Quotient (QuotientGroup.rightRel s) ≃ α ⧸ s

Full source

/-- Right cosets are in bijection with left cosets. -/
@[to_additive "Right cosets are in bijection with left cosets."]
def quotientRightRelEquivQuotientLeftRel : QuotientQuotient (QuotientGroup.rightRel s) ≃ α ⧸ s where
  toFun :=
    Quotient.map' (fun g => g⁻¹) fun a b => by
      rw [leftRel_apply, rightRel_apply]
      exact fun h => (congr_arg (· ∈ s) (by simp [mul_assoc])).mp (s.inv_mem h)
      -- Porting note: replace with `by group`
  invFun :=
    Quotient.map' (fun g => g⁻¹) fun a b => by
      rw [leftRel_apply, rightRel_apply]
      exact fun h => (congr_arg (· ∈ s) (by simp [mul_assoc])).mp (s.inv_mem h)
      -- Porting note: replace with `by group`
  left_inv g :=
    Quotient.inductionOn' g fun g =>
      Quotient.sound'
        (by
          simp only [inv_inv]
          exact Quotient.exact' rfl)
  right_inv g :=
    Quotient.inductionOn' g fun g =>
      Quotient.sound'
        (by
          simp only [inv_inv]
          exact Quotient.exact' rfl)

Bijection between Right and Left Coset Quotients

Informal description

The bijection between the quotient of a group $\alpha$ by the right coset equivalence relation of a subgroup $s$ and the left coset quotient $\alpha ⧸ s$. Specifically, the function maps each right coset $[g]_{\text{right}}$ to the left coset $[g^{-1}]_{\text{left}}$, and its inverse maps each left coset $[g]_{\text{left}}$ to the right coset $[g^{-1}]_{\text{right}}$. This establishes that right cosets are in bijection with left cosets.

QuotientGroup.mk abbrev

(a : α) : α ⧸ s

Full source

/-- The canonical map from a group `α` to the quotient `α ⧸ s`. -/
@[to_additive (attr := coe) "The canonical map from an `AddGroup` `α` to the quotient `α ⧸ s`."]
abbrev mk (a : α) : α ⧸ s :=
  Quotient.mk'' a

Canonical Projection to Quotient Group

Informal description

The canonical projection map from a group $\alpha$ to its quotient $\alpha ⧸ s$ by a subgroup $s$, sending each element $a \in \alpha$ to its corresponding left coset $a \cdot s$ in the quotient space.

QuotientGroup.mk_surjective theorem

: Function.Surjective <| @mk _ _ s

Full source

@[to_additive]
theorem mk_surjective : Function.Surjective <| @mk _ _ s :=
  Quotient.mk''_surjective

Surjectivity of the Quotient Group Projection

Informal description

The canonical projection map $\text{mk} : \alpha \to \alpha ⧸ s$ from a group $\alpha$ to its quotient by a subgroup $s$ is surjective. That is, every element of the quotient group $\alpha ⧸ s$ is the image of some element of $\alpha$ under the projection map.

QuotientGroup.range_mk theorem

: range (QuotientGroup.mk (s := s)) = univ

Full source

@[to_additive (attr := simp)]
lemma range_mk : range (QuotientGroup.mk (s := s)) = univ := range_eq_univ.mpr mk_surjective

Surjectivity of the Quotient Group Projection onto the Quotient Space

Informal description

The range of the canonical projection map $\pi : \alpha \to \alpha ⧸ s$ from a group $\alpha$ to its quotient by a subgroup $s$ is equal to the entire quotient group $\alpha ⧸ s$. In other words, every element of $\alpha ⧸ s$ is in the image of $\pi$.

QuotientGroup.induction_on theorem

{C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ z, C (QuotientGroup.mk z)) : C x

Full source

@[to_additive (attr := elab_as_elim)]
theorem induction_on {C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ z, C (QuotientGroup.mk z)) : C x :=
  Quotient.inductionOn' x H

Induction Principle for Quotient Groups

Informal description

Let $G$ be a group and $H$ a subgroup of $G$. For any predicate $C$ on the quotient group $G/H$ and any element $x \in G/H$, if $C$ holds for the image of every element $z \in G$ under the canonical projection $\pi: G \to G/H$ (i.e., $C(\pi(z))$ holds for all $z \in G$), then $C(x)$ holds.

QuotientGroup.instCoeQuotientSubgroup instance

: Coe α (α ⧸ s)

Full source

@[to_additive]
instance : Coe α (α ⧸ s) :=
  ⟨mk⟩

Canonical Map from Group to Quotient Group

Informal description

For any group $\alpha$ and subgroup $s$ of $\alpha$, there is a canonical map from $\alpha$ to the quotient group $\alpha ⧸ s$ that sends each element $a \in \alpha$ to its corresponding left coset $a \cdot s$.

QuotientGroup.quotient_liftOn_mk theorem

{β} (f : α → β) (h) (x : α) : Quotient.liftOn' (x : α ⧸ s) f h = f x

Full source

@[to_additive (attr := simp)]
theorem quotient_liftOn_mk {β} (f : α → β) (h) (x : α) : Quotient.liftOn' (x : α ⧸ s) f h = f x :=
  rfl

Lifted Function Evaluation on Coset Representatives

Informal description

Let $G$ be a group with subgroup $H$, and let $\alpha = G ⧸ H$ be the quotient group. For any function $f : G \to \beta$ that is constant on left cosets of $H$ (i.e., satisfies the condition $h$), and for any element $x \in G$, the value of the lifted function $\text{Quotient.liftOn}'$ applied to the coset $xH \in \alpha$ equals $f(x)$. In other words, $\text{Quotient.liftOn}'(xH, f, h) = f(x)$.

QuotientGroup.forall_mk theorem

{C : α ⧸ s → Prop} : (∀ x : α ⧸ s, C x) ↔ ∀ x : α, C x

Full source

@[to_additive]
theorem forall_mk {C : α ⧸ s → Prop} : (∀ x : α ⧸ s, C x) ↔ ∀ x : α, C x :=
  mk_surjective.forall

Universal Quantification over Quotient Group Elements via Representatives

Informal description

For any predicate $C$ on the quotient group $\alpha ⧸ s$, the universal quantification $\forall x \in \alpha ⧸ s, C(x)$ holds if and only if $\forall x \in \alpha, C(x)$, where $x$ is the canonical projection of $x$ to the quotient.

QuotientGroup.exists_mk theorem

{C : α ⧸ s → Prop} : (∃ x : α ⧸ s, C x) ↔ ∃ x : α, C x

Full source

@[to_additive]
theorem exists_mk {C : α ⧸ s → Prop} : (∃ x : α ⧸ s, C x) ↔ ∃ x : α, C x :=
  mk_surjective.exists

Existence in Quotient Group via Representatives: $(\exists x \in \alpha ⧸ s, C(x)) \leftrightarrow (\exists x \in \alpha, C(x))$

Informal description

For any predicate $C$ on the quotient group $\alpha ⧸ s$, there exists an element $x \in \alpha ⧸ s$ satisfying $C(x)$ if and only if there exists an element $x \in \alpha$ satisfying $C(x)$, where $x$ denotes the coset of $x$ in the quotient.

QuotientGroup.instInhabitedQuotientSubgroup instance

(s : Subgroup α) : Inhabited (α ⧸ s)

Full source

@[to_additive]
instance (s : Subgroup α) : Inhabited (α ⧸ s) :=
  ⟨((1 : α) : α ⧸ s)⟩

Quotient Group is Inhabited

Informal description

For any group $\alpha$ and subgroup $s$ of $\alpha$, the quotient $\alpha ⧸ s$ is inhabited (i.e., contains at least one element).

QuotientGroup.eq theorem

{a b : α} : (a : α ⧸ s) = b ↔ a⁻¹ * b ∈ s

Full source

@[to_additive]
protected theorem eq {a b : α} : (a : α ⧸ s) = b ↔ a⁻¹ * b ∈ s :=
  calc
    _ ↔ leftRel s a b := Quotient.eq''
    _ ↔ _ := by rw [leftRel_apply]

Characterization of Coset Equality: $a \equiv b \mod s \leftrightarrow a^{-1}b \in s$

Informal description

For any elements $a$ and $b$ in a group $\alpha$ and a subgroup $s$ of $\alpha$, the cosets of $a$ and $b$ in the quotient group $\alpha ⧸ s$ are equal if and only if $a^{-1}b \in s$.

QuotientGroup.out_eq' theorem

(a : α ⧸ s) : mk a.out = a

Full source

@[to_additive]
theorem out_eq' (a : α ⧸ s) : mk a.out = a :=
  Quotient.out_eq' a

Canonical Projection of Quotient Representative Equals Original Element

Informal description

For any element $a$ in the quotient group $\alpha ⧸ s$ of a group $\alpha$ by a subgroup $s$, the canonical projection of the representative of $a$ equals $a$ itself. That is, if $a \in \alpha ⧸ s$, then $\text{mk}(a.\text{out}) = a$.

QuotientGroup.mk_out_eq_mul theorem

(g : α) : ∃ h : s, (mk g : α ⧸ s).out = g * h

Full source

@[to_additive QuotientAddGroup.mk_out_eq_mul]
theorem mk_out_eq_mul (g : α) : ∃ h : s, (mk g : α ⧸ s).out = g * h :=
  ⟨⟨g⁻¹ * (mk g).out, QuotientGroup.eq.mp (mk g).out_eq'.symm⟩, by rw [mul_inv_cancel_left]⟩

Representative of Coset is Product with Subgroup Element

Informal description

For any element $g$ in a group $\alpha$ and a subgroup $s$ of $\alpha$, there exists an element $h \in s$ such that the representative of the coset $\pi(g) \in \alpha ⧸ s$ is equal to $g \cdot h$, where $\pi \colon \alpha \to \alpha ⧸ s$ is the canonical projection map.

QuotientGroup.mk_mul_of_mem theorem

(a : α) (hb : b ∈ s) : (mk (a * b) : α ⧸ s) = mk a

Full source

@[to_additive (attr := simp)]
theorem mk_mul_of_mem (a : α) (hb : b ∈ s) : (mk (a * b) : α ⧸ s) = mk a := by
  rwa [QuotientGroup.eq, mul_inv_rev, inv_mul_cancel_right, s.inv_mem_iff]

Quotient Projection Preserves Multiplication by Subgroup Elements

Informal description

For any element $a$ in a group $\alpha$ and any element $b$ in a subgroup $s$ of $\alpha$, the canonical projection of the product $a * b$ in the quotient group $\alpha ⧸ s$ is equal to the canonical projection of $a$. That is, $\pi(a * b) = \pi(a)$, where $\pi: \alpha \to \alpha ⧸ s$ is the canonical projection map.

QuotientGroup.preimage_image_mk theorem

(N : Subgroup α) (s : Set α) : mk ⁻¹' ((mk : α → α ⧸ N) '' s) = ⋃ x : N, (· * (x : α)) ⁻¹' s

Full source

@[to_additive]
theorem preimage_image_mk (N : Subgroup α) (s : Set α) :
    mkmk ⁻¹' ((mk : α → α ⧸ N) '' s) = ⋃ x : N, (· * (x : α)) ⁻¹' s := by
  ext x
  simp only [QuotientGroup.eq, SetLike.exists, exists_prop, Set.mem_preimage, Set.mem_iUnion,
    Set.mem_image, ← eq_inv_mul_iff_mul_eq]
  exact
    ⟨fun ⟨y, hs, hN⟩ => ⟨_, N.inv_mem hN, by simpa using hs⟩, fun ⟨z, hz, hxz⟩ =>
      ⟨x * z, hxz, by simpa using hz⟩⟩

Preimage of Quotient Image Equals Union of Cosets

Informal description

Let $G$ be a group with a subgroup $N$, and let $s$ be a subset of $G$. The preimage under the canonical projection $\pi: G \to G/N$ of the image of $s$ in the quotient group $G/N$ is equal to the union over all $x \in N$ of the left translation of $s$ by $x^{-1}$, i.e., \[ \pi^{-1}(\pi(s)) = \bigcup_{x \in N} x^{-1}s. \]

QuotientGroup.preimage_image_mk_eq_iUnion_image theorem

(N : Subgroup α) (s : Set α) : mk ⁻¹' ((mk : α → α ⧸ N) '' s) = ⋃ x : N, (· * (x : α)) '' s

Full source

@[to_additive]
theorem preimage_image_mk_eq_iUnion_image (N : Subgroup α) (s : Set α) :
    mkmk ⁻¹' ((mk : α → α ⧸ N) '' s) = ⋃ x : N, (· * (x : α)) '' s := by
  rw [preimage_image_mk, iUnion_congr_of_surjective (·⁻¹) inv_surjective]
  exact fun x ↦ image_mul_right'

Preimage of Quotient Image Equals Union of Right Cosets

Informal description

Let $G$ be a group with a subgroup $N$, and let $s$ be a subset of $G$. The preimage under the canonical projection $\pi: G \to G/N$ of the image of $s$ in the quotient group $G/N$ is equal to the union over all $x \in N$ of the right translation of $s$ by $x$, i.e., \[ \pi^{-1}(\pi(s)) = \bigcup_{x \in N} s \cdot x. \]

QuotientGroup.preimage_image_mk_eq_mul theorem

(N : Subgroup α) (s : Set α) : mk ⁻¹' ((mk : α → α ⧸ N) '' s) = s * N

Full source

@[to_additive]
theorem preimage_image_mk_eq_mul (N : Subgroup α) (s : Set α) :
    mkmk ⁻¹' ((mk : α → α ⧸ N) '' s) = s * N := by
  rw [preimage_image_mk_eq_iUnion_image, iUnion_subtype, ← image2_mul, ← iUnion_image_right]
  simp only [SetLike.mem_coe]

Preimage of Quotient Image Equals Product with Subgroup

Informal description

Let $G$ be a group with a normal subgroup $N$, and let $s$ be a subset of $G$. The preimage under the canonical projection $\pi: G \to G/N$ of the image of $s$ in the quotient group $G/N$ is equal to the product set $s \cdot N$, where $s \cdot N$ denotes the set of all products of elements of $s$ with elements of $N$.

Subgroup.quotientEquivOfEq definition

(h : s = t) : α ⧸ s ≃ α ⧸ t

Full source

/-- If two subgroups `M` and `N` of `G` are equal, their quotients are in bijection. -/
@[to_additive "If two subgroups `M` and `N` of `G` are equal, their quotients are in bijection."]
def quotientEquivOfEq (h : s = t) : α ⧸ sα ⧸ s ≃ α ⧸ t where
  toFun := Quotient.map' id fun _a _b h' => h ▸ h'
  invFun := Quotient.map' id fun _a _b h' => h.symm ▸ h'
  left_inv q := induction_on q fun _g => rfl
  right_inv q := induction_on q fun _g => rfl

Bijection between quotient groups of equal subgroups

Informal description

Given a group $\alpha$ and two subgroups $s$ and $t$ of $\alpha$ that are equal (i.e., $s = t$), there exists a bijection between the quotient groups $\alpha ⧸ s$ and $\alpha ⧸ t$. This bijection maps each coset in $\alpha ⧸ s$ to the corresponding coset in $\alpha ⧸ t$ via the identity function on the underlying elements of $\alpha$.

Subgroup.quotientEquivOfEq_mk theorem

(h : s = t) (a : α) : quotientEquivOfEq h (QuotientGroup.mk a) = QuotientGroup.mk a

Full source

theorem quotientEquivOfEq_mk (h : s = t) (a : α) :
    quotientEquivOfEq h (QuotientGroup.mk a) = QuotientGroup.mk a :=
  rfl

Coset Preservation under Quotient Group Bijection for Equal Subgroups

Informal description

Let $\alpha$ be a group with subgroups $s$ and $t$ such that $s = t$. For any element $a \in \alpha$, the bijection $\text{quotientEquivOfEq}\ h$ between the quotient groups $\alpha ⧸ s$ and $\alpha ⧸ t$ maps the coset of $a$ in $\alpha ⧸ s$ to the coset of $a$ in $\alpha ⧸ t$. In other words, the following diagram commutes: \[ \text{quotientEquivOfEq}\ h\ (a \cdot s) = a \cdot t \]