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.

theorem IsPrecomplete.congr_ringEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (I : Ideal R) (e : R ≃+* S) : IsPrecomplete (Ideal.map e I) S ↔ IsPrecomplete I R

theorem IsHausdorff.congr_ringEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (I : Ideal R) (e : R ≃+* S) : IsHausdorff (Ideal.map e I) S ↔ IsHausdorff I R

theorem IsAdicComplete.congr_ringEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (I : Ideal R) (e : R ≃+* S) : IsAdicComplete (Ideal.map e I) S ↔ IsAdicComplete I R