non-zero ideals of Zp are open

Stream: Is there code for X?

[Jz Pan]

Seems that there are missing APIs for topologies on Zp, or it's just me not figuring out how to do it?

For example, any non-zero ideals of Zp (we have classification of them docs#PadicInt.ideal_eq_span_pow_p) are open and docs#IsAdic.

[Yakov Pechersky]

Go from ideal to span to closed ball and then IsUltrametricDist.isOpen_closedBall?

[Yakov Pechersky]

We don't have anything that links IsAdicComplete with IsAdic afaict

[Jz Pan]

Yakov Pechersky said:

Go from ideal to span to closed ball and then IsUltrametricDist.isOpen_closedBall?

Let me try.

It works:

import Mathlib

theorem PadicInt.ideal_isOpen_of_ne_bot {p : ℕ} [Fact p.Prime]
    {s : Ideal ℤ_[p]} (hs : s ≠ ⊥) : IsOpen (s : Set ℤ_[p]) := by
  obtain ⟨n, rfl⟩ := PadicInt.ideal_eq_span_pow_p hs
  have : (p ^ (-n : ℤ) : ℝ) ≠ 0 := by simp [show p ≠ 0 from NeZero.out]
  convert IsUltrametricDist.isOpen_closedBall (0 : ℤ_[p]) this
  ext
  rw [SetLike.mem_coe, Metric.mem_closedBall, dist_zero_right,
    PadicInt.norm_le_pow_iff_mem_span_pow]

[Jz Pan]

... and I want to prove that the zero ideal is not open. My plan is the following: a set U is open if and only if for every point x in U there is an open ball with center on x contained in U (assuming IsUltrametricDist). Do we have this in mathlib?

[Jz Pan]

I found docs#dense_compl_singleton_iff_not_open and docs#not_isOpen_singleton but then stuck.

[Jz Pan]

... and next: Z is dense in Zp, or more generally, Set.range fun x => a * x + b where a b : Nat with a coprime to p is dense in Zp. Maybe I need to use definition to check this?

[EDIT] Found it: docs#PadicInt.denseRange_natCast

[Junyan Xu]

To show {0} is not open you may combine finite_of_compact_of_discrete and discreteTopology_of_isOpen_singleton_zero

[Jz Pan]

Junyan Xu said:

To show {0} is not open you may combine finite_of_compact_of_discrete and discreteTopology_of_isOpen_singleton_zero

Thank you! It works:

import Mathlib

theorem PadicInt.ideal_isOpen_of_ne_bot {p : ℕ} [Fact p.Prime]
    {s : Ideal ℤ_[p]} (hs : s ≠ ⊥) : IsOpen (s : Set ℤ_[p]) := by
  obtain ⟨n, rfl⟩ := PadicInt.ideal_eq_span_pow_p hs
  have : (p ^ (-n : ℤ) : ℝ) ≠ 0 := by simp [show p ≠ 0 from NeZero.out]
  convert IsUltrametricDist.isOpen_closedBall (0 : ℤ_[p]) this
  ext
  rw [SetLike.mem_coe, Metric.mem_closedBall, dist_zero_right,
    PadicInt.norm_le_pow_iff_mem_span_pow]

theorem PadicInt.ideal_isOpen_iff {p : ℕ} [Fact p.Prime]
    {s : Ideal ℤ_[p]} : IsOpen (s : Set ℤ_[p]) ↔ s ≠ ⊥ := by
  refine ⟨?_, PadicInt.ideal_isOpen_of_ne_bot⟩
  rintro h rfl
  rw [Submodule.bot_coe, ← discreteTopology_iff_isOpen_singleton_zero] at h
  have : Finite ℤ_[p] := finite_of_compact_of_discrete
  have : Infinite ℤ_[p] := .of_injective _ CharZero.cast_injective
  exact not_finite ℤ_[p]

[Junyan Xu]

a set U is open if and only if for every point x in U there is an open ball with center on x contained in U

I think you're looking for Metric.isOpen_iff (no need of ultrametricity)

[Jz Pan]

PR created as #23720.

[Jz Pan]

Note that I use a lengthier proof of PadicInt.ideal_isOpen_iff since finite_of_compact_of_discrete is not available in that file. Same as ideal_isClosed, I can't use the fact that an open subgroup is also closed.

[Jz Pan]

Superseded by #23757.

[Jz Pan]

I'm wondering that if results in that PRs could be generalized, e.g. all ideals in $\mathcal{O}_{\mathbb{C}_p}$ should be also closed, and is open if and only if it is not zero.

But $\mathcal{O}_{\mathbb{C}_p}$ is not Noetherian nor compact. Maybe this is also true for a T2 valuation ring?

[Kevin Buzzard]

I should think it's true for a very large class of rings with topology coming from a valuation

[Matthew Jasper]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/Valued/ValuationTopology.html#Valued.valuationSubring_isOpen could be extended to all non zero ideals are open + all ideals are closed, although maybe the assumptions are a little stronger than strictly necessary.

[Jz Pan]

Next question: a closed AddSubgroup in Zp must be an ideal. This should also be true for a DVR whose residue field is Fp.

[Matthew Jasper]

That doesn't sound true, for example there are finite (hence closed) subgroups of $F_p[[X]]$

[Jz Pan]

Oh, sorry. In fact I used that Z is dense in Zp. Seems that it's not true for any other DVRs.

[Jz Pan]

For open AddSubgroups it should still be true.

[Matthew Jasper]

I think you need a DVR where p is a uniformizer and the residue field is Fp for either version to be true.

[Kevin Buzzard]

Oh yes, there are some non-complete DVRs for which it's true

[Jz Pan]

I think an open AddSubgroup in a totally ramified finite extension of Zp is still a non-zero ideal.

[Jz Pan]

It must contains some m ^ n. Suppose it contains m ^ (n + 1) but does not contain m ^ n. Then I think it must equal to m ^ (n + 1), by considering its image in m ^ n / m ^ (n + 1) \equiv Fp. It's not the whole Fp so it can only be trivial.

[Kevin Buzzard]

This is not true. It contains m^(n+1) but its image in R/m^(n+1) can just be some arbitrary subgroup which isn't an ideal. It doesn't have an "image in m^n/m^(n+1)", I don't think this makes sense. Just imagine Z_p[sqrt(p)] mod p = F_p[eps] and choose the line spanned by 1+eps for example.

[Jz Pan]

Sorry, I erroneously assumed that it contained in m ^ n :man_facepalming:

[Jz Pan]

I realized that it's a stupid question, since if K / Qp is a finite extension, then O_K as a topological Zp-module should be just isomorphic to Zp ^ [K : Qp] which clearly has a lot of open and closed subgroups...