Adic completeness for cofinal ideals and for powers of an ideal

For ideals J ≤ I of a commutative ring R, the J-adic filtration J ^ m • ⊤ of an R-module M is finer than the I-adic one, so an I-adically Hausdorff module is J-adically Hausdorff. If moreover I ^ k ≤ J for some k, the two filtrations are cofinal in each other, and I-adic precompleteness and completeness transfer to J as well. The powers J = I ^ n with n ≠ 0 are the main instance of this, and precompleteness holds for n = 0 too, since every module is ⊤-adically precomplete.

The main use is Hensel's lemma at I ^ n: an I ^ n-adically complete ring is Henselian at I ^ n by Mathlib's IsAdicComplete.henselianRing, which lifts an approximate root modulo I ^ n to a root congruent to it modulo I ^ n, and not merely modulo I.

Main results

• IsHausdorff.of_le: adic Hausdorffness for I implies the same for every J ≤ I.
• IsPrecomplete.of_le_of_pow_le, IsAdicComplete.of_le_of_pow_le: adic precompleteness and completeness for I imply the same for every J with I ^ k ≤ J ≤ I.
• IsHausdorff.pow, IsAdicComplete.pow: adic Hausdorffness and completeness for I imply the same for I ^ n when n ≠ 0.
• IsPrecomplete.pow: adic precompleteness for I implies precompleteness for every I ^ n.

theorem IsHausdorff.of_le {R : Type u_1} [CommRing R] {I J : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] [IsHausdorff I M] (h : J ≤ I) : IsHausdorff J M

An I-adically Hausdorff module is J-adically Hausdorff for every J ≤ I.

theorem IsPrecomplete.of_le_of_pow_le {R : Type u_1} [CommRing R] {I J : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] [IsPrecomplete I M] (hJI : J ≤ I) {k : ℕ} (hIJ : I ^ k ≤ J) : IsPrecomplete J M

An I-adically precomplete module is J-adically precomplete for every J with I ^ k ≤ J ≤ I for some k.

theorem IsAdicComplete.of_le_of_pow_le {R : Type u_1} [CommRing R] {I J : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] [IsAdicComplete I M] (hJI : J ≤ I) {k : ℕ} (hIJ : I ^ k ≤ J) : IsAdicComplete J M

An I-adically complete module is J-adically complete for every J with I ^ k ≤ J ≤ I for some k.

theorem IsHausdorff.pow {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] [IsHausdorff I M] {n : ℕ} (hn : n ≠ 0) : IsHausdorff (I ^ n) M

An I-adically Hausdorff module is I ^ n-adically Hausdorff for n ≠ 0.

theorem IsPrecomplete.pow {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] [IsPrecomplete I M] (n : ℕ) : IsPrecomplete (I ^ n) M

An I-adically precomplete module is I ^ n-adically precomplete for every n.

theorem IsAdicComplete.pow {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] [IsAdicComplete I M] {n : ℕ} (hn : n ≠ 0) : IsAdicComplete (I ^ n) M

An I-adically complete module is I ^ n-adically complete for n ≠ 0.