Show explicit coercions?

Stream: new members

[Michael Stoll]

Is there a way to make the pretty printer indicate what specific coercion hides under a ↑? set_option pp.coercions true does not do that (and false apparently suppresses them completely), and using set_option pp.all true is way too much.
I'm trying to prove a result on p-adic numbers and can't seem to figure out what the ↑ in u - ↑(1 : zmod p) means (where u : ℤ_[p]). norm_cast seemingly cannot do anything with this expression, so I'm looking for a library lemma that gives me that ↑(1 : zmod p) = 1, and knowing what the coercion map is called would probably help.

[Heather Macbeth]

@Michael Stoll If you use VSCode, do you know about the ability to get this information by clicking on the arrow in the infoview?

[Michael Stoll]

Now I know...

[Michael Stoll]

It says coe zmod p ℤ_[p] coe_to_lift (1 : zmod p)). How do I interpret this?

[Heather Macbeth]

Hmm ... what do you get by clicking on the coe_to_lift?

[Heather Macbeth]

(You can keep clicking and clicking to dive deeper)

[Michael Stoll]

coe_to_lift zmod p ℤ_[p] zmod.has_coe_t p

[Michael Stoll]

And then from zmod.has_coe_t p:
zmod.has_coe_t ℤ_[p] padic_int.has_zero padic_int.has_one padic_int.has_add padic_int.has_neg p

[Heather Macbeth]

Right, so it's docs#zmod.has_coe_t

[Heather Macbeth]

which converts an element of zmod p to an element of any ring (or even any R satisfying [has_zero R] [has_one R] [has_add R] [has_neg R])

[Heather Macbeth]

If I remember correctly, the existence of this coercion is rather controversial, since it's so clearly badly behaved on a non-char-p ring.

[Michael Stoll]

But somehow I fail to see the statement that 1 : zmod p is mapped to 1 : ℤ_[p]...

[Yaël Dillies]

docs#padic_int.coe_one ?

[Yaël Dillies]

or is that the wrong way around?

[Yaël Dillies]

docs#zmod.cast_one ?

[Michael Stoll]

The first is ↑(1 : ℤ_[p]) = (1 : ℚ_[p])
The second has an assumption m | n

[Michael Stoll]

So the challenge is to prove

example variables (p : ℕ) [fact (nat.prime p)] : ((1 : zmod p) : ℤ_[p]) = 1

[Michael Stoll]

(deleted)

[Michael Stoll]

Replacing 1 by 0 (on both sides :smile:) is zmod.cast_zero (although both suggest and library_search give me a timeout).

[Michael Stoll]

There is zmod.cast_one', but it wants a target of characteristic p...

[Alex J. Best]

Yeah the library lemmas seem a bit inefficient, this works, but we need the cardinality at least two (which lean knows is implied by prime)

import data.zmod.basic

variables {p : nat} [fact (1 < p)] (R : Type*) [ring R]

@[simp] lemma cast_one : ((1 : zmod p) : R) = 1 :=
begin
  casesI p, exfalso, simp at *, apply (@fact.out _ (_inst_1)),
  casesI p, exfalso, simp at *, apply (@fact.out _ (_inst_1)),
  simp,
end

[Alex J. Best]

After that

example {p : nat} [fact p.prime] (R : Type*) [ring R] : ((1 : zmod p) : R) = 1 :=
begin
  simp,
end

works

[Michael Stoll]

Thanks! This looks like a useful addition to the library.

[Patrick Massot]

What is the intended mathematical content of this lemma?

[Patrick Massot]

Why would you expect a coercion from zmod p to any ring?

[Michael Stoll]

Here is now what all of this was about.

import tactic
import data.zmod.basic
import number_theory.padics
import number_theory.padics.ring_homs -- should not be necessary?
import number_theory.padics.hensel
import data.polynomial.derivative

namespace test

open polynomial

-- From Alex J. Best:
@[simp] lemma cast_one {p : ℕ} [fact (1 < p)] (R : Type*) [ring R] : ((1 : zmod p) : R) = 1 :=
begin
  casesI p, exfalso, simp at *, apply (@fact.out _ (_inst_1)),
  casesI p, exfalso, simp at *, apply (@fact.out _ (_inst_1)),
  simp,
end

theorem square_of_principal_unit (p : ℕ) [fact p.prime] (hp : p ≠ 2) (u : ℤ_[p]) (hu : u.to_zmod = 1) :
  ∃ s : ℤ_[p], s^2 = u :=
