Number Fields

Stream: LMFDB

[lmfdb-tunnel]

Chris Birkbeck: In the LMFDB, number fields have a label given by the degree, real signature, abs value of the discriminant and an index. How is this index determined? For example, why did 4.0.1008.1 get index one and 4.0.1008.2 get index two?

[lmfdb-tunnel]

David Roe: I believe that it's noncanonical, and is just determined by the order that the fields are added to the database. To identify a field, you use Pari's polredabs function and then loop through the fields with the same degree, signature and absolute value of discriminant.

[lmfdb-tunnel]

Chris Birkbeck: Aha ok I understand. I'm guessing there isn't some other invariants one could add to them to make the choice canonical (sorry these are maybe silly questions, I'd just never thought about this seriously before).

[lmfdb-tunnel]

David Roe: Nothing we're aware of. The other plausible option would be to compute all the fields of a given degree, signature, discriminant and then sort by their polredabs polynomials. But I'm not sure how expensive it would be.

[lmfdb-tunnel]

Chris Birkbeck: Fair enough, it was mostly a curiosity. I was just thinking about how one would import labels into mathlib, but I guess the index just can't be defined in mathlib then.

[lmfdb-tunnel]

David Roe: Yeah, for a lot objects in the LMFDB the plan should be to provide enough data to uniquely specify the object, and then look it up using that data.

[Chris Birkbeck]

So I have been experimenting with what a LMFDB tactic for number fields might look like. I've made an #LMFDB_search tactic here and what it currently does is given a degree, number of infinite places and absolute discriminant, finds fields in the LMFDB with those properties. You can then import the data into lean, which gives you something like :

noncomputable section

open NumberField

def min_poly_2_0_4_1 : Polynomial ℚ := (1) * Polynomial.X ^ 2 + (1)

abbrev K_2_0_4_1 := AdjoinRoot min_poly_2_0_4_1

instance : Fact (Irreducible min_poly_2_0_4_1) := by sorry

axiom LMFDB_NF_2_0_4_1_discr : discr K_2_0_4_1 = - 4

axiom LMFDB_NF_2_0_4_1_isGalois : IsGalois ℚ K_2_0_4_1

axiom LMFDB_NF_2_0_4_1_classNumber : classNumber K_2_0_4_1 = 1

axiom LMFDB_NF_2_0_4_1_totallyComplex : IsTotallyComplex K_2_0_4_1

instance LMFDB_NF_2_0_4_1_totallyComplexInstance : IsTotallyComplex K_2_0_4_1 := LMFDB_NF_2_0_4_1_totallyComplex

axiom LMFDB_NF_2_0_4_1_isCM : IsCMField K_2_0_4_1

end

Now, here is a question which I expect has a negative answer. Do we have any good tactics for proving polynomials are irreducible in Lean? At the moment I am importing them with a sorry (and everything else as an axiom), but of these things, the irreducibility is maybe the first one you'd want to check.

[Chris Birkbeck]

@Riccardo Brasca maybe you know of good ways to do this?

[Chris Birkbeck]

this is maybe a less trivial example than the one above:

noncomputable section

open NumberField

def min_poly_5_1_1609_1 : Polynomial ℚ := (1) * Polynomial.X ^ 5 + (-1) * Polynomial.X ^ 3 + (-1) * Polynomial.X ^ 2 + (1) * Polynomial.X + (1)

abbrev K_5_1_1609_1 := AdjoinRoot min_poly_5_1_1609_1

instance : Fact (Irreducible min_poly_5_1_1609_1) := by sorry

axiom LMFDB_NF_5_1_1609_1_discr : discr K_5_1_1609_1 = 1609

axiom LMFDB_NF_5_1_1609_1_isGalois : ¬ IsGalois ℚ K_5_1_1609_1

axiom LMFDB_NF_5_1_1609_1_classNumber : classNumber K_5_1_1609_1 = 1



end

[Riccardo Brasca]

Well, this is just hard mathematically, right? Anyway, have you had a look at how this is done in @Anne Baanen 's paper?

[Riccardo Brasca]

They use, I think, a computable version of polynomials, that is something almost surely useful

[Chris Birkbeck]

ah thanks yes. I'll have a look at that paper!

[Chris Birkbeck]

but yes I agree its hard, i just wanted to know if maybe for some small things we could do it.

[Riccardo Brasca]

Mathematically we have Eiseinstein criterion (with the nice variant in Mathlib.RingTheory.Polynomial.Eisenstein.Criterion)

[Riccardo Brasca]

For example, for X ^ 5 - X ^ 3 - X ^ 2 + X + 1 I don't see an immediate answer. It is irreducible mod 2 by a "brute force" argument since there is only an irreducible poly of degree 2 and so it is also irreducible in Z, but this seems a little annoying to formalize

[Chris Birkbeck]

Yeah, you're right that in general this would be hopeless. I'd forgotten that in this paper they had also done some of these things, which seems exactly what one would want.

[Riccardo Brasca]

Well, I guess proving Cohn's irreducibility criterion should not be very hard. Now, putting x = y + 1 gives the polynomial g = y^5 + 5 * y^4 + 9 * y^3 + 6 * y^2 + y + 1 and g 14 = 755791 is prime

[Riccardo Brasca]

the interesting part here is that x = y + 1 and 14 can be found by any unverified software

[Riccardo Brasca]

See also the discussion here

[Edgar Costa]

At some point @Alex J. Best @James Davenport @Mario Carneiro thought a bit about this.
And our approach was to get a computer algebra system to get enough bread crumbs from a computer algebra system to have a tactic build on top of it

[Edgar Costa]

Another approach is: https://arxiv.org/abs/2005.04633

[Alex J. Best]

@Alain Chavarri Villarello surely knows the state of the art here!

[Alain Chavarri Villarello]

In our paper Certifying Rings of Integers in Number Fields (with @Anne Baanenand @Sander Dahmen) we prove irreducibility of polynomials in $\mathbb{Z}[X]$ using a combination of degree analysis (looking at the degree of the irreducible factors after reducing modulo various primes) and the Large Prime Factor Witness Certificate described in the paper by Abbott that @Edgar Costa pointed to.
We indeed used a computable version of polynomials (lists, essentially) to carry out the computations. For the degree analysis, we had to prove irreducibility of polynomials over $\mathbb{F}_p$ and we used Rabin's test for that. I haven't PR'd these theorems to Mathlib yet (Theorem 4.1 and Proposition 4.4) but I plan to do that very soon.
Our certification approach uses data obtained from Sage and is described in Section 4 of the paper, however we did not write a tactic for it.

[Chris Birkbeck]

Yes this is great. I've been playing around with the code in the repo ( I bumped the sections relevant to polynomial irreducibly if that's of any use to you when PRing). So I guess you planning on PRing the computable polynomials stuff to mathlib? I also wanted to ask, have you thought about things like cerfiying class groups?

