Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.OpenIdeals
1import ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.Generators
3/-!
4# Open ideals in profinite rings
6This file develops open-ideal bases at zero in profinite rings, proves their quotients finite, and
7derives the finite-open-ideal quotient basis and linear-topology properties.
8-/
10open scoped Topology
12namespace CompletedGroupAlgebra
14universe u v w z
16/-- Open ideals form a neighborhood basis at zero. -/
17def HasOpenIdealBasisAtZero (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] : Prop :=
18 ∀ U ∈ 𝓝 (0 : Λ), ∃ I : Ideal Λ, IsOpen (I : Set Λ) ∧ (I : Set Λ) ⊆ U
20/-- Open ideals with finite quotient form a neighborhood basis at zero. -/
21def HasFiniteOpenIdealQuotientBasis (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] : Prop :=
22 ∀ U ∈ 𝓝 (0 : Λ), ∃ I : Ideal Λ,
23 IsOpen (I : Set Λ) ∧ (I : Set Λ) ⊆ U ∧ Nonempty (Fintype (Λ ⧸ I))
25/-- An open ideal of a compact topological ring has finite additive quotient. -/
26theorem finite_quotient_of_openIdeal
27 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsTopologicalRing Λ]
28 [CompactSpace Λ]
29 (I : Ideal Λ) (hI : IsOpen (I : Set Λ)) :
30 Nonempty (Fintype (Λ ⧸ I)) := by
31 letI : ContinuousAdd Λ := inferInstance
32 haveI : Finite (Λ ⧸ I) :=
33 AddSubgroup.quotient_finite_of_isOpen I.toAddSubgroup hI
34 exact ⟨Fintype.ofFinite (Λ ⧸ I)⟩
36/--
37Proposition 5.1.2(d/e), linear-topology interface: a profinite ring whose topology is linear has
38a fundamental system of open ideals with finite quotient.
39-/
40theorem profiniteRing_hasFiniteOpenIdealQuotientBasis_of_linearTopology
41 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsLinearTopology Λ Λ]
42 [IsTopologicalRing Λ] [CompactSpace Λ] :
43 HasFiniteOpenIdealQuotientBasis Λ := by
44 letI : ContinuousAdd Λ := inferInstance
45 intro U hU
46 rcases ((IsLinearTopology.hasBasis_open_ideal).mem_iff.mp hU) with
47 ⟨I, hIopen, hIU⟩
48 exact ⟨I, hIopen, hIU, finite_quotient_of_openIdeal Λ I hIopen⟩
50/-- Proposition 5.1.2(d/e), linear-topology part for profinite rings. -/
51theorem profiniteRing_isLinearTopology
52 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsTopologicalRing Λ]
53 [CompactSpace Λ] [T2Space Λ] [TotallyDisconnectedSpace Λ] :
54 IsLinearTopology Λ Λ := by
55 letI : ContinuousSMul Λ Λ :=
56 ContinuousSMul.mk (by simpa [smul_eq_mul] using continuous_mul)
57 exact profiniteModule_isLinearTopology Λ Λ
59/--
60Proposition 5.1.2(d/e): a profinite ring has a fundamental system of open ideals with finite
61quotient.
62-/
63theorem profiniteRing_hasFiniteOpenIdealQuotientBasis
64 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsTopologicalRing Λ]
65 [CompactSpace Λ] [T2Space Λ] [TotallyDisconnectedSpace Λ] :
66 HasFiniteOpenIdealQuotientBasis Λ := by
67 letI : IsLinearTopology Λ Λ := profiniteRing_isLinearTopology Λ
68 exact profiniteRing_hasFiniteOpenIdealQuotientBasis_of_linearTopology Λ
70/-- Proposition 5.1.2(d): a profinite ring has a basis of open ideals at zero. -/
71theorem profiniteRing_hasOpenIdealBasisAtZero
72 (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsTopologicalRing Λ]
73 [CompactSpace Λ] [T2Space Λ] [TotallyDisconnectedSpace Λ] :
74 HasOpenIdealBasisAtZero Λ := by
75 intro U hU
76 rcases profiniteRing_hasFiniteOpenIdealQuotientBasis Λ U hU with
77 ⟨I, hIopen, hIU, _hfin⟩
78 exact ⟨I, hIopen, hIU⟩
80end CompletedGroupAlgebra