Mathlib.GroupTheory.QuotientGroup.Basic

QuotientGroup.sound theorem

(U : Set (G ⧸ N)) (g : N.op) : g • (mk' N) ⁻¹' U = (mk' N) ⁻¹' U

Full source

@[to_additive]
theorem sound (U : Set (G ⧸ N)) (g : N.op) :
    g • (mk' N) ⁻¹' U = (mk' N) ⁻¹' U := by
  ext x
  simp only [Set.mem_preimage, Set.mem_smul_set_iff_inv_smul_mem]
  congr! 1
  exact Quotient.sound ⟨g⁻¹, rfl⟩

Invariance of Preimage under Normal Subgroup Action

Informal description

For any subset $U$ of the quotient group $G/N$ and any element $g$ of the normal subgroup $N$ (viewed as an element of the opposite group $N^{\text{op}}$), the action of $g$ on the preimage of $U$ under the canonical projection $\text{mk}'_N : G \to G/N$ is equal to the preimage itself. That is, $g \cdot (\text{mk}'_N)^{-1}(U) = (\text{mk}'_N)^{-1}(U)$.

QuotientGroup.mk_prod theorem

 {G ι : Type*} [CommGroup G] (N : Subgroup G) (s : Finset ι) {f : ι → G} :
  ((Finset.prod s f : G) : G ⧸ N) = Finset.prod s (fun i => (f i : G ⧸ N))

Full source

@[to_additive (attr := simp)]
theorem mk_prod {G ι : Type*} [CommGroup G] (N : Subgroup G) (s : Finset ι) {f : ι → G} :
    ((Finset.prod s f : G) : G ⧸ N) = Finset.prod s (fun i => (f i : G ⧸ N)) :=
  map_prod (QuotientGroup.mk' N) _ _

Canonical projection preserves finite products in quotient groups

Informal description

Let $G$ be a commutative group, $N$ a normal subgroup of $G$, and $f : \iota \to G$ a family of elements indexed by a finite set $s \subset \iota$. Then the canonical projection of the product of $f$ over $s$ equals the product of the canonical projections of each $f(i)$: \[ \left[\prod_{i \in s} f(i)\right] = \prod_{i \in s} [f(i)], \] where $[x]$ denotes the equivalence class of $x \in G$ in the quotient group $G/N$.

QuotientGroup.strictMono_comap_prod_map theorem

: StrictMono fun H : Subgroup G ↦ (H.comap N.subtype, H.map (mk' N))

Full source

@[to_additive QuotientAddGroup.strictMono_comap_prod_map]
theorem strictMono_comap_prod_map :
    StrictMono fun H : Subgroup G ↦ (H.comap N.subtype, H.map (mk' N)) :=
  strictMono_comap_prod_image N

Strict Monotonicity of Subgroup Pair Construction via Intersection and Quotient

Informal description

The function that maps a subgroup $H$ of $G$ to the pair $(H \cap N, H/N)$, where $N$ is a normal subgroup of $G$, is strictly monotone with respect to the subgroup inclusion order.

QuotientGroup.kerLift definition

: G ⧸ ker φ →* H

Full source

/-- The induced map from the quotient by the kernel to the codomain. -/
@[to_additive "The induced map from the quotient by the kernel to the codomain."]
def kerLift : G ⧸ ker φG ⧸ ker φ →* H :=
  lift _ φ fun _g => mem_ker.mp

Induced homomorphism from quotient by kernel

Informal description

The induced group homomorphism from the quotient group $ G / \ker \varphi $ to the codomain $ H $, defined by mapping the equivalence class $[g]$ of an element $ g \in G $ to $ \varphi(g) $. This map is well-defined since $ \ker \varphi $ is a normal subgroup of $ G $.

QuotientGroup.kerLift_mk theorem

(g : G) : (kerLift φ) g = φ g

Full source

@[to_additive (attr := simp)]
theorem kerLift_mk (g : G) : (kerLift φ) g = φ g :=
  lift_mk _ _ _

Evaluation of Kernel Lift on Cosets: $(\kerLift \varphi)([g]) = \varphi(g)$

Informal description

For any group homomorphism $\varphi \colon G \to H$ and any element $g \in G$, the induced homomorphism $\kerLift \varphi$ evaluated at the equivalence class $[g] \in G/\ker \varphi$ equals $\varphi(g)$, i.e., $(\kerLift \varphi)([g]) = \varphi(g)$.

QuotientGroup.kerLift_mk' theorem

(g : G) : (kerLift φ) (mk g) = φ g

Full source

@[to_additive (attr := simp)]
theorem kerLift_mk' (g : G) : (kerLift φ) (mk g) = φ g :=
  lift_mk' _ _ _

Evaluation of Induced Homomorphism on Cosets: $\kerLift(\varphi)([g]) = \varphi(g)$

Informal description

For any group homomorphism $\varphi \colon G \to H$ and any element $g \in G$, the induced homomorphism $\kerLift(\varphi)$ evaluated at the equivalence class $[g] \in G/\ker \varphi$ equals $\varphi(g)$. That is, $\kerLift(\varphi)([g]) = \varphi(g)$.

QuotientGroup.kerLift_injective theorem

: Injective (kerLift φ)

Full source

@[to_additive]
theorem kerLift_injective : Injective (kerLift φ) := fun a b =>
  Quotient.inductionOn₂' a b fun a b (h : φ a = φ b) =>
    Quotient.sound' <| by rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_cancel]

Injectivity of the Induced Homomorphism from Quotient by Kernel

Informal description

The induced group homomorphism $\kerLift \varphi \colon G / \ker \varphi \to H$ is injective. That is, for any $[g_1], [g_2] \in G / \ker \varphi$, if $\kerLift \varphi([g_1]) = \kerLift \varphi([g_2])$, then $[g_1] = [g_2]$.

QuotientGroup.rangeKerLift definition

: G ⧸ ker φ →* φ.range

Full source

/-- The induced map from the quotient by the kernel to the range. -/
@[to_additive "The induced map from the quotient by the kernel to the range."]
def rangeKerLift : G ⧸ ker φG ⧸ ker φ →* φ.range :=
  lift _ φ.rangeRestrict fun g hg => mem_ker.mp <| by rwa [ker_rangeRestrict]

Induced homomorphism from quotient by kernel to range

Informal description

The induced group homomorphism from the quotient group $ G / \ker \varphi $ to the range of $\varphi$, defined by mapping the equivalence class $[g]$ to $\varphi(g)$ for each $g \in G$.

QuotientGroup.rangeKerLift_injective theorem

: Injective (rangeKerLift φ)

Full source

@[to_additive]
theorem rangeKerLift_injective : Injective (rangeKerLift φ) := fun a b =>
  Quotient.inductionOn₂' a b fun a b (h : φ.rangeRestrict a = φ.rangeRestrict b) =>
    Quotient.sound' <| by
      rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
        φ.rangeRestrict.map_inv, inv_mul_cancel]

Injectivity of the Induced Homomorphism from Quotient by Kernel to Range

Informal description

The induced group homomorphism $\operatorname{rangeKerLift} \varphi \colon G / \ker \varphi \to \operatorname{range} \varphi$ is injective. That is, for any $[g_1], [g_2] \in G / \ker \varphi$, if $\operatorname{rangeKerLift} \varphi([g_1]) = \operatorname{rangeKerLift} \varphi([g_2])$, then $[g_1] = [g_2]$.

QuotientGroup.rangeKerLift_surjective theorem

: Surjective (rangeKerLift φ)

Full source

@[to_additive]
theorem rangeKerLift_surjective : Surjective (rangeKerLift φ) := by
  rintro ⟨_, g, rfl⟩
  use mk g
  rfl

Surjectivity of the Induced Homomorphism from Quotient by Kernel to Range

Informal description

The induced group homomorphism from the quotient group $G / \ker \varphi$ to the range of $\varphi$ is surjective. That is, for every element $h$ in the range of $\varphi$, there exists an equivalence class $[g] \in G / \ker \varphi$ such that the homomorphism maps $[g]$ to $h$.

QuotientGroup.quotientKerEquivRange definition

: G ⧸ ker φ ≃* range φ

Full source

/-- **Noether's first isomorphism theorem** (a definition): the canonical isomorphism between
`G/(ker φ)` to `range φ`. -/
@[to_additive "The first isomorphism theorem (a definition): the canonical isomorphism between
`G/(ker φ)` to `range φ`."]
noncomputable def quotientKerEquivRange : G ⧸ ker φG ⧸ ker φ ≃* range φ :=
  MulEquiv.ofBijective (rangeKerLift φ) ⟨rangeKerLift_injective φ, rangeKerLift_surjective φ⟩

First Isomorphism Theorem for Groups

Informal description

The canonical isomorphism between the quotient group $ G / \ker \varphi $ and the range of the group homomorphism $ \varphi $, given by mapping the equivalence class $[g]$ to $\varphi(g)$ for each $g \in G$.

QuotientGroup.quotientKerEquivOfRightInverse definition

(ψ : H → G) (hφ : RightInverse ψ φ) : G ⧸ ker φ ≃* H

Full source

/-- The canonical isomorphism `G/(ker φ) ≃* H` induced by a homomorphism `φ : G →* H`
with a right inverse `ψ : H → G`. -/
@[to_additive (attr := simps) "The canonical isomorphism `G/(ker φ) ≃+ H` induced by a homomorphism
`φ : G →+ H` with a right inverse `ψ : H → G`."]
def quotientKerEquivOfRightInverse (ψ : H → G) (hφ : RightInverse ψ φ) : G ⧸ ker φG ⧸ ker φ ≃* H :=
  { kerLift φ with
    toFun := kerLift φ
    invFun := mkmk ∘ ψ
    left_inv := fun x => kerLift_injective φ (by rw [Function.comp_apply, kerLift_mk', hφ])
    right_inv := hφ }

First Isomorphism Theorem (with right inverse)

Informal description

Given a group homomorphism $\varphi: G \to H$ with a right inverse $\psi: H \to G$ (i.e., $\varphi \circ \psi = \text{id}_H$), the canonical isomorphism $G/(\ker \varphi) \cong H$ is defined by mapping the equivalence class $[g]$ of an element $g \in G$ to $\varphi(g)$, with inverse given by composing the quotient map with $\psi$.

QuotientGroup.quotientBot definition

: G ⧸ (⊥ : Subgroup G) ≃* G

Full source

/-- The canonical isomorphism `G/⊥ ≃* G`. -/
@[to_additive (attr := simps!) "The canonical isomorphism `G/⊥ ≃+ G`."]
def quotientBot : G ⧸ (⊥ : Subgroup G)G ⧸ (⊥ : Subgroup G) ≃* G :=
  quotientKerEquivOfRightInverse (MonoidHom.id G) id fun _x => rfl

Isomorphism between $G/\{\text{id}_G\}$ and $G$

Informal description

The canonical isomorphism between the quotient group $ G / \{\text{id}_G\} $ and $ G $, where $\{\text{id}_G\}$ is the trivial subgroup of $G$. This isomorphism maps each equivalence class $[g]$ to $g$ itself.

QuotientGroup.quotientKerEquivOfSurjective definition

(hφ : Surjective φ) : G ⧸ ker φ ≃* H

Full source

/-- The canonical isomorphism `G/(ker φ) ≃* H` induced by a surjection `φ : G →* H`.

For a `computable` version, see `QuotientGroup.quotientKerEquivOfRightInverse`.
-/
@[to_additive "The canonical isomorphism `G/(ker φ) ≃+ H` induced by a surjection `φ : G →+ H`.
For a `computable` version, see `QuotientAddGroup.quotientKerEquivOfRightInverse`."]
noncomputable def quotientKerEquivOfSurjective (hφ : Surjective φ) : G ⧸ ker φG ⧸ ker φ ≃* H :=
  quotientKerEquivOfRightInverse φ _ hφ.hasRightInverse.choose_spec

First Isomorphism Theorem (surjective case)

Informal description

Given a surjective group homomorphism $\varphi: G \to H$, the canonical isomorphism $G/(\ker \varphi) \cong H$ is defined by mapping the equivalence class $[g]$ of an element $g \in G$ to $\varphi(g)$.

QuotientGroup.quotientMulEquivOfEq definition

{M N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) : G ⧸ M ≃* G ⧸ N

Full source

/-- If two normal subgroups `M` and `N` of `G` are the same, their quotient groups are
isomorphic. -/
@[to_additive "If two normal subgroups `M` and `N` of `G` are the same, their quotient groups are
isomorphic."]
def quotientMulEquivOfEq {M N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) : G ⧸ MG ⧸ M ≃* G ⧸ N :=
  { Subgroup.quotientEquivOfEq h with
    map_mul' := fun q r => Quotient.inductionOn₂' q r fun _g _h => rfl }

Isomorphism of quotient groups by equal normal subgroups

Informal description

Given a group $G$ and two normal subgroups $M$ and $N$ of $G$ that are equal, the quotient groups $G/M$ and $G/N$ are isomorphic as multiplicative groups. The isomorphism is induced by the equality $M = N$ and preserves the group structure.

QuotientGroup.quotientMulEquivOfEq_mk theorem

 {M N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) (x : G) :
  QuotientGroup.quotientMulEquivOfEq h (QuotientGroup.mk x) = QuotientGroup.mk x

Full source

@[to_additive (attr := simp)]
theorem quotientMulEquivOfEq_mk {M N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) (x : G) :
    QuotientGroup.quotientMulEquivOfEq h (QuotientGroup.mk x) = QuotientGroup.mk x :=
  rfl

Image of Coset under Quotient Group Isomorphism Induced by Equal Normal Subgroups

Informal description

Let $G$ be a group with normal subgroups $M$ and $N$ such that $M = N$. For any element $x \in G$, the image of the coset $[x]_M$ under the isomorphism $G/M \cong G/N$ induced by $M = N$ is equal to the coset $[x]_N$.

QuotientGroup.quotientMapSubgroupOfOfLe definition

 {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal] [_hBN : (B'.subgroupOf B).Normal] (h' : A' ≤ B')
  (h : A ≤ B) : A ⧸ A'.subgroupOf A →* B ⧸ B'.subgroupOf B

Full source

/-- Let `A', A, B', B` be subgroups of `G`. If `A' ≤ B'` and `A ≤ B`,
then there is a map `A / (A' ⊓ A) →* B / (B' ⊓ B)` induced by the inclusions. -/
@[to_additive "Let `A', A, B', B` be subgroups of `G`. If `A' ≤ B'` and `A ≤ B`, then there is a map
`A / (A' ⊓ A) →+ B / (B' ⊓ B)` induced by the inclusions."]
def quotientMapSubgroupOfOfLe {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal]
    [_hBN : (B'.subgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) :
    A ⧸ A'.subgroupOf AA ⧸ A'.subgroupOf A →* B ⧸ B'.subgroupOf B :=
  map _ _ (Subgroup.inclusion h) <| Subgroup.comap_mono h'

Induced homomorphism between subgroup quotients

Informal description

Given subgroups $A', A, B', B$ of a group $G$ with $A' \trianglelefteq A$ and $B' \trianglelefteq B$, if $A' \leq B'$ and $A \leq B$, then there exists an induced group homomorphism from the quotient group $A/(A' \cap A)$ to $B/(B' \cap B)$ defined by the inclusion maps.

QuotientGroup.quotientMapSubgroupOfOfLe_mk theorem

 {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal] [_hBN : (B'.subgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B)
  (x : A) : quotientMapSubgroupOfOfLe h' h x = ↑(Subgroup.inclusion h x : B)

Full source

@[to_additive (attr := simp)]
theorem quotientMapSubgroupOfOfLe_mk {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal]
    [_hBN : (B'.subgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) (x : A) :
    quotientMapSubgroupOfOfLe h' h x = ↑(Subgroup.inclusion h x : B) :=
  rfl

Image of Coset under Induced Quotient Homomorphism for Nested Subgroups

Informal description

Let $G$ be a group with subgroups $A', A, B', B$ such that $A'$ is normal in $A$ and $B'$ is normal in $B$. If $A' \leq B'$ and $A \leq B$, then for any $x \in A$, the image of the coset $[x]_{A'}$ under the induced homomorphism $A/A' \to B/B'$ is equal to the coset $[x]_{B'}$, where $x$ is considered as an element of $B$ via the inclusion map.

QuotientGroup.equivQuotientSubgroupOfOfEq definition

 {A' A B' B : Subgroup G} [hAN : (A'.subgroupOf A).Normal] [hBN : (B'.subgroupOf B).Normal] (h' : A' = B') (h : A = B) :
  A ⧸ A'.subgroupOf A ≃* B ⧸ B'.subgroupOf B

Full source

/-- Let `A', A, B', B` be subgroups of `G`.
If `A' = B'` and `A = B`, then the quotients `A / (A' ⊓ A)` and `B / (B' ⊓ B)` are isomorphic.

Applying this equiv is nicer than rewriting along the equalities, since the type of
`(A'.subgroupOf A : Subgroup A)` depends on `A`.
-/
@[to_additive "Let `A', A, B', B` be subgroups of `G`. If `A' = B'` and `A = B`, then the quotients
`A / (A' ⊓ A)` and `B / (B' ⊓ B)` are isomorphic. Applying this equiv is nicer than rewriting along
the equalities, since the type of `(A'.addSubgroupOf A : AddSubgroup A)` depends on `A`. "]
def equivQuotientSubgroupOfOfEq {A' A B' B : Subgroup G} [hAN : (A'.subgroupOf A).Normal]
    [hBN : (B'.subgroupOf B).Normal] (h' : A' = B') (h : A = B) :
    A ⧸ A'.subgroupOf AA ⧸ A'.subgroupOf A ≃* B ⧸ B'.subgroupOf B :=
  (quotientMapSubgroupOfOfLe h'.le h.le).toMulEquiv (quotientMapSubgroupOfOfLe h'.ge h.ge)
    (by ext ⟨x, hx⟩; rfl)
    (by ext ⟨x, hx⟩; rfl)

Isomorphism of Quotient Groups by Equal Subgroups

Informal description

Given subgroups $A', A, B', B$ of a group $G$ with $A' \trianglelefteq A$ and $B' \trianglelefteq B$, if $A' = B'$ and $A = B$, then the quotient groups $A/(A' \cap A)$ and $B/(B' \cap B)$ are isomorphic via a canonical isomorphism. This isomorphism is constructed using the inclusion maps induced by the equalities $A' = B'$ and $A = B$.

QuotientGroup.homQuotientZPowOfHom definition

: A ⧸ (zpowGroupHom n : A →* A).range →* B ⧸ (zpowGroupHom n : B →* B).range

Full source

/-- The map of quotients by powers of an integer induced by a group homomorphism. -/
@[to_additive "The map of quotients by multiples of an integer induced by an additive group
homomorphism."]
def homQuotientZPowOfHom :
    A ⧸ (zpowGroupHom n : A →* A).rangeA ⧸ (zpowGroupHom n : A →* A).range →* B ⧸ (zpowGroupHom n : B →* B).range :=
  lift _ ((mk' _).comp f) fun g ⟨h, (hg : h ^ n = g)⟩ =>
    (eq_one_iff _).mpr ⟨f h, by
      simp only [← hg, map_zpow, zpowGroupHom_apply]⟩

Induced homomorphism on quotient groups by $n$-th powers

Informal description

Given a group homomorphism $f \colon A \to B$ and an integer $n$, the map $\text{homQuotientZPowOfHom}(f, n)$ is the induced group homomorphism between the quotient groups $A/(A^n)$ and $B/(B^n)$, where $A^n$ denotes the range of the $n$-th power map on $A$. The homomorphism is defined by sending the equivalence class $[a] \in A/(A^n)$ to $[f(a)] \in B/(B^n)$.

QuotientGroup.homQuotientZPowOfHom_id theorem

: homQuotientZPowOfHom (MonoidHom.id A) n = MonoidHom.id _

Full source

@[to_additive (attr := simp)]
theorem homQuotientZPowOfHom_id : homQuotientZPowOfHom (MonoidHom.id A) n = MonoidHom.id _ :=
  monoidHom_ext _ rfl

Identity Homomorphism Induces Identity on Quotient by $n$-th Powers

Informal description

The induced homomorphism $\text{homQuotientZPowOfHom}(\text{id}_A, n)$ on the quotient group $A/(A^n)$ is equal to the identity homomorphism on $A/(A^n)$.

QuotientGroup.homQuotientZPowOfHom_comp theorem

: homQuotientZPowOfHom (f.comp g) n = (homQuotientZPowOfHom f n).comp (homQuotientZPowOfHom g n)

Full source

@[to_additive (attr := simp)]
theorem homQuotientZPowOfHom_comp :
    homQuotientZPowOfHom (f.comp g) n =
      (homQuotientZPowOfHom f n).comp (homQuotientZPowOfHom g n) :=
  monoidHom_ext _ rfl

Composition of Induced Homomorphisms on Quotient Groups by $n$-th Powers

Informal description

For any group homomorphisms $f \colon B \to C$ and $g \colon A \to B$, and any integer $n$, the induced homomorphism $\text{homQuotientZPowOfHom}(f \circ g, n)$ on the quotient groups $A/(A^n) \to C/(C^n)$ is equal to the composition $\text{homQuotientZPowOfHom}(f, n) \circ \text{homQuotientZPowOfHom}(g, n)$.

QuotientGroup.homQuotientZPowOfHom_comp_of_rightInverse theorem

(i : Function.RightInverse g f) : (homQuotientZPowOfHom f n).comp (homQuotientZPowOfHom g n) = MonoidHom.id _

Full source

@[to_additive (attr := simp)]
theorem homQuotientZPowOfHom_comp_of_rightInverse (i : Function.RightInverse g f) :
    (homQuotientZPowOfHom f n).comp (homQuotientZPowOfHom g n) = MonoidHom.id _ :=
  monoidHom_ext _ <| MonoidHom.ext fun x => congrArg _ <| i x

Composition of Induced Quotient Homomorphisms with Right Inverse Yields Identity

Informal description

Let $f \colon A \to B$ and $g \colon B \to A$ be group homomorphisms such that $g$ is a right inverse of $f$ (i.e., $f \circ g = \text{id}_B$). Then for any integer $n$, the composition of the induced homomorphisms $\text{homQuotientZPowOfHom}(f, n) \circ \text{homQuotientZPowOfHom}(g, n)$ on the quotient groups $A/(A^n)$ and $B/(B^n)$ is equal to the identity homomorphism on $B/(B^n)$.

QuotientGroup.equivQuotientZPowOfEquiv definition

: A ⧸ (zpowGroupHom n : A →* A).range ≃* B ⧸ (zpowGroupHom n : B →* B).range

Full source

/-- The equivalence of quotients by powers of an integer induced by a group isomorphism. -/
@[to_additive "The equivalence of quotients by multiples of an integer induced by an additive group
isomorphism."]
def equivQuotientZPowOfEquiv :
    A ⧸ (zpowGroupHom n : A →* A).rangeA ⧸ (zpowGroupHom n : A →* A).range ≃* B ⧸ (zpowGroupHom n : B →* B).range :=
  MonoidHom.toMulEquiv _ _
    (homQuotientZPowOfHom_comp_of_rightInverse (e.symm : B →* A) (e : A →* B) n e.left_inv)
    (homQuotientZPowOfHom_comp_of_rightInverse (e : A →* B) (e.symm : B →* A) n e.right_inv)

Isomorphism of quotient groups by $n$-th powers induced by a group isomorphism

Informal description

Given a group isomorphism $e \colon A \to B$ and an integer $n$, the map $\text{equivQuotientZPowOfEquiv}(e, n)$ is a group isomorphism between the quotient groups $A/(A^n)$ and $B/(B^n)$, where $A^n$ denotes the range of the $n$-th power map on $A$. The isomorphism is defined by sending the equivalence class $[a] \in A/(A^n)$ to $[e(a)] \in B/(B^n)$.

QuotientGroup.equivQuotientZPowOfEquiv_refl theorem

: MulEquiv.refl (A ⧸ (zpowGroupHom n : A →* A).range) = equivQuotientZPowOfEquiv (MulEquiv.refl A) n

Full source

@[to_additive (attr := simp)]
theorem equivQuotientZPowOfEquiv_refl :
    MulEquiv.refl (A ⧸ (zpowGroupHom n : A →* A).range) =
      equivQuotientZPowOfEquiv (MulEquiv.refl A) n := by
  ext x
  rw [← Quotient.out_eq' x]
  rfl

Identity Isomorphism Induces Identity on Quotient by $n$-th Powers

Informal description

For any group $A$ and integer $n$, the identity isomorphism on the quotient group $A/(A^n)$ is equal to the isomorphism induced by the identity map on $A$, i.e., $\text{id}_{A/(A^n)} = \text{equivQuotientZPowOfEquiv}(\text{id}_A, n)$.

QuotientGroup.equivQuotientZPowOfEquiv_symm theorem

: (equivQuotientZPowOfEquiv e n).symm = equivQuotientZPowOfEquiv e.symm n

Full source

@[to_additive (attr := simp)]
theorem equivQuotientZPowOfEquiv_symm :
    (equivQuotientZPowOfEquiv e n).symm = equivQuotientZPowOfEquiv e.symm n :=
  rfl

Inverse of Quotient Group Isomorphism Induced by Group Isomorphism

Informal description

The inverse of the isomorphism $\text{equivQuotientZPowOfEquiv}(e, n)$ between the quotient groups $A/(A^n)$ and $B/(B^n)$ is equal to the isomorphism $\text{equivQuotientZPowOfEquiv}(e^{-1}, n)$ between $B/(B^n)$ and $A/(A^n)$, where $e^{-1}$ is the inverse of the group isomorphism $e \colon A \to B$.

QuotientGroup.equivQuotientZPowOfEquiv_trans theorem

: (equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) = equivQuotientZPowOfEquiv (e.trans d) n

Full source

@[to_additive (attr := simp)]
theorem equivQuotientZPowOfEquiv_trans :
    (equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) =
      equivQuotientZPowOfEquiv (e.trans d) n := by
  ext x
  rw [← Quotient.out_eq' x]
  rfl

Composition of Induced Quotient Group Isomorphisms by $n$-th Powers

Informal description

Given group isomorphisms $e \colon A \to B$ and $d \colon B \to C$ and an integer $n$, the composition of the induced isomorphisms on the quotient groups $A/(A^n) \to B/(B^n)$ and $B/(B^n) \to C/(C^n)$ is equal to the isomorphism induced by the composition $e \circ d \colon A \to C$ on the quotient groups $A/(A^n) \to C/(C^n)$. In other words, the following diagram commutes: $$ A/(A^n) \xrightarrow{\text{equivQuotientZPowOfEquiv}(e, n)} B/(B^n) \xrightarrow{\text{equivQuotientZPowOfEquiv}(d, n)} C/(C^n) $$ is equal to: $$ A/(A^n) \xrightarrow{\text{equivQuotientZPowOfEquiv}(e \circ d, n)} C/(C^n) $$

QuotientGroup.quotientInfEquivProdNormalizerQuotient definition

 (H N : Subgroup G) (hLE : H ≤ N.normalizer) :
  letI := Subgroup.normal_subgroupOf_of_le_normalizer hLE
  letI := Subgroup.normal_subgroupOf_sup_of_le_normalizer hLE
  H ⧸ N.subgroupOf H ≃* (H ⊔ N : Subgroup G) ⧸ N.subgroupOf (H ⊔ N)

Full source

/-- **Noether's second isomorphism theorem**: given a subgroup `N` of `G` and a
subgroup `H` of the normalizer of `N` in `G`,
defines an isomorphism between `H/(H ∩ N)` and `(HN)/N`. -/
@[to_additive "Noether's second isomorphism theorem: given a subgroup `N` of `G` and a
subgroup `H` of the normalizer of `N` in `G`,
defines an isomorphism between `H/(H ∩ N)` and `(H + N)/N`"]
noncomputable def quotientInfEquivProdNormalizerQuotient (H N : Subgroup G)
    (hLE : H ≤ N.normalizer) :
    letI := Subgroup.normal_subgroupOf_of_le_normalizer hLE
    letI := Subgroup.normal_subgroupOf_sup_of_le_normalizer hLE
    H ⧸ N.subgroupOf HH ⧸ N.subgroupOf H ≃* (H ⊔ N : Subgroup G) ⧸ N.subgroupOf (H ⊔ N) :=
  letI := Subgroup.normal_subgroupOf_of_le_normalizer hLE
  letI := Subgroup.normal_subgroupOf_sup_of_le_normalizer hLE
  let
    φ :-- φ is the natural homomorphism H →* (HN)/N.
      H →*
      _ ⧸ N.subgroupOf (H ⊔ N) :=
    (mk' <| N.subgroupOf (H ⊔ N)).comp (inclusion le_sup_left)
  have φ_surjective : Surjective φ := fun x =>
    x.inductionOn' <| by
      rintro ⟨y, hy : y ∈ (H ⊔ N)⟩
      rw [← SetLike.mem_coe] at hy
      rw [coe_mul_of_left_le_normalizer_right H N hLE] at hy
      rcases hy with ⟨h, hh, n, hn, rfl⟩
      use ⟨h, hh⟩
      let _ : Setoid ↑(H ⊔ N) :=
        (@leftRel ↑(H ⊔ N) (H ⊔ N : Subgroup G).toGroup (N.subgroupOf (H ⊔ N)))
      -- Porting note: Lean couldn't find this automatically
      refine Quotient.eq.mpr ?_
      change leftRel _ _ _
      rw [leftRel_apply]
      change h⁻¹h⁻¹ * (h * n) ∈ N
      rwa [← mul_assoc, inv_mul_cancel, one_mul]
  (quotientMulEquivOfEq (by simp [φ, ← comap_ker])).trans
    (quotientKerEquivOfSurjective φ φ_surjective)

Noether's Second Isomorphism Theorem

Informal description

Given a group $G$, a subgroup $N$ of $G$, and a subgroup $H$ of the normalizer of $N$ in $G$, there is a natural isomorphism between the quotient groups $H/(H \cap N)$ and $(HN)/N$. Here, $HN$ denotes the subgroup generated by $H$ and $N$.

QuotientGroup.quotientInfEquivProdNormalQuotient definition

(H N : Subgroup G) [hN : N.Normal] : H ⧸ N.subgroupOf H ≃* (H ⊔ N : Subgroup G) ⧸ N.subgroupOf (H ⊔ N)

Full source

/-- **Noether's second isomorphism theorem**: given two subgroups `H` and `N` of a group `G`,
where `N` is normal, defines an isomorphism between `H/(H ∩ N)` and `(HN)/N`. -/
@[to_additive "Noether's second isomorphism theorem: given two subgroups `H` and `N` of a group `G`,
where `N` is normal, defines an isomorphism between `H/(H ∩ N)` and `(H + N)/N`"]
noncomputable def quotientInfEquivProdNormalQuotient (H N : Subgroup G) [hN : N.Normal] :
    H ⧸ N.subgroupOf HH ⧸ N.subgroupOf H ≃* (H ⊔ N : Subgroup G) ⧸ N.subgroupOf (H ⊔ N) :=
  quotientInfEquivProdNormalizerQuotient H N le_normalizer_of_normal

Noether's Second Isomorphism Theorem (Normal Subgroup Version)

Informal description

Given a group $G$, a subgroup $H$ of $G$, and a normal subgroup $N$ of $G$, there is a natural group isomorphism between the quotient groups $H/(H \cap N)$ and $(H \cdot N)/N$, where $H \cdot N$ denotes the subgroup generated by $H$ and $N$.

QuotientGroup.map_normal instance

: (M.map (QuotientGroup.mk' N)).Normal

Full source

@[to_additive]
instance map_normal : (M.map (QuotientGroup.mk' N)).Normal :=
  nM.map _ mk_surjective

Normality of the Image of a Subgroup in the Quotient Group

Informal description

For any group $G$ with normal subgroup $N$, and any subgroup $M$ of $G$ containing $N$, the image of $M$ under the canonical projection $G \to G/N$ is a normal subgroup of $G/N$.

QuotientGroup.quotientQuotientEquivQuotientAux definition

: (G ⧸ N) ⧸ M.map (mk' N) →* G ⧸ M

Full source

/-- The map from the third isomorphism theorem for groups: `(G / N) / (M / N) → G / M`. -/
@[to_additive "The map from the third isomorphism theorem for additive groups:
`(A / N) / (M / N) → A / M`."]
def quotientQuotientEquivQuotientAux : (G ⧸ N) ⧸ M.map (mk' N)(G ⧸ N) ⧸ M.map (mk' N) →* G ⧸ M :=
  lift (M.map (mk' N)) (map N M (MonoidHom.id G) h)
    (by
      rintro _ ⟨x, hx, rfl⟩
      rw [mem_ker, map_mk' N M _ _ x]
      exact (QuotientGroup.eq_one_iff _).mpr hx)

Canonical homomorphism for the third isomorphism theorem

Informal description

The canonical homomorphism from the double quotient group $(G/N)/(M/N)$ to the quotient group $G/M$, where $G$ is a group, $N$ is a normal subgroup of $G$, and $M$ is a normal subgroup of $G$ containing $N$. This homomorphism is defined by lifting the identity map on $G$ through the quotient maps.

QuotientGroup.quotientQuotientEquivQuotientAux_mk theorem

(x : G ⧸ N) : quotientQuotientEquivQuotientAux N M h x = QuotientGroup.map N M (MonoidHom.id G) h x

Full source

@[to_additive (attr := simp)]
theorem quotientQuotientEquivQuotientAux_mk (x : G ⧸ N) :
    quotientQuotientEquivQuotientAux N M h x = QuotientGroup.map N M (MonoidHom.id G) h x :=
  QuotientGroup.lift_mk' _ _ x

Canonical Homomorphism Commutes with Identity Map on Quotient Groups

Informal description

For any element $x \in G/N$ in the quotient group, the canonical homomorphism $\text{quotientQuotientEquivQuotientAux}$ evaluated at $x$ is equal to the induced homomorphism $\text{map}$ of the identity homomorphism $\text{id}_G$ evaluated at $x$. That is, $\text{quotientQuotientEquivQuotientAux}(x) = \text{map}(\text{id}_G)(x)$.

QuotientGroup.quotientQuotientEquivQuotientAux_mk_mk theorem

(x : G) : quotientQuotientEquivQuotientAux N M h (x : G ⧸ N) = x

Full source

@[to_additive]
theorem quotientQuotientEquivQuotientAux_mk_mk (x : G) :
    quotientQuotientEquivQuotientAux N M h (x : G ⧸ N) = x :=
  QuotientGroup.lift_mk' (M.map (mk' N)) _ x

Canonical Homomorphism Evaluation in Third Isomorphism Theorem

Informal description

For any group $G$ with normal subgroups $N \trianglelefteq M \trianglelefteq G$, and any element $x \in G$, the canonical homomorphism $\text{quotientQuotientEquivQuotientAux}$ evaluated at the equivalence class $[x] \in G/N$ equals $x$ in the quotient group $G/M$. That is, $\text{quotientQuotientEquivQuotientAux}([x]) = x$.

QuotientGroup.quotientQuotientEquivQuotient definition

: (G ⧸ N) ⧸ M.map (QuotientGroup.mk' N) ≃* G ⧸ M

Full source

/-- **Noether's third isomorphism theorem** for groups: `(G / N) / (M / N) ≃* G / M`. -/
@[to_additive
      "**Noether's third isomorphism theorem** for additive groups: `(A / N) / (M / N) ≃+ A / M`."]
def quotientQuotientEquivQuotient : (G ⧸ N) ⧸ M.map (QuotientGroup.mk' N)(G ⧸ N) ⧸ M.map (QuotientGroup.mk' N) ≃* G ⧸ M :=
  MonoidHom.toMulEquiv (quotientQuotientEquivQuotientAux N M h)
    (QuotientGroup.map _ _ (QuotientGroup.mk' N) (Subgroup.le_comap_map _ _))
    (by ext; simp)
    (by ext; simp)

Third Isomorphism Theorem for Groups

Informal description

Noether's third isomorphism theorem for groups: The canonical isomorphism between the double quotient group $(G/N)/(M/N)$ and the quotient group $G/M$, where $G$ is a group, $N$ is a normal subgroup of $G$, and $M$ is a normal subgroup of $G$ containing $N$.

QuotientGroup.le_comap_mk' theorem

(N : Subgroup G) [N.Normal] (H : Subgroup (G ⧸ N)) : N ≤ Subgroup.comap (QuotientGroup.mk' N) H

Full source

@[to_additive]
theorem le_comap_mk' (N : Subgroup G) [N.Normal] (H : Subgroup (G ⧸ N)) :
    N ≤ Subgroup.comap (QuotientGroup.mk' N) H := by
  simpa using Subgroup.comap_mono (f := mk' N) bot_le

Inclusion of Normal Subgroup in Preimage under Quotient Projection

Informal description

For any normal subgroup $N$ of a group $G$ and any subgroup $H$ of the quotient group $G/N$, the subgroup $N$ is contained in the preimage of $H$ under the canonical projection $\pi : G \to G/N$. In other words, $N \subseteq \pi^{-1}(H)$.

QuotientGroup.comap_map_mk' theorem

(N H : Subgroup G) [N.Normal] : Subgroup.comap (mk' N) (Subgroup.map (mk' N) H) = N ⊔ H

Full source

@[to_additive (attr := simp)]
theorem comap_map_mk' (N H : Subgroup G) [N.Normal] :
    Subgroup.comap (mk' N) (Subgroup.map (mk' N) H) = N ⊔ H := by
  simp [Subgroup.comap_map_eq, sup_comm]

Preimage of Projection Image Equals Join with Normal Subgroup

Informal description

For any normal subgroup $N$ of a group $G$ and any subgroup $H$ of $G$, the preimage under the canonical projection $\pi : G \to G/N$ of the image of $H$ under $\pi$ is equal to the join of $N$ and $H$, i.e., $\pi^{-1}(\pi(H)) = N \sqcup H$.

QuotientGroup.comapMk'OrderIso definition

(N : Subgroup G) [hn : N.Normal] : Subgroup (G ⧸ N) ≃o { H : Subgroup G // N ≤ H }

Full source

/-- The **correspondence theorem**, or lattice theorem,
or fourth isomorphism theorem for multiplicative groups -/
@[to_additive "The **correspondence theorem**, or lattice theorem,
  or fourth isomorphism theorem for additive groups"]
def comapMk'OrderIso (N : Subgroup G) [hn : N.Normal] :
    SubgroupSubgroup (G ⧸ N) ≃o { H : Subgroup G // N ≤ H } where
  toFun H' := ⟨Subgroup.comap (mk' N) H', le_comap_mk' N _⟩
  invFun H := Subgroup.map (mk' N) H
  left_inv H' := Subgroup.map_comap_eq_self <| by simp
  right_inv := fun ⟨H, hH⟩ => Subtype.ext_val <| by simpa
  map_rel_iff' := Subgroup.comap_le_comap_of_surjective <| mk'_surjective _

Correspondence Theorem for Groups (Fourth Isomorphism Theorem)

Informal description

The correspondence theorem for groups states that for any normal subgroup $N$ of a group $G$, there is an order-preserving bijection (order isomorphism) between the lattice of subgroups of the quotient group $G/N$ and the lattice of subgroups of $G$ containing $N$. Explicitly, the bijection maps: - Any subgroup $H'$ of $G/N$ to its preimage under the canonical projection $\pi: G \to G/N$ (which is a subgroup of $G$ containing $N$) - Any subgroup $H$ of $G$ containing $N$ to its image $\pi(H)$ in $G/N$ This bijection preserves inclusion relations between subgroups.

QuotientGroup.subsingleton_quotient_top theorem

: Subsingleton (G ⧸ (⊤ : Subgroup G))

Full source

@[to_additive]
theorem subsingleton_quotient_top : Subsingleton (G ⧸ (⊤ : Subgroup G)) := by
  dsimp [HasQuotient.Quotient, QuotientGroup.instHasQuotientSubgroup, Quotient]
  rw [leftRel_eq]
  exact Trunc.instSubsingletonTrunc

Quotient by Trivial Subgroup is Subsingleton

Informal description

The quotient group $G / \top$ is a subsingleton, where $\top$ denotes the trivial subgroup of $G$ consisting of all elements of $G$.

QuotientGroup.subgroup_eq_top_of_subsingleton theorem

(H : Subgroup G) (h : Subsingleton (G ⧸ H)) : H = ⊤

Full source

/-- If the quotient by a subgroup gives a singleton then the subgroup is the whole group. -/
@[to_additive "If the quotient by an additive subgroup gives a singleton then the additive subgroup
is the whole additive group."]
theorem subgroup_eq_top_of_subsingleton (H : Subgroup G) (h : Subsingleton (G ⧸ H)) : H = ⊤ :=
  top_unique fun x _ => by
    have this : 1⁻¹1⁻¹ * x ∈ H := QuotientGroup.eq.1 (Subsingleton.elim _ _)
    rwa [inv_one, one_mul] at this

Subgroup is Whole Group When Quotient is Singleton

Informal description

Let $H$ be a subgroup of a group $G$. If the quotient group $G/H$ is a singleton (i.e., has exactly one element), then $H$ is equal to the entire group $G$.

QuotientGroup.comap_comap_center theorem

 {H₁ : Subgroup G} [H₁.Normal] {H₂ : Subgroup (G ⧸ H₁)} [H₂.Normal] :
  ((Subgroup.center ((G ⧸ H₁) ⧸ H₂)).comap (mk' H₂)).comap (mk' H₁) =
    (Subgroup.center (G ⧸ H₂.comap (mk' H₁))).comap (mk' (H₂.comap (mk' H₁)))

Full source

@[to_additive]
theorem comap_comap_center {H₁ : Subgroup G} [H₁.Normal] {H₂ : Subgroup (G ⧸ H₁)} [H₂.Normal] :
    ((Subgroup.center ((G ⧸ H₁) ⧸ H₂)).comap (mk' H₂)).comap (mk' H₁) =
      (Subgroup.center (G ⧸ H₂.comap (mk' H₁))).comap (mk' (H₂.comap (mk' H₁))) := by
  ext x
  simp only [mk'_apply, Subgroup.mem_comap, Subgroup.mem_center_iff, forall_mk, ← mk_mul,
    eq_iff_div_mem, mk_div]

Double Quotient Center Preimage Equality

Informal description

Let $G$ be a group with a normal subgroup $H_1$, and let $H_2$ be a normal subgroup of the quotient group $G/H_1$. Then, the preimage under the canonical projection $G \to G/H_1$ of the preimage under the canonical projection $G/H_1 \to (G/H_1)/H_2$ of the center of $(G/H_1)/H_2$ is equal to the preimage under the canonical projection $G \to G/H_2'$ of the center of $G/H_2'$, where $H_2'$ is the preimage of $H_2$ under the canonical projection $G \to G/H_1$.

QuotientAddGroup.mk_nat_mul theorem

(n : ℕ) (a : R) : ((n * a : R) : R ⧸ N) = n • ↑a

Full source

@[simp]
theorem mk_nat_mul (n : ℕ) (a : R) : ((n * a : R) : R ⧸ N) = n • ↑a := by
  rw [← nsmul_eq_mul, mk_nsmul N a n]

Natural Number Multiplication in Quotient Additive Groups

Informal description

For any natural number $n$ and any element $a$ of an additive group $R$, the image of $n \cdot a$ in the quotient group $R/N$ is equal to $n$ times the image of $a$ in $R/N$, i.e., $[n \cdot a] = n \cdot [a]$ where $[x]$ denotes the equivalence class of $x$ in $R/N$.

QuotientAddGroup.mk_int_mul theorem

(n : ℤ) (a : R) : ((n * a : R) : R ⧸ N) = n • ↑a

Full source

@[simp]
theorem mk_int_mul (n : ℤ) (a : R) : ((n * a : R) : R ⧸ N) = n • ↑a := by
  rw [← zsmul_eq_mul, mk_zsmul N a n]

Quotient Group Homomorphism Preserves Integer Multiplication

Informal description

For any integer $n$ and any element $a$ in an additive group $R$, the image of the integer multiple $n \cdot a$ under the quotient map $R \to R/N$ is equal to the $n$-th scalar multiple of the image of $a$ in the quotient group $R/N$, i.e., $\overline{n \cdot a} = n \cdot \overline{a}$.

Mathlib.GroupTheory.QuotientGroup.Basic

Main statements

Tags