Mathlib.GroupTheory.Coset.Basic

mem_leftCoset theorem

{s : Set α} {x : α} (a : α) (hxS : x ∈ s) : a * x ∈ a • s

Full source

@[to_additive mem_leftAddCoset]
theorem mem_leftCoset {s : Set α} {x : α} (a : α) (hxS : x ∈ s) : a * x ∈ a • s :=
  mem_image_of_mem (fun b : α => a * b) hxS

Element Product Belongs to Left Coset

Informal description

Let $G$ be a group with a subset $s \subseteq G$ and an element $x \in s$. For any element $a \in G$, the product $a * x$ belongs to the left coset $a \cdot s$.

mem_rightCoset theorem

{s : Set α} {x : α} (a : α) (hxS : x ∈ s) : x * a ∈ op a • s

Full source

@[to_additive mem_rightAddCoset]
theorem mem_rightCoset {s : Set α} {x : α} (a : α) (hxS : x ∈ s) : x * a ∈ op a • s :=
  mem_image_of_mem (fun b : α => b * a) hxS

Element in Subset Implies Product in Right Coset

Informal description

For any element $a$ in a group $G$ and any subset $s \subseteq G$, if $x \in s$, then the product $x * a$ belongs to the right coset of $s$ by $a$, denoted $s \cdot a$.

LeftCosetEquivalence definition

(s : Set α) (a b : α)

Full source

/-- Equality of two left cosets `a * s` and `b * s`. -/
@[to_additive LeftAddCosetEquivalence "Equality of two left cosets `a + s` and `b + s`."]
def LeftCosetEquivalence (s : Set α) (a b : α) :=
  a • s = b • s

Left coset equivalence relation

Informal description

For a subset $s$ of a group $\alpha$, the relation $\sim$ on $\alpha$ defined by $a \sim b$ if and only if the left cosets $a \cdot s$ and $b \cdot s$ are equal.

leftCosetEquivalence_rel theorem

(s : Set α) : Equivalence (LeftCosetEquivalence s)

Full source

@[to_additive leftAddCosetEquivalence_rel]
theorem leftCosetEquivalence_rel (s : Set α) : Equivalence (LeftCosetEquivalence s) :=
  @Equivalence.mk _ (LeftCosetEquivalence s) (fun _ => rfl) Eq.symm Eq.trans

Left Coset Equivalence Relation is an Equivalence Relation

Informal description

For any subset $s$ of a group $\alpha$, the left coset equivalence relation $\sim$ defined by $a \sim b$ if and only if $a \cdot s = b \cdot s$ is an equivalence relation on $\alpha$.

RightCosetEquivalence definition

(s : Set α) (a b : α)

Full source

/-- Equality of two right cosets `s * a` and `s * b`. -/
@[to_additive RightAddCosetEquivalence "Equality of two right cosets `s + a` and `s + b`."]
def RightCosetEquivalence (s : Set α) (a b : α) :=
  op a • s = op b • s

Right coset equivalence

Informal description

Two elements $ a $ and $ b $ of a group $ G $ are said to be right coset equivalent with respect to a subset $ s \subseteq G $ if the right cosets $ s \cdot a $ and $ s \cdot b $ are equal. Here, $ s \cdot a $ denotes the right coset of $ s $ by $ a $, defined as the set $\{ x \cdot a \mid x \in s \}$.

rightCosetEquivalence_rel theorem

(s : Set α) : Equivalence (RightCosetEquivalence s)

Full source

@[to_additive rightAddCosetEquivalence_rel]
theorem rightCosetEquivalence_rel (s : Set α) : Equivalence (RightCosetEquivalence s) :=
  @Equivalence.mk _ (RightCosetEquivalence s) (fun _a => rfl) Eq.symm Eq.trans

Right Coset Equivalence is an Equivalence Relation

Informal description

For any subset $s$ of a group $\alpha$, the relation of right coset equivalence is an equivalence relation on $\alpha$. That is, it is reflexive, symmetric, and transitive.

leftCoset_assoc theorem

(s : Set α) (a b : α) : a • (b • s) = (a * b) • s

Full source

@[to_additive leftAddCoset_assoc]
theorem leftCoset_assoc (s : Set α) (a b : α) : a • (b • s) = (a * b) • s := by
  simp [← image_smul, (image_comp _ _ _).symm, Function.comp, mul_assoc]

Associativity of Left Coset Action: $a \cdot (b \cdot s) = (a * b) \cdot s$

Informal description

For any subset $s$ of a group $\alpha$ and any elements $a, b \in \alpha$, the left coset operation satisfies the associativity property: $a \cdot (b \cdot s) = (a * b) \cdot s$, where $\cdot$ denotes the left coset action and $*$ denotes the group multiplication.

rightCoset_assoc theorem

(s : Set α) (a b : α) : op b • op a • s = op (a * b) • s

Full source

@[to_additive rightAddCoset_assoc]
theorem rightCoset_assoc (s : Set α) (a b : α) : op b • op a • s = op (a * b) • s := by
  simp [← image_smul, (image_comp _ _ _).symm, Function.comp, mul_assoc]

Associativity of Right Coset Operation

Informal description

Let $G$ be a group, $s$ a subset of $G$, and $a, b$ elements of $G$. Then the right coset operation satisfies the associativity property: \[ b \cdot (a \cdot s) = (a * b) \cdot s \] where $a \cdot s$ denotes the right coset of $s$ by $a$ (using the opposite multiplication convention).

leftCoset_rightCoset theorem

(s : Set α) (a b : α) : op b • a • s = a • (op b • s)

Full source

@[to_additive leftAddCoset_rightAddCoset]
theorem leftCoset_rightCoset (s : Set α) (a b : α) : op b • a • s = a • (op b • s) := by
  simp [← image_smul, (image_comp _ _ _).symm, Function.comp, mul_assoc]

Interchange of Left and Right Cosets

Informal description

For any subset $s$ of a group $\alpha$ and any elements $a, b \in \alpha$, the right coset of the left coset $a \cdot s$ by $b$ is equal to the left coset of the right coset $b \cdot s$ by $a$. In symbols: $$ b \cdot (a \cdot s) = a \cdot (b \cdot s) $$ where $b \cdot s$ denotes the right coset of $s$ by $b$.

one_leftCoset theorem

: (1 : α) • s = s

Full source

@[to_additive zero_leftAddCoset]
theorem one_leftCoset : (1 : α) • s = s :=
  Set.ext <| by simp [← image_smul]

Left Coset Identity: $1 \cdot s = s$

Informal description

For any subset $s$ of a group $\alpha$, the left coset of $s$ by the identity element $1$ is equal to $s$ itself, i.e., $1 \cdot s = s$.

rightCoset_one theorem

: op (1 : α) • s = s

Full source

@[to_additive rightAddCoset_zero]
theorem rightCoset_one : op (1 : α) • s = s :=
  Set.ext <| by simp [← image_smul]

Right Coset of Identity Element Preserves Subset

Informal description

For any subset $s$ of a group $\alpha$, the right coset of $s$ by the identity element $1$ is equal to $s$ itself, i.e., $1 \cdot s = s$.

mem_own_leftCoset theorem

(a : α) : a ∈ a • (s : Set α)

Full source

@[to_additive mem_own_leftAddCoset]
theorem mem_own_leftCoset (a : α) : a ∈ a • (s : Set α) :=
  suffices a * 1 ∈ a • (s : Set α) by simpa
  mem_leftCoset a (one_mem s : 1 ∈ s)

Element Belongs to Its Own Left Coset

Informal description

For any element $a$ in a group $\alpha$ and any subset $s \subseteq \alpha$, the element $a$ belongs to the left coset $a \cdot s$.

mem_own_rightCoset theorem

(a : α) : a ∈ op a • (s : Set α)

Full source

@[to_additive mem_own_rightAddCoset]
theorem mem_own_rightCoset (a : α) : a ∈ op a • (s : Set α) :=
  suffices 1 * a ∈ op a • (s : Set α) by simpa
  mem_rightCoset a (one_mem s : 1 ∈ s)

