# 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.

The adic ring filter basis associated to an ideal `I`

is made of powers of `I`

.

## Equations

- I.ringFilterBasis = ⋯.toRingFilterBasis

## Instances For

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

## Instances For

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

## Instances For

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' := ⋯ }

## Instances For

A topological ring is `J`

-adic if and only if it admits the powers of `J`

as a basis of
open neighborhoods of zero.

## Equations

- WithIdeal.instTopologicalSpace R = WithIdeal.i.adicTopology

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

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