begin
  -- We want to use Hensel's lemma, so set up a suitable polynomial
  let F : polynomial ℤ_[p] := X^2 - C u,
  -- and show the relevant condition.
  have hnorm : ∥eval 1 F∥ < ∥eval 1 (derivative F)∥^2 :=
  by { simp,
       have h₂ : ∥(2 : ℤ_[p])∥ = 1 :=
       by { change ∥(2 : ℚ_[p])∥ = 1,
            rw [(by norm_cast : (2 : ℚ_[p]) = ((2 : ℚ) : ℚ_[p])), padic_norm_e.eq_padic_norm],
            norm_cast,
            rw [(by norm_cast : (2 : ℚ) = ↑(2 : ℕ)), padic_norm.padic_norm_of_prime_of_ne hp], },
       simp [h₂],
       have h₃ := padic_int.to_zmod_spec u,
       simp [hu] at h₃,
       rw [norm_sub_rev] at h₃,
       exact h₃, },
  have h := hensels_lemma hnorm,
  cases h with s h,
  use s,
  have hensel := h.left, clear h,
  simp [F] at hensel,
  rw sub_eq_zero at hensel,
  exact hensel,
end

end test

[Heather Macbeth]

Patrick Massot said:

Why would you expect a coercion from zmod p to any ring?

Patrick, sadly, we have this coercion and it's used in several places :). docs#zmod.has_coe_t

[Michael Stoll]

I'd be interested in seeing how one can do this (i.e., mostly the proof of hnorm) more elegantly.

[Michael Stoll]

@Patrick Massot @Heather Macbeth The point is docs#padic_int.to_zmod_spec, which uses exactly this map.

[Heather Macbeth]

There is even an issue to remove it: #3975

[Patrick Massot]

This map really sounds like a very bad idea.

[Michael Stoll]

In the context of p-adic numbers, one wants to have a map that sends a p-adic integer to an approximation in the integers (or naturals), so something like that will be necessary.

[Alex J. Best]

Probably if we had the teichmuller lift as a map from zmod p to Z_p in mathlib that could replace the coe in docs#padic_int.to_zmod_spec and everyone would be happy, but as far as I know we don't have it in this context yet (though it is there for Witt vectors)

[Michael Stoll]

I think one definitely wants a map to ℕ or ℤ here. The Teichmüller lift would also be useful, but would not be an adequate replacement.

[Michael Stoll]

Also, it is not just about ℤ/pℤ, but also ℤ/p^nℤ...

[Johan Commelin]

@Michael Stoll I agree the map should be there. But I think it shouldn't be a coercion.
We have #3975 to remind us that this coercion should be down-graded to an ordinary map. I haven't actually done the work yet.

[Michael Stoll]

@Johan Commelin I think what is missing is something like

theorem padic_int.to_zmod_spec {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]) : z.to_zmod.val = z.zmod_repr := ...
theorem padic_int.to_zmod_pow_spec {p : ℕ} [fact (nat.prime p)] (n : ℕ) (z : ℤ_[p]) : (⇑(padic_int.to_zmod_pow n) z).val = z.appr n := ...

Then one can do reasonable computations.

[Michael Stoll]

As a side note, I would suggest to switch the arguments of padic_int.to_zmopd_pow so that one can write z.to_zmod_pow n instead of padic_int.to_zmod_pow n z.

[Johan Commelin]

I think you should still be able to do that. Does it fail?

[Michael Stoll]

I haven't tried yet. I assume the proofs should be easy, since this should be basically the definition of to_zmod/to_zmod_pow.

[Johan Commelin]

X.foobar Y looks at the type of X, say quux, and then looks up the declaration quux.foobar. It then plugs X into the first explicit argument with type quux. But X doesn't need to be the first explicit argument. Just the first one with type quux.

[Michael Stoll]

IIRC, when I tried to write z.to_zmod_pow n, it complained...

[Michael Stoll]

Perhaps because nat has a coercion to p-adic integers?

[Michael Stoll]

variable (z : ℤ_[2])

#check z.to_zmod_pow 3

gives invalid field notation, function 'padic_int.to_zmod_pow' does not have explicit argument with type (padic_int ...)

[Michael Stoll]

#check padic_int.to_zmod_pow --> Π (n : ℕ), ℤ_[?M_1] →+* zmod (?M_1 ^ n)

[Johan Commelin]

Hmm, that's a surprising error message. Because it clearly does have such an explicit argument.

[Michael Stoll]

