Connection between adic properties and topological properties

Main results

• IsAdic.isPrecomplete_iff: IsPrecomplete I R is equivalent to CompleteSpace R in the adic topology.
• IsAdic.isAdicComplete_iff: IsAdicComplete I R is equivalent to CompleteSpace R and T2Space R in the adic topology.

theorem IsAdic.isHausdorff_iff {R : Type u_1} [CommRing R] [TopologicalSpace R] {I : Ideal R} (hI : IsAdic I) : IsHausdorff I R ↔ T2Space R

IsHausdorff I R is equivalent to being Hausdorff in the adic topology.

theorem IsAdic.isPrecomplete_iff {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] {I : Ideal R} (hI : IsAdic I) : IsPrecomplete I R ↔ CompleteSpace R

IsPrecomplete I R is equivalent to being complete in the adic topology.

theorem IsAdic.isAdicComplete_iff {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] {I : Ideal R} (hI : IsAdic I) : IsAdicComplete I R ↔ CompleteSpace R ∧ T2Space R

IsAdicComplete I R is equivalent to being complete and hausdorff in the adic topology.