Source: ProCGroups.FreeProC.FiniteRankSourceData
1import ProCGroups.FreeProC.FiniteBasis
3/-!
4# Finite-rank free pro-C source data
6This module packages a finite-rank epimorphically free pro-\(C\) group as the canonical
7source-data structure and records the cardinality of its lifted finite basis.
8-/
10namespace CrowellExactSequence
12universe u
14variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
15variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
17/-- Package a finite-rank epimorphically free pro-\(\Sigma\) group using the canonical
18ProCGroups source-data structure. -/
19noncomputable def finiteRank_epimorphicallyFreeProCSourceData
20 {sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
22 (C := (ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
23 (Fin r) F X) :
24 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
25 (ProCGroups.FiniteGroupClass.sigmaGroup sigma) := by
26 exact
27 { basis := ULift.{u} (Fin r)
28 carrier := ProCGrp.of
29 (ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma)
30 (ProfiniteGrp.of F) hFree.hasOpenNormalBasisInClass
31 inclusion := fun i => X i.down
32 isEpimorphicallyFree := by
33 refine ⟨hFree.hasOpenNormalBasisInClass, ?_, ?_, ?_⟩
34 · exact
36 (G := F) (fun i : ULift.{u} (Fin r) => X i.down)
37 · have hrange :
38 Set.range (fun i : ULift.{u} (Fin r) => X i.down) =
39 Set.range X := by
40 ext x
41 constructor
42 · rintro ⟨i, rfl⟩
43 exact ⟨i.down, rfl⟩
44 · rintro ⟨i, rfl⟩
45 exact ⟨ULift.up i, rfl⟩
46 change
48 (G := F) (Set.range (fun i : ULift.{u} (Fin r) => X i.down))
49 rw [hrange]
50 exact hFree.generates_range
51 · intro G _ _ _ _ _ _ hG φ _hφ hgen
52 let φFin : Fin r → G := fun i => φ (ULift.up i)
53 have hφFinConv :
55 (G := G) φFin :=
57 have hφFinGen :
59 (G := G) (Set.range φFin) := by
60 have hrange : Set.range φFin = Set.range φ := by
61 ext g
62 constructor
63 · rintro ⟨i, rfl⟩
64 exact ⟨ULift.up i, rfl⟩
65 · rintro ⟨i, rfl⟩
66 exact ⟨i.down, by cases i; rfl⟩
67 rw [hrange]
68 exact hgen
69 rcases hFree.existsUnique_lift hG φFin hφFinConv hφFinGen with
70 ⟨f, hf, huniq⟩
71 refine ⟨f, ⟨hf.1, ?_⟩, ?_⟩
72 · intro i
73 cases i with
74 | up i => exact hf.2 i
75 · intro g hg
76 apply huniq
77 refine ⟨hg.1, ?_⟩
78 intro i
79 exact hg.2 (ULift.up i) }
81/-- The finite-rank free pro-\(C\) source data has the expected basis cardinality. -/
82theorem finiteRank_epimorphicallyFreeProCSourceData_basis_card
83 {sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
85 (C := (ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
86 (Fin r) F X) :
87 Cardinal.mk (finiteRank_epimorphicallyFreeProCSourceData (F := F) X hFree).basis = r := by
88 simp only [finiteRank_epimorphicallyFreeProCSourceData, Cardinal.mk_fintype, Fintype.card_ulift,
89 Fintype.card_fin]
91end CrowellExactSequence