An additive endomorphism which sends I ^ n into I ^ (n + 1) is topologically nilpotent for the I-adic topology. Completeness therefore solves the affine fixed-point equation
x = b + T x
uniquely. The proof uses the successive approximations x₀ = 0, xₙ₊₁ = b + T xₙ and mathlib's IsPrecomplete.prec.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace IsAdicComplete
variable {R : Type*} [CommRing R]def contractingApproximation
(T : R →+ R) (b : R) : ℕ → R
| 0 => 0
| n + 1 => b + T (contractingApproximation T b n)Surrounding namespaces, section variables, and local commands at this declaration.
namespace IsAdicComplete
variable {R : Type*} [CommRing R]theorem contractingApproximation_succ
(T : R →+ R) (b : R) (n : ℕ) :
contractingApproximation T b (n + 1) =
b + T (contractingApproximation T b n)Surrounding namespaces, section variables, and local commands at this declaration.
namespace IsAdicComplete
variable {R : Type*} [CommRing R]theorem ideal_smul_top_eq_self (J : Ideal R) :
J • (⊤ : Submodule R R) = (J : Submodule R R)Surrounding namespaces, section variables, and local commands at this declaration.
namespace IsAdicComplete
variable {R : Type*} [CommRing R]theorem map_smodEq_pow_succ
(I : Ideal R) (T : R →+ R)
(hT : ∀ (n : ℕ) {x : R}, x ∈ I ^ n → T x ∈ I ^ (n + 1))
(n : ℕ) {x y : R}
(hxy : x ≡ y [SMOD (I ^ n : Ideal R)]) :
T x ≡ T y [SMOD (I ^ (n + 1) : Ideal R)]Surrounding namespaces, section variables, and local commands at this declaration.
namespace IsAdicComplete
variable {R : Type*} [CommRing R]theorem contractingApproximation_sub_mem_pow
(I : Ideal R) (T : R →+ R)
(hT : ∀ (n : ℕ) {x : R}, x ∈ I ^ n → T x ∈ I ^ (n + 1))
(b : R) :
∀ n, contractingApproximation T b n -
contractingApproximation T b (n + 1) ∈ I ^ nSurrounding namespaces, section variables, and local commands at this declaration.
namespace IsAdicComplete
variable {R : Type*} [CommRing R]theorem contractingApproximation_limit_is_fixed
(I : Ideal R) [IsHausdorff I R]
(T : R →+ R)
(hT : ∀ (n : ℕ) {x : R}, x ∈ I ^ n → T x ∈ I ^ (n + 1))
(b a : R)
(ha : ∀ n, contractingApproximation T b n ≡
a [SMOD (I ^ n : Ideal R)]) :
a = b + T aSurrounding namespaces, section variables, and local commands at this declaration.
namespace IsAdicComplete
variable {R : Type*} [CommRing R]theorem eq_of_eq_add_of_maps_pow_succ
(I : Ideal R) [IsHausdorff I R]
(T : R →+ R)
(hT : ∀ (n : ℕ) {x : R}, x ∈ I ^ n → T x ∈ I ^ (n + 1))
(b : R) {x y : R}
(hx : x = b + T x) (hy : y = b + T y) :
x = yAn additive endomorphism which raises the I-adic filtration by one has a unique affine fixed point on an I-adically complete ring.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace IsAdicComplete
variable {R : Type*} [CommRing R]theorem existsUnique_eq_add_of_maps_pow_succ
(I : Ideal R) [IsAdicComplete I R]
(T : R →+ R)
(hT : ∀ (n : ℕ) {x : R}, x ∈ I ^ n → T x ∈ I ^ (n + 1))
(b : R) :
∃! x : R, x = b + T x