Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.Definitions
1import ProCGroups.InverseSystems.FiniteStageFactorization
3/-!
4# Bundled profinite rings and modules
6This file defines profinite rings, commutative profinite coefficient rings, and profinite modules.
7It also states their free-extension, discreteness, and finite-index submodule-basis properties.
8-/
10open scoped Topology
12namespace CompletedGroupAlgebra
14universe u v w z
16/-- A profinite ring object. Its standard algebraic and topological structures are stored once on
17the carrier. -/
18structure ProfiniteRing where
19 /-- The underlying profinite space. -/
20 toProfinite : Profinite.{u}
21 /-- The ring structure on the underlying profinite space. -/
22 [ring : Ring toProfinite]
23 /-- The assertion that the ring operations are continuous. -/
24 [isTopologicalRing : IsTopologicalRing toProfinite]
26attribute [instance] ProfiniteRing.ring ProfiniteRing.isTopologicalRing
28namespace ProfiniteRing
30/-- A bundled profinite ring coerces to its underlying profinite type. -/
31instance : CoeSort ProfiniteRing.{u} (Type u) where
32 coe Λ := Λ.toProfinite
34end ProfiniteRing
36/-- A commutative profinite ring, used as the coefficient object for completed group algebras.
37The completed algebra itself may be noncommutative and therefore uses `ProfiniteRing`. This
38separate bundle avoids installing a second `Ring` instance on `ProfiniteRing`. -/
39structure ProfiniteCommRing where
40 /-- The underlying profinite space. -/
41 toProfinite : Profinite.{u}
42 /-- The commutative ring structure on the underlying profinite space. -/
43 [commRing : CommRing toProfinite]
44 /-- The assertion that the ring operations are continuous. -/
45 [isTopologicalRing : IsTopologicalRing toProfinite]
47attribute [instance] ProfiniteCommRing.commRing ProfiniteCommRing.isTopologicalRing
49namespace ProfiniteCommRing
51/-- A bundled profinite commutative ring coerces to its underlying profinite type. -/
52instance : CoeSort ProfiniteCommRing.{u} (Type u) where
53 coe R := R.toProfinite
55/-- Forget commutativity while retaining the bundled profinite ring object. -/
56def toProfiniteRing (R : ProfiniteCommRing.{u}) : ProfiniteRing.{u} where
57 toProfinite := R.toProfinite
58 ring := inferInstance
59 isTopologicalRing := inferInstance
61end ProfiniteCommRing
63/-- A topological module over a topological ring. -/
64def IsTopologicalModuleOver (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ]
65 [AddCommGroup M] [TopologicalSpace M] [Module Λ M] : Prop :=
66 IsTopologicalRing Λ ∧ IsTopologicalAddGroup M ∧ ContinuousSMul Λ M
68/-- A profinite module object over a fixed profinite ring. -/
69structure ProfiniteModule (Λ : ProfiniteRing.{u}) where
70 /-- The underlying profinite space. -/
71 toProfinite : Profinite.{v}
72 /-- The additive commutative group structure on the underlying profinite space. -/
73 [addCommGroup : AddCommGroup toProfinite]
74 /-- The \(\Lambda\)-module structure on the underlying profinite space. -/
75 [module : Module Λ toProfinite]
76 /-- The assertion that addition and negation are continuous. -/
77 [isTopologicalAddGroup : IsTopologicalAddGroup toProfinite]
78 /-- The assertion that scalar multiplication by \(\Lambda\) is jointly continuous. -/
79 [continuousSMul : ContinuousSMul Λ toProfinite]
81attribute [instance] ProfiniteModule.addCommGroup
82attribute [instance] ProfiniteModule.module
83attribute [instance] ProfiniteModule.isTopologicalAddGroup
84attribute [instance] ProfiniteModule.continuousSMul
86namespace ProfiniteModule
88/-- A bundled profinite module coerces to its underlying profinite type. -/
89instance (Λ : ProfiniteRing.{u}) : CoeSort (ProfiniteModule.{u, v} Λ) (Type v) where
90 coe M := M.toProfinite
92/-- The extension-and-uniqueness property from a candidate free profinite module to one bundled
93target. Keeping the target as an argument makes this API universe-polymorphic without `ULift`. -/
94def HasFreeLiftTo {Λ : ProfiniteRing.{u}} (M : ProfiniteModule.{u, w} Λ)
95 (X : Type v) [TopologicalSpace X] (ι : X → M)
96 (N : ProfiniteModule.{u, z} Λ) : Prop :=
97 ∀ f : X → N, Continuous f →
98 ∃! F : M →L[Λ] N, ∀ x : X, F (ι x) = f x
100/-- Universal-property predicate for a free profinite module in a fixed ambient universe.
101Cross-universe targets use `HasFreeLiftTo` directly. The scalar, generator, and source/target
102modules are bundled objects, so their profiniteness is part of the statement. -/
103def IsFreeOn {Λ : ProfiniteRing.{u}} (M : ProfiniteModule.{u, w} Λ)
104 (X : Profinite.{v}) (ι : X → M) : Prop :=
105 Continuous ι ∧
106 closure (Submodule.span Λ (Set.range ι) : Set M) = Set.univ ∧
107 ∀ N : ProfiniteModule.{u, w} Λ, HasFreeLiftTo M X ι N
109end ProfiniteModule
111/-- A topological module whose underlying module topology is discrete. -/
112def IsDiscreteModule (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ]
113 [AddCommGroup M] [TopologicalSpace M] [Module Λ M] : Prop :=
114 IsTopologicalModuleOver Λ M ∧ DiscreteTopology M
116/-- Finite-index submodules form a neighborhood basis at zero. -/
117def HasFiniteIndexSubmoduleBasis (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace M]
118 [AddCommGroup M] [Module Λ M] : Prop :=
119 ∀ U ∈ 𝓝 (0 : M), ∃ N : Submodule Λ M,
120 IsOpen (N : Set M) ∧ (N : Set M) ⊆ U ∧ Nonempty (Fintype (M ⧸ N))
122end CompletedGroupAlgebra