CompletedGroupAlgebra.ProfiniteModules.Basic.Definitions
This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.
def IsProfiniteRing (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] : Prop :=
IsTopologicalRing Λ ∧ CompactSpace Λ ∧ T2Space Λ ∧ TotallyDisconnectedSpace ΛA compact Hausdorff totally disconnected topological ring.
theorem isTopologicalRing (hΛ : IsProfiniteRing Λ) : IsTopologicalRing ΛA profinite ring carries a topological ring structure.
Show proof
hΛ.1Proof. Work with open ideals at zero in the compact Hausdorff totally disconnected topological ring. Open ideals form the linear neighborhood basis, and quotienting by an open ideal gives a finite discrete ring or module. Ring operations, scalar actions, and quotient maps are continuous and compatible with refinement, so the finite-quotient and inverse-limit statements follow from the open-ideal basis.
□theorem compactSpace (hΛ : IsProfiniteRing Λ) : CompactSpace ΛThe compact-space instance on a profinite ring.
Show proof
hΛ.2.1Proof. Work with open ideals at zero in the compact Hausdorff totally disconnected topological ring. Open ideals form the linear neighborhood basis, and quotienting by an open ideal gives a finite discrete ring or module. Ring operations, scalar actions, and quotient maps are continuous and compatible with refinement, so the finite-quotient and inverse-limit statements follow from the open-ideal basis.
□theorem t2Space (hΛ : IsProfiniteRing Λ) : T2Space ΛThe Hausdorff space structure on a profinite ring.
Show proof
hΛ.2.2.1Proof. Work with open ideals at zero in the compact Hausdorff totally disconnected topological ring. Open ideals form the linear neighborhood basis, and quotienting by an open ideal gives a finite discrete ring or module. Ring operations, scalar actions, and quotient maps are continuous and compatible with refinement, so the finite-quotient and inverse-limit statements follow from the open-ideal basis.
□theorem t1Space (hΛ : IsProfiniteRing Λ) : T1Space ΛA profinite ring is \(T_1\).
Show proof
by
letI : T2Space Λ := hΛ.t2Space
infer_instanceProof. Work with open ideals at zero in the compact Hausdorff totally disconnected topological ring. Open ideals form the linear neighborhood basis, and quotienting by an open ideal gives a finite discrete ring or module. Ring operations, scalar actions, and quotient maps are continuous and compatible with refinement, so the finite-quotient and inverse-limit statements follow from the open-ideal basis.
□theorem totallyDisconnectedSpace (hΛ : IsProfiniteRing Λ) : TotallyDisconnectedSpace ΛA profinite ring is totally disconnected as a topological space.
Show proof
hΛ.2.2.2Proof. Work with open ideals at zero in the compact Hausdorff totally disconnected topological ring. Open ideals form the linear neighborhood basis, and quotienting by an open ideal gives a finite discrete ring or module. Ring operations, scalar actions, and quotient maps are continuous and compatible with refinement, so the finite-quotient and inverse-limit statements follow from the open-ideal basis.
□theorem isProfiniteSpace (hΛ : IsProfiniteRing Λ) :
ProCGroups.InverseSystems.IsProfiniteSpace ΛThe underlying topological space of a profinite ring is profinite.
Show proof
⟨hΛ.compactSpace, hΛ.t2Space, hΛ.totallyDisconnectedSpace⟩Proof. Work with open ideals at zero in the compact Hausdorff totally disconnected topological ring. Open ideals form the linear neighborhood basis, and quotienting by an open ideal gives a finite discrete ring or module. Ring operations, scalar actions, and quotient maps are continuous and compatible with refinement, so the finite-quotient and inverse-limit statements follow from the open-ideal basis.
□def IsTopologicalModuleOver (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ]
[AddCommGroup M] [TopologicalSpace M] [Module Λ M] : Prop :=
IsTopologicalRing Λ ∧ IsTopologicalAddGroup M ∧ ContinuousSMul Λ MA topological module over a topological ring.
def IsProfiniteModule (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ]
[AddCommGroup M] [TopologicalSpace M] [Module Λ M] : Prop :=
IsProfiniteRing Λ ∧ IsTopologicalAddGroup M ∧ ContinuousSMul Λ M ∧
CompactSpace M ∧ T2Space M ∧ TotallyDisconnectedSpace MA profinite module over a profinite ring. This predicate is intentionally a Prop, not a typeclass. The bundled public object for data formulations is ProfiniteModule; theorem statements may keep taking explicit hM: IsProfiniteModule \(\Lambda\) M hypotheses.
def IsFreeProfiniteModuleOn (Λ : Type u) (X : Type v) (M : Type w)
[Ring Λ] [TopologicalSpace Λ] [TopologicalSpace X] [AddCommGroup M] [TopologicalSpace M]
[Module Λ M] (ι : X -> M) : Prop :=
IsProfiniteRing Λ ∧ IsProfiniteModule Λ M ∧ Continuous ι ∧
closure (Submodule.span Λ (Set.range ι) : Set M) = Set.univ ∧
∀ (N : Type w) [AddCommGroup N] [TopologicalSpace N] [Module Λ N],
IsProfiniteModule Λ N →
∀ f : X -> N, Continuous f →
∃! F : M →L[Λ] N, ∀ x : X, F (ι x) = f xThe universal property of the free profinite module on a profinite space. This is a minimal public interface used by the completed group algebra universal property. The larger construction libraries live outside the public completed-group-algebra root.
def IsFreeProfiniteModuleOnPointed (Λ : Type u) (X : Type v) (M : Type w)
[Ring Λ] [TopologicalSpace Λ] [TopologicalSpace X] [AddCommGroup M] [TopologicalSpace M]
[Module Λ M] (base : X) (ι : X -> M) : Prop :=
IsProfiniteRing Λ ∧ IsProfiniteModule Λ M ∧ Continuous ι ∧ ι base = 0 ∧
closure (Submodule.span Λ (Set.range ι) : Set M) = Set.univ ∧
∀ (N : Type w) [AddCommGroup N] [TopologicalSpace N] [Module Λ N],
IsProfiniteModule Λ N →
∀ f : X -> N, Continuous f → f base = 0 →
∃! F : M →L[Λ] N, ∀ x : X, F (ι x) = f xThis is the pointed version of IsFreeProfiniteModuleOn, with the base point mapped to zero.
structure ProfiniteModule (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] where
carrier : Type v
[addCommGroup : AddCommGroup carrier]
[topologicalSpace : TopologicalSpace carrier]
[module : Module Λ carrier]
isProfinite : IsProfiniteModule Λ carrierThis structure bundles profinite modules over a fixed profinite ring. Use this when a public data structure should carry a profinite module as an object rather than as separate carrier data, instances, and \(IsProfiniteModule\) proof fields.
theorem isProfiniteRing (hM : IsProfiniteModule Λ M) : IsProfiniteRing ΛThe scalar ring of a profinite module is a profinite ring.
Show proof
hM.1Proof. Work in the linear topology of the profinite module. Open submodules form the neighborhoods of zero, and quotienting by an open submodule gives a finite discrete module. Separation, continuity, and inverse-limit claims are checked after all open-submodule quotients. Compactness, Hausdorffness, and total disconnectedness come from the profinite-module hypotheses, while scalar compatibility follows from continuity of the module action and from passing to sufficiently small open submodules stable under the finite set of scalars involved.
□theorem isTopologicalAddGroup (hM : IsProfiniteModule Λ M) : IsTopologicalAddGroup MThe additive group of a profinite module is a topological group.
Show proof
hM.2.1Proof. Work in the linear topology of the profinite module. Open submodules form the neighborhoods of zero, and quotienting by an open submodule gives a finite discrete module. Separation, continuity, and inverse-limit claims are checked after all open-submodule quotients. Compactness, Hausdorffness, and total disconnectedness come from the profinite-module hypotheses, while scalar compatibility follows from continuity of the module action and from passing to sufficiently small open submodules stable under the finite set of scalars involved.
□theorem continuousSMul (hM : IsProfiniteModule Λ M) : ContinuousSMul Λ MThe scalar action of a profinite module is continuous.
Show proof
hM.2.2.1Proof. Work in the linear topology of the profinite module. Open submodules form the neighborhoods of zero, and quotienting by an open submodule gives a finite discrete module. Separation, continuity, and inverse-limit claims are checked after all open-submodule quotients. Compactness, Hausdorffness, and total disconnectedness come from the profinite-module hypotheses, while scalar compatibility follows from continuity of the module action and from passing to sufficiently small open submodules stable under the finite set of scalars involved.
□theorem compactSpace (hM : IsProfiniteModule Λ M) : CompactSpace MThe compact-space instance on a profinite module.
Show proof
hM.2.2.2.1Proof. Work in the linear topology of the profinite module. Open submodules form the neighborhoods of zero, and quotienting by an open submodule gives a finite discrete module. Separation, continuity, and inverse-limit claims are checked after all open-submodule quotients. Compactness, Hausdorffness, and total disconnectedness come from the profinite-module hypotheses, while scalar compatibility follows from continuity of the module action and from passing to sufficiently small open submodules stable under the finite set of scalars involved.
□theorem t2Space (hM : IsProfiniteModule Λ M) : T2Space MThe Hausdorff space structure on a profinite module.
Show proof
hM.2.2.2.2.1Proof. Work in the linear topology of the profinite module. Open submodules form the neighborhoods of zero, and quotienting by an open submodule gives a finite discrete module. Separation, continuity, and inverse-limit claims are checked after all open-submodule quotients. Compactness, Hausdorffness, and total disconnectedness come from the profinite-module hypotheses, while scalar compatibility follows from continuity of the module action and from passing to sufficiently small open submodules stable under the finite set of scalars involved.
□theorem t1Space (hM : IsProfiniteModule Λ M) : T1Space MA profinite module is \(T_1\).
Show proof
by
letI : T2Space M := hM.t2Space
infer_instanceProof. Work in the linear topology of the profinite module. Open submodules form the neighborhoods of zero, and quotienting by an open submodule gives a finite discrete module. Separation, continuity, and inverse-limit claims are checked after all open-submodule quotients. Compactness, Hausdorffness, and total disconnectedness come from the profinite-module hypotheses, while scalar compatibility follows from continuity of the module action and from passing to sufficiently small open submodules stable under the finite set of scalars involved.
□theorem totallyDisconnectedSpace (hM : IsProfiniteModule Λ M) :
TotallyDisconnectedSpace MA profinite module is totally disconnected as a topological space.
Show proof
hM.2.2.2.2.2Proof. Work in the linear topology of the profinite module. Open submodules form the neighborhoods of zero, and quotienting by an open submodule gives a finite discrete module. Separation, continuity, and inverse-limit claims are checked after all open-submodule quotients. Compactness, Hausdorffness, and total disconnectedness come from the profinite-module hypotheses, while scalar compatibility follows from continuity of the module action and from passing to sufficiently small open submodules stable under the finite set of scalars involved.
□theorem isTopologicalModuleOver (hM : IsProfiniteModule Λ M) :
IsTopologicalModuleOver Λ MA profinite module is a topological module over its scalar ring.
Show proof
⟨hM.isProfiniteRing.isTopologicalRing, hM.isTopologicalAddGroup, hM.continuousSMul⟩Proof. Work in the linear topology of the profinite module. Open submodules form the neighborhoods of zero, and quotienting by an open submodule gives a finite discrete module. Separation, continuity, and inverse-limit claims are checked after all open-submodule quotients. Compactness, Hausdorffness, and total disconnectedness come from the profinite-module hypotheses, while scalar compatibility follows from continuity of the module action and from passing to sufficiently small open submodules stable under the finite set of scalars involved.
□theorem isProfiniteSpace (hM : IsProfiniteModule Λ M) :
ProCGroups.InverseSystems.IsProfiniteSpace MThe underlying topological space of a profinite module is profinite.
Show proof
⟨hM.compactSpace, hM.t2Space, hM.totallyDisconnectedSpace⟩Proof. Work in the linear topology of the profinite module. Open submodules form the neighborhoods of zero, and quotienting by an open submodule gives a finite discrete module. Separation, continuity, and inverse-limit claims are checked after all open-submodule quotients. Compactness, Hausdorffness, and total disconnectedness come from the profinite-module hypotheses, while scalar compatibility follows from continuity of the module action and from passing to sufficiently small open submodules stable under the finite set of scalars involved.
□def IsDiscreteModule (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ]
[AddCommGroup M] [TopologicalSpace M] [Module Λ M] : Prop :=
IsTopologicalModuleOver Λ M ∧ DiscreteTopology MA topological module whose underlying module topology is discrete.
def IsFiniteSubmodule {Λ : Type u} {M : Type v} [Ring Λ] [AddCommGroup M] [Module Λ M]
(N : Submodule Λ M) : Prop :=
(N : Set M).FiniteA submodule whose underlying set is finite.
def IsUnionOfFiniteSubmodules (Λ : Type u) (M : Type v) [Ring Λ] [AddCommGroup M]
[Module Λ M] : Prop :=
∀ m : M, ∃ N : Submodule Λ M, IsFiniteSubmodule N ∧ m ∈ NEvery element lies in a finite submodule.
def HasFiniteIndexSubmoduleBasis (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace M]
[AddCommGroup M] [Module Λ M] : Prop :=
∀ U ∈ 𝓝 (0 : M), ∃ N : Submodule Λ M,
IsOpen (N : Set M) ∧ (N : Set M) ⊆ U ∧ Nonempty (Fintype (M ⧸ N))Finite-index submodules form a neighborhood basis at zero.
def IsInverseLimitOfFiniteQuotientModules (Λ : Type u) (M : Type v) [Ring Λ]
[TopologicalSpace M] [AddCommGroup M] [Module Λ M] : Prop :=
HasFiniteIndexSubmoduleBasis Λ M ∧
∀ U ∈ 𝓝 (0 : M), ∃ N : Submodule Λ M,
IsOpen (N : Set M) ∧ (N : Set M) ⊆ U ∧ Nonempty (Fintype (M ⧸ N))A profinite module is represented by its finite quotient modules.
theorem inverseLimitOfFiniteQuotientModules_iff_finiteIndexSubmoduleBasis
(Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace M] [AddCommGroup M]
[Module Λ M] :
IsInverseLimitOfFiniteQuotientModules Λ M ↔ HasFiniteIndexSubmoduleBasis Λ MIn Lemma 5.1.1(b), predicate form, in this development the inverse-limit formulation is recorded by a finite-index open-submodule basis at zero.
Show proof
by
constructor
· intro h
exact h.1
· intro h
exact ⟨h, h⟩Proof. Work in the linear topology of the profinite module. Open submodules form the neighborhoods of zero, and quotienting by an open submodule gives a finite discrete module. Separation, continuity, and inverse-limit claims are checked after all open-submodule quotients. Compactness, Hausdorffness, and total disconnectedness come from the profinite-module hypotheses, while scalar compatibility follows from continuity of the module action and from passing to sufficiently small open submodules stable under the finite set of scalars involved.
□