Additions to the IsAdic API #
Consequences of IsAdic I for a topological ring: the topology is linear, and elements
of I are topologically nilpotent. These are the IsAdic counterparts of
Ideal.isLinearTopology and WithIdeal.isTopologicallyNilpotent_of_mem.
theorem
IsAdic.isLinearTopology
{R : Type u_1}
[CommRing R]
[TopologicalSpace R]
{I : Ideal R}
(hI : IsAdic I)
:
IsLinearTopology R R
A ring with the I-adic topology is linearly topologized.
theorem
IsAdic.nonarchimedeanRing
{R : Type u_1}
[CommRing R]
[TopologicalSpace R]
{I : Ideal R}
(hI : IsAdic I)
:
A ring with an adic topology is nonarchimedean.
theorem
IsAdic.isOpen_pow
{R : Type u_1}
[CommRing R]
[TopologicalSpace R]
{I : Ideal R}
(hI : IsAdic I)
(n : ℕ)
:
In a ring with the I-adic topology, the powers of I are open.
theorem
IsAdic.isClosed_pow
{R : Type u_1}
[CommRing R]
[TopologicalSpace R]
{I : Ideal R}
(hI : IsAdic I)
(n : ℕ)
:
In a ring with the I-adic topology, the powers of I are closed.
theorem
IsAdic.isTopologicallyNilpotent_of_mem
{R : Type u_1}
[CommRing R]
[TopologicalSpace R]
{I : Ideal R}
(hI : IsAdic I)
{a : R}
(ha : a ∈ I)
:
In a ring with the I-adic topology, elements of I are topologically nilpotent.
theorem
IsAdic.tendsto_zero_of_mem_pow
{R : Type u_1}
[CommRing R]
[TopologicalSpace R]
{I : Ideal R}
(hI : IsAdic I)
{γ : Type u_2}
{l : Filter γ}
{g : γ → R}
{e : γ → ℕ}
(hg : ∀ (i : γ), g i ∈ I ^ e i)
(he : Filter.Tendsto e l Filter.atTop)
:
Filter.Tendsto g l (nhds 0)
In an I-adic ring, a family lying in growing powers of I (the exponents tending to
∞) tends to 0.