ProCGroups/FreeConstructions/AmalgamsAndModules.lean
1import Mathlib.GroupTheory.PGroup
2import Mathlib.GroupTheory.Solvable
3import ProCGroups.FreeConstructions.Framework
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/FreeConstructions/AmalgamsAndModules.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Abstract free construction framework
16Provides reusable universal-property infrastructure for free constructions, comparison maps, and uniqueness principles in topological group settings.
17-/
19noncomputable section
21namespace ProCGroups.FreeConstructions
23universe u
25variable {G A B H : Type u} [Group G] [Group A] [Group B] [Group H]
26variable [TopologicalSpace G] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace H]
27variable [IsTopologicalGroup G] [IsTopologicalGroup A] [IsTopologicalGroup B] [IsTopologicalGroup H]
29omit [TopologicalSpace G] [IsTopologicalGroup G] in
30/-- A finite nontrivial `p`-group has a nontrivial central element. This is the group-theoretic
33 (p : ℕ) [Fact p.Prime] (N : Subgroup G) :
34 IsFiniteSubgroup N → Nontrivial N → IsPGroup p N →
35 ∃ z : N, z ≠ 1 ∧ z ∈ Subgroup.center N := by
36 intro hfinite hnontrivial hpN
37 letI : Finite N := hfinite
38 letI : Nontrivial N := hnontrivial
39 have hcenter : Nontrivial (Subgroup.center N) := IsPGroup.center_nontrivial hpN
40 obtain ⟨z, hz⟩ := exists_ne (1 : Subgroup.center N)
41 exact ⟨z.1, fun hz1 => hz (Subtype.ext hz1), z.2⟩
43omit [IsTopologicalGroup G] [IsTopologicalGroup A] [IsTopologicalGroup B] [IsTopologicalGroup H] in
44/-- If an amalgamated free pro-`C` product embeds both factors into a solvable group `G`, then
45the factors are solvable. -/
46theorem solvable_amalgam_criterion
47 (C : ProCGroups.FiniteGroupClass.{u}) :
48 AmalgamatedFreeProCProductData C G A B H →
49 IsSolvable G → IsSolvable A ∧ IsSolvable B := by
50 intro hprod hG
51 rcases hprod with
52 ⟨_, _, _, _, left, right, inl, inr, _hleft, _hright, hinl, hinr, _hcompat, _huniv⟩
53 letI : IsSolvable G := hG
54 exact
55 ⟨solvable_of_solvable_injective (f := inl.toMonoidHom) hinl,
56 solvable_of_solvable_injective (f := inr.toMonoidHom) hinr⟩
58end ProCGroups.FreeConstructions