[Alain Chavarri Villarello]

Yes, I’ve actually been working on certifying class groups :smiley:

Here's where we are so far: using pseudoremainder sequences we can now efficiently certify the discriminant of the defining polynomial and thus, together with a basis for the ring of integers, the discriminant of the number field. We can also certify the signature, compute the Minkowski bound, and certify a $p$-maximal system of independent units. 
For a given non-principal ideal, we can certify its non-principality using this partial knowledge on units, discrete logarithms in $(\mathcal{O}/\mathfrak{q} )^{*}$, and linear algebra over $\mathbb{F}_p$ (this is a saturation technique used in some CAS). 
The most computationally heavy part is proving that we have generated the full class group. For this, we currently use the standard approach of considering all prime ideals of norm up to the Minkowski bound. However, we might want to assume GRH and Bach’s bound at some point when the complexity becomes intractable. 

By proving all prime ideals up to the Minkowski bound, the non-principality of a generator, and the corresponding relations, we’ve managed to prove the class group in a couple of degree-five examples with cyclic class group. For instance, for the number field defined by

def T : ℤ[X] := X^5 + 10*X^3 - 10*X^2 - 15*X - 18
def K := AdjoinRoot (map (algebraMap ℤ ℚ) T)

with Minkowski bound $\approx 155.6$, we can give sorry-free proofs of: 

theorem K_discr : NumberField.discr K = 6250000 := by ...
theorem K_nrComplexPlaces : NumberField.InfinitePlace.nrComplexPlaces K = 2 := by ...
theorem K_minkowski : MinkowskiBound K ≤ (155.6393380746308 : ℝ) := by ...
def class_group_equiv : ZMod 5 ≃+ Additive (ClassGroup (NumberField.RingOfIntegers K)) := by ...
theorem class_number_K_eq_5 : NumberField.classNumber K = 5 := by ...

