Subgroup.commutator_le
theorem Subgroup.commutator_le :
∀ {G : Type u_1} [inst : Group G] {H₁ H₂ H₃ : Subgroup G}, ⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ H₃ := by
sorry
This theorem states that for any type `G` that forms a group with some operation, and for any subgroups `H₁`, `H₂`, and `H₃` of `G`, the commutator subgroup generated by `H₁` and `H₂` is a subset of `H₃` if and only if for every element `g₁` in `H₁` and every element `g₂` in `H₂`, the commutator of `g₁` and `g₂` is an element of `H₃`. The commutator of two elements in a group is defined as the product of the first element and the second, followed by the product of the inverse of the first and the inverse of the second.
More concisely: The commutator subgroup of subgroups H₁ and H₂ in a group G is contained in H₃ if and only if every commutator of an element from H₁ and an element from H₂ belongs to H₃.
|
Subgroup.commutator_commutator_eq_bot_of_rotate
theorem Subgroup.commutator_commutator_eq_bot_of_rotate :
∀ {G : Type u_1} [inst : Group G] {H₁ H₂ H₃ : Subgroup G},
⁅⁅H₂, H₃⁆, H₁⁆ = ⊥ → ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥ → ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥
This theorem is known as "The Three Subgroups Lemma" and it is proven via the Hall-Witt identity. The theorem states that for any type `G` that forms a group, and for any three subgroups `H₁`, `H₂`, and `H₃` of `G`, if the commutator subgroup of the commutator subgroup of `H₂` and `H₃` with `H₁` is the trivial group, and the commutator subgroup of the commutator subgroup of `H₃` and `H₁` with `H₂` is also the trivial group, then the commutator subgroup of the commutator subgroup of `H₁` and `H₂` with `H₃` must also be the trivial group. In other words, if the first two double commutators are trivial, then the third one is also trivial.
More concisely: If the commutator subgroups of `H₂` and `H₃` with `H₁` and the commutator subgroups of `H₃` and `H₁` with `H₂` are both trivial in a group `G`, then the commutator subgroup of `H₁` and `H₂` with `H₃` is also trivial.
|
Subgroup.commutator_pi_pi_of_finite
theorem Subgroup.commutator_pi_pi_of_finite :
∀ {η : Type u_4} [inst : Finite η] {Gs : η → Type u_5} [inst : (i : η) → Group (Gs i)]
(H K : (i : η) → Subgroup (Gs i)),
⁅Subgroup.pi Set.univ H, Subgroup.pi Set.univ K⁆ = Subgroup.pi Set.univ fun i => ⁅H i, K i⁆
The theorem `Subgroup.commutator_pi_pi_of_finite` states that for any finite index set `η`, and any family of groups `Gs : η → Type u_5`, if we have two families of subgroups `H` and `K` indexed by `η`, then the commutator of the direct product group formed by `H` is contained in the direct product of the commutators of `H` and `K`. In other words, if we construct a group as the direct product of a collection of subgroups, then its commutator is equal to the direct product of the commutators of the original subgroups.
Here, `Subgroup.pi Set.univ H` forms a direct product group across all `H` (where `H` is a function from the index set to subgroups), and `⁅H i, K i⁆` denotes the commutator of `H i` and `K i`. Therefore, the theorem says that commutation and direct product operations can be swapped for finite collections of subgroups.
More concisely: For any finite index set η and families Gs : η → Type u\_5 of groups, H and K indexed by η of subgroups, the commutator of their direct product Subgroup.π Set.univ H lies in the direct product of the commutators of the individual subgroups ⁅Hi, Ki⁆.
|
Subgroup.commutator_pi_pi_le
theorem Subgroup.commutator_pi_pi_le :
∀ {η : Type u_4} {Gs : η → Type u_5} [inst : (i : η) → Group (Gs i)] (H K : (i : η) → Subgroup (Gs i)),
⁅Subgroup.pi Set.univ H, Subgroup.pi Set.univ K⁆ ≤ Subgroup.pi Set.univ fun i => ⁅H i, K i⁆
This theorem states that for any index type `η` and a family of group types `Gs : η → Type`, where each `Gs i` is a group, given two families of subgroups `H` and `K` of the groups `Gs i`, the commutator of the product of the subgroups `H` and `K` is contained in the product of the commutators of the subgroups `H i` and `K i` for each `i`. In other words, if you create a subgroup that's the product of the `H` subgroups and another that's the product of the `K` subgroups, then the commutator of these two product subgroups is a subgroup of the product of the individual commutators. A more compact, but less detailed version, would be: "the commutator of the direct product of subgroups is contained within the direct product of the individual commutators".
More concisely: For any index type `η` and families of groups `Gs : η → Type` and subgroups `H` and `K` of `Gs i` for each `i`, the commutator of `H i ⊭ K i` is contained in `(H i ⊭ Ki)⊃ Gs i`, where `⊭` denotes the commutator and `⊃` denotes the subgroup generated by.
|
Subgroup.commutator_mono
theorem Subgroup.commutator_mono :
∀ {G : Type u_1} [inst : Group G] {H₁ H₂ K₁ K₂ : Subgroup G}, H₁ ≤ K₁ → H₂ ≤ K₂ → ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆
This theorem states that for any type `G` equipped with a group structure, and for any four subgroups `H₁`, `H₂`, `K₁`, and `K₂` of `G`, if `H₁` is a subgroup of `K₁` and `H₂` is a subgroup of `K₂`, then the subgroup generated by the commutators of elements in `H₁` and `H₂` is a subgroup of the subgroup generated by the commutators of elements in `K₁` and `K₂`. In notation, if `H₁ ≤ K₁` and `H₂ ≤ K₂`, then `⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆`.
More concisely: If `H₁` is a subgroup of `K₁` and `H₂` is a subgroup of `K₂` in a group `G`, then the subgroup generated by the commutators of elements in `H₁` and `H₂` is contained in the subgroup generated by the commutators of elements in `K₁` and `K₂`.
|
Subgroup.commutator_le_right
theorem Subgroup.commutator_le_right :
∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G) [h : H₂.Normal], ⁅H₁, H₂⁆ ≤ H₂
This theorem states that for any given type `G` that forms a group, and given two subgroups `H₁` and `H₂` of `G`, if `H₂` is a normal subgroup of `G`, then the commutator subgroup generated by `H₁` and `H₂` is a subset of `H₂`. Here, `⁅H₁, H₂⁆` represents the commutator subgroup generated by `H₁` and `H₂`, and the sign `≤` denotes subgroup inclusion.
More concisely: If `H₁` and `H₂` are subgroups of a group `G` with `H₂` normal in `G`, then `⁅H₁, H₂⁆ ≤ H₂`.
|
Subgroup.commutator_mem_commutator
theorem Subgroup.commutator_mem_commutator :
∀ {G : Type u_1} [inst : Group G] {g₁ g₂ : G} {H₁ H₂ : Subgroup G}, g₁ ∈ H₁ → g₂ ∈ H₂ → ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆ := by
sorry
This theorem states that for any type `G` that is a group, given two elements `g₁` and `g₂` of `G` and two subgroups `H₁` and `H₂` of `G`, if `g₁` is in `H₁` and `g₂` is in `H₂`, then the commutator (denoted by `⁅ , ⁆`) of `g₁` and `g₂` is in the commutator subgroup of `H₁` and `H₂`. In more mathematical terms: for all groups G, all elements g₁, g₂ in G, and all subgroups H₁, H₂ of G, if g₁ is in H₁ and g₂ is in H₂, then the element resulting from the group commutator operation with g₁ and g₂ is an element of the subgroup resulting from the commutator operation with H₁ and H₂.
More concisely: For any groups G, subgroups H₁ and H₂, and elements g₁ in H₁ and g₂ in H₂, the commutator [g₁, g₂] lies in the subgroup generated by the commutators of elements from H₁ and H₂.
|
Subgroup.map_commutator
theorem Subgroup.map_commutator :
∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H₁ H₂ : Subgroup G) (f : G →* G'),
Subgroup.map f ⁅H₁, H₂⁆ = ⁅Subgroup.map f H₁, Subgroup.map f H₂⁆
The theorem `Subgroup.map_commutator` states that for any two subgroups `H₁` and `H₂` of a group `G`, and any group homomorphism `f` from `G` to another group `G'`, the image of the commutator subgroup of `H₁` and `H₂` under `f` is equal to the commutator subgroup of the images of `H₁` and `H₂` under `f`. In other words, map operation commutes with the commutator operation in the context of subgroups and group homomorphisms.
More concisely: For any group homomorphism $f$ and subgroups $H\_1$ and $H\_2$ of a group $G$, we have $[[H\_1, H\_2]] = [f(H\_1), f(H\_2)]$, where $[[.,.]]$ denotes the commutator subgroup.
|
Commute.commutator_eq
theorem Commute.commutator_eq : ∀ {G : Type u_1} [inst : Group G] {g₁ g₂ : G}, Commute g₁ g₂ → ⁅g₁, g₂⁆ = 1
The theorem `Commute.commutator_eq` states that for any type `G` that forms a group (denoted by `[inst : Group G]`), for any two elements `g₁` and `g₂` of type `G`, if `g₁` and `g₂` commute (as defined by the `Commute` definition, i.e., `g₁ * g₂ = g₂ * g₁`), then their group commutator (denoted by `⁅g₁, g₂⁆`), is equal to the identity element of the group `1`. In mathematical notation, for all `g₁, g₂` in a group `G`, if `g₁ * g₂ = g₂ * g₁`, then `⁅g₁, g₂⁆ = 1`. Here, `⁅g₁, g₂⁆` represents the group commutator of `g₁` and `g₂`, defined as `g₁ * g₂ * g₁⁻¹ * g₂⁻¹`.
More concisely: In a group `G`, if `g₁` and `g₂` commute (i.e., `g₁ * g₂ = g₂ * g₁`), then their group commutator `[g₁, g₂] = g₁ * g₂ * g₁⁻¹ * g₂⁻¹` equals the identity element `1`.
|