Yamaguchi Lean 4 Library
ProCGroups/FreeConstructions/Framework.lean
ProCGroups/FreeConstructions/Framework/Source

ProCGroups/FreeConstructions/Framework.lean

1import ProCGroups.FreeProducts.UniversalProperty
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/FreeConstructions/Framework.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Abstract free construction framework
14Provides reusable universal-property infrastructure for free constructions, comparison maps, and uniqueness principles in topological group settings.
15-/
17noncomputable section
19open scoped Cardinal
21universe u v
23namespace ProCGroups.FreeConstructions
25/-- A finite subgroup, stated on an actual subgroup of an actual group. -/
26def IsFiniteSubgroup {G : Type u} [Group G] (H : Subgroup G) : Prop :=
27 Finite H
29/-- A subgroup is conjugate into the image of a homomorphism. -/
30def IsConjugateIntoImage {G A : Type u} [Group G] [Group A]
31 (H : Subgroup G) (ι : A →* G) : Prop :=
32 ∃ g : G, ∀ h : H, ∃ a : A, (h : G) = g * ι a * g⁻¹
34/-- A subgroup is conjugate into a closed continuous image. -/
35def IsConjugateIntoClosedContinuousImage {G A : Type u} [Group G] [Group A]
36 [TopologicalSpace G] [TopologicalSpace A] (H : Subgroup G) (ι : A →ₜ* G) : Prop :=
37 IsClosed (Set.range fun a : A => ι a) ∧ IsConjugateIntoImage H ι.toMonoidHom
39/-- The group is generated by at most `r` elements, expressed by an actual generating map. -/
40def AbstractGeneratorRankLE (G : Type u) [Group G] (r : Nat) : Prop :=
41 ∃ gen : Fin r → G, Subgroup.closure (Set.range gen) = ⊤
43/-- The group is generated by two finite subgroups of coprime orders, each generated by at most
44`r` elements as an abstract group. -/
45def GeneratedByTwoFiniteCoprimeSubgroupsAtRank (G : Type u) [Group G] (r : Nat) : Prop :=
46 ∃ A B : Subgroup G,
47 Finite A ∧ Finite B ∧ Nat.Coprime (Nat.card A) (Nat.card B) ∧
48 Subgroup.closure ((A : Set G) ∪ (B : Set G)) = ⊤ ∧
51/-- An index family has cardinality `s`. -/
52def SubgroupFamilyCardinality {ι : Type v} (s : Nat) : Prop :=
53 Nat.card ι = s
55/-- The subgroups in a family generate the ambient group. -/
56def SubgroupFamilyGenerates {ι : Type v} {G : Type u} [Group G]
57 (F : ι → Subgroup G) : Prop :=
58 Subgroup.closure (Set.iUnion fun i => (F i : Set G)) = ⊤
60/-- Every subgroup in a family is generated by at most `r` elements. -/
61def SubgroupFamilyEachGeneratedByAtMost {ι : Type v} {G : Type u} [Group G]
62 (F : ι → Subgroup G) (r : Nat) : Prop :=
65/-- Amalgamated free pro-`C` product data, with the constituent groups pro-`C` and the
66structural maps recorded as the embeddings used in the book statement. -/
67def AmalgamatedFreeProCProductData (C : ProCGroups.FiniteGroupClass.{u})
68 (G A B H : Type u) [Group G] [Group A] [Group B] [Group H]
69 [TopologicalSpace G] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace H] :
70 Prop :=
71 ProCGroups.ProC.IsProCGroup C H ∧ ProCGroups.ProC.IsProCGroup C A ∧
72 ProCGroups.ProC.IsProCGroup C B ∧ ProCGroups.ProC.IsProCGroup C G ∧
73 ∃ left : H →ₜ* A, ∃ right : H →ₜ* B, ∃ inl : A →ₜ* G, ∃ inr : B →ₜ* G,
74 Function.Injective left ∧ Function.Injective right ∧
75 Function.Injective inl ∧ Function.Injective inr ∧
76 inl.comp left = inr.comp right ∧
77 ∀ {T : Type u} [Group T] [TopologicalSpace T] [IsTopologicalGroup T],
78 ProCGroups.ProC.IsProCGroup C T → (fA : A →ₜ* T) → (fB : B →ₜ* T) →
79 fA.comp left = fB.comp right →
80 ∃! f : G →ₜ* T, f.comp inl = fA ∧ f.comp inr = fB
82end ProCGroups.FreeConstructions