ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.OpenIdeals

5 Theorems | 2 Definitions

This file develops open-ideal bases at zero in profinite rings, proves their quotients finite, and derives the finite-open-ideal quotient basis and linear-topology properties.

import

ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.Generators

Imported by

Definition CompletedGroupAlgebra.HasOpenIdealBasisAtZero

def HasOpenIdealBasisAtZero (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] : Prop :=
  ∀ U ∈ 𝓝 (0 : Λ), ∃ I : Ideal Λ, IsOpen (I : Set Λ) ∧ (I : Set Λ) ⊆ U

Open ideals form a neighborhood basis at zero.

Definition CompletedGroupAlgebra.HasFiniteOpenIdealQuotientBasis

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.

Theorem CompletedGroupAlgebra.finite_quotient_of_openIdeal

theorem finite_quotient_of_openIdeal
    (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsTopologicalRing Λ]
    [CompactSpace Λ]
    (I : Ideal Λ) (hI : IsOpen (I : Set Λ)) :
    Nonempty (Fintype (Λ ⧸ I))

An open ideal of a compact topological ring has finite additive quotient.

Show Lean proof

Theorem CompletedGroupAlgebra.profiniteRing_hasFiniteOpenIdealQuotientBasis_of_linearTopology

theorem profiniteRing_hasFiniteOpenIdealQuotientBasis_of_linearTopology
    (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsLinearTopology Λ Λ]
    [IsTopologicalRing Λ] [CompactSpace Λ] :
    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 Lean proof

Theorem CompletedGroupAlgebra.profiniteRing_isLinearTopology

theorem profiniteRing_isLinearTopology
    (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsTopologicalRing Λ]
    [CompactSpace Λ] [T2Space Λ] [TotallyDisconnectedSpace Λ] :
    IsLinearTopology Λ Λ

Proposition 5.1.2(d/e), linear-topology part for profinite rings.

Show Lean proof

Theorem CompletedGroupAlgebra.profiniteRing_hasFiniteOpenIdealQuotientBasis

theorem profiniteRing_hasFiniteOpenIdealQuotientBasis
    (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsTopologicalRing Λ]
    [CompactSpace Λ] [T2Space Λ] [TotallyDisconnectedSpace Λ] :
    HasFiniteOpenIdealQuotientBasis Λ

Proposition 5.1.2(d/e): a profinite ring has a fundamental system of open ideals with finite quotient.

Show Lean proof

Theorem CompletedGroupAlgebra.profiniteRing_hasOpenIdealBasisAtZero

theorem profiniteRing_hasOpenIdealBasisAtZero
    (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsTopologicalRing Λ]
    [CompactSpace Λ] [T2Space Λ] [TotallyDisconnectedSpace Λ] :
    HasOpenIdealBasisAtZero Λ

Proposition 5.1.2(d): a profinite ring has a basis of open ideals at zero.

Show Lean proof

ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.OpenIdeals

Declarations