There is an implicit ⇑ involved, but I have no idea whether this is relevant.

[Johan Commelin]

@Eric Wieser Do you understand what's going on?

[Michael Stoll]

While trying to prove the first of the two theorems I stated above:

theorem padic_int.to_zmod_spec {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]):
  z.to_zmod.val = z.zmod_repr :=
begin
  simp [padic_int.to_zmod, padic_int.to_zmod_hom, padic_int.zmod_repr],
  -- turns the goal into ↑(classical.some _).val = classical.some _
  -- what to do with that?
end

[Johan Commelin]

That doesn't look pleasant.

[Johan Commelin]

Let me take a look

[Michael Stoll]

Shouldn't there be a constructive way of defining to_zmod? By definition of a Cauchy sequence, there must be an index n such that the corresponding and all following terms have nonnegative valuation and the lowest p-adic bit stays fixed; then take the image of that term.

[Michael Stoll]

That would require the homomorphism from {x : ℚ // ¬ p ∣ x.denom} (i.e., the localization of ℤ at the prime ideal generated by p) to zmod p. Is this available?

[Johan Commelin]

theorem padic_int.to_zmod_spec' {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]) :
  z.to_zmod.val = z.zmod_repr :=
begin
  dsimp only [padic_int.to_zmod, padic_int.to_zmod_hom, ring_hom.coe_mk],
  rw zmod.val_cast_of_lt,
  exact padic_int.zmod_repr_lt_p z,
end

[Johan Commelin]

Note that I added a ' to the name, to avoid a conflict.

[Ruben Van de Velde]

theorem padic_int.to_zmod_spec' {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]):
  z.to_zmod.val = z.zmod_repr :=
begin
  simp only [ring_hom.coe_mk, padic_int.to_zmod, padic_int.to_zmod_hom],
  rw zmod.val_cast_of_lt,
  exact padic_int.zmod_repr_lt_p z,
end

... pretty close :)

[Michael Stoll]

OK, then also:

theorem padic_int.to_zmod_pow_spec' {p : ℕ} [fact (nat.prime p)] (n : ℕ) (z : ℤ_[p]) :
  ((padic_int.to_zmod_pow n) z).val = z.appr n :=
begin
  dsimp only [padic_int.to_zmod_pow, padic_int.to_zmod_hom, ring_hom.coe_mk],
  rw zmod.val_cast_of_lt,
  exact padic_int.appr_lt z n,
end

[Johan Commelin]

As a general remark, if your goal looks like

-- turns the goal into ↑(classical.some _).val = classical.some _

then you have most likely unfolded one definition too many.

[Eric Wieser]

But if you can redefine it without classical.some, it may be worth doing so

[Johan Commelin]

In this case the definition of zmod.repr

[Eric Wieser]

docs#zmod.repr doesn't seem to exist

[Eric Wieser]

Ah, docs#padic_int.zmod_repr

[Johan Commelin]

Sorry, my bad

[Eric Wieser]

Michael Stoll said:

Shouldn't there be a constructive way of defining to_zmod? By definition of a Cauchy sequence, there must be an index n such that the corresponding and all following terms have nonnegative valuation and the lowest p-adic bit stays fixed; then take the image of that term.

I don't think this is enough to compute with, as "the corresponding and all following terms have nonnegative valuation" doesn't look like a decidable predicate to me.

[Reid Barton]

Right, you would need to work with modulated Cauchy sequences: don't just take a quotient of (sequences such that for all $\epsilon$, there exists $n$, ...) but rather a quotient of (sequences together with a modulus of convergence function sending $\epsilon$ to $n$)

[Michael Stoll]

OK, I guess I'll leave this for the time being.

[Michael Stoll]

If one does not take the route to define ℚ_p as a completion of ℚ and then ℤ_p as a subring of ℚ_p, but instead defines ℤ_p as the projective limit of the finite rings ℤ/p^nℤ and then ℚ_p as its field of fractions (or by inverting p), the maps from ℤ_p to ℤ/pℤ etc. would be constructive and immediate.

[Kevin Buzzard]

I was discussing with a post-doc the idea of refactoring Q_p so it's defined the "Bourbaki way" as the uniform space completion of Q with respect to the uniform structure coming from the p-adic metric. But I'm not sure it's worth it.

[Michael Stoll]

My point is that I want to use p-adics, in particular to do computations with them. For this, the more concrete the construction is, the better.

[Kevin Buzzard]

