Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Hensel's lemma over the p-adic integers #337

Closed
wants to merge 29 commits into from

Conversation

Projects
None yet
6 participants
@robertylewis
Copy link
Collaborator

robertylewis commented Sep 11, 2018

This PR has many additions to the p-adic numbers, most importantly a proof of Hensel's lemma.

There's some cleanup to be done at the points where topology meets the Cauchy sequence construction. I think the pain comes from the fact that Q_p should "really" be constructed with a general normed space completion. In any case, there's a bit more movement between epsilon-delta and tendsto arguments than I'd like. I'll work on cleaning this up.

There are a couple of polynomial identities used in Hensel's lemma that are possibly of more general use, but I'm not sure. Do they belong elsewhere?

TO CONTRIBUTORS:

Make sure you have:

  • reviewed and applied the coding style: coding, naming
  • for tactics:
  • make sure definitions and lemmas are put in the right files
  • make sure definitions and lemmas are not redundant

For reviewers: code review check list

@jcommelin
Copy link
Collaborator

jcommelin left a comment

Wow! This is really cool. That's a very nice result.

apply (pow_add_expansion _ _ _).property
end

private lemma poly_binom_aux2 (p : polynomial α) (x y : α) :

This comment has been minimized.

Copy link
@jcommelin

jcommelin Sep 11, 2018

Collaborator

This is definitely a matter of taste, but in a file related to the p-adics I would prefer if polynomials were not called p but rather something like f.

This comment has been minimized.

Copy link
@robertylewis

robertylewis Sep 11, 2018

Author Collaborator

Fair point! This was moved from another file. I'm still not sure if it belongs here or somewhere else.

@jcommelin

This comment has been minimized.

Copy link
Collaborator

jcommelin commented Sep 11, 2018

A more general question (not meant as criticism, just curiosity): there is a notion of is_henselian : Prop for local rings whose definition certainly isn't hard to formalise. Then there is a theorem that every complete local ring is a henselian ring. We have local rings, and we have complete rings. Do you have any clue how much of your code could be reused for this generalisation? Do we already know that Z_p is a complete local ring?

@robertylewis

This comment has been minimized.

Copy link
Collaborator Author

robertylewis commented Sep 11, 2018

