Yamaguchi Lean 4 Library
CompletedGroupAlgebra/ProfiniteModules/Basic/Definitions.lean
CompletedGroupAlgebra/ProfiniteModules/Basic/Definitions/Source

CompletedGroupAlgebra/ProfiniteModules/Basic/Definitions.lean

1import ProCGroups.InverseSystems.FiniteStageFactorization
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/ProfiniteModules/Basic/Definitions.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Basic predicates for profinite modules
13-/
15open scoped Topology
19universe u v w z
21/-- A compact Hausdorff totally disconnected topological ring. -/
22def IsProfiniteRing (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] : Prop :=
23 IsTopologicalRing Λ ∧ CompactSpace Λ ∧ T2Space Λ ∧ TotallyDisconnectedSpace Λ
27variable {Λ : Type u} [Ring Λ] [TopologicalSpace Λ]
29/-- The topological-ring component of a profinite ring. -/
30theorem isTopologicalRing (hΛ : IsProfiniteRing Λ) : IsTopologicalRing Λ :=
31 hΛ.1
33/-- The compactness component of a profinite ring. -/
34theorem compactSpace (hΛ : IsProfiniteRing Λ) : CompactSpace Λ :=
35 hΛ.2.1
37/-- The Hausdorff component of a profinite ring. -/
38theorem t2Space (hΛ : IsProfiniteRing Λ) : T2Space Λ :=
39 hΛ.2.2.1
41/-- The `T1` component of a profinite ring. -/
42theorem t1Space (hΛ : IsProfiniteRing Λ) : T1Space Λ := by
43 letI : T2Space Λ := hΛ.t2Space
44 infer_instance
46/-- The totally disconnected component of a profinite ring. -/
47theorem totallyDisconnectedSpace (hΛ : IsProfiniteRing Λ) : TotallyDisconnectedSpace Λ :=
48 hΛ.2.2.2
50/-- The underlying topological space of a profinite ring is profinite. -/
51theorem isProfiniteSpace (hΛ : IsProfiniteRing Λ) :
53 ⟨hΛ.compactSpace, hΛ.t2Space, hΛ.totallyDisconnectedSpace⟩
57/-- A topological module over a topological ring. -/
58def IsTopologicalModuleOver (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ]
59 [AddCommGroup M] [TopologicalSpace M] [Module Λ M] : Prop :=
60 IsTopologicalRing Λ ∧ IsTopologicalAddGroup M ∧ ContinuousSMul Λ M
62/-- A profinite module over a profinite ring.
64This predicate is intentionally a `Prop`, not a typeclass. The bundled public object for data
65APIs is `ProfiniteModule`; theorem statements may keep taking explicit
66`hM : IsProfiniteModule Λ M` hypotheses. -/
67def IsProfiniteModule (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ]
68 [AddCommGroup M] [TopologicalSpace M] [Module Λ M] : Prop :=
69 IsProfiniteRing Λ ∧ IsTopologicalAddGroup M ∧ ContinuousSMul Λ M ∧
70 CompactSpace M ∧ T2Space M ∧ TotallyDisconnectedSpace M
72/-- The universal property of the free profinite module on a profinite space.
74This is a minimal public interface used by the completed group algebra universal property. The
75larger construction libraries live outside the public completed-group-algebra root. -/
76def IsFreeProfiniteModuleOn (Λ : Type u) (X : Type v) (M : Type w)
77 [Ring Λ] [TopologicalSpace Λ] [TopologicalSpace X] [AddCommGroup M] [TopologicalSpace M]
78 [Module Λ M] (ι : X -> M) : Prop :=
79 IsProfiniteRing Λ ∧ IsProfiniteModule Λ M ∧ Continuous ι ∧
80 closure (Submodule.span Λ (Set.range ι) : Set M) = Set.univ ∧
81 ∀ (N : Type w) [AddCommGroup N] [TopologicalSpace N] [Module Λ N],
83 ∀ f : X -> N, Continuous f →
84 ∃! F : M →L[Λ] N, ∀ x : X, F (ι x) = f x
86/-- Pointed version of `IsFreeProfiniteModuleOn`, with the base point mapped to zero. -/
87def IsFreeProfiniteModuleOnPointed (Λ : Type u) (X : Type v) (M : Type w)
88 [Ring Λ] [TopologicalSpace Λ] [TopologicalSpace X] [AddCommGroup M] [TopologicalSpace M]
89 [Module Λ M] (base : X) (ι : X -> M) : Prop :=
90 IsProfiniteRing Λ ∧ IsProfiniteModule Λ M ∧ Continuous ι ∧ ι base = 0 ∧
91 closure (Submodule.span Λ (Set.range ι) : Set M) = Set.univ ∧
92 ∀ (N : Type w) [AddCommGroup N] [TopologicalSpace N] [Module Λ N],
94 ∀ f : X -> N, Continuous f → f base = 0 →
95 ∃! F : M →L[Λ] N, ∀ x : X, F (ι x) = f x
97/-- Bundled profinite modules over a fixed profinite ring.
99Use this when a public data structure should carry a profinite module as an object rather than
100separate carrier, instances, and `IsProfiniteModule` proof fields. -/
101structure ProfiniteModule (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] where
102 carrier : Type v
103 [addCommGroup : AddCommGroup carrier]
104 [topologicalSpace : TopologicalSpace carrier]
105 [module : Module Λ carrier]
106 isProfinite : IsProfiniteModule Λ carrier
108attribute [instance] ProfiniteModule.addCommGroup
109attribute [instance] ProfiniteModule.topologicalSpace
110attribute [instance] ProfiniteModule.module
114variable {Λ : Type u} {M : Type v} [Ring Λ] [TopologicalSpace Λ]
115 [AddCommGroup M] [TopologicalSpace M] [Module Λ M]
117/-- The profinite-ring component of a profinite module. -/
119 hM.1
121/-- The additive topological-group component of a profinite module. -/
122theorem isTopologicalAddGroup (hM : IsProfiniteModule Λ M) : IsTopologicalAddGroup M :=
123 hM.2.1
125/-- The continuous scalar-action component of a profinite module. -/
126theorem continuousSMul (hM : IsProfiniteModule Λ M) : ContinuousSMul Λ M :=
127 hM.2.2.1
129/-- The compactness component of a profinite module. -/
130theorem compactSpace (hM : IsProfiniteModule Λ M) : CompactSpace M :=
131 hM.2.2.2.1
133/-- The Hausdorff component of a profinite module. -/
134theorem t2Space (hM : IsProfiniteModule Λ M) : T2Space M :=
135 hM.2.2.2.2.1
137/-- The `T1` component of a profinite module. -/
138theorem t1Space (hM : IsProfiniteModule Λ M) : T1Space M := by
139 letI : T2Space M := hM.t2Space
140 infer_instance
142/-- The totally disconnected component of a profinite module. -/
143theorem totallyDisconnectedSpace (hM : IsProfiniteModule Λ M) :
144 TotallyDisconnectedSpace M :=
145 hM.2.2.2.2.2
147/-- A profinite module is a topological module over its scalar ring. -/
150 ⟨hM.isProfiniteRing.isTopologicalRing, hM.isTopologicalAddGroup, hM.continuousSMul⟩
152/-- The underlying topological space of a profinite module is profinite. -/
153theorem isProfiniteSpace (hM : IsProfiniteModule Λ M) :
155 ⟨hM.compactSpace, hM.t2Space, hM.totallyDisconnectedSpace⟩
159/-- A discrete topological module. -/
160def IsDiscreteModule (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ]
161 [AddCommGroup M] [TopologicalSpace M] [Module Λ M] : Prop :=
162 IsTopologicalModuleOver Λ M ∧ DiscreteTopology M
164/-- A submodule whose underlying set is finite. -/
165def IsFiniteSubmodule {Λ : Type u} {M : Type v} [Ring Λ] [AddCommGroup M] [Module Λ M]
166 (N : Submodule Λ M) : Prop :=
167 (N : Set M).Finite
169/-- Every element lies in a finite submodule. -/
170def IsUnionOfFiniteSubmodules (Λ : Type u) (M : Type v) [Ring Λ] [AddCommGroup M]
171 [Module Λ M] : Prop :=
172 ∀ m : M, ∃ N : Submodule Λ M, IsFiniteSubmodule N ∧ m ∈ N
174/-- Finite-index submodules form a neighborhood basis at zero. -/
175def HasFiniteIndexSubmoduleBasis (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace M]
176 [AddCommGroup M] [Module Λ M] : Prop :=
177 ∀ U ∈ 𝓝 (0 : M), ∃ N : Submodule Λ M,
178 IsOpen (N : Set M) ∧ (N : Set M) ⊆ U ∧ Nonempty (Fintype (M ⧸ N))
180/-- A profinite module is represented by its finite quotient modules. -/
181def IsInverseLimitOfFiniteQuotientModules (Λ : Type u) (M : Type v) [Ring Λ]
182 [TopologicalSpace M] [AddCommGroup M] [Module Λ M] : Prop :=
184 ∀ U ∈ 𝓝 (0 : M), ∃ N : Submodule Λ M,
185 IsOpen (N : Set M) ∧ (N : Set M) ⊆ U ∧ Nonempty (Fintype (M ⧸ N))
187/-- Lemma 5.1.1(b), predicate form: in this development the inverse-limit formulation is recorded
188by a finite-index open-submodule basis at zero. -/
190 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace M] [AddCommGroup M]
191 [Module Λ M] :
193 constructor
194 · intro h
195 exact h.1
196 · intro h
197 exact ⟨h, h⟩