Does it really make a difference what the construction is? Can't you write tactics to do computations? I don't know anything about these matters but with Lean 4 around the corner (where computations will become feasible) I'm interested to hear what you mean. What kind of computations?

[Michael Stoll]

My fairly immediate concern is to be able to prove statements like "if z = 1 mod 8 in ℤ_2, then z is a square" without having to go through contortions. For this, it would be advantageous (or so I think) to have the maps to the finite ring quotients in a fairly explicit way, so that it is easy to use them (instead of having to go via the p-adic norm, for example).

[Damiano Testa]

I had similar concerns when I started using Lean. However, my impression now is that the definition is actually irrelevant, as long as it is equivalent to the definition that you want.

What is certainly important is that one of the lemmas is going to say that elements of $\mathbb{Z}_p$ are coherent sequences elements of $\mathbb{Z}/p^n\mathbb{Z}$.

Of course, there should be a proof of Hensel's lemma as well.

Michael, I think that the contortions that you are worrying about will involve the first few lemmas after the actual definition. Once those are done, I imagine that what the definition actually was will be irrelevant.

[Johan Commelin]

My impression, during the Witt vector project, was that the API for ℤ_[p] would be easier to setup if the definition is the algebraic one.

[Johan Commelin]

But I never tested that claim

[Johan Commelin]

One hybrid approach would be to take the analytic definition of ℚ_[p] and the algebraic definition of ℤ_[p]. And then show is_fraction_ring to glue the two together.

[Michael Stoll]

@Damiano Testa A version of docs#hensels_lemma is actually there. However, I've written a variant (the simpler version using that the reduction mod p is zero for the polynomial and nonzero for the derivative) that I hope will be easier to apply.

[Damiano Testa]

Could there be a coercion from ℤ_[p] to ℚ_[p] with the hybrid approach? Maybe the answer is trivially yes, I'm not sure...

[Johan Commelin]

Yes, but maybe not trivially yes (-;

[Michael Stoll]

Where I had to go through contortions was here (not directly related to p-adics):

lemma two_nonzero_mod_odd_prime (p : ℕ) [fact p.prime] (hp : p ≠ 2) : (2 : zmod p) ≠ 0 :=
begin
  rw (by norm_cast : (2 : zmod p) = ((2 : ℤ) : zmod p)),
  intro hf,
  rw zmod.int_coe_zmod_eq_zero_iff_dvd at hf,
  norm_cast at hf,
  rw nat.prime_dvd_prime_iff_eq _inst_1.1 nat.prime_two at hf,
  exact hp hf,
end

I'm wondering how to deal with this in a better way. Any suggestions?

[Johan Commelin]

@Michael Stoll Note that there is also docs#henselian_ring. And mathlib knows that ℤ_[p] is an example.

[Damiano Testa]

Michael, I think that what you are doing is precisely developping the API to make "some" definition workable. This is exactly what needs to be done and what ultimately makes the initial definition irrelevant, since all the ways in which you might want to use it have already been implemented.

[Johan Commelin]

docs#henselian_local_ring.tfae gives some versions of Hensel's lemma. But other versions are missing, because the proof is actually non-trivial that they are equivalent. You need a bunch about etale maps, iirc

[Michael Stoll]

@Johan Commelin Henselian rings feel way more abstract than what I need...

[Damiano Testa]

Michael I'm not at a computer right now, but I would try to prove that 2 < p, being p prime and not two and then use that to conclude the incongruence. I'm not sure whether it would be faster or not, though...

[Michael Stoll]

OK, here is a one-liner: exact_mod_cast zmod.prime_ne_zero p 2 hp
EDIT: ...which is not found by library_search or suggest using hp.

[Adam Topaz]

It seems to me that we need to figure out how to fill in the following blank:

import number_theory.number_field

variables (K : Type*) [field K] [number_field K]

class is_completion (P : ideal (number_field.ring_of_integers K)) (hP : P.is_prime)
  (L : Type*) [field L] [algebra K L] := _

[Michael Stoll]

I think a student of @Kevin Buzzard has done something related.

[Kevin Buzzard]

The dumb thing you can do is just ask for a K-algebra isomorphism to the completion (which Maria has, as Michael says).

[Alex J. Best]

Michael Stoll said:

OK, here is a one-liner: exact_mod_cast zmod.prime_ne_zero p 2 hp
EDIT: ...which is not found by library_search or suggest using hp.

Library search and suggest will only ever really find one refine or exact statement that matches the goal. So specialized tactics like exact_mod_cast can definitely do more in the situations they are designed for.