But this is still very much work in progress and there are still many optimization to be made and more general cases to consider, etc.

[Alain Chavarri Villarello]

Regarding computable polynomials: as far as I know, the discussion about whether Mathlib should include computable polynomials, and which implementation to adopt, has not been settled yet. So I'm not quite sure what the current plan is. There have already been a few new implementations popping up this month https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Computable.20polynomial.20representation.20based.20on.20sorted.20list/near/540630240

[Chris Birkbeck]

Wow this is fantastic! It'll be great to be able to certify even just some class groups but also discriminants and Minkowski bounds. This is exactly the stuff I'd like to add to the LMFDB tactics (since it would be nice to have less axioms).

[Chris Birkbeck]

So I'm not an expert on this, but I know one can compute class groups using the genus class group. But (unless I'm mistaken) you're not doing this here right? So what does your certificate for the class group look like?

[Chris Birkbeck]

As for computable polynomials, this seems to be getting out of hand. Maybe you should just open a PR with your version and let the chaos commence! :p

[Riccardo Brasca]

I seriously think we should start somewhere. Basically everybody wants computable polynomials, the only problem is the implementation. There is for sure no perfect solution, but not having them cannot be the answer.

[Chris Birkbeck]

I completely agree!

[Ruben Van de Velde]

Ah, but does everyone want the same computable polynomials :)

[Riccardo Brasca]

Of course not, that's the issue. But currently we cannot compute X + X = 2 * Xand I am pretty sure any version would do

[Riccardo Brasca]

I hope sooner or later we will have something like Trocq for Lean

[Riccardo Brasca]

(I even know people who are interested in implementing it, but nobody that is actually doing it)

[Chris Birkbeck]

yesterday I found out I couldn't even prove something like X^2+1 is monic without using the computable polynomial stuff, which is also crazy.

[Riccardo Brasca]

we have the monicity tactic for that

[Chris Birkbeck]

oh nice I didnt know about that! thanks!

[Riccardo Brasca]

import Mathlib

open Polynomial

example : (X^2+1 : ℝ[X]).Monic := by
  monicity!

[Chris Birkbeck]

Luckly I said "I cant prove", not we :P

[Riccardo Brasca]

but having a gazilion of tactics cannot be the solution

[Riccardo Brasca]

without saying that those can prove stuff, but still cannot compute. In the sense that I can use compute_degree to show that the degree is 2, but still Lean is unable to find the 2 by itself

[Alain Chavarri Villarello]

Chris Birkbeck ha dicho:

So I'm not an expert on this, but I know one can compute class groups using the genus class group. But (unless I'm mistaken) you're not doing this here right? So what does your certificate for the class group look like?

Indeed! We don’t use the genus class group (or any class field theory). As far as I know, the genus class group gives a factor of the class number, but I believe proving a tight upper bound for the class number would still be computationally hard.

Our approach is algebraic and relies heavily on explicit computations with ideals, and thus we wrote methods for certifying $I = J$, $I * J = K$, a $\mathbb{Z}$-basis for $I$, $\operatorname{Nrm}(I)$, primality of $I$, and other operations on explicitly given ideals.

The certificate consists of two parts, and it's based on the standard approach of determining generators for the class group and relations among them. For ideals $J_1, .., J_m$ of $\mathcal{O}_K$:

• Certify that $\operatorname{Cl}_K = \langle [J_1], .., [J_m] \rangle$.
• Certify that $\langle [J_1], .., [J_m]\rangle = \mathbb{Z}/n_1 \times … \times \mathbb{Z}/n_m$ (where $[J_i] ^ {n_i} = 1$).

These two parts prove that $\prod_{i}n_i$ is an upper and lower bound, respectively, for the class number. Here's a rough description of each part if you want to see more details:

Part 1

Certificate: A collection of ideals $\mathfrak{p}_1, …, \mathfrak{p}_k$, an integer matrix $A$ of size $k \times m$ , a collection of pairs $(\alpha_1, \beta_1),…, (\alpha_k, \beta_k)$ in $\mathcal{O}_K \times \mathcal{O}_K$. 

