English
In a topological Dedekind domain under the given hypotheses, every nonzero ideal is open.
Русский
В топологическом кольце Дедекина под заданными условиями каждый ненулевой идеал открыт.
LaTeX
$$$ I \neq ⊥ \Rightarrow IsOpen(I) $$$
Lean4
theorem isOpen_of_ne_bot [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ ⊥) : IsOpen (X := R) I :=
by
rw [← Ideal.finprod_heightOneSpectrum_factorization hI,
finprod_eq_finset_prod_of_mulSupport_subset _ (s := (Ideal.finite_mulSupport hI).toFinset) (by simp)]
refine
@AddSubgroup.isOpen_of_isClosed_of_finiteIndex _ _ _ _ (Submodule.toAddSubgroup _) ?_
(IsNoetherianRing.isClosed_ideal _)
refine @AddSubgroup.finiteIndex_of_finite_quotient _ _ _ ?_
refine Ideal.finite_quotient_prod _ _ (fun _ _ ↦ IsNoetherian.noetherian _) fun _ _ ↦ ?_
exact Ideal.finite_quotient_pow (IsNoetherian.noetherian _) _