Element Belongs to Its Own Right Coset

Informal description

For any element $a$ in a group $\alpha$ and any subset $s \subseteq \alpha$, the element $a$ belongs to the right coset of $s$ by $a$, i.e., $a \in s \cdot a$.

mem_leftCoset_leftCoset theorem

{a : α} (ha : a • (s : Set α) = s) : a ∈ s

Full source

@[to_additive mem_leftAddCoset_leftAddCoset]
theorem mem_leftCoset_leftCoset {a : α} (ha : a • (s : Set α) = s) : a ∈ s := by
  rw [← SetLike.mem_coe, ← ha]; exact mem_own_leftCoset s a

Element in Subgroup When Left Coset Equals Subgroup

Informal description

For any element $a$ in a group $\alpha$ and any subset $s \subseteq \alpha$, if the left coset $a \cdot s$ equals $s$, then $a$ belongs to $s$.

mem_rightCoset_rightCoset theorem

{a : α} (ha : op a • (s : Set α) = s) : a ∈ s

Full source

@[to_additive mem_rightAddCoset_rightAddCoset]
theorem mem_rightCoset_rightCoset {a : α} (ha : op a • (s : Set α) = s) : a ∈ s := by
  rw [← SetLike.mem_coe, ← ha]; exact mem_own_rightCoset s a

Element in Subgroup When Right Coset Equals Subgroup

Informal description

For any element $a$ in a group $\alpha$ and any subset $s \subseteq \alpha$, if the right coset $s \cdot a$ equals $s$, then $a$ belongs to $s$.

mem_leftCoset_iff theorem

(a : α) : x ∈ a • s ↔ a⁻¹ * x ∈ s

Full source

@[to_additive mem_leftAddCoset_iff]
theorem mem_leftCoset_iff (a : α) : x ∈ a • sx ∈ a • s ↔ a⁻¹ * x ∈ s :=
  Iff.intro (fun ⟨b, hb, Eq⟩ => by simp [Eq.symm, hb]) fun h => ⟨a⁻¹ * x, h, by simp⟩

Characterization of Left Coset Membership: $x \in a \cdot s \leftrightarrow a^{-1} \cdot x \in s$

Informal description

For any element $a$ in a group $\alpha$ and any subset $s$ of $\alpha$, an element $x$ belongs to the left coset $a \cdot s$ if and only if $a^{-1} \cdot x$ belongs to $s$.

mem_rightCoset_iff theorem

(a : α) : x ∈ op a • s ↔ x * a⁻¹ ∈ s

Full source

@[to_additive mem_rightAddCoset_iff]
theorem mem_rightCoset_iff (a : α) : x ∈ op a • sx ∈ op a • s ↔ x * a⁻¹ ∈ s :=
  Iff.intro (fun ⟨b, hb, Eq⟩ => by simp [Eq.symm, hb]) fun h => ⟨x * a⁻¹, h, by simp⟩

Characterization of Right Coset Membership: $x \in a \cdot s \leftrightarrow x \cdot a^{-1} \in s$

Informal description

For any element $a$ in a group $\alpha$ and any subset $s$ of $\alpha$, an element $x$ belongs to the right coset $a \cdot s$ if and only if $x \cdot a^{-1}$ belongs to $s$.

leftCoset_mem_leftCoset theorem

{a : α} (ha : a ∈ s) : a • (s : Set α) = s

Full source

@[to_additive leftAddCoset_mem_leftAddCoset]
theorem leftCoset_mem_leftCoset {a : α} (ha : a ∈ s) : a • (s : Set α) = s :=
  Set.ext <| by simp [mem_leftCoset_iff, mul_mem_cancel_left (s.inv_mem ha)]

Left Coset of Subgroup Element Equals Subgroup

Informal description

For any element $a$ in a subgroup $s$ of a group $\alpha$, the left coset $a \cdot s$ is equal to $s$ itself.

rightCoset_mem_rightCoset theorem

{a : α} (ha : a ∈ s) : op a • (s : Set α) = s

Full source

@[to_additive rightAddCoset_mem_rightAddCoset]
theorem rightCoset_mem_rightCoset {a : α} (ha : a ∈ s) : op a • (s : Set α) = s :=
  Set.ext fun b => by simp [mem_rightCoset_iff, mul_mem_cancel_right (s.inv_mem ha)]

Right Coset of Subgroup by Its Own Element Equals Subgroup

Informal description

For any element $a$ in a subgroup $s$ of a group $\alpha$, the right coset of $s$ by $a$ is equal to $s$ itself, i.e., $a \cdot s = s$.

orbit_subgroup_eq_rightCoset theorem

(a : α) : MulAction.orbit s a = op a • s

Full source

@[to_additive]
theorem orbit_subgroup_eq_rightCoset (a : α) : MulAction.orbit s a = op a • s :=
  Set.ext fun _b => ⟨fun ⟨c, d⟩ => ⟨c, c.2, d⟩, fun ⟨c, d, e⟩ => ⟨⟨c, d⟩, e⟩⟩

Orbit of Subgroup Action Equals Right Coset

Informal description

For any element $a$ in a type $\alpha$ acted upon by a subgroup $s$ of a group $G$, the orbit of $a$ under the action of $s$ is equal to the right coset of $s$ by $a$, i.e., $\text{orbit}_s(a) = \text{op}\, a \cdot s$.

orbit_subgroup_eq_self_of_mem theorem

{a : α} (ha : a ∈ s) : MulAction.orbit s a = s

Full source

@[to_additive]
theorem orbit_subgroup_eq_self_of_mem {a : α} (ha : a ∈ s) : MulAction.orbit s a = s :=
  (orbit_subgroup_eq_rightCoset s a).trans (rightCoset_mem_rightCoset s ha)

Orbit of Subgroup Element Equals Subgroup

Informal description

For any element $a$ in a subgroup $s$ of a group $\alpha$, the orbit of $a$ under the action of $s$ is equal to $s$ itself, i.e., $\text{orbit}_s(a) = s$.

orbit_subgroup_one_eq_self theorem

: MulAction.orbit s (1 : α) = s

Full source

@[to_additive]
theorem orbit_subgroup_one_eq_self : MulAction.orbit s (1 : α) = s :=
  orbit_subgroup_eq_self_of_mem s s.one_mem

Orbit of Identity Under Subgroup Action Equals Subgroup

Informal description

For any subgroup $s$ of a group $\alpha$ acting on itself by multiplication, the orbit of the identity element $1$ under the action of $s$ is equal to $s$ itself, i.e., $\text{orbit}_s(1) = s$.

normal_of_eq_cosets theorem

(h : ∀ g : α, g • (s : Set α) = op g • s) : s.Normal

Full source

@[to_additive normal_of_eq_addCosets]
theorem normal_of_eq_cosets (h : ∀ g : α, g • (s : Set α) = op g • s) : s.Normal :=
  ⟨fun a ha g =>
    show g * a * g⁻¹ ∈ (s : Set α) by rw [← mem_rightCoset_iff, ← h]; exact mem_leftCoset g ha⟩

Normal Subgroup Criterion via Coset Equality

Informal description

Let $G$ be a group and $H \subseteq G$ a subgroup. If for every element $g \in G$ the left coset $gH$ equals the right coset $Hg$, then $H$ is a normal subgroup of $G$.

normal_iff_eq_cosets theorem

: s.Normal ↔ ∀ g : α, g • (s : Set α) = op g • s

Full source

@[to_additive normal_iff_eq_addCosets]
theorem normal_iff_eq_cosets : s.Normal ↔ ∀ g : α, g • (s : Set α) = op g • s :=
  ⟨@eq_cosets_of_normal _ _ s, normal_of_eq_cosets s⟩

Normal Subgroup Characterization via Coset Equality

Informal description

A subgroup $H$ of a group $G$ is normal if and only if for every element $g \in G$, the left coset $gH$ equals the right coset $Hg$.

leftCoset_eq_iff theorem

