Mathlib.GroupTheory.QuotientGroup.Defs

QuotientGroup.con definition

: Con G

Full source

/-- The congruence relation generated by a normal subgroup. -/
@[to_additive "The additive congruence relation generated by a normal additive subgroup."]
protected def con : Con G where
  toSetoid := leftRel N
  mul' := fun {a b c d} hab hcd => by
    rw [leftRel_eq] at hab hcd ⊢
    dsimp only
    calc
      c⁻¹c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) ∈ N := N.mul_mem (nN.conj_mem _ hab _) hcd
      _ = (a * c)⁻¹ * (b * d) := by
        simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]

Congruence relation generated by a normal subgroup

Informal description

The congruence relation on a group $G$ generated by a normal subgroup $N$ of $G$, where two elements $a, b \in G$ are related if and only if $a^{-1}b \in N$. This relation is an equivalence relation that preserves the group multiplication.

QuotientGroup.Quotient.group instance

: Group (G ⧸ N)

Full source

@[to_additive]
instance Quotient.group : Group (G ⧸ N) :=
  (QuotientGroup.con N).group

Group Structure on the Quotient by a Normal Subgroup

Informal description

For any group $G$ and normal subgroup $N$ of $G$, the quotient $G/N$ inherits a group structure where the multiplication is defined by $[x] \cdot [y] = [x \cdot y]$ for $x, y \in G$, the identity element is $[1]$, and the inverse of $[x]$ is $[x^{-1}]$.

QuotientGroup.con_ker_eq_conKer theorem

(f : G →* M) : QuotientGroup.con f.ker = Con.ker f

Full source