Verification: 
- Prove that $\{ \mathfrak{p}_1, …, \mathfrak{p}_k\}$ contains all the prime ideals of norm below the Minkowski bound (this step requires a certificate on its own and is the most computationally intensive part).  
- Check that $\alpha_i \mathfrak{p}_i = \beta_i \prod_{j}J_j ^ {A_{ij}}$ for every $i$.

This proves $\operatorname{Cl}_K = \langle [J_1], .., [J_m] \rangle$.

For the second part, consider the cyclic case (an analogous method works in general). To prove $\langle [J] \rangle = \mathbb{Z}/n$ we use a certificate based on saturation techniques implemented in some CASs. Consider a prime $p \mid n$ (for simplicity, assume $p$ does not divide the torsion order of $K$) and let $(r,s)$ be the signature of the number field.  

Part 2

Certificate: A collection of units $\zeta_1, …, \zeta_{r+ s - 1}$, an element $\alpha \in \mathcal{O}_K$ , a set of prime ideals $\mathfrak{q}_1,…,  \mathfrak{q}_k$ such that $p \mid N(\mathfrak{q}_i) -1$, a collection of elements $\xi_1, …, \xi_k$ in $\mathcal{O}_K$, an integer matrix $M$ of size $k \times (r + s)$. 

Verification: 
- Verify that $J ^ n = (\alpha)$
- For every $i$, check that $\xi_i$ is a primitive root in $(\mathcal{O}/\mathfrak{q}_i)^{*}$
- For every $i, j$, verify that $\zeta_j = \xi_i ^ {M_{i j}}$ in $(\mathcal{O}/\mathfrak{q}_i)$ and $\alpha = \xi_i ^ {M_{i (r + s)}}$  in $(\mathcal{O}/\mathfrak{q}_i)$
- Verify that the rank of $(M \mod p)$ equals $r + s$.

This certifies that the set  $\zeta_1, …, \zeta_{r+ s - 1}$ is a $p$-maximal system of units and that $\alpha$ is not of the form $u\beta^ p$ with $u$ a unit and $\beta$ in $\mathcal{O}_K$. Hence, $J^{n/p}$ is not principal. Doing this for every $p \mid n$ shows $\langle [J] \rangle = \mathbb{Z}/n$.

In particular, obtaining the certificate involves 'difficult' tasks such as finding a bunch of relations between ideal classes and computing discrete logarithms, which are delegated to an external CAS.

The efficient certification of the signature of the number field and the Minkowski bound (or a good upper bound for it) were necessary ingredients. That's why we were also interested in those :)

[lmfdb-tunnel]

Andrew Sutherland: As I'm sure you know, part 1 can be greatly sped up by using GRH to improve the Minkowski bound. Indeed, many class groups in the LMFDB are only claimed to be correct under GRH because it would not be computationally feasible to compute them otherwise, and if the choice is between a GRH-conditional result and nothing, the former is preferable. It would be nice to formalize the bounds coming from GRH and the notion of a GRH-dependent certificate. I realize this is not a trivial ask, but it would enable the ceritification of exponentially more class groups.

[Kevin Buzzard]

Can you say more precisely exactly what you mean by "GRH"? Usually when people say "assuming GRH" they mean something a bit weaker and much more precise, such as "the nontrivial zeros of the zeta functions of every imaginary quadratic field are on Re(s)=1/2" or "the nontrivial zeros of L(chi,s) are on Re(s)=1/2 for all Dirichlet characters chi" or whatever. We have the statement of the Riemann hypothesis in Mathlib already and I think that it would be very desirable to have more general statements, but I have seen people using "GRH" to mean hugely complex statements about automorphic L-functions for GL_n or whatever (by "complex" I mean "it's complicated to define the L-functions they're talking about"). What exactly do you mean here?

[lmfdb-tunnel]

Andrew Sutherland: We essentially only care about L-functions associated to ray class characters, see https://arxiv.org/abs/1607.02430 for an example of the current state of the art in terms of proving explicit bounds of this type, and the exact hypotheses that are needed. Bach uses what he calls the "extended Riemann hypothesis" (ERH), which states that all Hecke L-functions are zero-free in the half-plane Re(s) > 1/2; see Bach's paper, in which he proves (in particular) that under EHR the prime ideals of norm up to 6*log^2|D| generate the class group.

[Xavier Roblot]