{x y : α} : x • (s : Set α) = y • s ↔ x⁻¹ * y ∈ s

Full source

@[to_additive leftAddCoset_eq_iff]
theorem leftCoset_eq_iff {x y : α} : x • (s : Set α) = y • s ↔ x⁻¹ * y ∈ s := by
  rw [Set.ext_iff]
  simp_rw [mem_leftCoset_iff, SetLike.mem_coe]
  constructor
  · intro h
    apply (h y).mpr
    rw [inv_mul_cancel]
    exact s.one_mem
  · intro h z
    rw [← mul_inv_cancel_right x⁻¹ y]
    rw [mul_assoc]
    exact s.mul_mem_cancel_left h

Characterization of Equal Left Cosets: $xH = yH \iff x^{-1}y \in H$

Informal description

Let $G$ be a group and $H \subseteq G$ a subgroup. For any two elements $x, y \in G$, the left cosets $xH$ and $yH$ are equal if and only if $x^{-1}y \in H$.

rightCoset_eq_iff theorem

{x y : α} : op x • (s : Set α) = op y • s ↔ y * x⁻¹ ∈ s

Full source

@[to_additive rightAddCoset_eq_iff]
theorem rightCoset_eq_iff {x y : α} : opop x • (s : Set α) = op y • s ↔ y * x⁻¹ ∈ s := by
  rw [Set.ext_iff]
  simp_rw [mem_rightCoset_iff, SetLike.mem_coe]
  constructor
  · intro h
    apply (h y).mpr
    rw [mul_inv_cancel]
    exact s.one_mem
  · intro h z
    rw [← inv_mul_cancel_left y x⁻¹]
    rw [← mul_assoc]
    exact s.mul_mem_cancel_right h

Characterization of Equal Right Cosets: $Hx = Hy \iff yx^{-1} \in H$

Informal description

Let $G$ be a group and $H \subseteq G$ a subgroup. For any two elements $x, y \in G$, the right cosets $Hx$ and $Hy$ are equal if and only if $yx^{-1} \in H$.

QuotientGroup.leftRel_r_eq_leftCosetEquivalence theorem

: ⇑(QuotientGroup.leftRel s) = LeftCosetEquivalence s

Full source

theorem leftRel_r_eq_leftCosetEquivalence :
    ⇑(QuotientGroup.leftRel s) = LeftCosetEquivalence s := by
  ext
  rw [leftRel_eq]
  exact (leftCoset_eq_iff s).symm

Left Coset Equivalence Relation Characterization

Informal description

The left coset equivalence relation $\text{leftRel}\, s$ on a group $G$ with respect to a subgroup $s$ is equal to the relation $\text{LeftCosetEquivalence}\, s$, which defines two elements $x, y \in G$ to be equivalent if and only if their left cosets $x \cdot s$ and $y \cdot s$ are equal.

QuotientGroup.leftRel_prod theorem

