CompletedGroupAlgebra.ProfiniteModules.Basic.OpenIdeals
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 HasOpenIdealBasisAtZero (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] : Prop :=
∀ U ∈ 𝓝 (0 : Λ), ∃ I : Ideal Λ, IsOpen (I : Set Λ) ∧ (I : Set Λ) ⊆ UOpen ideals form a neighborhood basis at zero.
def HasFiniteOpenIdealQuotientBasis (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] : Prop :=
∀ U ∈ 𝓝 (0 : Λ), ∃ I : Ideal Λ,
IsOpen (I : Set Λ) ∧ (I : Set Λ) ⊆ U ∧ Nonempty (Fintype (Λ ⧸ I))Open ideals with finite quotient form a neighborhood basis at zero.
def IsInverseLimitOfFiniteRingQuotients (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] : Prop :=
HasFiniteOpenIdealQuotientBasis ΛThe finite-quotient characterization of a profinite ring.
theorem finite_quotient_of_openIdeal
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ)
(I : Ideal Λ) (hI : IsOpen (I : Set Λ)) :
Nonempty (Fintype (Λ ⧸ I))An open ideal of a compact topological ring has finite additive quotient.
Show proof
by
letI : IsTopologicalRing Λ := hΛ.1
letI : ContinuousAdd Λ := inferInstance
letI : CompactSpace Λ := hΛ.2.1
haveI : Finite (Λ ⧸ I) :=
AddSubgroup.quotient_finite_of_isOpen I.toAddSubgroup hI
exact ⟨Fintype.ofFinite (Λ ⧸ I)⟩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.
□theorem quotient_openIdeal_isDiscreteModule
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ)
(I : Ideal Λ) (hI : IsOpen (I : Set Λ)) :
IsDiscreteModule Λ (Λ ⧸ I)The quotient by an open ideal is a discrete module over the original ring.
Show proof
by
letI : IsTopologicalRing Λ := hΛ.1
letI : IsTopologicalAddGroup Λ := inferInstance
letI : ContinuousAdd Λ := inferInstance
letI : ContinuousSMul Λ Λ := inferInstance
haveI : DiscreteTopology (Λ ⧸ I) :=
QuotientAddGroup.discreteTopology (N := I.toAddSubgroup) hI
exact ⟨⟨hΛ.1, inferInstance, inferInstance⟩, inferInstance⟩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.
□theorem quotient_openIdeal_finiteDiscreteModule
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ)
(I : Ideal Λ) (hI : IsOpen (I : Set Λ)) :
IsDiscreteModule Λ (Λ ⧸ I) ∧ Nonempty (Fintype (Λ ⧸ I))Open ideal quotients are finite discrete modules over the original ring.
Show proof
⟨quotient_openIdeal_isDiscreteModule Λ hΛ I hI,
finite_quotient_of_openIdeal Λ hΛ I hI⟩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.
□theorem profiniteRing_hasFiniteOpenIdealQuotientBasis_of_linearTopology
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsLinearTopology Λ Λ]
(hΛ : IsProfiniteRing Λ) :
HasFiniteOpenIdealQuotientBasis ΛProposition 5.1.2(d/e), linear-topology interface: a profinite ring whose topology is linear has a fundamental system of open ideals with finite quotient.
Show proof
by
letI : IsTopologicalRing Λ := hΛ.1
letI : ContinuousAdd Λ := inferInstance
intro U hU
rcases ((IsLinearTopology.hasBasis_open_ideal).mem_iff.mp hU) with
⟨I, hIopen, hIU⟩
exact ⟨I, hIopen, hIU, finite_quotient_of_openIdeal Λ hΛ I hIopen⟩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.
□theorem profiniteRing_isInverseLimitOfFiniteRingQuotients_of_linearTopology
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsLinearTopology Λ Λ]
(hΛ : IsProfiniteRing Λ) :
IsInverseLimitOfFiniteRingQuotients ΛProposition 5.1.2(e) gives the inverse-limit formulation by finite ring quotients under the same linear-topology hypothesis.
Show proof
profiniteRing_hasFiniteOpenIdealQuotientBasis_of_linearTopology Λ hΛ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.
□theorem profiniteRing_self_isProfiniteModule
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ) :
IsProfiniteModule Λ ΛA profinite ring is a profinite module over itself by left multiplication.
Show proof
by
letI : IsTopologicalRing Λ := hΛ.1
have hsmul : ContinuousSMul Λ Λ :=
ContinuousSMul.mk (by simpa [smul_eq_mul] using continuous_mul)
exact ⟨hΛ, inferInstance, hsmul, hΛ.2.1, hΛ.2.2.1, hΛ.2.2.2⟩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.
□theorem profiniteRing_isLinearTopology
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ) :
IsLinearTopology Λ ΛProposition 5.1.2(d/e), linear-topology part for profinite rings.
Show proof
by
exact profiniteModule_isLinearTopology Λ Λ (profiniteRing_self_isProfiniteModule Λ hΛ)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.
□theorem profiniteRing_hasFiniteOpenIdealQuotientBasis
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ) :
HasFiniteOpenIdealQuotientBasis ΛProposition 5.1.2(d/e): a profinite ring has a fundamental system of open ideals with finite quotient.
Show proof
by
letI : IsLinearTopology Λ Λ := profiniteRing_isLinearTopology Λ hΛ
exact profiniteRing_hasFiniteOpenIdealQuotientBasis_of_linearTopology Λ hΛ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.
□theorem profiniteRing_hasOpenIdealBasisAtZero
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] (hΛ : IsProfiniteRing Λ) :
HasOpenIdealBasisAtZero ΛProposition 5.1.2(d): a profinite ring has a basis of open ideals at zero.
Show proof
by
intro U hU
rcases profiniteRing_hasFiniteOpenIdealQuotientBasis Λ hΛ U hU with
⟨I, hIopen, hIU, _hfin⟩
exact ⟨I, hIopen, hIU⟩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.
□