One way to the computation without needing the Minkowski bound would be to proceed as in Buchmann algorithm. Once we have computed (what you think is) the class group $C$ and the group of units $U$, we compute the product $|C| \, Reg(U)$. If it is close enough to some approximation that you deduced from the analytic class number formula, then you know they are correct. I guess the problem here is that you need to get a good enough approximation (although you only need an approximation up to a factor $2$ if I remember correctly) which might be costly (but there again GRH can help) and furthermore, we need to do some numerical computations which might tricky to do with Lean.
Anyway, that's just my two cents. You probably already thought about that and deduced that it was impractical.

[Alain Chavarri Villarello]

Thanks for the input! We did consider using the analytic class number formula to get an approximation of $h_KR_K$. However, if one doesn’t assume GRH, then computing the residue of the Dedekind zeta function with (proven) high enough precision seems to be quite impractical. If one assumes GRH, then this is doable in polynomial time using truncated Euler products for which there are effective error bounds. However, we indeed decided to avoid analytic methods. Partly because we wanted to have certifications not relying on GRH, and mainly because it would require a significant development of numerical infrastructure (root approximation, computations with logarithmic embeddings, ball arithmetic etc.) which seemed impractical for now (although it would be cool to have eventually, of course). 

Regarding the avoidance of the Minkowski bound using this. I don't quite see how this could be done without first having to prove a system of fundamental units. Maybe I'm misunderstanding something, but in Buchmann's algorithm one starts with a set of ideals that we know generates the class group, which allows one, after finding enough relations, to compute a good candidate for the class number (this will be a proven multiple of the actual class number), and a candidate system of units (which gives us a proven integer multiple of the regulator of the number field). Then comparing their product to $h_KR_K$ certifies that indeed the class number and regulator we found are correct. This would allow us to skip the saturation part (Part II). 

However, I don’t see how we could bypass the computation of a factor base of ideals up to the Minkowski bound (or Bach’s, if we assume GRH) without proving a system of fundamental units to start with. Say we only have a proven subgroup of the class group (so a proven factor of the class number) and a proven system of independent units (so a proven integer multiple of the regulator), then knowing $h_KR_K$ is not enough to certify correctness. Or am I perhaps missing something?  :face_with_peeking_eye:

Of course, one could certify that we indeed have a system of fundamental units by proving $R(U) = R_K$. This could be done by bounding the index $[\mathcal{O}^{*}_K : \mu_K U] = R(U)/R_K$ < $m$ (using a, perhaps very bad, lower bound for the regulator of the number field $R_K$) and proving that $U$ is $p$-maximal for every $p$ less than $m$. Thus allowing us to find the value for $h_K$ once we know $h_KR_K$. But this seems to be at least of subexponential complexity as well (as far as I can tell).

[Alain Chavarri Villarello]

lmfdb-tunnel ha dicho:

Andrew Sutherland: As I'm sure you know, part 1 can be greatly sped up by using GRH to improve the Minkowski bound. Indeed, many class groups in the LMFDB are only claimed to be correct under GRH because it would not be computationally feasible to compute them otherwise, and if the choice is between a GRH-conditional result and nothing, the former is preferable. It would be nice to formalize the bounds coming from GRH and the notion of a GRH-dependent certificate. I realize this is not a trivial ask, but it would enable the ceritification of exponentially more class groups.