We know that Z_p is a local ring (https://github.com/leanprover/mathlib/pull/337/files#diff-5536b5bb44990238c3178716137a7c14R268) and that it's Cauchy complete (https://github.com/leanprover/mathlib/pull/337/files#diff-5536b5bb44990238c3178716137a7c14R278). As I said, the interface to filtery completeness isn't perfect yet. Is a normed ring that's complete wrt its norm a complete ring? Then we're very close to that. How does the proof go in the more general setting? This one uses the norm on Z_p heavily, so I'm not sure how nicely it would generalize.

@jcommelin

This comment has been minimized.

Copy link
Collaborator

jcommelin commented Sep 11, 2018

So, there is: https://en.wikipedia.org/wiki/Henselian_ring and https://stacks.math.columbia.edu/tag/04GE with the crazy https://stacks.math.columbia.edu/tag/04GG. I'm not sure if these are helpful. But they certainly give an idea about the mathematics.
Concerning complete rings: there are two notions of being complete, a topological and an algebraic one. In all the cases we are interested in these coincide. The topological notion is indeed in mathlib. The algebraic notion is saying that the ring is isomorphic to the (categorical) limit of all quotients modulo powers of the maximal ideal. (I'm not sure, but I think the two notions coincide exactly when the topology is Hausdorff.) See also https://en.wikipedia.org/wiki/Completion_(algebra)
According to https://stacks.math.columbia.edu/tag/03QG the proof in the general case is just using Newton's method, like for Z_p. So that is encouraging. If you click through to https://stacks.math.columbia.edu/tag/04GM you get the details spelled out (mathematically). What do you think?
The key thing that might be missing is the algebraic notion of completeness.

@robertylewis

This comment has been minimized.

Copy link
Collaborator Author

robertylewis commented Sep 12, 2018

Thanks for the references. As far as I can tell, we are indeed missing the algebraic notion of completeness. And I'm not sure we have all the algebra needed to make the more general proof go through yet. Structurally the arguments are the same, and some parts will coincide, but it's definitely not trivial to go from this to the more general version.

@kbuzzard

This comment has been minimized.

Copy link
Collaborator

kbuzzard commented Sep 12, 2018

Patrick is working on this sort of thing right now. We need a theory of complete topological rings and completions for the perfectoid project. In the near future we should be able to take a very general commutative ring and complete it at an ideal, which will give a very general class of rings for which a whole bunch of things like Hensel's Lemma are true. Johan has commented that we might need p-adics for the perfectoid project, but for that particular project I don't see any particular need for what in that optic can just be regarded as a simple special case of a general theory -- we need completions of general rings, not the p-adic numbers. The uses for the p-adics which I envisage are elsewhere (lots of number-theoretic applications to Q and Z). For example here's a proof that there's no rational whose square is 2: if there were, then there would be a 2-adic rational whose square is 2, immediately contadicting the valuation axiom (2*v(x)=1, v an integer).

@kbuzzard

This comment has been minimized.

Copy link
Collaborator

kbuzzard commented Sep 13, 2018

Nobody in number theory calls $$\mathbb{Q}_p$$ "the p-adic rationals" any more -- it's "the p-adic numbers" or even "the p-adics". I find the file name a bit jarring.

@robertylewis

This comment has been minimized.

Copy link
Collaborator Author

robertylewis commented Sep 14, 2018

I went with this file name since, for someone who's just looking for ℚ_p or ℤ_p, it seemed less ambiguous which could be found where. But maybe the cleanest solution is to add a default.lean that imports both, so nobody has to know the file names at all. The term "p-adic rationals" isn't used anywhere else in the files.

@kbuzzard

This comment has been minimized.

Copy link
Collaborator

kbuzzard commented Sep 14, 2018

I propose that we call the file padic_numbers.lean. The "p-adic rationals" terminology is archaic.

@johoelzl
Copy link
Collaborator

johoelzl left a comment

Looks good to me.

Mostly just some indentation nitpicking.

@@ -134,6 +134,17 @@ by_cases
tendsto_inverse_at_top_nhds_0,
tendsto_cong this $ univ_mem_sets' $ by simp *)

lemma tendsto_coe_iff {f : ℕ ℕ} : tendsto f at_top at_top tendsto (λ n, (f n : ℝ)) at_top at_top :=

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

This should be a rewrite rule, i.e. the more complicated term should be on the right.
Can you flip the statement?

Show resolved Hide resolved analysis/normed_space.lean
@@ -412,6 +417,11 @@ begin
end,
ext $ assume a, by simp [single_apply, this]

lemma sum_single' [add_comm_monoid γ] [has_zero β] {a b} (g : α β γ) (hg : g a 0 = 0) :

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

this is sum_single_index

section identities
open polynomial

lemma pow_add_expansion {α : Type*} [comm_semiring α] (x y : α) : (n : ℕ),

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

If it is a subtype shouldn't it be also a definition?

cases pow_add_expansion (k+1) with z hz,
rw [_root_.pow_succ, hz],
existsi (x*z + (k+1)*x^k+z*y),
simp [_root_.pow_succ], ring -- expensive!

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

put ring on its own line.

variables {α : Type*} [decidable_eq α] [comm_ring α]

private lemma poly_binom_aux1 (x y : α) (e : ℕ) (a : α) :
{k : α // a * (x + y)^e = a * (x^e + e*x^(e-1)*y + k*y^2)} :=

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

again subtype and def?


local attribute [instance] classical.prop_decidable

section identities

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

I think these identities should be part of data.polynomial

This comment has been minimized.

Copy link
@robertylewis

robertylewis Sep 17, 2018

Author Collaborator

Okay, I can do that. But pow_add_expansion and pow_sub_pow_factor (should those be renamed?) aren't really specific to polynomials. Still want them there, or should I put those somewhere in algebra?

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

Maybe in group_power?

This comment has been minimized.

Copy link
@robertylewis

robertylewis Sep 17, 2018

Author Collaborator

Ugh, both identities use ring to avoid some nasty computations, and ring depends on group_power. We could add a new file in algebra, factor_identities or something like that. Or just leave them in data.polynomial.

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

I'm fine with adding these identities to ring.

This comment has been minimized.

Copy link
@robertylewis

robertylewis Sep 17, 2018

Author Collaborator

Sorry, I meant tactic.ring, not algebra.ring. They definitely don't belong there.


private lemma comp_tendsto_lim {p : ℕ} {hp : p.prime} {F : polynomial ℤ_[hp]}
(ncs : cau_seq ℤ_[hp] norm) : tendsto (λ i, F.eval (ncs i)) at_top
(nhds (F.eval (padic_int.cau_seq_lim ncs))) :=

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

What about putting the tendsto on one line.

variables {p : ℕ} {hp : p.prime} (F : polynomial ℤ_[hp])

lemma padic_polynomial_dist (x y : ℤ_[hp]) :
∥F.eval x - F.eval y∥ ∥x - y∥ :=

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

usually the indentation here would be just 2.

by convert tendsto_const_nhds; ext; rw ncs_der_val

private lemma ncs_tendsto_lim : tendsto (λ i, ∥F.derivative.eval (ncs i)∥) at_top
(nhds (∥F.derivative.eval (padic_int.cau_seq_lim ncs)∥)) :=

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

does the tendsto fit on one line by itself?

@robertylewis robertylewis force-pushed the robertylewis:padic branch from 73ec997 to cbf056e Sep 17, 2018

@robertylewis

This comment has been minimized.

Copy link
Collaborator Author

robertylewis commented Sep 17, 2018

I've addressed @johoelzl and @kbuzzard 's comments, and rebased to fix some conflicts.

@robertylewis robertylewis force-pushed the robertylewis:padic branch from cbf056e to 0d8f3aa Sep 17, 2018

@robertylewis robertylewis force-pushed the robertylewis:padic branch from 0d8f3aa to 840436d Sep 24, 2018

@robertylewis robertylewis force-pushed the robertylewis:padic branch from 840436d to c199015 Sep 27, 2018

@PatrickMassot

This comment has been minimized.

Copy link
Collaborator

PatrickMassot commented on analysis/limits.lean in b72cc01 Sep 28, 2018

This up-arrow is useless

@PatrickMassot

This comment has been minimized.

Copy link
Collaborator

PatrickMassot commented on analysis/limits.lean in b72cc01 Sep 28, 2018

This up-arrow is also useless

robertylewis and others added some commits Sep 29, 2018

@robertylewis

This comment has been minimized.

Copy link
Collaborator Author

robertylewis commented Oct 2, 2018

I've updated things to use nat.prime as a type class. As expected, it's a lot cleaner. Right now, it's a global attribute, but only added in padic_norm.lean; I suspect this will be more generally useful, so we might want to add it higher up.

I've also tried to clean up the connections between Cauchy completeness and filter completeness. There's more to do here, but I think it's much better than it was.

Johannes, the merge commit you added on my branch has made the history kind of complicated. If this isn't going to be squashed and merged soon, I'll squash everything myself to clean it up.

@johoelzl

This comment has been minimized.

Copy link
Collaborator

johoelzl commented Oct 2, 2018

I'm fine with merging, with one exception: Please don't import topology in data/polynomial. I guess we need a analysis/polynomial.lean for the continuity statement.

I don't like this, as we get into a huge mess if we have too much cyclic dependencies between the top level directories. I think data shouldn't depend on analysis or the *_theory directories.

@robertylewis

This comment has been minimized.

Copy link
Collaborator Author

robertylewis commented Oct 2, 2018

Fair enough. Would you rather have analysis/polynomial.lean with one lemma in it, or put that lemma in one of the existing topology files?

@johoelzl

This comment has been minimized.

Copy link
Collaborator

johoelzl commented Oct 2, 2018

For the beginning analysis.polynomial. I guess with time we might get more continuity etc statements on polynomials.

`padic_norm {p} : prime p → ℚ → ℚ`. Note that this does not lead to a useful instance of
`has_norm` since `p` cannot be inferred from the input, and it is not a norm for
composite `p`. `padic_norm` is shown to be a non-archimedean absolute value.
* Fix `p` and `hp : prime p`. `padic_rationals.lean` defines `ℚ_[hp]` as the Cauchy completion of

This comment has been minimized.

Copy link
@rwbarton

rwbarton Oct 2, 2018

Collaborator

This is just ℚ_[p] now.

This comment has been minimized.

Copy link
@johoelzl

johoelzl Oct 2, 2018

Collaborator

I will fix it

@johoelzl johoelzl closed this in b84e2db Oct 2, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.