ProCGroups.FreeConstructions.Framework
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
def IsFiniteSubgroup {G : Type u} [Group G] (H : Subgroup G) : Prop :=
Finite HA finite subgroup, formulated on an actual subgroup of an actual group.
def IsConjugateIntoImage {G A : Type u} [Group G] [Group A]
(H : Subgroup G) (ι : A →* G) : Prop :=
∃ g : G, ∀ h : H, ∃ a : A, (h : G) = g * ι a * g⁻¹A subgroup is conjugate into the image of a homomorphism.
def IsConjugateIntoClosedContinuousImage {G A : Type u} [Group G] [Group A]
[TopologicalSpace G] [TopologicalSpace A] (H : Subgroup G) (ι : A →ₜ* G) : Prop :=
IsClosed (Set.range fun a : A => ι a) ∧ IsConjugateIntoImage H ι.toMonoidHomA subgroup is conjugate into a closed continuous image.
def AbstractGeneratorRankLE (G : Type u) [Group G] (r : Nat) : Prop :=
∃ gen : Fin r → G, Subgroup.closure (Set.range gen) = ⊤The group is generated by at most \(r\) elements, expressed by an actual generating map.
def GeneratedByTwoFiniteCoprimeSubgroupsAtRank (G : Type u) [Group G] (r : Nat) : Prop :=
∃ A B : Subgroup G,
Finite A ∧ Finite B ∧ Nat.Coprime (Nat.card A) (Nat.card B) ∧
Subgroup.closure ((A : Set G) ∪ (B : Set G)) = ⊤ ∧
AbstractGeneratorRankLE A r ∧ AbstractGeneratorRankLE B rThe group is generated by two finite subgroups of coprime orders, each generated by at most \(r\) elements as an abstract group.
def SubgroupFamilyCardinality {ι : Type v} (s : Nat) : Prop :=
Nat.card ι = sAn index family has cardinality \(s\).
def SubgroupFamilyGenerates {ι : Type v} {G : Type u} [Group G]
(F : ι → Subgroup G) : Prop :=
Subgroup.closure (Set.iUnion fun i => (F i : Set G)) = ⊤The subgroups in a family generate the ambient group.
def SubgroupFamilyEachGeneratedByAtMost {ι : Type v} {G : Type u} [Group G]
(F : ι → Subgroup G) (r : Nat) : Prop :=
∀ i, AbstractGeneratorRankLE (F i) rEvery subgroup in a family is generated by at most \(r\) elements.
def AmalgamatedFreeProCProductData (C : ProCGroups.FiniteGroupClass.{u})
(G A B H : Type u) [Group G] [Group A] [Group B] [Group H]
[TopologicalSpace G] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace H] :
Prop :=
ProCGroups.ProC.IsProCGroup C H ∧ ProCGroups.ProC.IsProCGroup C A ∧
ProCGroups.ProC.IsProCGroup C B ∧ ProCGroups.ProC.IsProCGroup C G ∧
∃ left : H →ₜ* A, ∃ right : H →ₜ* B, ∃ inl : A →ₜ* G, ∃ inr : B →ₜ* G,
Function.Injective left ∧ Function.Injective right ∧
Function.Injective inl ∧ Function.Injective inr ∧
inl.comp left = inr.comp right ∧
∀ {T : Type u} [Group T] [TopologicalSpace T] [IsTopologicalGroup T],
ProCGroups.ProC.IsProCGroup C T → (fA : A →ₜ* T) → (fB : B →ₜ* T) →
fA.comp left = fB.comp right →
∃! f : G →ₜ* T, f.comp inl = fA ∧ f.comp inr = fBAmalgamated free pro-\(C\) product data, with the constituent groups pro-\(C\) and the structural maps recorded as the embeddings used in the book statement.