We've definitely considered using Bach’s bound (or other improved bounds conditional on GRH) when the computations become infeasible. For now, in our current project, we're thinking of simply adding the corresponding theorem as an axiom (or hypothesis) when we need it (although in the small number of examples that we've verified so far —with relatively small discriminant— Bach’s bound is still larger than Minkowksi’s). That said, I completely agree that it would be great to have the formalized proofs of these bounds assuming GRH, that would be a worthwhile project.

[Xavier Roblot]

@Alain Chavarri Villarello , thanks for the detailed answer. Yes, you are right that Minkowski's bound will be necessary to build the factor base. Sorry I forgot about that and for the noise.

[David Ang]

We're discussing if it's possible to compute and verify regulators, and seems like I'm entirely unfamiliar with the number field API! Here is the set up:

import Mathlib.NumberTheory.NumberField.DedekindZeta

open Polynomial

namespace NF_6_0_19683_1

noncomputable def poly : Polynomial ℚ := X^6 - X^3 + 1
abbrev K : Type := AdjoinRoot poly
instance isIrreducible : Fact (Irreducible poly) := sorry -- this should be filled with the irreducibility certificate mentioned above
noncomputable def a : K := AdjoinRoot.root poly

end NF_6_0_19683_1

The regulator can be defined as the determinant of some explicit logs via regulator_eq_det' (or det), but this requires writing down a fundSystem of units (defined in terms of basisModTorsion), and presumably an explicit set of infinite places (minus one). For this example, SageMath tells me that the fundamental units are -a + 1 and a^5 + a, and there are 0 real embeddings and 3 pairs of complex embeddings (hence the unit rank is 2) given by representatives:

a |--> -0.766044443118978 - 0.642787609686539*I
a |--> -0.173648177666930 - 0.984807753012208*I
a |--> 0.939692620785908 - 0.342020143325669*I

By removing any one of these embeddings, and doing the computation by hand gives me the regulator matrix:

[ 1.26188944840409 -2.11515362714987]
[0.853264178745778  1.26188944840409]

My question is: what's the best way to express the fundamental system of units and the set of embeddings in Lean?

[Riccardo Brasca]

We have everything in mathlib!

[Riccardo Brasca]

I am not saying we have it a form that is suitable for computations though :sweat_smile:

[Riccardo Brasca]

For example the regulator is NumberField.Units.regulator

[Riccardo Brasca]

For the embeddings I think we use K →+* ℂ

[Xavier Roblot]

It is probably easy to add in Mathlib a result that says that, in your case, the embeddings are in bijection with the roots of poly in ℂ. Also, we should add a def to make your element a an algebraic integer similar to what is done with docs#IsPrimitiveRoot.toInteger. One way to prove that -a + 1 is a unit would be to compute its norm but we don't have much API for the resultant in Mathlib, so it is probably easier just to provide its inverse and check that their product is1 (well, this would require to make AdjoinRoot computable). To compute the regulator, you should use instead docs#NumberField.Units.regOfFamily_eq_det'. We could add a result saying that if the family (+ torsion) generates the full unit group then its regulator is equal to the regulator of the field (that should be easy too). The real problem though, as pointed ou by Riccardo, is that most of these things are probably not suited for computations...

[Bhavik Mehta]

Riccardo Brasca said:

I am not saying we have it a form that is suitable for computations though :sweat_smile:

I have a bunch of ideas for doing the computational parts (David + Chris + I have been discussing this recently), from my side the input should be a matrix whose entries are easy to approximate by rationals, and I think I know how to verify a determinant of that. And "easy to approximate by rataionals" includes logs of rationals, since I have code to approximate those by rationals, and presumably we can approximate algebraic integers by rationals easily too, so log of those are covered.

[David Ang]

Riccardo Brasca said:

I am not saying we have it a form that is suitable for computations though :sweat_smile:

Yep, I'm aware that everything is in mathlib, but it's more that I don't really know the API and the constructors (if there are any!)

[David Ang]

Xavier Roblot said:

It is probably easy to add in Mathlib a result that says that, in your case, the embeddings are in bijection with the roots of poly in ℂ. Also, we should add a def to make your element a an algebraic integer similar to what is done with docs#IsPrimitiveRoot.toInteger. One way to prove that -a + 1 is a unit would be to compute its norm but we don't have much API for the resultant in Mathlib, so it is probably easier just to provide its inverse and check that their product is1 (well, this would require to make AdjoinRoot computable). To compute the regulator, you should use instead docs#NumberField.Units.regOfFamily_eq_det'. We could add a result saying that if the family (+ torsion) generates the full unit group then its regulator is equal to the regulator of the field (that should be easy too). The real problem though, as pointed ou by Riccardo, is that most of these things are probably not suited for computations...

Thanks! We're not working with "computations" in the sense that polynomials/fields have to be computable; instead we want to verify the regulator to a certain number of decimal places as a real number, which Bhavik has kindly given us a lot of ideas for.

I'm happy with writing down -a + 1 as a unit, but I wasn't sure how to include it into fundSystem. I wasn't aware of regOfFamily_eq_det', but that looks a lot easier to use than regulator_eq_det' (assuming we have a proof that they're equal)!

Regarding the log embedding: would you just construct the embedding function from an explicit mapping, bundle it to an embedding, consider its equivalence class, consider its associated infinite place, etc...? Are there better constructors for this?

