solvable_of_ker_le_range
theorem solvable_of_ker_le_range :
∀ {G : Type u_1} [inst : Group G] {G' : Type u_3} {G'' : Type u_4} [inst_1 : Group G'] [inst_2 : Group G'']
(f : G' →* G) (g : G →* G''), g.ker ≤ f.range → ∀ [hG' : IsSolvable G'] [hG'' : IsSolvable G''], IsSolvable G
The theorem `solvable_of_ker_le_range` asserts that for any three groups `G`, `G'`, and `G''`, and any two group homomorphisms `f: G' -> G` and `g: G -> G''`, if the kernel of `g` is a subset of the range of `f`, then if `G'` and `G''` are solvable, it follows that `G` is also solvable. Here, a group is solvable if it has a series of normal subgroups such that each factor group is abelian.
More concisely: If groups G, G', and G'' have homomorphisms f : G' -> G and g : G -> G'' such that the kernel of g is contained in the image of f, and G' and G'' are solvable, then so is G.
|
IsSolvable.solvable
theorem IsSolvable.solvable : ∀ {G : Type u_1} [inst : Group G] [self : IsSolvable G], ∃ n, derivedSeries G n = ⊥ := by
sorry
The theorem `IsSolvable.solvable` states that a group `G` is considered solvable if there exists a number `n` such that the `n`th term of the derived series of `G` is the trivial subgroup. The derived series of `G` is a sequence of subgroups obtained by starting with the entire group `G` and repeatedly taking the commutator of the previous subgroup with itself. In the context of the theorem, a group is solvable if this process eventually yields the trivial subgroup, which consists of only the identity element.
More concisely: A group is solvable if and only if its derived series reaches the identity subgroup after a finite number of steps.
|
solvable_of_solvable_injective
theorem solvable_of_solvable_injective :
∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'},
Function.Injective ⇑f → ∀ [inst_2 : IsSolvable G'], IsSolvable G
The theorem `solvable_of_solvable_injective` states that for any two types `G` and `G'` that have a group structure, if there is an injective group homomorphism `f` from `G` to `G'`, and if the group `G'` is solvable, then the group `G` is also solvable. This theorem is essentially saying that the solvability of a group is preserved under injective homomorphisms.
More concisely: If `f` is an injective group homomorphism from the solvable group `G` to `G'`, then `G` is also a solvable group.
|
solvable_of_surjective
theorem solvable_of_surjective :
∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'},
Function.Surjective ⇑f → ∀ [inst : IsSolvable G], IsSolvable G'
The theorem `solvable_of_surjective` states that for all types `G` and `G'`, where `G` and `G'` are groups (denoted by `[inst : Group G]` and `[inst_1 : Group G']` respectively), if there exists a surjective group homomorphism `f` from `G` to `G'` (symbolized by `Function.Surjective ⇑f`), then if `G` is solvable (expressed by `[inst : IsSolvable G]`), it implies that `G'` is also solvable (denoted by `IsSolvable G'`). In simpler terms, if a group `G` mapping onto a group `G'` through a surjective group homomorphism is solvable, then `G'` is also solvable.
More concisely: If `G` is a solvable group and `f` is a surjective group homomorphism from `G` to `G'`, then `G'` is also a solvable group.
|