QuotientAddGroup.lift_mk'
theorem QuotientAddGroup.lift_mk' :
∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [inst_1 : AddMonoid M]
{φ : G →+ M} (HN : N ≤ φ.ker) (g : G), (QuotientAddGroup.lift N φ HN) ↑g = φ g
The theorem `QuotientAddGroup.lift_mk'` states that for any additive group `G`, subgroup `N` of `G` that is normal, additive monoid `M`, and an additive group homomorphism `φ` from `G` to `M` such that `N` is a subset of the kernel of `φ`, and any element `g` of `G`, the result of applying the `lift` of `φ` over the quotient group `G/N` to the coset of `g` (denoted `(QuotientAddGroup.lift N φ HN) ↑g`) is equal to the result of applying `φ` to `g` (denoted `φ g`). Essentially, it means that lifting a homomorphism to the quotient group and applying it to a coset gives the same result as applying the original homomorphism to the representative of the coset.
More concisely: For any additive group homomorphism φ from a normal subgroup N of an additive group G to an additive monoid M such that the kernel of φ contains N, the diagram commutes: φ ∘ (QuotientAddGroup.lift N) = (QuotientAddGroup.lift N ∘ ι), where ι is the inclusion map from G to G/N.
|
QuotientGroup.monoidHom_ext
theorem QuotientGroup.monoidHom_ext :
∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [inst_1 : Monoid M]
⦃f g : G ⧸ N →* M⦄, f.comp (QuotientGroup.mk' N) = g.comp (QuotientGroup.mk' N) → f = g
The theorem `QuotientGroup.monoidHom_ext` states that for any group `G`, normal subgroup `N` of `G`, and monoid `M`, if we have two monoid homomorphisms `f` and `g` from the quotient group `G ⧸ N` to `M`, then `f` and `g` are equal if their compositions with the group homomorphism `QuotientGroup.mk'`, which maps from `G` to `G ⧸ N`, are equal. This theorem is typically used in situations where we want to show that two monoid homomorphisms are equal based on their actions when composed with another specific homomorphism.
More concisely: If two monoid homomorphisms from the quotient group of a group by a normal subgroup to a monoid have equal compositions with the quotient group homomorphism, then they are equal.
|
Mathlib.GroupTheory.QuotientGroup._auxLemma.5
theorem Mathlib.GroupTheory.QuotientGroup._auxLemma.5 :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {A : Set β} {a : α} {x : β},
(x ∈ a • A) = (a⁻¹ • x ∈ A)
This theorem from the group theory module in Mathlib states that for any type `G` with an addition group structure, and any normal addition subgroup `N` of `G`, a particular element `x` from `G` is in `N` if and only if the additive quotient of `x` is zero. Essentially, it establishes a relationship between the membership of an element in a subgroup and the quotient of that element being zero.
More concisely: For any additive group `G` and normal subgroup `N`, an element `x` in `G` belongs to `N` if and only if `x` has additive quotient `0` in `G/N`.
|
QuotientGroup.ker_mk'
theorem QuotientGroup.ker_mk' :
∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal], (QuotientGroup.mk' N).ker = N
This theorem states that for any group `G` and any normal subgroup `N` of `G`, the multiplicative kernel of the group homomorphism from `G` to the quotient group `G/N` is equal to `N`. The multiplicative kernel of a group homomorphism is the subgroup of elements `x` in `G` such that the homomorphism maps `x` to the identity in `G/N`. In other words, the set of elements in `G` that get mapped to the identity in the quotient group `G/N` is exactly the set of elements in the normal subgroup `N`.
More concisely: The normal subgroup of a group is the multiplicative kernel of the corresponding quotient homomorphism.
|
QuotientAddGroup.mk_zero
theorem QuotientAddGroup.mk_zero : ∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal], ↑0 = 0 := by
sorry
The theorem `QuotientAddGroup.mk_zero` states that for any type `G` that forms an additive group, and any additive subgroup `N` of `G` that is normal, the canonical projection of the zero element from `G` to the quotient group `G/N` is also the zero element. In other words, in the quotient group, the equivalence class of the zero element of the original group is the zero element of the quotient group.
More concisely: For any normal additive subgroup `N` of an additive group `G`, the canonical projection of the group's zero element maps to the zero element in the quotient group `G/N`.
|
QuotientAddGroup.ker_mk'
theorem QuotientAddGroup.ker_mk' :
∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal], (QuotientAddGroup.mk' N).ker = N
The theorem `QuotientAddGroup.ker_mk'` states that for any additive group `G` and any normal subgroup `N` of `G`, the kernel of the additive group homomorphism from `G` to the quotient group `G/N` is equal to `N`. Here, the kernel of a homomorphism is the subgroup of elements that are mapped to the identity element (zero in the case of additive groups). This theorem is essentially saying that the elements that get mapped to zero in the quotient group are exactly the elements of the subgroup `N`.
More concisely: The kernel of the additive group homomorphism from a group G to its quotient by a normal subgroup N equals N.
|
QuotientAddGroup.addMonoidHom_ext
theorem QuotientAddGroup.addMonoidHom_ext :
∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [inst_1 : AddMonoid M]
⦃f g : G ⧸ N →+ M⦄, f.comp (QuotientAddGroup.mk' N) = g.comp (QuotientAddGroup.mk' N) → f = g
This theorem states that for any type `G` with the structure of an additive group, a subgroup `N` of `G` that is normal, and any type `M` with the structure of an additive monoid, if two additive monoid homomorphisms `f` and `g` from the quotient group `G ⧸ N` to `M` have the property that their compositions with the function `QuotientAddGroup.mk' N` are equal, then `f` and `g` themselves must be equal. This means that if the homomorphisms `f` and `g` map elements from the same coset (i.e., the equivalence class of elements in `G` that differ by an element of `N`) to the same element in `M`, then `f` and `g` are the same homomorphism.
More concisely: Given an additive group `G`, a normal subgroup `N`, and additive monoids `M`, if two additive group homomorphisms from `G / N` to `M` agree on the image of `QuotientAddGroup.mk' N`, then they are equal.
|
QuotientGroup.subgroup_eq_top_of_subsingleton
theorem QuotientGroup.subgroup_eq_top_of_subsingleton :
∀ {G : Type u} [inst : Group G] (H : Subgroup G), Subsingleton (G ⧸ H) → H = ⊤
This theorem states that if the quotient of a group `G` by a subgroup `H` results in a singleton (a set with only one element), then the subgroup `H` must be equal to the entire group `G`. In other words, if dividing the group `G` into equivalence classes based on the subgroup `H` only produces one equivalence class, then the subgroup `H` is identical to the group `G`.
More concisely: If a group `G` has only one subgroup `H` with index 1 (i.e., `G/H` is a singleton set), then `H` equals `G`.
|
QuotientAddGroup.eq_zero_iff
theorem QuotientAddGroup.eq_zero_iff :
∀ {G : Type u} [inst : AddGroup G] {N : AddSubgroup G} [nN : N.Normal] (x : G), ↑x = 0 ↔ x ∈ N
This theorem, `QuotientAddGroup.eq_zero_iff`, states that for any type `G` that has an `AddGroup` instance, given any `AddSubgroup` `N` of `G` that is normal, and an element `x` of `G`, the coset of `x` is equal to zero if and only if `x` is an element of `N`. This is a statement in the context of quotient groups in group theory. In mathematical terms, it states that $x \equiv 0 (\mod N)$ if and only if $x \in N$ for an additive group $G$ and its normal subgroup $N$.
More concisely: In an additive group G with a normal subgroup N, an element x belongs to N if and only if the coset of x is equal to the identity element. In other words, x ≡ 0 (mod N) if and only if x ∈ N.
|
QuotientGroup.mk'_surjective
theorem QuotientGroup.mk'_surjective :
∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal], Function.Surjective ⇑(QuotientGroup.mk' N) := by
sorry
The theorem `QuotientGroup.mk'_surjective` states that for any type `G` that is a group, and for any `N` which is a normal subgroup of `G`, the group homomorphism from `G` to the quotient group `G/N`, given by the function `QuotientGroup.mk' N`, is surjective. This means that for every element in the quotient group `G/N`, there exists an element in the original group `G` such that applying the `QuotientGroup.mk' N` function to this element results in the given element of the quotient group.
More concisely: For any group `G` and normal subgroup `N`, the homomorphism `QuotientGroup.mk' N : G → G/N` is surjective.
|
QuotientGroup.lift_mk'
theorem QuotientGroup.lift_mk' :
∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [inst_1 : Monoid M] {φ : G →* M}
(HN : N ≤ φ.ker) (g : G), (QuotientGroup.lift N φ HN) ↑g = φ g
The theorem `QuotientGroup.lift_mk'` states that for any group `G`, normal subgroup `N` of `G`, monoid `M`, and a group homomorphism `φ` from `G` to `M` such that `N` is a subset of the kernel of `φ`, and for any element `g` of `G`, the homomorphism from the quotient group `G/N` to `M` induced by `φ` (denoted as `QuotientGroup.lift N φ HN`) applied to the coset of `g` in `G/N` (denoted as `↑g`) is equal to the image of `g` under `φ`. In mathematical terms, if `φ: G → M` is a group homomorphism and `N` is a normal subgroup of `G` included in the kernel of `φ`, then there exists a unique group homomorphism `ψ: G/N → M` such that `ψ(gN) = φ(g)` for all `g` in `G`, this `ψ` is the lift of `φ`.
More concisely: For any group homomorphism φ from a group G to a monoid M with normal subgroup N in the kernel, the homomorphism induced by φ from the quotient group G/N to M maps the coset ↑g to φ(g) for all g in G.
|
QuotientAddGroup.addSubgroup_eq_top_of_subsingleton
theorem QuotientAddGroup.addSubgroup_eq_top_of_subsingleton :
∀ {G : Type u} [inst : AddGroup G] (H : AddSubgroup G), Subsingleton (G ⧸ H) → H = ⊤
This theorem states that for any type `G` which forms an additive group, if the quotient of `G` by an additive subgroup `H` results in a subsingleton (a set with at most one element), then the additive subgroup `H` must be equal to the entire additive group `G`. In other words, if dividing the group by a subgroup leaves only one distinct coset, then the subgroup must have been the whole group to begin with.
More concisely: If a group `G` has a subgroup `H` such that `G/H` is a subsingleton, then `H = G`.
|
QuotientGroup.eq_one_iff
theorem QuotientGroup.eq_one_iff :
∀ {G : Type u} [inst : Group G] {N : Subgroup G} [nN : N.Normal] (x : G), ↑x = 1 ↔ x ∈ N
This theorem states that for any group `G` and any subgroup `N` of `G` that is normal, an element `x` of `G` satisfies the property that its canonical projection (or quotient) with respect to `N` is the identity element if and only if `x` belongs to `N`. In terms of group theory, it says that the canonical map from `G` to the quotient group `G/N` sends `x` to the identity if and only if `x` is in the kernel of this map, which is `N` itself.
More concisely: For any normal subgroup `N` of a group `G`, an element `x` in `G` maps to the identity in the quotient `G/N` if and only if `x` is in `N`.
|