[Xavier Roblot]

I guess you could try to use docs#NumberField.InfinitePlace.mkReal and docs#NumberField.InfinitePlace.mkComplex but indeed things are a bit more complicated for complex places.

[Riccardo Brasca]

Have you already computed a fundamental unit in some nontrivial examples? I think this would be something very nice to do

[David Ang]

Riccardo Brasca said:

import Mathlib

open Polynomial

example : (X^2+1 : ℝ[X]).Monic := by
  monicity!

Hmm...

import Mathlib

example : (Polynomial.X - 1 : Polynomial ℤ).Monic := by
  monicity!

example : (Polynomial.X + -1 : Polynomial ℤ).Monic := by
  monicity!
  rw [Polynomial.coeff_one]
  rfl

Aside: is there a tactic that checks if a polynomial is non-zero directly (rather than calling monicity/compute_degree, then using a lemma)?

[Riccardo Brasca]

Not that I am aware of

[Kenny Lau]

how would you do it aside from computing its degree? you could just add a custom tactic to do that

[Kenny Lau]

import Mathlib

example : (Polynomial.X - 1 : Polynomial ℤ) ≠ 0 := by
  refine Polynomial.degree_ne_bot.mp ?_
  convert WithBot.coe_ne_bot
  compute_degree!
  simp

[David Ang]

Yeah sure, I'm just asking if there is a NeZero tactic already rather than writing one myself (because I still don't know how to write tactics)

[Kenny Lau]

@David Ang

import Mathlib

elab "polynomial_ne_zero" : tactic => Lean.Elab.Tactic.evalTacticSeq =<< `(tacticSeq|
  refine Polynomial.degree_ne_bot.mp ?_
  convert WithBot.coe_ne_bot
  compute_degree!)

example : (Polynomial.X - 1 : Polynomial ℤ) ≠ 0 := by
  polynomial_ne_zero
  simp

I'm happy to write more tactics if you need

[Riccardo Brasca]

Can you use NatDegree and avoid the simp?

[Riccardo Brasca]

Sorry, of course you can not

[Riccardo Brasca]

but still avoiding the last simp would be nice

[Riccardo Brasca]

import Mathlib

elab "polynomial_ne_zero" : tactic => Lean.Elab.Tactic.evalTacticSeq =<< `(tacticSeq|
  refine Polynomial.degree_ne_bot.mp ?_
  convert WithBot.coe_ne_bot
  compute_degree!
  simp)

example : (Polynomial.X - 1 : Polynomial ℤ) ≠ 0 := by
  polynomial_ne_zero

this is ok, but maybe it's not robust

[Kenny Lau]

I don't like this because presumably the simp to discharge the goal should have been the job of compute_degree! (but maybe you know more than me about the tactic)

[Kenny Lau]

import Mathlib

example : (Polynomial.X - 1 : Polynomial ℤ) ≠ 0 := by
  have hn : (Polynomial.X - 1 : Polynomial ℤ).natDegree = (?n : ℕ) := by
    compute_degree!

it seems like sometimes it doesn't work if RHS is mvar?

[Kenny Lau]

yeah, it looks like the tests never tested for metavariables

[Kenny Lau]

import Mathlib.Tactic.ComputeDegree

namespace Mathlib.Tactic.ComputeDegree

open Lean Polynomial

/-- Estimate the natDegree of a given polynomial expression. Assumes that all the coefficients are
non-zero, and produces no proof.