{β : Type*} [Group β] (s' : Subgroup β) : leftRel (s.prod s') = (leftRel s).prod (leftRel s')

Full source

@[to_additive leftRel_prod]
lemma leftRel_prod {β : Type*} [Group β] (s' : Subgroup β) :
    leftRel (s.prod s') = (leftRel s).prod (leftRel s') := by
  refine Setoid.ext fun x y ↦ ?_
  rw [Setoid.prod_apply]
  simp_rw [leftRel_apply]
  rfl

Product of Left Coset Equivalence Relations Equals Left Coset Equivalence of Product Subgroups

Informal description

Let $G$ and $H$ be groups with subgroups $s \subseteq G$ and $s' \subseteq H$ respectively. The left coset equivalence relation on the product group $G \times H$ with respect to the product subgroup $s \times s'$ is equal to the product of the left coset equivalence relations on $G$ with respect to $s$ and on $H$ with respect to $s'$.

QuotientGroup.leftRel_pi theorem

 {ι : Type*} {β : ι → Type*} [∀ i, Group (β i)] (s' : ∀ i, Subgroup (β i)) :
  leftRel (Subgroup.pi Set.univ s') = @piSetoid _ _ fun i ↦ leftRel (s' i)

Full source

@[to_additive]
lemma leftRel_pi {ι : Type*} {β : ι → Type*} [∀ i, Group (β i)] (s' : ∀ i, Subgroup (β i)) :
    leftRel (Subgroup.pi Set.univ s') = @piSetoid _ _ fun i ↦ leftRel (s' i) := by
  refine Setoid.ext fun x y ↦ ?_
  simp [Setoid.piSetoid_apply, leftRel_apply, Subgroup.mem_pi]

Product of Left Coset Equivalence Relations for Product Groups

Informal description

Let $\{β_i\}_{i \in \iota}$ be a family of groups, and for each $i \in \iota$, let $s'_i$ be a subgroup of $β_i$. The left coset equivalence relation on the product group $\prod_{i \in \iota} β_i$ with respect to the product subgroup $\prod_{i \in \iota} s'_i$ is equal to the product of the left coset equivalence relations on each $β_i$ with respect to $s'_i$.

QuotientGroup.rightRel_r_eq_rightCosetEquivalence theorem

: ⇑(QuotientGroup.rightRel s) = RightCosetEquivalence s

Full source

theorem rightRel_r_eq_rightCosetEquivalence :
    ⇑(QuotientGroup.rightRel s) = RightCosetEquivalence s := by
  ext
  rw [rightRel_eq]
  exact (rightCoset_eq_iff s).symm

Right Coset Equivalence Relation Characterization

Informal description

The right coset equivalence relation `rightRel s` on a group $G$ with respect to a subgroup $s$ is equal to the relation `RightCosetEquivalence s`, which defines two elements $x, y \in G$ to be equivalent if and only if $y * x^{-1} \in s$.

QuotientGroup.rightRel_prod theorem

{β : Type*} [Group β] (s' : Subgroup β) : rightRel (s.prod s') = (rightRel s).prod (rightRel s')

Full source

@[to_additive rightRel_prod]
lemma rightRel_prod {β : Type*} [Group β] (s' : Subgroup β) :
    rightRel (s.prod s') = (rightRel s).prod (rightRel s') := by
  refine Setoid.ext fun x y ↦ ?_
  rw [Setoid.prod_apply]
  simp_rw [rightRel_apply]
  rfl

Right Coset Equivalence Relation on Product Group as Product of Equivalence Relations

Informal description

Let $G$ and $H$ be groups with subgroups $s \leq G$ and $s' \leq H$. The right coset equivalence relation on the product group $G \times H$ with respect to the product subgroup $s \times s'$ is equal to the product of the right coset equivalence relations on $G$ with respect to $s$ and on $H$ with respect to $s'$.

QuotientGroup.rightRel_pi theorem

 {ι : Type*} {β : ι → Type*} [∀ i, Group (β i)] (s' : ∀ i, Subgroup (β i)) :
  rightRel (Subgroup.pi Set.univ s') = @piSetoid _ _ fun i ↦ rightRel (s' i)

Full source

@[to_additive]
lemma rightRel_pi {ι : Type*} {β : ι → Type*} [∀ i, Group (β i)] (s' : ∀ i, Subgroup (β i)) :
    rightRel (Subgroup.pi Set.univ s') = @piSetoid _ _ fun i ↦ rightRel (s' i) := by
  refine Setoid.ext fun x y ↦ ?_
  simp [Setoid.piSetoid_apply, rightRel_apply, Subgroup.mem_pi]

Right Coset Equivalence Relation on Product Group as Product of Equivalence Relations

Informal description

For a family of groups $\{\beta_i\}_{i \in \iota}$ and a family of subgroups $s' = (s'_i)_{i \in \iota}$ where each $s'_i$ is a subgroup of $\beta_i$, the right coset equivalence relation on the product group $\prod_{i \in \iota} \beta_i$ with respect to the product subgroup $\prod_{i \in \iota} s'_i$ is equal to the product of the right coset equivalence relations on each $\beta_i$ with respect to $s'_i$. In other words, the equivalence relation $\text{rightRel}(\prod_{i} s'_i)$ on $\prod_{i} \beta_i$ is equal to the product equivalence relation $\prod_{i} \text{rightRel}(s'_i)$.

QuotientGroup.fintypeQuotientRightRel instance

[Fintype (α ⧸ s)] : Fintype (Quotient (QuotientGroup.rightRel s))

Full source

@[to_additive]
instance fintypeQuotientRightRel [Fintype (α ⧸ s)] :
    Fintype (Quotient (QuotientGroup.rightRel s)) :=
  Fintype.ofEquiv (α ⧸ s) (QuotientGroup.quotientRightRelEquivQuotientLeftRel s).symm

Finiteness of the Right Coset Quotient for Finite Left Coset Quotient

Informal description

For any group $\alpha$ with a subgroup $s$ such that the left coset quotient $\alpha ⧸ s$ is finite, the quotient by the right coset equivalence relation is also finite.

QuotientGroup.card_quotient_rightRel theorem

[Fintype (α ⧸ s)] : Fintype.card (Quotient (QuotientGroup.rightRel s)) = Fintype.card (α ⧸ s)

Full source

@[to_additive]
theorem card_quotient_rightRel [Fintype (α ⧸ s)] :
    Fintype.card (Quotient (QuotientGroup.rightRel s)) = Fintype.card (α ⧸ s) :=
  Fintype.ofEquiv_card (QuotientGroup.quotientRightRelEquivQuotientLeftRel s).symm

Cardinality Equality of Left and Right Coset Quotients for Finite Groups

Informal description

For any finite left coset quotient $\alpha ⧸ s$ of a group $\alpha$ by a subgroup $s$, the cardinality of the quotient by the right coset equivalence relation equals the cardinality of the left coset quotient, i.e., $|\alpha / \text{rightRel}(s)| = |\alpha ⧸ s|$.

QuotientGroup.fintype instance

[Fintype α] (s : Subgroup α) [DecidableRel (leftRel s).r] : Fintype (α ⧸ s)

Full source

@[to_additive]
instance fintype [Fintype α] (s : Subgroup α) [DecidableRel (leftRel s).r] : Fintype (α ⧸ s) :=
  Quotient.fintype (leftRel s)

Finite Quotient Group of Finite Group by Subgroup

Informal description

For any finite group $\alpha$ and subgroup $s$ of $\alpha$, the quotient group $\alpha ⧸ s$ is finite.

QuotientGroup.strictMono_comap_prod_image theorem

: StrictMono fun t : Subgroup α ↦ (t.comap s.subtype, mk (s := s) '' t)

Full source

/-- 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. -/
@[to_additive QuotientAddGroup.strictMono_comap_prod_image "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 strictMono_comap_prod_image :
    StrictMono fun t : Subgroup α ↦ (t.comap s.subtype, mk (s := s) '' t) := by
  refine fun t₁ t₂ h ↦ ⟨⟨Subgroup.comap_mono h.1, Set.image_mono h.1⟩,
    mt (fun ⟨le1, le2⟩ a ha ↦ ?_) h.2⟩
  obtain ⟨a', h', eq⟩ := le2 ⟨_, ha, rfl⟩
  convert ← t₁.mul_mem h' (@le1 ⟨_, QuotientGroup.eq.1 eq⟩ <| t₂.mul_mem (t₂.inv_mem <| h.1 h') ha)
  apply mul_inv_cancel_left

Strict Monotonicity of Subgroup Intersection and Quotient Image

Informal description

For a subgroup $s$ of a group $\alpha$, the function that maps each subgroup $t$ of $\alpha$ to the pair $(t \cap s, \pi(t))$ is strictly increasing, where $\pi: \alpha \to \alpha ⧸ s$ is the canonical projection map sending $a$ to its left coset $a \cdot s$.

QuotientGroup.orbit_mk_eq_smul theorem

(x : α) : MulAction.orbitRel.Quotient.orbit (x : α ⧸ s) = x • s

Full source

@[to_additive]
lemma orbit_mk_eq_smul (x : α) : MulAction.orbitRel.Quotient.orbit (x : α ⧸ s) = x • s := by
  ext
  rw [orbitRel.Quotient.mem_orbit]
  simpa [mem_smul_set_iff_inv_smul_mem, ← leftRel_apply, Quotient.eq''] using Setoid.comm' _

Orbit of Quotient Class Equals Left Coset

Informal description

For any element $x$ in a group $\alpha$ and any subgroup $s$ of $\alpha$, the orbit of the equivalence class of $x$ in the quotient group $\alpha ⧸ s$ under the action of $\alpha$ is equal to the left coset $x \cdot s$.

QuotientGroup.orbit_eq_out_smul theorem

(x : α ⧸ s) : MulAction.orbitRel.Quotient.orbit x = x.out • s

Full source

@[to_additive]
lemma orbit_eq_out_smul (x : α ⧸ s) : MulAction.orbitRel.Quotient.orbit x = x.out • s := by
  induction x using QuotientGroup.induction_on
  simp only [orbit_mk_eq_smul, ← eq_class_eq_leftCoset, Quotient.out_eq']

Orbit of Quotient Element Equals Left Coset by Representative

Informal description

For any element $x$ in the quotient group $\alpha ⧸ s$ of a group $\alpha$ by a subgroup $s$, the orbit of $x$ under the group action is equal to the left coset of $s$ by a representative element $x.\text{out}$ of the equivalence class $x$, i.e., $\text{orbit}(x) = x.\text{out} \cdot s$.

Subgroup.leftCosetEquivSubgroup definition

(g : α) : (g • s : Set α) ≃ s

Full source

/-- The natural bijection between a left coset `g * s` and `s`. -/
@[to_additive "The natural bijection between the cosets `g + s` and `s`."]
def leftCosetEquivSubgroup (g : α) : (g • s : Set α) ≃ s :=
  ⟨fun x => ⟨g⁻¹ * x.1, (mem_leftCoset_iff _).1 x.2⟩, fun x => ⟨g * x.1, x.1, x.2, rfl⟩,
    fun ⟨x, _⟩ => Subtype.eq <| by simp, fun ⟨g, _⟩ => Subtype.eq <| by simp⟩

Bijection between left coset and subgroup

Informal description

For any element $ g $ of a group $ \alpha $ and any subgroup $ s $ of $ \alpha $, there is a natural bijection between the left coset $ g \cdot s $ and the subgroup $ s $. The bijection is given by: - The forward map sends $ x \in g \cdot s $ to $ g^{-1} \cdot x \in s $ - The backward map sends $ y \in s $ to $ g \cdot y \in g \cdot s $

Subgroup.rightCosetEquivSubgroup definition

(g : α) : (op g • s : Set α) ≃ s

Full source

/-- The natural bijection between a right coset `s * g` and `s`. -/
@[to_additive "The natural bijection between the cosets `s + g` and `s`."]
def rightCosetEquivSubgroup (g : α) : (op g • s : Set α) ≃ s :=
  ⟨fun x => ⟨x.1 * g⁻¹, (mem_rightCoset_iff _).1 x.2⟩, fun x => ⟨x.1 * g, x.1, x.2, rfl⟩,
    fun ⟨x, _⟩ => Subtype.eq <| by simp, fun ⟨g, _⟩ => Subtype.eq <| by simp⟩

Bijection between a right coset and its subgroup

Informal description

For any element $ g $ in a group $ \alpha $ and any subgroup $ s $ of $ \alpha $, the right coset $ s \cdot g $ is in bijection with $ s $ itself. The bijection is given by: - The forward map sends $ x \in s \cdot g $ to $ x \cdot g^{-1} \in s $. - The backward map sends $ y \in s $ to $ y \cdot g \in s \cdot g $.

Subgroup.groupEquivQuotientProdSubgroup definition

: α ≃ (α ⧸ s) × s

Full source

/-- A (non-canonical) bijection between a group `α` and the product `(α/s) × s` -/
@[to_additive addGroupEquivQuotientProdAddSubgroup
  "A (non-canonical) bijection between an add_group `α` and the product `(α/s) × s`"]
noncomputable def groupEquivQuotientProdSubgroup : α ≃ (α ⧸ s) × s :=
  calc
    α ≃ ΣL : α ⧸ s, { x : α // (x : α ⧸ s) = L } := (Equiv.sigmaFiberEquiv QuotientGroup.mk).symm
    _ ≃ ΣL : α ⧸ s, (Quotient.out L • s : Set α)calc
    α ≃ ΣL : α ⧸ s, { x : α // (x : α ⧸ s) = L } := (Equiv.sigmaFiberEquiv QuotientGroup.mk).symm
    _ ≃ ΣL : α ⧸ s, (Quotient.out L • s : Set α) :=
      Equiv.sigmaCongrRight fun L => by
        rw [← eq_class_eq_leftCoset]
        show
          (_root_.Subtype fun x : α => Quotient.mk'' x = L) ≃
            _root_.Subtype fun x : α => Quotient.mk'' x = Quotient.mk'' _
        simp
        rfl
    _ ≃ Σ _L : α ⧸ s, scalc
    α ≃ ΣL : α ⧸ s, { x : α // (x : α ⧸ s) = L } := (Equiv.sigmaFiberEquiv QuotientGroup.mk).symm
    _ ≃ ΣL : α ⧸ s, (Quotient.out L • s : Set α) :=
      Equiv.sigmaCongrRight fun L => by
        rw [← eq_class_eq_leftCoset]
        show
          (_root_.Subtype fun x : α => Quotient.mk'' x = L) ≃
            _root_.Subtype fun x : α => Quotient.mk'' x = Quotient.mk'' _
        simp
        rfl
    _ ≃ Σ _L : α ⧸ s, s := Equiv.sigmaCongrRight fun _ => leftCosetEquivSubgroup _
    _ ≃ (α ⧸ s) × s := Equiv.sigmaEquivProd _ _

Group decomposition as quotient times subgroup

Informal description

For any group $\alpha$ and subgroup $s$ of $\alpha$, there exists a (non-canonical) bijection between $\alpha$ and the product $(\alpha ⧸ s) \times s$ of the quotient group $\alpha ⧸ s$ with the subgroup $s$. This equivalence is constructed through the following steps: 1. First, $\alpha$ is identified with the sigma type of pairs $(L, x)$ where $L$ is a left coset in $\alpha ⧸ s$ and $x$ is an element of $\alpha$ belonging to $L$. 2. Each fiber $\{x \in \alpha \mid x \in L\}$ is then identified with the left coset $g \cdot s$ (where $g$ is any representative of $L$). 3. Each left coset $g \cdot s$ is in bijection with $s$ itself via the map $x \mapsto g^{-1} \cdot x$. 4. Finally, the sigma type is identified with the product $(\alpha ⧸ s) \times s$.

Subgroup.quotientEquivProdOfLE' definition

 (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientGroup.mk) : α ⧸ s ≃ (α ⧸ t) × t ⧸ s.subgroupOf t

Full source

/-- 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`. -/
@[to_additive (attr := simps) 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`."]
def quotientEquivProdOfLE' (h_le : s ≤ t) (f : α ⧸ t → α)
    (hf : Function.RightInverse f QuotientGroup.mk) : α ⧸ sα ⧸ s ≃ (α ⧸ t) × t ⧸ s.subgroupOf t where
  toFun a :=
    ⟨a.map' id fun _ _ h => leftRel_apply.mpr (h_le (leftRel_apply.mp h)),
      a.map' (fun g : α => ⟨(f (Quotient.mk'' g))⁻¹ * g, leftRel_apply.mp (Quotient.exact' (hf g))⟩)
        fun b c h => by
        rw [leftRel_apply]
        change ((f b)⁻¹ * b)⁻¹ * ((f c)⁻¹ * c) ∈ s
        have key : f b = f c :=
          congr_arg f (Quotient.sound' (leftRel_apply.mpr (h_le (leftRel_apply.mp h))))
        rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]⟩
  invFun a := by
    refine a.2.map' (fun (b : { x // x ∈ t}) => f a.1 * b) fun b c h => by
      rw [leftRel_apply] at h ⊢
      change (f a.1 * b)⁻¹(f a.1 * b)⁻¹ * (f a.1 * c) ∈ s
      rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
  left_inv := by
    refine Quotient.ind' fun a => ?_
    simp_rw [Quotient.map'_mk'', id, mul_inv_cancel_left]
  right_inv := by
    refine Prod.rec ?_
    refine Quotient.ind' fun a => ?_
    refine Quotient.ind' fun b => ?_
    have key : Quotient.mk'' (f (Quotient.mk'' a) * b) = Quotient.mk'' a :=
      (QuotientGroup.mk_mul_of_mem (f a) b.2).trans (hf a)
    simp_rw [Quotient.map'_mk'', id, key, inv_mul_cancel_left]

Constructive equivalence between quotients $\alpha/s$ and $(\alpha/t) \times (t/s)$

Informal description

Given a group $\alpha$ with subgroups $s \leq t$ and a right inverse $f$ of the canonical projection $\alpha \to \alpha ⧸ t$, there is a natural equivalence between the quotient $\alpha ⧸ s$ and the product $(\alpha ⧸ t) \times (t ⧸ s)$. The equivalence is constructed as: - The forward map sends a coset $a \in \alpha ⧸ s$ to the pair consisting of: - The image of $a$ under the natural projection $\alpha ⧸ s \to \alpha ⧸ t$ - The coset $(f(\overline{a}))^{-1} \cdot a \in t ⧸ s$, where $\overline{a}$ is the projection of $a$ in $\alpha ⧸ t$ - The backward map sends a pair $(a, b) \in (\alpha ⧸ t) \times (t ⧸ s)$ to the coset $f(a) \cdot b \in \alpha ⧸ s$ This provides a constructive version of the classical isomorphism $\alpha/s \cong (\alpha/t) \times (t/s)$.

Subgroup.quotientEquivProdOfLE definition

(h_le : s ≤ t) : α ⧸ s ≃ (α ⧸ t) × t ⧸ s.subgroupOf t

Full source

/-- If `H ≤ K`, then `G/H ≃ G/K × K/H` nonconstructively.
The constructive version is `quotientEquivProdOfLE'`. -/
@[to_additive (attr := simps!) quotientEquivProdOfLE
  "If `H ≤ K`, then `G/H ≃ G/K × K/H` nonconstructively. The
constructive version is `quotientEquivProdOfLE'`."]
noncomputable def quotientEquivProdOfLE (h_le : s ≤ t) : α ⧸ sα ⧸ s ≃ (α ⧸ t) × t ⧸ s.subgroupOf t :=
  quotientEquivProdOfLE' h_le Quotient.out Quotient.out_eq'

Nonconstructive equivalence between $\alpha/s$ and $(\alpha/t) \times (t/s)$

Informal description

Given a group $\alpha$ with subgroups $s \leq t$, there is a natural bijection between the quotient $\alpha ⧸ s$ and the product $(\alpha ⧸ t) \times (t ⧸ s)$. Here, $t ⧸ s$ denotes the quotient of $t$ by the subgroup $s$ (viewed as a subgroup of $t$ via `subgroupOf`). The bijection is constructed nonconstructively using the axiom of choice via `Quotient.out`, which selects representatives from each coset. This provides a decomposition of the larger quotient $\alpha ⧸ s$ in terms of the smaller quotient $\alpha ⧸ t$ and the relative quotient $t ⧸ s$.

Subgroup.quotientSubgroupOfEmbeddingOfLE definition

(H : Subgroup α) (h : s ≤ t) : s ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t

Full source

/-- If `s ≤ t`, then there is an embedding `s ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t`. -/
@[to_additive "If `s ≤ t`, then there is an embedding
 `s ⧸ H.addSubgroupOf s ↪ t ⧸ H.addSubgroupOf t`."]
def quotientSubgroupOfEmbeddingOfLE (H : Subgroup α) (h : s ≤ t) :
    s ⧸ H.subgroupOf ss ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t where
  toFun :=
    Quotient.map' (inclusion h) fun a b => by
      simp_rw [leftRel_eq]
      exact id
  inj' :=
    Quotient.ind₂' <| by
      intro a b h
      simpa only [Quotient.map'_mk'', QuotientGroup.eq] using h

Embedding of quotient groups under subgroup inclusion

Informal description

Given a group $\alpha$ with subgroups $s \leq t$ and a subgroup $H$ of $\alpha$, there is an embedding from the quotient group $s / (H \cap s)$ to the quotient group $t / (H \cap t)$. This embedding is induced by the inclusion map from $s$ to $t$.

Subgroup.quotientSubgroupOfEmbeddingOfLE_apply_mk theorem

 (H : Subgroup α) (h : s ≤ t) (g : s) :
  quotientSubgroupOfEmbeddingOfLE H h (QuotientGroup.mk g) = QuotientGroup.mk (inclusion h g)

Full source

@[to_additive (attr := simp)]
theorem quotientSubgroupOfEmbeddingOfLE_apply_mk (H : Subgroup α) (h : s ≤ t) (g : s) :
    quotientSubgroupOfEmbeddingOfLE H h (QuotientGroup.mk g) = QuotientGroup.mk (inclusion h g) :=
  rfl

Embedding of Quotient Groups Preserves Cosets under Inclusion

Informal description

Let $G$ be a group with subgroups $s \leq t$ and $H \leq G$. For any element $g \in s$, the image of the coset $g \cdot (H \cap s)$ under the embedding $$s / (H \cap s) \hookrightarrow t / (H \cap t)$$ is equal to the coset $\iota(g) \cdot (H \cap t)$, where $\iota: s \hookrightarrow t$ is the inclusion map.

Subgroup.quotientSubgroupOfMapOfLE definition

(H : Subgroup α) (h : s ≤ t) : H ⧸ s.subgroupOf H → H ⧸ t.subgroupOf H

Full source

/-- If `s ≤ t`, then there is a map `H ⧸ s.subgroupOf H → H ⧸ t.subgroupOf H`. -/
@[to_additive "If `s ≤ t`, then there is a map `H ⧸ s.addSubgroupOf H → H ⧸ t.addSubgroupOf H`."]
def quotientSubgroupOfMapOfLE (H : Subgroup α) (h : s ≤ t) :
    H ⧸ s.subgroupOf H → H ⧸ t.subgroupOf H :=
  Quotient.map' id fun a b => by
    simp_rw [leftRel_eq]
    apply h

Quotient group map under subgroup inclusion

Informal description

Given a group $\alpha$ with subgroups $s \leq t$ and a subgroup $H$ of $\alpha$, there is a map from the quotient group $H / (s \cap H)$ to the quotient group $H / (t \cap H)$ induced by the inclusion $s \leq t$. This map sends each coset representative to itself, respecting the equivalence relation defined by the subgroup containment.

Subgroup.quotientSubgroupOfMapOfLE_apply_mk theorem

(H : Subgroup α) (h : s ≤ t) (g : H) : quotientSubgroupOfMapOfLE H h (QuotientGroup.mk g) = QuotientGroup.mk g

Full source

@[to_additive (attr := simp)]
theorem quotientSubgroupOfMapOfLE_apply_mk (H : Subgroup α) (h : s ≤ t) (g : H) :
    quotientSubgroupOfMapOfLE H h (QuotientGroup.mk g) = QuotientGroup.mk g :=
  rfl

Quotient Map Preserves Cosets under Subgroup Inclusion

Informal description

Let $G$ be a group with subgroups $s \leq t$ and $H \leq G$. For any element $g \in H$, the image of the coset $g \cdot (H \cap s)$ under the quotient map $$H / (H \cap s) \to H / (H \cap t)$$ induced by the inclusion $s \leq t$ is equal to the coset $g \cdot (H \cap t)$.

Subgroup.quotientMapOfLE definition

(h : s ≤ t) : α ⧸ s → α ⧸ t

Full source

/-- If `s ≤ t`, then there is a map `α ⧸ s → α ⧸ t`. -/
@[to_additive "If `s ≤ t`, then there is a map `α ⧸ s → α ⧸ t`."]
def quotientMapOfLE (h : s ≤ t) : α ⧸ s → α ⧸ t :=
  Quotient.map' id fun a b => by
    simp_rw [leftRel_eq]
    apply h

Quotient group map under subgroup inclusion

Informal description

Given a group $\alpha$ and subgroups $s \leq t$ of $\alpha$, there is a natural map from the quotient group $\alpha / s$ to the quotient group $\alpha / t$ that sends each coset representative to itself. This map is well-defined because the equivalence relation defined by $s$ is finer than that defined by $t$.

Subgroup.quotientMapOfLE_apply_mk theorem

(h : s ≤ t) (g : α) : quotientMapOfLE h (QuotientGroup.mk g) = QuotientGroup.mk g

Full source

@[to_additive (attr := simp)]
theorem quotientMapOfLE_apply_mk (h : s ≤ t) (g : α) :
    quotientMapOfLE h (QuotientGroup.mk g) = QuotientGroup.mk g :=
  rfl

Quotient Map Under Subgroup Inclusion Preserves Cosets

Informal description

Let $G$ be a group with subgroups $s \leq t$, and let $g \in G$. The quotient map $\text{quotientMapOfLE}\ h$ induced by the inclusion $h : s \leq t$ satisfies \[ \text{quotientMapOfLE}\ h\ (\text{QuotientGroup.mk}\ g) = \text{QuotientGroup.mk}\ g, \] where $\text{QuotientGroup.mk}\ g$ denotes the canonical projection of $g$ onto the quotient group $G ⧸ s$ (or $G ⧸ t$).

Subgroup.quotientiInfSubgroupOfEmbedding definition

 {ι : Type*} (f : ι → Subgroup α) (H : Subgroup α) : H ⧸ (⨅ i, f i).subgroupOf H ↪ ∀ i, H ⧸ (f i).subgroupOf H

Full source

/-- The natural embedding `H ⧸ (⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H`. -/
@[to_additive (attr := simps) "The natural embedding
 `H ⧸ (⨅ i, f i).addSubgroupOf H) ↪ Π i, H ⧸ (f i).addSubgroupOf H`."]
def quotientiInfSubgroupOfEmbedding {ι : Type*} (f : ι → Subgroup α) (H : Subgroup α) :
    H ⧸ (⨅ i, f i).subgroupOf HH ⧸ (⨅ i, f i).subgroupOf H ↪ ∀ i, H ⧸ (f i).subgroupOf H where
  toFun q i := quotientSubgroupOfMapOfLE H (iInf_le f i) q
  inj' :=
    Quotient.ind₂' <| by
      simp_rw [funext_iff, quotientSubgroupOfMapOfLE_apply_mk, QuotientGroup.eq, mem_subgroupOf,
        mem_iInf, imp_self, forall_const]

Embedding of quotient by intersection of subgroups into product of quotients

Informal description

For a group $\alpha$, a family of subgroups $f : \iota \to \text{Subgroup } \alpha$, and a subgroup $H$ of $\alpha$, there is a natural embedding from the quotient group $H / (\bigcap_i f_i) \cap H$ into the product of quotient groups $\prod_i H / (f_i \cap H)$. The embedding maps each coset representative to its equivalence class in each component quotient.

Subgroup.quotientiInfSubgroupOfEmbedding_apply_mk theorem

 {ι : Type*} (f : ι → Subgroup α) (H : Subgroup α) (g : H) (i : ι) :
  quotientiInfSubgroupOfEmbedding f H (QuotientGroup.mk g) i = QuotientGroup.mk g

Full source

@[to_additive (attr := simp)]
theorem quotientiInfSubgroupOfEmbedding_apply_mk {ι : Type*} (f : ι → Subgroup α) (H : Subgroup α)
    (g : H) (i : ι) :
    quotientiInfSubgroupOfEmbedding f H (QuotientGroup.mk g) i = QuotientGroup.mk g :=
  rfl

Component-wise Coset Equality in Quotient Embedding

Informal description

Let $\alpha$ be a group, $f : \iota \to \text{Subgroup } \alpha$ a family of subgroups, and $H$ a subgroup of $\alpha$. For any element $g \in H$ and any index $i \in \iota$, the image of the coset $[g]$ under the embedding \[ H ⧸ (\bigcap_i f_i) \cap H \hookrightarrow \prod_i H ⧸ (f_i \cap H) \] at index $i$ is equal to the coset $[g]$ in the quotient $H ⧸ (f_i \cap H)$. In other words, the $i$-th component of the embedded coset is the coset of $g$ modulo $f_i \cap H$.

Subgroup.quotientiInfEmbedding definition

{ι : Type*} (f : ι → Subgroup α) : (α ⧸ ⨅ i, f i) ↪ ∀ i, α ⧸ f i

Full source

/-- The natural embedding `α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i`. -/
@[to_additive (attr := simps) "The natural embedding `α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i`."]
def quotientiInfEmbedding {ι : Type*} (f : ι → Subgroup α) : (α ⧸ ⨅ i, f i) ↪ ∀ i, α ⧸ f i where
  toFun q i := quotientMapOfLE (iInf_le f i) q
  inj' :=
    Quotient.ind₂' <| by
      simp_rw [funext_iff, quotientMapOfLE_apply_mk, QuotientGroup.eq, mem_iInf, imp_self,
        forall_const]

Embedding of quotient by intersection into product of quotients

Informal description

For a group $\alpha$ and a family of subgroups $f : \iota \to \text{Subgroup } \alpha$, the embedding $\alpha ⧸ (\bigcap_i f_i) \hookrightarrow \prod_i (\alpha ⧸ f_i)$ maps each coset $[g]$ in the quotient by the intersection of subgroups to the family of cosets $([g])_i$ in each individual quotient $\alpha ⧸ f_i$. This embedding is injective, meaning that two cosets are equal in $\alpha ⧸ (\bigcap_i f_i)$ if and only if their images are equal in each $\alpha ⧸ f_i$.

Subgroup.quotientiInfEmbedding_apply_mk theorem

 {ι : Type*} (f : ι → Subgroup α) (g : α) (i : ι) : quotientiInfEmbedding f (QuotientGroup.mk g) i = QuotientGroup.mk g

Full source

@[to_additive (attr := simp)]
theorem quotientiInfEmbedding_apply_mk {ι : Type*} (f : ι → Subgroup α) (g : α) (i : ι) :
    quotientiInfEmbedding f (QuotientGroup.mk g) i = QuotientGroup.mk g :=
  rfl

Component-wise Coset Equality in Quotient Embedding: $[g]_i = [g]$ for all $i$

Informal description

For a group $\alpha$, a family of subgroups $f : \iota \to \text{Subgroup } \alpha$, an element $g \in \alpha$, and an index $i \in \iota$, the $i$-th component of the image of the coset $[g]$ under the embedding \[ \alpha ⧸ (\bigcap_i f_i) \hookrightarrow \prod_i \alpha ⧸ f_i \] is equal to the coset $[g]$ in the quotient $\alpha ⧸ f_i$. In other words, the embedding maps the coset of $g$ modulo the intersection of all subgroups $f_i$ to the family of cosets where each component is the coset of $g$ modulo the corresponding subgroup $f_i$.

MonoidHom.fiberEquivKer definition

(f : α →* H) (a : α) : f ⁻¹' {f a} ≃ f.ker

Full source

/-- An equivalence between any non-empty fiber of a `MonoidHom` and its kernel. -/
@[to_additive "An equivalence between any non-empty fiber of an `AddMonoidHom` and its kernel."]
def fiberEquivKer (f : α →* H) (a : α) : f ⁻¹' {f a}f ⁻¹' {f a} ≃ f.ker :=
  .trans
    (Equiv.setCongr <| Set.ext fun _ => by
      rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm])
    (Subgroup.leftCosetEquivSubgroup a)

Bijection between fiber and kernel of a group homomorphism

Informal description

For any group homomorphism $ f : \alpha \to H $ and any element $ a \in \alpha $, there is a natural bijection between the fiber $ f^{-1}(\{f(a)\}) $ (the set of elements in $ \alpha $ that map to $ f(a) $) and the kernel $ \ker f $ of $ f $. The bijection is given by: - The forward map sends $ g \in f^{-1}(\{f(a)\}) $ to $ a^{-1} \cdot g \in \ker f $ - The backward map sends $ h \in \ker f $ to $ a \cdot h \in f^{-1}(\{f(a)\}) $

MonoidHom.fiberEquivKer_apply theorem

(f : α →* H) (a : α) (g : f ⁻¹' {f a}) : f.fiberEquivKer a g = a⁻¹ * g

Full source

@[to_additive (attr := simp)]
lemma fiberEquivKer_apply (f : α →* H) (a : α) (g : f ⁻¹' {f a}) : f.fiberEquivKer a g = a⁻¹ * g :=
  rfl

Fiber-to-Kernel Bijection Formula: $ g \mapsto a^{-1} \cdot g $

Informal description

For any group homomorphism $ f \colon \alpha \to H $, any element $ a \in \alpha $, and any element $ g $ in the fiber $ f^{-1}(\{f(a)\}) $, the bijection between the fiber and the kernel of $ f $ maps $ g $ to $ a^{-1} \cdot g $.

MonoidHom.fiberEquivKer_symm_apply theorem

(f : α →* H) (a : α) (g : f.ker) : (f.fiberEquivKer a).symm g = a * g

Full source

@[to_additive (attr := simp)]
lemma fiberEquivKer_symm_apply (f : α →* H) (a : α) (g : f.ker) :
    (f.fiberEquivKer a).symm g = a * g :=
  rfl

Inverse of Fiber-Kernel Bijection for Group Homomorphism

Informal description

For any group homomorphism $f \colon \alpha \to H$, any element $a \in \alpha$, and any element $g$ in the kernel of $f$, the inverse of the bijection between the fiber $f^{-1}(\{f(a)\})$ and $\ker f$ maps $g$ to $a \cdot g$.

MonoidHom.fiberEquivKerOfSurjective definition

{f : α →* H} (hf : Function.Surjective f) (h : H) : f ⁻¹' { h } ≃ f.ker

Full source

/-- An equivalence between any fiber of a surjective `MonoidHom` and its kernel. -/
@[to_additive "An equivalence between any fiber of a surjective `AddMonoidHom` and its kernel."]
noncomputable def fiberEquivKerOfSurjective {f : α →* H} (hf : Function.Surjective f) (h : H) :
    f ⁻¹' {h}f ⁻¹' {h} ≃ f.ker :=
  (hf h).choose_spec ▸ f.fiberEquivKer (hf h).choose

Bijection between fiber and kernel of a surjective group homomorphism

Informal description

For any surjective group homomorphism $ f \colon \alpha \to H $ and any element $ h \in H $, there is a natural bijection between the fiber $ f^{-1}(\{h\}) $ (the set of elements in $ \alpha $ that map to $ h $) and the kernel $ \ker f $ of $ f $. The bijection is constructed by first choosing a preimage $ a \in \alpha $ of $ h $ (which exists because $ f $ is surjective) and then using the bijection $ f.fiberEquivKer a $.

MonoidHom.fiberEquiv definition

(f : α →* H) (a b : α) : f ⁻¹' {f a} ≃ f ⁻¹' {f b}

Full source

/-- An equivalence between any two non-empty fibers of a `MonoidHom`. -/
@[to_additive "An equivalence between any two non-empty fibers of an `AddMonoidHom`."]
def fiberEquiv (f : α →* H) (a b : α) : f ⁻¹' {f a}f ⁻¹' {f a} ≃ f ⁻¹' {f b} :=
  (f.fiberEquivKer a).trans (f.fiberEquivKer b).symm

Bijection between fibers of a group homomorphism

Informal description

For any group homomorphism $ f : \alpha \to H $ and any elements $ a, b \in \alpha $, there is a natural bijection between the fibers $ f^{-1}(\{f(a)\}) $ and $ f^{-1}(\{f(b)\}) $. The bijection is constructed by composing the bijection from $ f^{-1}(\{f(a)\}) $ to the kernel $ \ker f $ with the inverse of the bijection from $ f^{-1}(\{f(b)\}) $ to $ \ker f $.

MonoidHom.fiberEquiv_apply theorem

(f : α →* H) (a b : α) (g : f ⁻¹' {f a}) : f.fiberEquiv a b g = b * (a⁻¹ * g)

Full source

@[to_additive (attr := simp)]
lemma fiberEquiv_apply (f : α →* H) (a b : α) (g : f ⁻¹' {f a}) :
    f.fiberEquiv a b g = b * (a⁻¹ * g) :=
  rfl

Fiber Equivalence Formula for Group Homomorphisms

Informal description

For any group homomorphism $f \colon \alpha \to H$ and elements $a, b \in \alpha$, the fiber equivalence map $\text{fiberEquiv}$ satisfies $\text{fiberEquiv}\, f\, a\, b\, g = b \cdot (a^{-1} \cdot g)$ for any $g$ in the fiber $f^{-1}(\{f(a)\})$.

MonoidHom.fiberEquiv_symm_apply theorem

(f : α →* H) (a b : α) (g : f ⁻¹' {f b}) : (f.fiberEquiv a b).symm g = a * (b⁻¹ * g)

Full source

@[to_additive (attr := simp)]
lemma fiberEquiv_symm_apply (f : α →* H) (a b : α) (g : f ⁻¹' {f b}) :
    (f.fiberEquiv a b).symm g = a * (b⁻¹ * g) :=
  rfl

Inverse Fiber Bijection Formula for Group Homomorphisms

Informal description

For any group homomorphism $f \colon \alpha \to H$ and elements $a, b \in \alpha$, the inverse of the fiber bijection $\text{fiberEquiv}$ satisfies $(f.\text{fiberEquiv}\, a\, b)^{-1}(g) = a \cdot (b^{-1} \cdot g)$ for any $g$ in the fiber $f^{-1}(\{f(b)\})$.

MonoidHom.fiberEquivOfSurjective definition

{f : α →* H} (hf : Function.Surjective f) (h h' : H) : f ⁻¹' { h } ≃ f ⁻¹' { h' }

Full source

/-- An equivalence between any two fibers of a surjective `MonoidHom`. -/
@[to_additive "An equivalence between any two fibers of a surjective `AddMonoidHom`."]
noncomputable def fiberEquivOfSurjective {f : α →* H} (hf : Function.Surjective f) (h h' : H) :
    f ⁻¹' {h}f ⁻¹' {h} ≃ f ⁻¹' {h'} :=
  (fiberEquivKerOfSurjective hf h).trans (fiberEquivKerOfSurjective hf h').symm

Bijection between fibers of a surjective group homomorphism

Informal description

For any surjective group homomorphism $ f \colon \alpha \to H $ and any two elements $ h, h' \in H $, there is a natural bijection between the fibers $ f^{-1}(\{h\}) $ and $ f^{-1}(\{h'\}) $. This bijection is constructed by composing the bijection from $ f^{-1}(\{h\}) $ to the kernel $ \ker f $ with the inverse of the bijection from $ f^{-1}(\{h'\}) $ to $ \ker f $.

QuotientGroup.preimageMkEquivSubgroupProdSet definition

(s : Subgroup α) (t : Set (α ⧸ s)) : QuotientGroup.mk ⁻¹' t ≃ s × t

Full source

/-- 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`. -/
@[to_additive preimageMkEquivAddSubgroupProdSet
"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`."]
noncomputable def preimageMkEquivSubgroupProdSet (s : Subgroup α) (t : Set (α ⧸ s)) :
    QuotientGroup.mkQuotientGroup.mk ⁻¹' tQuotientGroup.mk ⁻¹' t ≃ s × t where
  toFun a :=
    ⟨⟨((Quotient.out (QuotientGroup.mk a)) : α)⁻¹ * a,
        leftRel_apply.mp (@Quotient.exact' _ (leftRel s) _ _ <| Quotient.out_eq' _)⟩,
      ⟨QuotientGroup.mk a, a.2⟩⟩
  invFun a :=
    ⟨Quotient.out a.2.1 * a.1.1,
      show QuotientGroup.mk _ ∈ t by
        rw [mk_mul_of_mem _ a.1.2, out_eq']
        exact a.2.2⟩
  left_inv := fun ⟨a, _⟩ => Subtype.eq <| show _ * _ = a by simp
  right_inv := fun ⟨⟨a, ha⟩, ⟨x, hx⟩⟩ => by ext <;> simp [ha]

Bijection between preimage of quotient subset and subgroup-product

Informal description

Given a subgroup $s$ of a group $\alpha$ and a subset $t$ of the quotient $\alpha ⧸ s$, there exists a bijection between the preimage of $t$ under the canonical projection $\text{mk} : \alpha \to \alpha ⧸ s$ and the product $s \times t$. The bijection is constructed as follows: - The forward map sends an element $a$ in the preimage to the pair $\langle ((\text{out} (\text{mk} a))^{-1} \cdot a, \text{mk} a \rangle$, where $\text{out}$ is a choice function selecting a representative from each coset. - The inverse map sends a pair $\langle h, x \rangle \in s \times t$ to $\text{out} x \cdot h$. Here, $\text{mk} a$ denotes the left coset $a \cdot s$ in the quotient $\alpha ⧸ s$.

QuotientGroup.univ_eq_iUnion_smul theorem

(H : Subgroup α) : (Set.univ (α := α)) = ⋃ x : α ⧸ H, x.out • (H : Set _)

Full source

/-- A group is made up of a disjoint union of cosets of a subgroup. -/
@[to_additive "An additive group is made up of a disjoint union of cosets of an additive
subgroup."]
lemma univ_eq_iUnion_smul (H : Subgroup α) :
    (Set.univ (α := α)) = ⋃ x : α ⧸ H, x.out • (H : Set _) := by
  simp_rw [univ_eq_iUnion_orbit H.op, orbit_eq_out_smul]
  rfl

Decomposition of Group into Left Cosets of Subgroup

Informal description

For any subgroup $H$ of a group $\alpha$, the universal set of $\alpha$ is equal to the union of all left cosets of $H$ in $\alpha$. That is, $\alpha = \bigcup_{x \in \alpha/H} x.\text{out} \cdot H$, where $x.\text{out}$ is a chosen representative of the coset $x$ in the quotient group $\alpha/H$.

QuotientGroup.quotientEquivSelf definition

: α ⧸ (⊥ : Subgroup α) ≃ α

Full source

/-- `α ⧸ ⊥` is in bijection with `α`. See `QuotientGroup.quotientBot` for a multiplicative
version. -/
@[to_additive "`α ⧸ ⊥` is in bijection with `α`. See `QuotientAddGroup.quotientBot` for an additive
version."]
def quotientEquivSelf : α ⧸ (⊥ : Subgroup α)α ⧸ (⊥ : Subgroup α) ≃ α where
  toFun := Quotient.lift id <| fun x y (h : leftRel ⊥ x y) ↦
    eq_of_inv_mul_eq_one <| by rwa [leftRel_apply, Subgroup.mem_bot] at h
  invFun := QuotientGroup.mk
  left_inv x := by induction x using Quotient.inductionOn; simp
  right_inv x := by simp

Bijection between group and quotient by trivial subgroup

Informal description

The quotient group $\alpha ⧸ \{\text{id}\}$ is in bijection with $\alpha$ itself. The bijection is given by the canonical projection map from $\alpha$ to the quotient, and its inverse lifts elements of the quotient back to $\alpha$ by choosing representatives.

Mathlib.GroupTheory.Coset.Basic

Main definitions

Notation

TODO