mathlib3 documentation

topology.algebra.nonarchimedean.adic_topology

Adic topology #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 is_adic 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 with_ideal, 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.adic_topology: the adic topology associated to an ideal. It has the above basis for neighborhoods of zero.
ideal.nonarchimedean: the adic topology is non-archimedean
is_ideal_adic_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.
with_ideal: 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 a R-module.

theorem ideal.adic_basis {R : Type u_1} [comm_ring R] (I : ideal R) :

submodules_ring_basis (λ (n : ℕ), I ^ n • ⊤)

def ideal.ring_filter_basis {R : Type u_1} [comm_ring R] (I : ideal R) :

ring_filter_basis R

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

Equations

I.ring_filter_basis = _.to_ring_filter_basis

def ideal.adic_topology {R : Type u_1} [comm_ring R] (I : ideal R) :

topological_space 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.adic_topology = _.topology

theorem ideal.nonarchimedean {R : Type u_1} [comm_ring R] (I : ideal R) :

nonarchimedean_ring R

theorem ideal.has_basis_nhds_zero_adic {R : Type u_1} [comm_ring R] (I : ideal R) :

(nhds 0).has_basis (λ (n : ℕ), true) (λ (n : ℕ), ↑(I ^ n))

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

theorem ideal.has_basis_nhds_adic {R : Type u_1} [comm_ring R] (I : ideal R) (x : R) :

(nhds x).has_basis (λ (n : ℕ), true) (λ (n : ℕ), (λ (y : R), x + y) '' ↑(I ^ n))

theorem ideal.adic_module_basis {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R M] :

I.ring_filter_basis.submodules_basis (λ (n : ℕ), I ^ n • ⊤)

def ideal.adic_module_topology {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R M] :

topological_space M

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

Equations

I.adic_module_topology M = (I.ring_filter_basis.module_filter_basis _).topology

def ideal.open_add_subgroup {R : Type u_1} [comm_ring R] (I : ideal R) (n : ℕ) :

open_add_subgroup R

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

Equations

I.open_add_subgroup n = {to_add_subgroup := {carrier := (submodule.to_add_subgroup (I ^ n)).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}, is_open' := _}

def is_adic {R : Type u_1} [comm_ring R] [H : topological_space R] (J : ideal R) :

Prop

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

Equations

is_adic J = (H = J.adic_topology)

theorem is_adic_iff {R : Type u_1} [comm_ring R] [top : topological_space R] [topological_ring R] {J : ideal R} :

is_adic J ↔ (∀ (n : ℕ), is_open ↑(J ^ n)) ∧ ∀ (s : set R), 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} [comm_ring R] [topological_space R] [topological_ring R] {J : ideal R} (h : is_adic J) {n : ℕ} (hn : 0 < n) :

is_adic (J ^ n)

theorem is_bot_adic_iff {A : Type u_1} [comm_ring A] [topological_space A] [topological_ring A] :

is_adic ⊥ ↔ discrete_topology A

@[class]

structure with_ideal (R : Type u_2) [comm_ring R] :

Type u_2

I : ideal R

The ring R is equipped with a preferred ideal.

Instances for with_ideal

with_ideal.has_sizeof_inst

@[protected, instance]

def with_ideal.topological_space (R : Type u_1) [comm_ring R] [with_ideal R] :

topological_space R

Equations

with_ideal.topological_space R = with_ideal.I.adic_topology

@[protected, instance]

def with_ideal.nonarchimedean_ring (R : Type u_1) [comm_ring R] [with_ideal R] :

nonarchimedean_ring R

@[protected, instance]

def with_ideal.uniform_space (R : Type u_1) [comm_ring R] [with_ideal R] :

uniform_space R

Equations

with_ideal.uniform_space R = topological_add_group.to_uniform_space R

@[protected, instance]

def with_ideal.uniform_add_group (R : Type u_1) [comm_ring R] [with_ideal R] :

uniform_add_group R

def with_ideal.topological_space_module (R : Type u_1) [comm_ring R] [with_ideal R] (M : Type u_2) [add_comm_group M] [module R M] :

topological_space M

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

Equations

with_ideal.topological_space_module R M = with_ideal.I.adic_module_topology M