English
Same equivalence as above but stated in terms of sets and open subgroups; equivalently, adic structure is determined by open powers and neighborhoods of zero.
Русский
Та же эквивалентность, выраженная через множества и открытые подгруппы; адическая структура определяется открытыми степенями и окрестностями нуля.
LaTeX
$$$\\text{IsAdic } J \\iff (\\forall n, IsOpen((J^n)^\\ast)) \\land (\\forall s \\in nhds(0), \\exists n, (J^n) \\subseteq s)$$$
Lean4
/-- A topological ring is `J`-adic if and only if it admits the powers of `J` as a basis of
open neighborhoods of zero. -/
theorem isAdic_iff [top : TopologicalSpace R] [IsTopologicalRing R] {J : Ideal R} :
IsAdic J ↔
(∀ n : ℕ, IsOpen ((J ^ n : Ideal R) : Set R)) ∧ ∀ s ∈ 𝓝 (0 : R), ∃ n : ℕ, ((J ^ n : Ideal R) : Set R) ⊆ s :=
by
constructor
· intro H
change _ = _ at H
rw [H]
letI := J.adicTopology
constructor
· intro n
exact (J.openAddSubgroup n).isOpen'
· intro s hs
simpa using J.hasBasis_nhds_zero_adic.mem_iff.mp hs
· rintro ⟨H₁, H₂⟩
apply IsTopologicalAddGroup.ext
· apply @IsTopologicalRing.to_topologicalAddGroup
· apply (RingSubgroupsBasis.toRingFilterBasis _).toAddGroupFilterBasis.isTopologicalAddGroup
· ext s
letI := Ideal.adic_basis J
rw [J.hasBasis_nhds_zero_adic.mem_iff]
constructor <;> intro H
· rcases H₂ s H with ⟨n, h⟩
exact ⟨n, trivial, h⟩
· rcases H with ⟨n, -, hn⟩
rw [mem_nhds_iff]
exact ⟨_, hn, H₁ n, (J ^ n).zero_mem⟩
