Ideal.hasBasis_nhds_zero_adic
theorem Ideal.hasBasis_nhds_zero_adic :
∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), (nhds 0).HasBasis (fun _n => True) fun n => ↑(I ^ n)
This theorem states that for the `I`-adic topology on a commutative ring `R`, the neighborhoods of the zero element have a basis given by the powers of an ideal `I`. This means that every neighborhood of zero contains (and is in fact generated by) some power of `I`, or in other words, some additive submonoid of `R` where for any element `b` in the submonoid, the product of any element of `R` and `b` is also in the submonoid.
More concisely: The `I`-adic topology on a commutative ring `R` has the zero element's neighborhoods as a basis given by the powers of the ideal `I`.
|
Ideal.adic_basis
theorem Ideal.adic_basis : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), SubmodulesRingBasis fun n => I ^ n • ⊤
This theorem states that for any commutative ring `R` and any ideal `I` of `R`, the set of all submodules of `R` that can be obtained by taking the `n`th power of `I` (denoted `I^n`) and scaling the entire ring `R` (denoted `⊤`) forms a basis with respect to the ring structure. This is often referred to as an 'adic basis'.
More concisely: For any commutative ring `R` and ideal `I`, the set of all scaled `n`th powers of `I` (`{⊤ * I^n | n : ℕ}`) forms a basis for the submodule lattice of `R`.
|
isAdic_iff
theorem isAdic_iff :
∀ {R : Type u_1} [inst : CommRing R] [top : TopologicalSpace R] [inst_1 : TopologicalRing R] {J : Ideal R},
IsAdic J ↔ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ nhds 0, ∃ n, ↑(J ^ n) ⊆ s
The theorem `isAdic_iff` states that for any given commutative ring `R` with a topological space structure and an associated topological ring structure, and an ideal `J` of `R`, the ring `R` is `J`-adic if and only if the following two conditions are satisfied:
1. The powers of `J` form a basis of open neighborhoods of the zero element in the ring, meaning that for any natural number `n`, the set of elements in `J` raised to the power `n` is an open set in the topology of `R`.
2. For any set `s` which is a neighborhood of the zero element in the topology of `R`, there exists a natural number `n` such that the set of elements in `J` raised to the power `n` is a subset of `s`. This asserts that every neighborhood of zero contains some power of `J`.
More concisely: A commutative ring `R` with a topology and an ideal `J` is `J`-adic if and only if the powers of `J` form a basis of open neighborhoods of the zero element and every neighborhood of zero contains some power of `J`.
|