/--
The congruence relation defined by the kernel of a group homomorphism is equal to its kernel
as a congruence relation.
-/
@[to_additive QuotientAddGroup.con_ker_eq_addConKer
"The additive congruence relation defined by the kernel of an additive group homomorphism is
equal to its kernel as an additive congruence relation."]
theorem con_ker_eq_conKer (f : G →* M) : QuotientGroup.con f.ker = Con.ker f := by
  ext
  rw [QuotientGroup.con, Con.rel_mk, Setoid.comm', leftRel_apply, Con.ker_rel, MonoidHom.eq_iff]

Congruence Relation of Kernel Equals Kernel Congruence Relation

Informal description

For any group homomorphism $f \colon G \to M$, the congruence relation on $G$ defined by the kernel of $f$ is equal to the kernel congruence relation of $f$. That is, the equivalence relation where $x \sim y$ if and only if $f(x) = f(y)$ coincides with the relation where $x \sim y$ if and only if $x^{-1}y \in \ker f$.

QuotientGroup.mk' definition

: G →* G ⧸ N

Full source

/-- The group homomorphism from `G` to `G/N`. -/
@[to_additive "The additive group homomorphism from `G` to `G/N`."]
def mk' : G →* G ⧸ N :=
  MonoidHom.mk' QuotientGroup.mk fun _ _ => rfl

Canonical projection from a group to its quotient by a normal subgroup

Informal description

The canonical group homomorphism from a group $G$ to the quotient group $G/N$, where $N$ is a normal subgroup of $G$, sending each element $x \in G$ to its equivalence class $[x] \in G/N$.

QuotientGroup.coe_mk' theorem

: (mk' N : G → G ⧸ N) = mk

Full source

@[to_additive (attr := simp)]
theorem coe_mk' : (mk' N : G → G ⧸ N) = mk :=
  rfl

Equality of Underlying Function and Quotient Map in Group Quotient

Informal description

The underlying function of the canonical group homomorphism `mk' N` from $G$ to $G/N$ is equal to the quotient map `mk`, which sends each element $x \in G$ to its equivalence class $[x] \in G/N$.

QuotientGroup.mk'_apply theorem

(x : G) : mk' N x = x

Full source

@[to_additive (attr := simp)]
theorem mk'_apply (x : G) : mk' N x = x :=
  rfl

Canonical Projection Maps Elements to Their Equivalence Classes

Informal description

For any element $x$ in a group $G$, the canonical projection $\pi : G \to G/N$ maps $x$ to its equivalence class $[x]$ in the quotient group $G/N$, i.e., $\pi(x) = [x]$.

QuotientGroup.mk'_surjective theorem

: Surjective <| mk' N

Full source

@[to_additive]
theorem mk'_surjective : Surjective <| mk' N :=
  @mk_surjective _ _ N

Surjectivity of the Quotient Group Projection

Informal description

The canonical projection map $\pi \colon G \to G/N$ from a group $G$ to its quotient by a normal subgroup $N$ is surjective.

QuotientGroup.mk'_eq_mk' theorem

{x y : G} : mk' N x = mk' N y ↔ ∃ z ∈ N, x * z = y

Full source

@[to_additive]
theorem mk'_eq_mk' {x y : G} : mk'mk' N x = mk' N y ↔ ∃ z ∈ N, x * z = y :=
  QuotientGroup.eq.trans <| by
    simp only [← _root_.eq_inv_mul_iff_mul_eq, exists_prop, exists_eq_right]

Equality of Cosets in Quotient Group by Normal Subgroup

Informal description

For any elements $x, y$ in a group $G$ with normal subgroup $N$, the equivalence classes $[x]$ and $[y]$ in the quotient group $G/N$ are equal if and only if there exists an element $z \in N$ such that $x * z = y$.

QuotientGroup.monoidHom_ext theorem

⦃f g : G ⧸ N →* M⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g

Full source

/-- Two `MonoidHom`s from a quotient group are equal if their compositions with
`QuotientGroup.mk'` are equal.

See note [partially-applied ext lemmas]. -/
@[to_additive (attr := ext 1100) "Two `AddMonoidHom`s from an additive quotient group are equal if
 their compositions with `AddQuotientGroup.mk'` are equal.

 See note [partially-applied ext lemmas]. "]
theorem monoidHom_ext ⦃f g : G ⧸ NG ⧸ N →* M⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g :=
  MonoidHom.ext fun x => QuotientGroup.induction_on x <| (DFunLike.congr_fun h :)

Uniqueness of Monoid Homomorphisms from Quotient Group via Projection

Informal description

Let $G$ be a group with a normal subgroup $N$, and let $M$ be a monoid. For any two monoid homomorphisms $f, g \colon G/N \to M$, if $f \circ \pi = g \circ \pi$ where $\pi \colon G \to G/N$ is the canonical projection, then $f = g$.

QuotientGroup.range_mk' theorem

: (QuotientGroup.mk' N).range = ⊤

Full source

@[to_additive (attr := simp)]
theorem range_mk' : (QuotientGroup.mk' N).range = ⊤ :=
  MonoidHom.range_eq_top.mpr (mk'_surjective N)

Range of Quotient Projection is Entire Quotient Group

Informal description

The range of the canonical projection homomorphism $\pi \colon G \to G/N$ is the entire quotient group $G/N$, i.e., $\text{range}(\pi) = G/N$.

QuotientGroup.ker_le_range_iff theorem

 {I : Type w} [MulOneClass I] (f : G →* H) [f.range.Normal] (g : H →* I) :
  g.ker ≤ f.range ↔ (mk' f.range).comp g.ker.subtype = 1

Full source

@[to_additive]
theorem ker_le_range_iff {I : Type w} [MulOneClass I] (f : G →* H) [f.range.Normal] (g : H →* I) :
    g.ker ≤ f.range ↔ (mk' f.range).comp g.ker.subtype = 1 :=
  ⟨fun h => MonoidHom.ext fun ⟨_, hx⟩ => (eq_one_iff _).mpr <| h hx,
    fun h x hx => (eq_one_iff _).mp <| by exact DFunLike.congr_fun h ⟨x, hx⟩⟩

Kernel-Range Containment Criterion for Group Homomorphisms

Informal description

Let $G$, $H$, and $I$ be groups, with $f \colon G \to H$ and $g \colon H \to I$ group homomorphisms. Suppose the range of $f$ is a normal subgroup of $H$. Then the kernel of $g$ is contained in the range of $f$ if and only if the composition of the canonical projection $H \to H/f.\text{range}$ with the inclusion $g.\text{ker} \hookrightarrow H$ is the trivial homomorphism.

QuotientGroup.ker_mk' theorem

: MonoidHom.ker (QuotientGroup.mk' N : G →* G ⧸ N) = N

Full source

@[to_additive (attr := simp)]
theorem ker_mk' : MonoidHom.ker (QuotientGroup.mk' N : G →* G ⧸ N) = N :=
  Subgroup.ext eq_one_iff

Kernel of Quotient Projection Equals Normal Subgroup

Informal description

The kernel of the canonical projection homomorphism $\pi : G \to G/N$ is equal to the normal subgroup $N$, i.e., $\ker \pi = N$.

QuotientGroup.Quotient.commGroup instance

{G : Type*} [CommGroup G] (N : Subgroup G) : CommGroup (G ⧸ N)

Full source

@[to_additive]
instance Quotient.commGroup {G : Type*} [CommGroup G] (N : Subgroup G) : CommGroup (G ⧸ N) :=
  { toGroup := have := N.normal_of_comm; QuotientGroup.Quotient.group N
    mul_comm := fun a b => Quotient.inductionOn₂' a b fun a b => congr_arg mk (mul_comm a b) }

Commutativity of Quotient Groups from Commutative Groups

Informal description

For any commutative group $G$ and normal subgroup $N$ of $G$, the quotient group $G/N$ is also commutative.

QuotientGroup.mk_one theorem

: ((1 : G) : Q ) = 1

Full source

@[to_additive (attr := simp)]
theorem mk_one : ((1 : G) : Q) = 1 :=
  rfl

Identity Preservation in Quotient Group Projection

Informal description

The canonical projection of the identity element $1$ of a group $G$ onto the quotient group $G/N$ is equal to the identity element of $G/N$, i.e., $[1] = 1_{G/N}$.

QuotientGroup.mk_mul theorem

(a b : G) : ((a * b : G) : Q ) = a * b

Full source

@[to_additive (attr := simp)]
theorem mk_mul (a b : G) : ((a * b : G) : Q) = a * b :=
  rfl

Multiplication in Quotient Group Preserves Group Operation

Informal description

For any elements $a, b$ in a group $G$ with normal subgroup $N$, the equivalence class of the product $a * b$ in the quotient group $G/N$ is equal to the product of the equivalence classes of $a$ and $b$ in $G/N$, i.e., $[a * b] = [a] \cdot [b]$.

QuotientGroup.mk_inv theorem

(a : G) : ((a⁻¹ : G) : Q ) = (a : Q )⁻¹

Full source

@[to_additive (attr := simp)]
theorem mk_inv (a : G) : ((a⁻¹ : G) : Q) = (a : Q)⁻¹ :=
  rfl

Inverse Preservation in Quotient Group Projection

Informal description

For any element $a$ in a group $G$ with normal subgroup $N$, the equivalence class of the inverse $a^{-1}$ in the quotient group $G/N$ is equal to the inverse of the equivalence class of $a$ in $G/N$, i.e., $[a^{-1}] = [a]^{-1}$.

QuotientGroup.mk_div theorem

(a b : G) : ((a / b : G) : Q ) = a / b

Full source

@[to_additive (attr := simp)]
theorem mk_div (a b : G) : ((a / b : G) : Q) = a / b :=
  rfl

Quotient Operation Preservation in Quotient Group: $[a / b] = [a] / [b]$

Informal description

For any elements $a, b$ in a group $G$ with normal subgroup $N$, the equivalence class of the quotient $a / b$ in the quotient group $G/N$ is equal to the quotient of the equivalence classes of $a$ and $b$ in $G/N$, i.e., $[a / b] = [a] / [b]$.

QuotientGroup.mk_pow theorem

(a : G) (n : ℕ) : ((a ^ n : G) : Q ) = (a : Q ) ^ n

Full source

@[to_additive (attr := simp)]
theorem mk_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = (a : Q) ^ n :=
  rfl

Power of Image Equals Image of Power in Quotient Group

Informal description

For any element $a$ in a group $G$ and any natural number $n$, the image of $a^n$ in the quotient group $G/N$ equals the $n$-th power of the image of $a$ in $G/N$. That is, $[a^n] = [a]^n$ where $[a]$ denotes the equivalence class of $a$ in $G/N$.

QuotientGroup.mk_zpow theorem

(a : G) (n : ℤ) : ((a ^ n : G) : Q ) = (a : Q ) ^ n

Full source

@[to_additive (attr := simp)]
theorem mk_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = (a : Q) ^ n :=
  rfl

Power Preservation in Quotient Groups: $[a^n] = [a]^n$

Informal description

For any element $a$ in a group $G$ and any integer $n$, the image of $a^n$ under the canonical projection $G \to G/N$ equals the $n$-th power of the image of $a$ in the quotient group $G/N$. In other words, $[a^n] = [a]^n$ where $[\, \cdot \,]$ denotes the equivalence class in $G/N$.

QuotientGroup.map_mk'_self theorem

: N.map (mk' N) = ⊥

Full source

@[to_additive (attr := simp)] lemma map_mk'_self : N.map (mk' N) = ⊥ := by aesop

Trivial Image of Normal Subgroup in Quotient Group

Informal description

The image of the normal subgroup $N$ under the canonical projection $\text{mk}' : G \to G/N$ is the trivial subgroup $\{\bot\}$ of $G/N$.

Con.subgroup definition

(c : Con G) : Subgroup G

Full source

/--
The subgroup defined by the class of `1` for a congruence relation on a group.
-/
@[to_additive
"The `AddSubgroup` defined by the class of `0` for an additive congruence relation
on an `AddGroup`."]
protected def _root_.Con.subgroup (c : Con G) : Subgroup G where
  carrier := { x | c x 1 }
  one_mem' := c.refl 1
  mul_mem' hx hy := by simpa using c.mul hx hy
  inv_mem' h := by simpa using c.inv h

Subgroup associated with a congruence relation

Informal description

Given a congruence relation $c$ on a group $G$, the subgroup associated with $c$ consists of all elements $x \in G$ such that $x$ is congruent to the identity element $1$ under $c$. This subgroup is closed under multiplication and inversion, and contains the identity element.

Con.mem_subgroup_iff theorem

{c : Con G} {x : G} : x ∈ c.subgroup ↔ c x 1

Full source

@[to_additive (attr := simp)]
theorem _root_.Con.mem_subgroup_iff {c : Con G} {x : G} :
    x ∈ c.subgroupx ∈ c.subgroup ↔ c x 1 := Iff.rfl

Characterization of Subgroup Membership via Congruence Relation

Informal description

For a congruence relation $c$ on a group $G$ and an element $x \in G$, $x$ belongs to the subgroup associated with $c$ if and only if $x$ is congruent to the identity element $1$ under $c$.

QuotientGroup.instNormalSubgroup instance

(c : Con G) : c.subgroup.Normal

Full source

@[to_additive]
instance (c : Con G) : c.subgroup.Normal :=
  ⟨fun x hx g ↦ by simpa using (c.mul (c.mul (c.refl g) hx) (c.refl g⁻¹))⟩

Normality of the Subgroup Associated with a Congruence Relation

Informal description

For any congruence relation $c$ on a group $G$, the associated subgroup $c.subgroup$ is normal in $G$.

Con.subgroup_quotientGroupCon theorem

(H : Subgroup G) [H.Normal] : (QuotientGroup.con H).subgroup = H

Full source

@[to_additive (attr := simp)]
theorem _root_.Con.subgroup_quotientGroupCon (H : Subgroup G) [H.Normal] :
    (QuotientGroup.con H).subgroup = H := by
  ext
  simp [QuotientGroup.con, leftRel_apply]

Subgroup-Congruence Correspondence for Normal Subgroups

Informal description

For any normal subgroup $H$ of a group $G$, the subgroup associated with the congruence relation $\text{QuotientGroup.con}(H)$ is equal to $H$ itself.

QuotientGroup.con_subgroup theorem

(c : Con G) : QuotientGroup.con c.subgroup = c

Full source

@[to_additive (attr := simp)]
theorem con_subgroup (c : Con G) :
    QuotientGroup.con c.subgroup = c := by
  ext x y
  rw [QuotientGroup.con, Con.rel_mk, leftRel_apply, Con.mem_subgroup_iff]
  exact ⟨fun h ↦ by simpa using c.mul (c.refl x) (c.symm h),
    fun h ↦ by simpa using c.mul (c.refl x⁻¹) (c.symm h)⟩

Congruence Relation Generated by Associated Subgroup Equals Original Congruence

Informal description

For any congruence relation $c$ on a group $G$, the congruence relation generated by the subgroup associated with $c$ is equal to $c$ itself. In other words, $\text{QuotientGroup.con}(c.\text{subgroup}) = c$.

Subgroup.orderIsoCon definition

: { N : Subgroup G // N.Normal } ≃o Con G

Full source

/--
The normal subgroups correspond to the congruence relations on a group.
-/
@[to_additive (attr := simps) AddSubgroup.orderIsoAddCon
"The normal subgroups correspond to the additive congruence relations on an `AddGroup`."]
def _root_.Subgroup.orderIsoCon :
    { N : Subgroup G // N.Normal }{ N : Subgroup G // N.Normal } ≃o Con G where
  toFun N := letI : N.val.Normal := N.prop; QuotientGroup.con N
  invFun c := ⟨c.subgroup, inferInstance⟩
  left_inv := fun ⟨N, _⟩ ↦ Subtype.mk_eq_mk.mpr (Con.subgroup_quotientGroupCon N)
  right_inv c := QuotientGroup.con_subgroup c
  map_rel_iff' := by
    simp only [QuotientGroup.con, Equiv.coe_fn_mk, Con.le_def, Con.rel_mk, leftRel_apply]
    refine ⟨fun h x _ ↦ ?_, fun hle _ _ h ↦ hle h⟩
    specialize @h 1 x
    simp_all

Order isomorphism between normal subgroups and congruence relations

Informal description

The order isomorphism between the set of normal subgroups of a group $G$ and the set of congruence relations on $G$. Specifically, it maps a normal subgroup $N$ to the congruence relation where two elements $a, b \in G$ are related if and only if $a^{-1}b \in N$, and conversely, maps a congruence relation $c$ to the normal subgroup consisting of elements $x \in G$ such that $x$ is congruent to the identity element under $c$.

QuotientGroup.con_le_iff theorem

{N M : Subgroup G} [N.Normal] [M.Normal] : QuotientGroup.con N ≤ QuotientGroup.con M ↔ N ≤ M

Full source

@[to_additive (attr := simp)]
lemma con_le_iff {N M : Subgroup G} [N.Normal] [M.Normal] :
    QuotientGroup.conQuotientGroup.con N ≤ QuotientGroup.con M ↔ N ≤ M :=
  (Subgroup.orderIsoCon.map_rel_iff (a := ⟨N, inferInstance⟩) (b := ⟨M, inferInstance⟩))

Order Correspondence Between Normal Subgroups and Congruence Relations: $N \leq M \leftrightarrow \text{con}(N) \leq \text{con}(M)$

Informal description

For any two normal subgroups $N$ and $M$ of a group $G$, the congruence relation $\text{QuotientGroup.con}(N)$ is less than or equal to $\text{QuotientGroup.con}(M)$ if and only if $N$ is a subgroup of $M$.

QuotientGroup.con_mono theorem

{N M : Subgroup G} [hN : N.Normal] [hM : M.Normal] (h : N ≤ M) : QuotientGroup.con N ≤ QuotientGroup.con M

Full source

@[to_additive (attr := gcongr)]
lemma con_mono {N M : Subgroup G} [hN : N.Normal] [hM : M.Normal] (h : N ≤ M) :
    QuotientGroup.con N ≤ QuotientGroup.con M :=
  con_le_iff.mpr h

Monotonicity of Congruence Relation with Respect to Normal Subgroup Inclusion

Informal description

For any two normal subgroups $N$ and $M$ of a group $G$, if $N$ is a subgroup of $M$, then the congruence relation $\text{con}(N)$ is less than or equal to the congruence relation $\text{con}(M)$. That is, $N \leq M$ implies $\text{con}(N) \leq \text{con}(M)$.

QuotientGroup.lift definition

(φ : G →* M) (HN : N ≤ φ.ker) : Q →* M

Full source

/-- A group homomorphism `φ : G →* M` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a
group homomorphism `G/N →* M`. -/
@[to_additive "An `AddGroup` homomorphism `φ : G →+ M` with `N ⊆ ker(φ)` descends (i.e. `lift`s)
 to a group homomorphism `G/N →* M`."]
def lift (φ : G →* M) (HN : N ≤ φ.ker) : QQ →* M :=
  (QuotientGroup.con N).lift φ <| con_ker_eq_conKer φ ▸ con_mono HN

Lift of a group homomorphism to the quotient group

Informal description

Given a group homomorphism $\varphi \colon G \to M$ with $N \subseteq \ker \varphi$, there exists a unique group homomorphism $\text{lift}(\varphi) \colon G/N \to M$ such that $\text{lift}(\varphi)([g]) = \varphi(g)$ for all $g \in G$, where $[g]$ denotes the equivalence class of $g$ in the quotient group $G/N$.

QuotientGroup.lift_mk theorem

{φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (g : Q ) = φ g

Full source

@[to_additive (attr := simp)]
theorem lift_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (g : Q) = φ g :=
  rfl

Lifted Homomorphism Evaluates to Original on Cosets

Informal description

Given a group homomorphism $\varphi \colon G \to M$ with $N \subseteq \ker \varphi$, and any element $g \in G$, the lifted homomorphism $\text{lift}(\varphi)$ evaluated at the equivalence class $[g] \in G/N$ equals $\varphi(g)$. That is, $\text{lift}(\varphi)([g]) = \varphi(g)$.

QuotientGroup.lift_mk' theorem

{φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (mk g : Q ) = φ g

Full source

@[to_additive (attr := simp)]
theorem lift_mk' {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (mk g : Q) = φ g :=
  rfl

Lifted Homomorphism Evaluates to Original on Cosets

Informal description

Given a group homomorphism $\varphi \colon G \to M$ such that $N \subseteq \ker \varphi$, and any element $g \in G$, the lifted homomorphism $\text{lift}(\varphi)$ evaluated at the equivalence class $[g] \in G/N$ equals $\varphi(g)$. That is, $\text{lift}(\varphi)([g]) = \varphi(g)$.

QuotientGroup.lift_comp_mk' theorem

(φ : G →* M) (HN : N ≤ φ.ker) : (QuotientGroup.lift N φ HN).comp (QuotientGroup.mk' N) = φ

Full source

@[to_additive (attr := simp)]
theorem lift_comp_mk' (φ : G →* M) (HN : N ≤ φ.ker) :
    (QuotientGroup.lift N φ HN).comp (QuotientGroup.mk' N) = φ :=
  rfl

Composition of Lift and Projection Equals Original Homomorphism

Informal description

Given a group homomorphism $\varphi \colon G \to M$ with $N \subseteq \ker \varphi$, the composition of the lifted homomorphism $\text{lift}(\varphi) \colon G/N \to M$ with the canonical projection $\text{mk}' \colon G \to G/N$ equals $\varphi$, i.e., $\text{lift}(\varphi) \circ \text{mk}' = \varphi$.

QuotientGroup.lift_quot_mk theorem

{φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (Quot.mk _ g : Q ) = φ g

Full source

@[to_additive (attr := simp)]
theorem lift_quot_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) :
    lift N φ HN (Quot.mk _ g : Q) = φ g :=
  rfl

Lift Evaluation on Quotient Class: $\text{lift}(\varphi)([g]) = \varphi(g)$

Informal description

Given a group homomorphism $\varphi \colon G \to M$ with $N \subseteq \ker \varphi$, for any element $g \in G$, the lift of $\varphi$ to the quotient group $G/N$ evaluated at the equivalence class of $g$ equals $\varphi(g)$, i.e., $\text{lift}(\varphi)([g]) = \varphi(g)$.

QuotientGroup.lift_surjective_of_surjective theorem

(φ : G →* M) (hφ : Function.Surjective φ) (HN : N ≤ φ.ker) : Function.Surjective (QuotientGroup.lift N φ HN)

Full source

@[to_additive]
theorem lift_surjective_of_surjective (φ : G →* M) (hφ : Function.Surjective φ) (HN : N ≤ φ.ker) :
    Function.Surjective (QuotientGroup.lift N φ HN) :=
  Quotient.lift_surjective _ _ hφ

Surjectivity of the Lifted Homomorphism from Quotient Group

Informal description

Let $G$ be a group with a normal subgroup $N$, and let $\varphi \colon G \to M$ be a surjective group homomorphism such that $N \subseteq \ker \varphi$. Then the induced homomorphism $\text{lift}(\varphi) \colon G/N \to M$ is also surjective.

QuotientGroup.ker_lift theorem

(φ : G →* M) (HN : N ≤ φ.ker) : (QuotientGroup.lift N φ HN).ker = Subgroup.map (QuotientGroup.mk' N) φ.ker

Full source

@[to_additive]
theorem ker_lift (φ : G →* M) (HN : N ≤ φ.ker) :
    (QuotientGroup.lift N φ HN).ker = Subgroup.map (QuotientGroup.mk' N) φ.ker := by
  rw [← congrArg MonoidHom.ker (lift_comp_mk' N φ HN), ← MonoidHom.comap_ker,
    Subgroup.map_comap_eq_self_of_surjective (mk'_surjective N)]

Kernel of Lifted Homomorphism Equals Projection of Kernel

Informal description

Let $G$ be a group with a normal subgroup $N$, and let $\varphi \colon G \to M$ be a group homomorphism such that $N \subseteq \ker \varphi$. Then the kernel of the induced homomorphism $\text{lift}(\varphi) \colon G/N \to M$ is equal to the image of $\ker \varphi$ under the canonical projection $\pi \colon G \to G/N$.

QuotientGroup.map definition

(M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) : G ⧸ N →* H ⧸ M

Full source

/-- A group homomorphism `f : G →* H` induces a map `G/N →* H/M` if `N ⊆ f⁻¹(M)`. -/
@[to_additive
      "An `AddGroup` homomorphism `f : G →+ H` induces a map `G/N →+ H/M` if `N ⊆ f⁻¹(M)`."]
def map (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) : G ⧸ NG ⧸ N →* H ⧸ M := by
  refine QuotientGroup.lift N ((mk' M).comp f) ?_
  intro x hx
  refine QuotientGroup.eq.2 ?_
  rw [mul_one, Subgroup.inv_mem_iff]
  exact h hx

Induced homomorphism between quotient groups

Informal description

Given a group homomorphism $f \colon G \to H$ and normal subgroups $N \trianglelefteq G$ and $M \trianglelefteq H$ such that $N \subseteq f^{-1}(M)$, there exists an induced group homomorphism $\text{map}(f) \colon G/N \to H/M$ defined by $\text{map}(f)([g]) = [f(g)]$ for all $g \in G$, where $[g]$ denotes the equivalence class of $g$ in the quotient group.

QuotientGroup.map_mk theorem

(M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) : map N M f h ↑x = ↑(f x)

Full source

@[to_additive (attr := simp)]
theorem map_mk (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
    map N M f h ↑x = ↑(f x) :=
  rfl

Commutativity of Quotient Map with Group Homomorphism

Informal description

Let $G$ and $H$ be groups with normal subgroups $N \trianglelefteq G$ and $M \trianglelefteq H$, and let $f \colon G \to H$ be a group homomorphism such that $N \subseteq f^{-1}(M)$. Then for any $x \in G$, the induced homomorphism $\text{map}(f) \colon G/N \to H/M$ satisfies $\text{map}(f)([x]) = [f(x)]$, where $[x]$ denotes the equivalence class of $x$ in $G/N$ and $[f(x)]$ denotes the equivalence class of $f(x)$ in $H/M$.

QuotientGroup.map_mk' theorem

(M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) : map N M f h (mk' _ x) = ↑(f x)

Full source

@[to_additive]
theorem map_mk' (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
    map N M f h (mk' _ x) = ↑(f x) :=
  rfl

Commutativity of Quotient Map with Canonical Projection

Informal description

Given a group homomorphism $f \colon G \to H$, normal subgroups $N \trianglelefteq G$ and $M \trianglelefteq H$ such that $N \subseteq f^{-1}(M)$, and an element $x \in G$, the induced homomorphism $\text{map}(f) \colon G/N \to H/M$ satisfies $\text{map}(f)([x]) = [f(x)]$, where $[x]$ denotes the equivalence class of $x$ in $G/N$ and $[f(x)]$ denotes the equivalence class of $f(x)$ in $H/M$.

QuotientGroup.map_surjective_of_surjective theorem

 (M : Subgroup H) [M.Normal] (f : G →* H) (hf : Function.Surjective (mk ∘ f : G → H ⧸ M)) (h : N ≤ M.comap f) :
  Function.Surjective (map N M f h)

Full source

@[to_additive]
theorem map_surjective_of_surjective (M : Subgroup H) [M.Normal] (f : G →* H)
    (hf : Function.Surjective (mkmk ∘ f : G → H ⧸ M)) (h : N ≤ M.comap f) :
    Function.Surjective (map N M f h) :=
  lift_surjective_of_surjective _ _ hf _

Surjectivity of Induced Homomorphism Between Quotient Groups

Informal description

Let $G$ and $H$ be groups with normal subgroups $N \trianglelefteq G$ and $M \trianglelefteq H$, respectively. Given a group homomorphism $f \colon G \to H$ such that $N \subseteq f^{-1}(M)$, if the composition of $f$ with the canonical projection $H \to H/M$ is surjective, then the induced homomorphism $\text{map}(f) \colon G/N \to H/M$ is also surjective.

QuotientGroup.ker_map theorem

 (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) :
  (map N M f h).ker = Subgroup.map (mk' N) (M.comap f)

Full source

@[to_additive]
theorem ker_map (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) :
    (map N M f h).ker = Subgroup.map (mk' N) (M.comap f) := by
  simp_rw [← ker_mk' M, MonoidHom.comap_ker]
  exact QuotientGroup.ker_lift _ _ _

Kernel of Induced Homomorphism Between Quotient Groups Equals Projection of Preimage

Informal description

Let $G$ and $H$ be groups with normal subgroups $N \trianglelefteq G$ and $M \trianglelefteq H$, respectively. Given a group homomorphism $f \colon G \to H$ such that $N \subseteq f^{-1}(M)$, the kernel of the induced homomorphism $\text{map}(f) \colon G/N \to H/M$ is equal to the image of $f^{-1}(M)$ under the canonical projection $\pi \colon G \to G/N$.

QuotientGroup.image_coe theorem

: ((↑) : G → Q ) '' N = 1

Full source

@[to_additive (attr := simp)] lemma image_coe : ((↑) : G → Q) '' N = 1 :=
  congr_arg ((↑) : Subgroup Q → Set Q) <| map_mk'_self N

Image of Normal Subgroup in Quotient is Trivial

Informal description

The image of the normal subgroup $N$ under the canonical projection $\pi: G \to G/N$ is the trivial subgroup $\{1\}$ of the quotient group $G/N$.

QuotientGroup.preimage_image_coe theorem

(s : Set G) : ((↑) : G → Q ) ⁻¹' ((↑) '' s) = N * s

Full source

@[to_additive]
lemma preimage_image_coe (s : Set G) : ((↑) : G → Q) ⁻¹' ((↑) '' s) = N * s := by
  ext a
  constructor
  · rintro ⟨b, hb, h⟩
    refine ⟨a / b, (QuotientGroup.eq_one_iff _).1 ?_, b, hb, div_mul_cancel _ _⟩
    simp only [h, QuotientGroup.mk_div, div_self']
  · rintro ⟨a, ha, b, hb, rfl⟩
    refine ⟨b, hb, ?_⟩
    simpa only [QuotientGroup.mk_mul, right_eq_mul, QuotientGroup.eq_one_iff]

Preimage-Image Relation for Quotient Group Projection

Informal description

For any subset $s$ of a group $G$ and normal subgroup $N$ of $G$, the preimage under the canonical projection $\pi: G \to G/N$ of the image of $s$ under $\pi$ is equal to the product $N \cdot s$, i.e., $$\pi^{-1}(\pi(s)) = N \cdot s$$ where $\pi(g) = gN$ denotes the coset of $g$ modulo $N$ and $N \cdot s = \{n \cdot g \mid n \in N, g \in s\}$.

QuotientGroup.image_coe_inj theorem

{s t : Set G} : ((↑) : G → Q ) '' s = ((↑) : G → Q ) '' t ↔ ↑N * s = N * t

Full source

@[to_additive]
lemma image_coe_inj {s t : Set G} : ((↑) : G → Q) '' s((↑) : G → Q) '' s = ((↑) : G → Q) '' t ↔ ↑N * s = N * t := by
  simp_rw [← preimage_image_coe]
  exact QuotientGroup.mk_surjective.preimage_injective.eq_iff.symm

Injectivity of Quotient Map on Subsets Modulo Normal Subgroup

Informal description

For any subsets $s$ and $t$ of a group $G$, the images of $s$ and $t$ under the canonical projection $G \to G/N$ are equal if and only if the product of the normal subgroup $N$ with $s$ is equal to the product of $N$ with $t$, i.e., $$ \pi(s) = \pi(t) \iff N \cdot s = N \cdot t $$ where $\pi: G \to G/N$ is the quotient map and $N \cdot s$ denotes the product of $N$ and $s$ in $G$.

QuotientGroup.congr definition

(e : G ≃* H) (he : G'.map e = H') : G ⧸ G' ≃* H ⧸ H'

Full source

/-- `QuotientGroup.congr` lifts the isomorphism `e : G ≃ H` to `G ⧸ G' ≃ H ⧸ H'`,
given that `e` maps `G` to `H`. -/
@[to_additive "`QuotientAddGroup.congr` lifts the isomorphism `e : G ≃ H` to `G ⧸ G' ≃ H ⧸ H'`,
 given that `e` maps `G` to `H`."]
def congr (e : G ≃* H) (he : G'.map e = H') : G ⧸ G'G ⧸ G' ≃* H ⧸ H' :=
  { map G' H' e (he ▸ G'.le_comap_map (e : G →* H)) with
    toFun := map G' H' e (he ▸ G'.le_comap_map (e : G →* H))
    invFun := map H' G' e.symm (he ▸ (G'.map_equiv_eq_comap_symm e).le)
    left_inv := fun x => by
      rw [map_map G' H' G' e e.symm (he ▸ G'.le_comap_map (e : G →* H))
        (he ▸ (G'.map_equiv_eq_comap_symm e).le)]
      simp only [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
        MulEquiv.coe_monoidHom_refl, map_id_apply]
    right_inv := fun x => by
      rw [map_map H' G' H' e.symm e (he ▸ (G'.map_equiv_eq_comap_symm e).le)
        (he ▸ G'.le_comap_map (e : G →* H)) ]
      simp only [← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
        MulEquiv.coe_monoidHom_refl, map_id_apply] }

Isomorphism of quotient groups induced by a group isomorphism

Informal description

Given a group isomorphism $e \colon G \to H$ and normal subgroups $G' \trianglelefteq G$ and $H' \trianglelefteq H$ such that $e$ maps $G'$ to $H'$ (i.e., $e(G') = H'$), the function `QuotientGroup.congr` lifts $e$ to an isomorphism between the quotient groups $G/G'$ and $H/H'$. Specifically, for any $g \in G$, the image of the coset $[g] \in G/G'$ under this isomorphism is the coset $[e(g)] \in H/H'$.

QuotientGroup.congr_mk theorem

(e : G ≃* H) (he : G'.map ↑e = H') (x) : congr G' H' e he (mk x) = e x

Full source

@[simp]
theorem congr_mk (e : G ≃* H) (he : G'.map ↑e = H') (x) : congr G' H' e he (mk x) = e x :=
  rfl

Compatibility of Quotient Group Isomorphism with Coset Representation

Informal description

Given a group isomorphism $e \colon G \to H$ and normal subgroups $G' \trianglelefteq G$ and $H' \trianglelefteq H$ such that $e(G') = H'$, the induced isomorphism $\overline{e} \colon G/G' \to H/H'$ satisfies $\overline{e}([x]) = e(x)$ for all $x \in G$, where $[x]$ denotes the coset of $x$ in $G/G'$.

QuotientGroup.congr_mk' theorem

(e : G ≃* H) (he : G'.map ↑e = H') (x) : congr G' H' e he (mk' G' x) = mk' H' (e x)

Full source

theorem congr_mk' (e : G ≃* H) (he : G'.map ↑e = H') (x) :
    congr G' H' e he (mk' G' x) = mk' H' (e x) :=
  rfl

Commutativity of Quotient Group Isomorphism with Canonical Projection

Informal description

Given a group isomorphism $e \colon G \to H$ and normal subgroups $G' \trianglelefteq G$ and $H' \trianglelefteq H$ such that $e(G') = H'$, the induced isomorphism $\overline{e} \colon G/G' \to H/H'$ satisfies $\overline{e}([x]_{G'}) = [e(x)]_{H'}$ for all $x \in G$, where $[x]_{G'}$ denotes the coset of $x$ in $G/G'$ and $[e(x)]_{H'}$ denotes the coset of $e(x)$ in $H/H'$.

QuotientGroup.congr_apply theorem

(e : G ≃* H) (he : G'.map ↑e = H') (x : G) : congr G' H' e he x = mk' H' (e x)

Full source

@[simp]
theorem congr_apply (e : G ≃* H) (he : G'.map ↑e = H') (x : G) :
    congr G' H' e he x = mk' H' (e x) :=
  rfl

Image of Coset under Quotient Group Isomorphism

Informal description

Given a group isomorphism $e \colon G \to H$ and normal subgroups $G' \trianglelefteq G$ and $H' \trianglelefteq H$ such that $e(G') = H'$, the induced isomorphism $\overline{e} \colon G/G' \to H/H'$ satisfies $\overline{e}([x]) = [e(x)]$ for all $x \in G$, where $[x]$ denotes the coset of $x$ in $G/G'$ and $[e(x)]$ denotes the coset of $e(x)$ in $H/H'$.

QuotientGroup.congr_symm theorem

 (e : G ≃* H) (he : G'.map ↑e = H') :
  (congr G' H' e he).symm = congr H' G' e.symm ((Subgroup.map_symm_eq_iff_map_eq _).mpr he)

Full source

@[simp]
theorem congr_symm (e : G ≃* H) (he : G'.map ↑e = H') :
    (congr G' H' e he).symm = congr H' G' e.symm ((Subgroup.map_symm_eq_iff_map_eq _).mpr he) :=
  rfl

Inverse of Quotient Group Isomorphism Induced by Group Isomorphism

Informal description

Given a group isomorphism $e \colon G \to H$ and normal subgroups $G' \trianglelefteq G$ and $H' \trianglelefteq H$ such that $e(G') = H'$, the inverse of the induced isomorphism $\overline{e} \colon G/G' \to H/H'$ is equal to the isomorphism $\overline{e^{-1}} \colon H/H' \to G/G'$ induced by the inverse isomorphism $e^{-1} \colon H \to G$.

Mathlib.GroupTheory.QuotientGroup.Defs

Main definitions

Tags