CompletedGroupAlgebra/ProfiniteModules/Basic/OpenIdeals.lean
1import CompletedGroupAlgebra.ProfiniteModules.Basic.Generators
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/ProfiniteModules/Basic/OpenIdeals.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Open ideals in profinite rings
13-/
15open scoped Topology
17namespace CompletedGroupAlgebra
19universe u v w z
21/-- Open ideals form a neighborhood basis at zero. -/
22def HasOpenIdealBasisAtZero (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] : Prop :=
23 ∀ U ∈ 𝓝 (0 : Λ), ∃ I : Ideal Λ, IsOpen (I : Set Λ) ∧ (I : Set Λ) ⊆ U
25/-- Open ideals with finite quotient form a neighborhood basis at zero. -/
26def HasFiniteOpenIdealQuotientBasis (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] : Prop :=
27 ∀ U ∈ 𝓝 (0 : Λ), ∃ I : Ideal Λ,
28 IsOpen (I : Set Λ) ∧ (I : Set Λ) ⊆ U ∧ Nonempty (Fintype (Λ ⧸ I))
30/-- The finite-quotient characterization of a profinite ring. -/
31def IsInverseLimitOfFiniteRingQuotients (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] : Prop :=
34/-- An open ideal of a compact topological ring has finite additive quotient. -/
35theorem finite_quotient_of_openIdeal
36 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ)
37 (I : Ideal Λ) (hI : IsOpen (I : Set Λ)) :
38 Nonempty (Fintype (Λ ⧸ I)) := by
39 letI : IsTopologicalRing Λ := hΛ.1
40 letI : ContinuousAdd Λ := inferInstance
41 letI : CompactSpace Λ := hΛ.2.1
42 haveI : Finite (Λ ⧸ I) :=
43 AddSubgroup.quotient_finite_of_isOpen I.toAddSubgroup hI
44 exact ⟨Fintype.ofFinite (Λ ⧸ I)⟩
46/-- The quotient by an open ideal is a discrete module over the original ring. -/
48 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ)
49 (I : Ideal Λ) (hI : IsOpen (I : Set Λ)) :
50 IsDiscreteModule Λ (Λ ⧸ I) := by
51 letI : IsTopologicalRing Λ := hΛ.1
52 letI : IsTopologicalAddGroup Λ := inferInstance
53 letI : ContinuousAdd Λ := inferInstance
54 letI : ContinuousSMul Λ Λ := inferInstance
55 haveI : DiscreteTopology (Λ ⧸ I) :=
56 QuotientAddGroup.discreteTopology (N := I.toAddSubgroup) hI
57 exact ⟨⟨hΛ.1, inferInstance, inferInstance⟩, inferInstance⟩
59/-- Open ideal quotients are finite discrete modules over the original ring. -/
61 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ)
62 (I : Ideal Λ) (hI : IsOpen (I : Set Λ)) :
63 IsDiscreteModule Λ (Λ ⧸ I) ∧ Nonempty (Fintype (Λ ⧸ I)) :=
64 ⟨quotient_openIdeal_isDiscreteModule Λ hΛ I hI,
65 finite_quotient_of_openIdeal Λ hΛ I hI⟩
67/-- Proposition 5.1.2(d/e), linear-topology interface: a profinite ring whose topology is linear
70 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsLinearTopology Λ Λ]
71 (hΛ : IsProfiniteRing Λ) :
72 HasFiniteOpenIdealQuotientBasis Λ := by
73 letI : IsTopologicalRing Λ := hΛ.1
74 letI : ContinuousAdd Λ := inferInstance
75 intro U hU
76 rcases ((IsLinearTopology.hasBasis_open_ideal).mem_iff.mp hU) with
77 ⟨I, hIopen, hIU⟩
78 exact ⟨I, hIopen, hIU, finite_quotient_of_openIdeal Λ hΛ I hIopen⟩
80/-- Proposition 5.1.2(e), inverse-limit finite-ring-quotient formulation under the same
81linear-topology hypothesis. -/
83 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsLinearTopology Λ Λ]
84 (hΛ : IsProfiniteRing Λ) :
88/-- A profinite ring is a profinite module over itself by left multiplication. -/
90 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ) :
91 IsProfiniteModule Λ Λ := by
92 letI : IsTopologicalRing Λ := hΛ.1
93 have hsmul : ContinuousSMul Λ Λ :=
94 ContinuousSMul.mk (by simpa [smul_eq_mul] using continuous_mul)
95 exact ⟨hΛ, inferInstance, hsmul, hΛ.2.1, hΛ.2.2.1, hΛ.2.2.2⟩
97/-- Proposition 5.1.2(d/e), linear-topology part for profinite rings. -/
98theorem profiniteRing_isLinearTopology
99 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ) :
100 IsLinearTopology Λ Λ := by
101 exact profiniteModule_isLinearTopology Λ Λ (profiniteRing_self_isProfiniteModule Λ hΛ)
103/-- Proposition 5.1.2(d/e): a profinite ring has a fundamental system of open ideals with finite
104quotient. -/
106 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ) :
107 HasFiniteOpenIdealQuotientBasis Λ := by
108 letI : IsLinearTopology Λ Λ := profiniteRing_isLinearTopology Λ hΛ
111/-- Proposition 5.1.2(d): a profinite ring has a basis of open ideals at zero. -/
113 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ) :
114 HasOpenIdealBasisAtZero Λ := by
115 intro U hU
116 rcases profiniteRing_hasFiniteOpenIdealQuotientBasis Λ hΛ U hU with
117 ⟨I, hIopen, hIU, _hfin⟩
118 exact ⟨I, hIopen, hIU⟩