Adic completeness of finite products

For an ideal I of a commutative ring R and a family of R-modules M i, the product ∀ i, M i is I-adically Hausdorff as soon as every factor is. If the family is finite, the analogous result holds for adic precompleteness and completeness. In particular a finite free module Fin n → R over an I-adically complete ring is I-adically complete, which is what the complete Nakayama lemma (surjective_of_mkQ_comp_surjective) requires of the source of a map out of a finite free module. For a principal ideal (π), the (π)-adic filtration of a product ι → R is read off coordinatewise: x ∈ (π)^n • ⊤ exactly when π ^ n divides every coordinate of x.

Main results

• TauCeti.mem_span_singleton_pow_smul_top_iff: membership in (π)^n • ⊤ on a product module is coordinatewise divisibility by π ^ n.
• AdicCompletion.pi_of: the product of the completions of the factors receives the canonical map from the product as the product of the canonical maps.
• IsHausdorff.pi: adic Hausdorffness passes to products.
• IsPrecomplete.pi, IsAdicComplete.pi: adic precompleteness and completeness pass to finite products.

theorem TauCeti.mem_span_singleton_pow_smul_top_iff {R : Type u_1} [CommSemiring R] {ι : Type u_2} (π : R) (x : ι → R) (n : ℕ) : x ∈ Ideal.span {π} ^ n • ⊤ ↔ ∀ (i : ι), π ^ n ∣ x i

On a product module, membership in (π)^n • ⊤ is coordinatewise divisibility by π ^ n.

@[simp]

theorem AdicCompletion.pi_of {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (x : (i : ι) → M i) (j : ι) : (pi I M) ((of I ((i : ι) → M i)) x) j = (of I (M j)) (x j)

The canonical map from a product to its adic completion, followed by the comparison map AdicCompletion.pi to the product of the completions, is the product of the canonical maps of the factors.

instance IsHausdorff.pi {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), IsHausdorff I (M i)] : IsHausdorff I ((i : ι) → M i)

A product of I-adically Hausdorff modules is I-adically Hausdorff.

instance IsPrecomplete.pi {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Finite ι] [∀ (i : ι), IsPrecomplete I (M i)] : IsPrecomplete I ((i : ι) → M i)

A finite product of I-adically precomplete modules is I-adically precomplete.

instance IsAdicComplete.pi {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Finite ι] [∀ (i : ι), IsAdicComplete I (M i)] : IsAdicComplete I ((i : ι) → M i)

A finite product of I-adically complete modules is I-adically complete.