Adic topology

Given a commutative ring R and an ideal I in R, this file constructs the unique topology on R which is compatible with the ring structure and such that a set is a neighborhood of zero if and only if it contains a power of I. This topology is non-archimedean: every neighborhood of zero contains an open subgroup, namely a power of I.

It also studies the predicate IsAdic which states that a given topological ring structure is adic, proving a characterization and showing that raising an ideal to a positive power does not change the associated topology.

Finally, it defines WithIdeal, a class registering an ideal in a ring and providing the corresponding adic topology to the type class inference system.

Main definitions and results

• Ideal.adic_basis: the basis of submodules given by powers of an ideal.
• Ideal.adicTopology: the adic topology associated to an ideal. It has the above basis for neighborhoods of zero.
• Ideal.nonarchimedean: the adic topology is non-archimedean
• isAdic_iff: A topological ring is J-adic if and only if it admits the powers of J as a basis of open neighborhoods of zero.
• WithIdeal: a class registering an ideal in a ring.

Implementation notes

The I-adic topology on a ring R has a contrived definition using I^n • ⊤ instead of I to make sure it is definitionally equal to the I-topology on R seen as an R-module.

theorem Ideal.adic_basis {R : Type u_1} [CommRing R] (I : Ideal R) : SubmodulesRingBasis fun (n : ℕ) => I ^ n • ⊤

def Ideal.ringFilterBasis {R : Type u_1} [CommRing R] (I : Ideal R) : RingFilterBasis R

The adic ring filter basis associated to an ideal I is made of powers of I.

Equations

• I.ringFilterBasis = ⋯.toRingFilterBasis

def Ideal.adicTopology {R : Type u_1} [CommRing R] (I : Ideal R) : TopologicalSpace R

The adic topology associated to an ideal I. This topology admits powers of I as a basis of neighborhoods of zero. It is compatible with the ring structure and is non-archimedean.

Equations

• I.adicTopology = ⋯.topology

theorem Ideal.nonarchimedean {R : Type u_1} [CommRing R] (I : Ideal R) : NonarchimedeanRing R

theorem Ideal.hasBasis_nhds_zero_adic {R : Type u_1} [CommRing R] (I : Ideal R) : (nhds 0).HasBasis (fun (_n : ℕ) => True) fun (n : ℕ) => ↑(I ^ n)

For the I-adic topology, the neighborhoods of zero has basis given by the powers of I.

theorem Ideal.hasBasis_nhds_adic {R : Type u_1} [CommRing R] (I : Ideal R) (x : R) : (nhds x).HasBasis (fun (_n : ℕ) => True) fun (n : ℕ) => (fun (y : R) => x + y) '' ↑(I ^ n)

theorem Ideal.adic_module_basis {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : I.ringFilterBasis.SubmodulesBasis fun (n : ℕ) => I ^ n • ⊤

def Ideal.adicModuleTopology {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : TopologicalSpace M

The topology on an R-module M associated to an ideal M. Submodules $I^n M$, written I^n • ⊤ form a basis of neighborhoods of zero.

Equations

• I.adicModuleTopology M = (I.ringFilterBasis.moduleFilterBasis ⋯).topology

def Ideal.openAddSubgroup {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : OpenAddSubgroup R

The elements of the basis of neighborhoods of zero for the I-adic topology on an R-module M, seen as open additive subgroups of M.

Equations

• I.openAddSubgroup n = { toAddSubgroup := Submodule.toAddSubgroup (I ^ n), isOpen' := ⋯ }

def IsAdic {R : Type u_1} [CommRing R] [H : TopologicalSpace R] (J : Ideal R) : Prop

Given a topology on a ring R and an ideal J, IsAdic J means the topology is the J-adic one.

Equations

• IsAdic J = (H = J.adicTopology)

theorem isAdic_iff {R : Type u_1} [CommRing R] [top : TopologicalSpace R] [IsTopologicalRing R] {J : Ideal R} : IsAdic J ↔ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ nhds 0, ∃ (n : ℕ), ↑(J ^ n) ⊆ s

A topological ring is J-adic if and only if it admits the powers of J as a basis of open neighborhoods of zero.

theorem is_ideal_adic_pow {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] {J : Ideal R} (h : IsAdic J) {n : ℕ} (hn : 0 < n) : IsAdic (J ^ n)

theorem is_bot_adic_iff {A : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] : IsAdic ⊥ ↔ DiscreteTopology A

class WithIdeal (R : Type u_2) [CommRing R] : Type u_2

The ring R is equipped with a preferred ideal.

• i : Ideal R

@[instance 100]

instance WithIdeal.instTopologicalSpace (R : Type u_1) [CommRing R] [WithIdeal R] : TopologicalSpace R

Equations

• WithIdeal.instTopologicalSpace R = WithIdeal.i.adicTopology

@[instance 100]

instance WithIdeal.instNonarchimedeanRing (R : Type u_1) [CommRing R] [WithIdeal R] : NonarchimedeanRing R

@[instance 100]

instance WithIdeal.instUniformSpace (R : Type u_1) [CommRing R] [WithIdeal R] : UniformSpace R

Equations

• WithIdeal.instUniformSpace R = IsTopologicalAddGroup.toUniformSpace R

@[instance 100]

instance WithIdeal.instIsUniformAddGroup (R : Type u_1) [CommRing R] [WithIdeal R] : IsUniformAddGroup R

def WithIdeal.topologicalSpaceModule (R : Type u_1) [CommRing R] [WithIdeal R] (M : Type u_2) [AddCommGroup M] [Module R M] : TopologicalSpace M

The adic topology on an R module coming from the ideal WithIdeal.I. This cannot be an instance because R cannot be inferred from M.

Equations

• WithIdeal.topologicalSpaceModule R M = WithIdeal.i.adicModuleTopology M