This is a very low-level function and has a lot of bugs. For example, it will not work correctly
with `Polynomial (Polynomial R)`.
-/
partial def estimateNatDegree (p : Expr) : Nat :=
  match p.getAppFnArgs with
  | (``X, _) => 1
  | (``HPow.hPow, #[_, .const ``Nat [], _, _, lhs, rhs]) =>
    have rhsNat := rhs.nat?.getD 0
    estimateNatDegree lhs * rhsNat
  | (``HAdd.hAdd, #[_, _, _, _, lhs, rhs]) =>
    max (estimateNatDegree lhs) (estimateNatDegree rhs)
  | (``HSub.hSub, #[_, _, _, _, lhs, rhs]) =>
    max (estimateNatDegree lhs) (estimateNatDegree rhs)
  | (``HMul.hMul, #[_, _, _, _, lhs, rhs]) =>
    estimateNatDegree lhs + estimateNatDegree rhs
  -- return 0 for everything else
  | _ => 0

theorem ne_zero_proof {R : Type*} [Semiring R] {p : R[X]} {n : ℕ}
    (h₁ : p.natDegree = n) (h₂ : 0 < n) : p ≠ 0 :=
  ne_zero_of_natDegree_gt <| h₁ ▸ h₂

open Elab Tactic Meta

elab "polynomial_ne_zero" : tactic => withMainContext do
  let tgt ← getMainGoal
  let goal ← inferType (.mvar tgt)
  let (``Ne, #[ptype, lhs, _]) := goal.getAppFnArgs | throwError "goal must be _ ≠ 0"
  let (``Polynomial, #[type, inst]) := ptype.getAppFnArgs | throwError "lhs must be polynomial"
  let .succ u ← getLevel ptype | panic "internal"
  have deg := mkNatLit <| estimateNatDegree lhs
  trace[Tactic.compute_degree] m!"Computed degree: {deg}"
  have degStatement := mkApp3 (mkConst ``Eq [1]) (mkConst ``Nat)
    (mkApp3 (mkConst ``natDegree [u]) type inst lhs) deg
  let degPf ← mkFreshMVarId
  degPf.assign =<< elabTerm (← `(term| by compute_degree!)) degStatement
  have posStatement := mkApp4 (mkConst ``LT.lt [0]) (mkConst ``Nat) (mkConst ``instLTNat)
    (mkNatLit 0) deg
  let posPf ← mkFreshMVarId
  posPf.assign =<< elabTerm (← `(term| by norm_num)) posStatement
  tgt.assign <| mkApp6 (mkConst ``ne_zero_proof [u]) type inst lhs deg
    (.mvar degPf) (.mvar posPf)

end Mathlib.Tactic.ComputeDegree

example : (Polynomial.X - 1 : Polynomial ℤ) ≠ 0 := by
  polynomial_ne_zero

[Kenny Lau]

@David Ang i've got this working now

[Kevin Buzzard]

David Ang said:

Yeah sure, I'm just asking if there is a NeZero tactic already rather than writing one myself (because I still don't know how to write tactics)

You should come to the metaprogramming talks on Tuesday mornings at Imperial!

[David Ang]

Thanks!

Kenny Lau said:

David Ang i've got this working now

[David Ang]

Kevin Buzzard said:

David Ang said:

Yeah sure, I'm just asking if there is a NeZero tactic already rather than writing one myself (because I still don't know how to write tactics)

You should come to the metaprogramming talks on Tuesday mornings at Imperial!

I would! But the seminar in UEA is on Tuesdays…

[Kenny Lau]

the best way to learn tactics is to ask someone who knows how to write tactics a lot of basic questions for a week and then you'll be able to learn on your own

[Chris Birkbeck]

I know you first hand that one can write ugly tactics using gemini/chatgpt/claude.

[Riccardo Brasca]

There are also reasonable videos online

[David Ang]

Yeah maybe I should do that

Kenny Lau said:

the best way to learn tactics is to ask someone who knows how to write tactics a lot of basic questions for a week and then you'll be able to learn on your own

[David Ang]

I will grill you with questions one of these weeks!

[Riccardo Brasca]

heather's talks in NYC were for example very good

[Chris Birkbeck]

One suggestion from the last LLL is that we turn all of this computable polynomial stuff into a tactic which sounds interesting to me. That would let you do this and more (like irreducibility proofs).

[Bhavik Mehta]

I think writing basic macros also gets you pretty far, eg

macro "polynomial_ne_zero" : tactic => `(tactic|
  focus
    refine Polynomial.degree_ne_bot.mp ?_
    convert WithBot.coe_ne_bot
    compute_degree! )

like Kenny's from above. There's basically no boilerplate here; just the focus combining the sequence into one tactic (alternatively, you could use elabTacticSeq, but I think the focus one looks less scary!). This is also what Jovan was suggesting to Chris at LLL instead of writing the code as a string. And some "tactics" used in mathlib are basically this already, like the swap and aesop_cat tactics

[Kenny Lau]

I wrote the more detailed code above because compute_degree doesn't actually compute the degree :rofl:

[David Ang]

Yeah I can write basic macros! But only really chaining existing tactics rather than doing something clever