Zulip Chat Archive

Stream: maths

Topic: Simple lemma about irreducible polynomial factors


Eric Wieser (Apr 17 2022 at 14:42):

You asked this on stackexchange too, right?

Eric Wieser (Apr 17 2022 at 14:46):

I think the first bit of the first line translates as (P_xy : mv_polynomial (fin 2) (algebraic_closure ℚ)) (hP : P_xy.coeff 0 = 0)

Eric Wieser (Apr 17 2022 at 15:05):

What does Q[X,Y]Q[X]Q[Y]\overline{ℚ}[X,Y] ∖ \overline{ℚ}[X] ∖ \overline{ℚ}[Y] mean to you? Is that terms where every monomial has at least one X and one Y? Is 0 included?

Ingmar Velien (Apr 17 2022 at 15:19):

Q[X]\overline{\mathbb{Q}}[X] is a ring extension of Q\overline{\mathbb{Q}}. It contains Q:  \overline{\mathbb{Q}}:\ \ Q[X]\overline{\mathbb{Q}}[X] is the set of the univariate XX-containing polynomials and the constant polynomials over Q\overline{\mathbb{Q}}. Q[X,Y]Q[X]Q[Y]\overline{\mathbb{Q}}[X,Y]\setminus\overline{\mathbb{Q}}[X]\setminus\overline{\mathbb{Q}}[Y] is therefore the set of all non-constant bivariate polynomials in XX and YY.

Eric Wieser (Apr 17 2022 at 15:41):

Thanks; the diffculty here arises from the word "contains". As an example, in lean doesn't "contain" ; instead it contains the range of the "obvious" injection from the naturals

Eric Wieser (Apr 17 2022 at 15:47):

That is, you can write

-- the set of all positive integers corresponding to a natural
example : set  := set.range nat.cast
-- the above is a subset of ℤ
example : set.range nat.cast  (set.univ : set ) :=
set.subset_univ _

or

-- the above, along with the proof it forms a semiring
example : subsemiring  := (nat.cast_ring_hom _).range

but not

example :    := sorry -- error, meaningless
example : (set.univ : set )  (set.univ : set ) := sorry -- error, meaningless

Ingmar Velien (Apr 17 2022 at 16:49):

I would expect a hierarchy of the terms in lean/mathlib, not only a list like https://leanprover-community.github.io/mathlib-overview.html#general-algebra. Why isn't available/imported the whole matlib library? Which parts of mathlib do I have to import for (P_xy : mv_polynomial (fin 2) (algebraic_closure ℚ)) (hP : P_xy.coeff 0 = 0)?

Eric Wieser (Apr 17 2022 at 18:04):

If you open the mathlib API docs, you can search for those words in the top right

Eric Wieser (Apr 17 2022 at 18:05):

And the result will tell you the file to import at the top of the page

Eric Wieser (Apr 17 2022 at 18:05):

Searching for mv_polynomial will take you to docs#mv_polynomial

Ingmar Velien (Apr 17 2022 at 21:14):

How can I declare Q[X]\overline{\mathbb{Q}}[X] and Q[X,Y]\overline{\mathbb{Q}}[X,Y] (ring extensions of Q\overline{\mathbb{Q}})?

Eric Wieser (Apr 17 2022 at 22:09):

The first could be mv_polynomial (fin 1) (algebraic_closure ℚ) or polynomial (algebraic_closure ℚ), the latter is the mv_polynomial (fin 2) (algebraic_closure ℚ) that you mentioned in your original message.

Eric Wieser (Apr 17 2022 at 22:10):

(note the () are missing in your original message)

Ingmar Velien (Apr 18 2022 at 09:22):

mv_polynomial is the polynomial, not the ring that contains it. I could reformulate my lemma without Q[X,Y]\overline{\mathbb{Q}}[X,Y], Q[X]\overline{\mathbb{Q}}[X], Q[Y]\overline{\mathbb{Q}}[Y]. But let's try to use the mathematical formulation of the lemma: with these rings . (Someday I have to use these rings and fields like Q(X,Y)\overline{\mathbb{Q}}(X,Y).)
How can I declare a ring extension and a ring extension by adjunction?
Should XX and YY be declared as variables therefore?
Is a ring implemented as a set?
How can the setminus be used?

Johan Commelin (Apr 18 2022 at 09:48):

Ingmar Velien said:

Proof assistants, and Lean, are completely new to me.

  1. How can I derive the following simple lemma in Lean?
  2. How can I let Lean check if the lemma is efficiently written?

This lemma is my first trial to read and write things with Lean. I already know Lean documentation and introductions, but I couldn't find the answers to my questions and the starting point.

Lemma:
Let P(X,Y)Q[X,Y]QP(X,Y)\in\overline{\mathbb{Q}}[X,Y]\setminus\overline{\mathbb{Q}} doesn't have factors pX(X)Q[X]Qp_X(X)\in\overline{\mathbb{Q}}[X]\setminus\overline{\mathbb{Q}} and doesn't have factors pY(Y)Q[Y]Qp_Y(Y)\in\overline{\mathbb{Q}}[Y]\setminus\overline{\mathbb{Q}}.
There are an nN+n\in\mathbb{N}_+ and Q\overline{\mathbb{Q}}-irredcucible P1(X,Y),...,Pn(X,Y)Q[X,Y]Q[X]Q[Y]P_1(X,Y),...,P_n(X,Y)\in\overline{\mathbb{Q}}[X,Y]\setminus\overline{\mathbb{Q}}[X]\setminus\overline{\mathbb{Q}}[Y] so that the equation P(x,y)=0P(x,y)=0 is splitting into the equations P1(x,y)=0,...,Pn(x,y)=0P_1(x,y)=0,...,P_n(x,y)=0.

I already got the answer "mv_polynomial (fin 2) algebraic_closure ℚ", but I don't know how to start.

Do you think this is a reasonable formalisation of the statement you had in mind?

import data.mv_polynomial.comm_ring
import field_theory.is_alg_closed.algebraic_closure
.

noncomputable theory

open mv_polynomial

variables {σ : Type*} {K : Type*} [field K] [is_alg_closed K]

/-- A polynomial `f` in `K[(X_i)_{i ∈ σ}]` is nondegenerate if every divisor `g` of `f`
is either constant or every variable `X_i` occurs in `g`. -/
def nondeg (f : mv_polynomial σ K) : Prop :=
 g : mv_polynomial σ K, g  f  g.degrees = 0  ( i : σ, i  g.degrees)

lemma ingmar (f : mv_polynomial bool K)
  (hf :  g : mv_polynomial bool K, g  f  nondeg g) :
   P : multiset (mv_polynomial bool K),
    ( p  P, irreducible p) 
    ( p  P, nondeg p) 
    P.prod = f :=
sorry

Johan Commelin (Apr 18 2022 at 09:50):

You say

the equation P(x,y)=0P(x,y)=0 is splitting into the equations P1(x,y)=0,...,Pn(x,y)=0P_1(x,y)=0,...,P_n(x,y)=0.

which I translated to P.prod = f. In other words: PP is the product of the PiP_i. If you really want to talk about _=0\_ = 0 equations, then we'll have to rewrite a bit.

Johan Commelin (Apr 18 2022 at 09:52):

Note that I also generalized from Qˉ\bar{\mathbb{Q}} to a random alg.closed KK.

Eric Wieser (Apr 18 2022 at 10:29):

mv_polynomial is the polynomial, not the ring that contains it.

mv_polynomial _ _ is the type containing all such polynomials, and is equipped with a ring structure. So arguably, mv_polynomial _ _ is the ring containing the polynomial, in the same way that ℚ "is" the field containing 12\frac{1}{2}

Eric Wieser (Apr 18 2022 at 10:32):

Strictly speaking ℚ (docs#rat) isn't the field itself though, it's the representation / carrier "set" over which docs#rat.field applies

Ingmar Velien (Apr 18 2022 at 12:30):

Now I have a starting point and I can try to understand it and play with it. Many many thanks.

Junyan Xu (Apr 18 2022 at 13:19):

This is a much cleaner formalization than the original statement, but unfortunately not exactly true when f is a constant other than 0 and 1, in which case there are no irreducible factors and the empty product is 1. That's why we have the associated in the statement of docs#unique_factorization_monoid.iff_exists_prime_factors.

The definition of nondeg can be simplified a bit:

def nondeg (f : mv_polynomial σ K) [fintype σ] : Prop :=
 g : mv_polynomial σ K, g  f  g.vars =   g.vars = 

docs#mv_polynomial.vars

A formalization closer to the original statement is:

def nondeg' (f : mv_polynomial bool K) : Prop :=
 g : mv_polynomial bool K, g  f  g  supported K ({tt} : set bool)  g  supported K ({ff} : set bool)

(needs to import docs#mv_polynomial.supported from data.mv_polynomial.supported)

Kevin Buzzard (Apr 18 2022 at 13:22):

(hf : ∀ g : mv_polynomial bool K, g ∣ f → nondeg g) -- this is I think OK but overkill: why not just ask for nondeg f?

Junyan Xu (Apr 18 2022 at 13:27):

Hmm. It seems ∀ g : mv_polynomial σ K, g ∣ f → should be removed from def nondeg

Kevin Buzzard (Apr 18 2022 at 13:28):

you have to be careful here or else XYXY is a counterexample.

Kevin Buzzard (Apr 18 2022 at 13:28):

You want all divisors to be non-one-variable

Junyan Xu (Apr 18 2022 at 13:29):

Yeah, you don't remove ∀ g : mv_polynomial bool K, g ∣ f → from hf

Johan Commelin (Apr 18 2022 at 13:40):

Aah, right. I refactored my code, but not in the right way :face_palm:

Ingmar Velien (Apr 18 2022 at 14:36):

I need this lemma and its proof for extending the main theorem in [Lin 1983] (Theorem 4, page 49) about non-solvability of equations in the elementary functions by elementary numbers, that is cited also in [Chow 1983] (Theorem 1, page 443), from irreducible polynomials to the more general case of polynomials without single-variable factors.

I already formulated the necessary lemmas, theorems and proofs. Clearly, they are obvious for mathematicians - but only if they once have been formulated. But because I'm not a mathematician, I need assistance and confirmation of my derivations - from mathematicians or software proof assistants.

[Chow 1999] Chow, T.: What is a closed-form number. Am. Math. Monthly 106 (1999) (5) 440-448 http://timothychow.net/closedform.pdf

[Lin 1983] Ferng-Ching Lin: Schanuel's Conjecture Implies Ritt's Conjectures. Chin. J. Math. 11 (1983) (1) 41-50 https://www.jstor.org/stable/43836165

Junyan Xu (Apr 19 2022 at 01:35):

@Ingmar Velien As it turns out, this is a rather trivial statement, which only uses that K[X] is a docs#wf_dvd_domain (aka ascending chain condition on principal ideals, in particular satisfied by Noetherian rings), and that K is a field (in order for nonzero constants to be units):

import data.mv_polynomial.supported
import ring_theory.polynomial.basic

open mv_polynomial unique_factorization_monoid

lemma wf_dvd_domain.exists_factors_eq {α : Type*} [comm_monoid_with_zero α] [wf_dvd_monoid α] (a : α) :
  a  0  ¬ is_unit a   (f : multiset α), ( (b : α), b  f  irreducible b)  f.prod = a :=
begin
  intros hn0 hnu, obtain P,hi,u,rfl := wf_dvd_monoid.exists_factors a hn0,
  rw  P.prod_to_list at hn0 hnu, /- TODO: extract `multiset.prod_erase` -/
  have hP : P.to_list  list.nil,
  { rintro he, apply hnu, rw [he, list.prod_nil, one_mul], exact u.is_unit },
  obtain p,h := list.exists_mem_of_ne_nil _ hP,
  classical, use (P.to_list.erase p).cons (p * u), split,
  { intros a ha, rw [multiset.mem_coe, list.mem_cons_iff] at ha, cases ha,
    { apply associated.irreducible _ (hi p $ (P.mem_to_list p).1 h), rw ha, use u },
    { exact hi a ((P.mem_to_list a).1 $ list.mem_of_mem_erase ha) } },
  { rw [multiset.coe_prod, list.prod_cons, mul_comm p, mul_assoc,
        list.prod_erase h, multiset.prod_to_list, mul_comm] },
end

lemma mv_polynomial.is_unit_fin (n : ) {R : Type*} [comm_ring R] [is_domain R]
  {f : mv_polynomial (fin n) R} (hu : is_unit f) :  r : R, is_unit r  C r = f :=
begin
  induction n with n h,
  { exact is_empty_alg_equiv R _ f, hu.map _, alg_equiv.left_inv (is_empty_alg_equiv R _) f },
  { obtain r',hu',he := polynomial.is_unit_iff.1 (hu.map $ fin_succ_equiv R n),
    obtain r,hu,rfl := h hu', use [r, hu], rw  fin_succ_equiv_comp_C_eq_C, dsimp, rw he,
    apply alg_equiv.symm_apply_apply },
end

lemma mv_polynomial.is_unit {σ R : Type*} [fintype σ] [comm_ring R] [is_domain R]
  {f : mv_polynomial σ R} (hu : is_unit f) :  r : R, is_unit r  C r = f :=
begin
  obtain r,hu,he := mv_polynomial.is_unit_fin _ (hu.map $ rename_equiv R $ fintype.equiv_fin σ),
  use [r, hu], convert  congr_arg (rename_equiv R $ fintype.equiv_fin σ).symm he,
  { apply rename_C }, { apply alg_equiv.symm_apply_apply },
end

lemma ingmar {K : Type*} [field K] (f : mv_polynomial bool K)
  (hf₁ : vars f  )
  (hf₂ :  g : mv_polynomial bool K, g  f  vars g =   vars g = ) :
   P : multiset (mv_polynomial bool K),
    ( p  P, irreducible p) 
    ( p  P, vars p = ) 
    P.prod = f :=
  /- ⊥ is the empty set and ⊤ is the set of all variables (here {tt, ff}) -/
begin
  /- decomposition into prime factors times a unit -/
  obtain P,hi,rfl := wf_dvd_domain.exists_factors_eq f (by {rintro rfl, exact hf₁ vars_0}) _,
  swap, { intro hu, obtain k,_,rfl := mv_polynomial.is_unit hu, exact hf₁ vars_C },
  use [P, hi], split, swap, refl,
  { /- p is irreducible implies it's nonzero and not a unit, i.e. not a constant. -/
    intros p hP, specialize hi p hP,
    apply (hf₂ p $ multiset.dvd_prod hP).resolve_left,
    intro h, have := mem_supported_vars p,
    erw [h, supported_empty, algebra.mem_bot] at this,
    obtain k,rfl := this, by_cases k = 0,
    { apply hi.ne_zero, rw h, apply map_zero },
    { apply hi.not_unit, apply is_unit.map, exact is_unit_iff_ne_zero.2 h } },
end

Ingmar Velien (Apr 28 2022 at 19:46):

Let X,YX,Y indeterminates.
How can I define the set σ={X,Y}σ=\{X,Y\} ?
How can I define a polynomial P over Q\overline{\mathbb{Q}} in dependence of X and Y?
Should I use "constant", "variable", or "def" for that? And how do I proceed for defining that?
Thanks.

Eric Wieser (Apr 28 2022 at 20:00):

I think one way of doing that was described above. Another approach would be something like

-- let A be some commutative algebra over Qbar
variables {A : Type*} [comm_ring A] [algebra (algebraic_closure ) A]
-- X and Y are two arbitrary elements, P is formed from only them and the scalars
variables (X Y : A) (P : A) (hP : P  algebra.adjoin (algebraic_closure ) {X, Y})

Eric Wieser (Apr 28 2022 at 20:06):

Note if you set A = mv_polynomial (fin 2) (algebraic_closure ℚ), X = mv_polynomial.X 0 and Y = mv_polynomial.X 1 then hP is vacuous and you end up with the same formulation as was suggested earlier

Ingmar Velien (Apr 28 2022 at 20:26):

I typed in:

import algebra.ring.basic
import algebra.algebra.subalgebra.basic
import data.mv_polynomial.supported
import data.mv_polynomial.comm_ring
import field_theory.is_alg_closed.algebraic_closure
import ring_theory.polynomial.basic
noncomputable theory
--open mv_polynomial
-- let A be some commutative algebra over Qbar
variables {A : Type*} [comm_ring A] [algebra (algebraic_closure ) A]
-- X and Y are two arbitrary elements, P is formed from only them and the scalars
variables (X Y : A) (P : A) (hP : P  algebra.adjoin (algebraic_closure ) {X, Y})

I got:

15:38: error:
don't know how to synthesize placeholder context:
A : Type u_1,
_inst_1 : comm_ring A,
_inst_2 : algebra (algebraic_closure ) A,
X Y P : A
 Type ?

Eric Wieser (Apr 28 2022 at 20:33):

Maybe you need ({X, Y} : set A) instead of {X, Y}

Ingmar Velien (Apr 28 2022 at 20:35):

Oh yes, that works. Fine. Thanks.

Johan Commelin (Apr 29 2022 at 03:23):

I need this lemma and its proof for extending the main theorem in [Lin 1983] (Theorem 4, page 49) about non-solvability of equations in the elementary functions by elementary numbers, that is cited also in [Chow 1983] (Theorem 1, page 443), from irreducible polynomials to the more general case of polynomials without single-variable factors.

@Ingmar Velien Given that you have :this: application in mind. I think it is much better to work with mv_polynomial as explained upstairs.

Ingmar Velien (Apr 29 2022 at 14:07):

Thanks. I will consider that.

I want to formulate the lemma as much as possible like its mathematical formulations / formulas. I don't want to write an extensive and error-prone software program with a general field KK, an arbitrary number of indeterminates and the set of indices of the indeterminates. (I had expected that a proof assistant for mathematics does understand mathematical formulas / language directly.)

Let X,YX,Y indeterminates. How is the set S={X,Y}S=\{X,Y\} constructed? Is the following the only and simplest way? And what types (????) should I use here?

???? X  Y : ????
inductive S : ????
| X
| Y

Eric Wieser (Apr 29 2022 at 14:21):

inductive S : Type
| X
| Y

Is enough by itself; this creates the two "indeterminates" with names S.X and S.Y

Eric Wieser (Apr 29 2022 at 14:22):

You can then use S anywhere we previously suggested bool or fin 2

Eric Wieser (Apr 29 2022 at 14:26):

The polynomial 2 + 3XY can then be written

example : mv_polynomial S (algebraic_closure ) :=
2 + 3*mv_polynomial.X S.X * mv_polynomial.X S.Y

Reid Barton (Apr 29 2022 at 14:45):

You will probably want to set up some notation so you don't have to type that

Eric Wieser (Apr 29 2022 at 14:47):

... or use Johan's suggestion, where instead of mv_polynomial.X S.X and mv_polynomial.X S.Y you can just use X ff and X tt as there's no S.X to worry about ambiguity with

Ingmar Velien (Apr 30 2022 at 20:18):

How can the following definition of the polynomial P be translated literally into Lean?
Definition:
P : mv_polynomial (fin 2) (algebraic_closure ℚ) so that \nexists p : mv_polynomial (fin 1) (algebraic_closure ℚ), p | P

Eric Wieser (Apr 30 2022 at 20:21):

In lean that statement doesn't make sense because p and P have different types

Eric Wieser (Apr 30 2022 at 20:22):

So you need to explicitly name the "obvious" map between them (it doesn't know whether you want to send 0 : fin 1 to 0 : fin 2 or 1 : fin 2)

Eric Wieser (Apr 30 2022 at 20:23):

I would guess something near docs#mv_polynomial.rename can help here

Eric Wieser (Apr 30 2022 at 20:24):

The statement will be:

import field_theory.is_alg_closed.algebraic_closure

example (P : mv_polynomial (fin 2) (algebraic_closure )) :
  ¬∃ p : mv_polynomial (fin 1) (algebraic_closure ),
    mv_polynomial.rename fin.cast_succ p  P :=
sorry -- this is obviously false, but maybe you have extra assumptions!

Eric Wieser (Apr 30 2022 at 20:24):

(sending 0 to 1 would be docs#fin.succ instead of docs#fin.cast_succ)

Jireh Loreaux (May 01 2022 at 03:07):

Eric, I think that "not exists" was supposed to be another hypothesis on P, not the output type, but maybe I'm wrong. Ingmar, do you want it to be the case that there is no polynomial in either variable alone that divides P? If that's the case, you would need both fin.succ and fin.cast_succ and it would be two hypotheses.

Junyan Xu (May 01 2022 at 05:01):

I think what he wants is (hf₂ : ∀ g : mv_polynomial σ K, g ∣ f → vars g = ⊥ ∨ vars g = ⊤) in my StackExchange answer. Notice that vars g = ⊥ is necessary, since the nonzero constants always divides f; the original question is right about this, but it seems omitted above. @Ingmar Velien If you are not convinced that my formalization captures your mathematical statement, I am happy to explain; formalizing it another way (more literally) would just make it harder to work with, in my opinion. Notice that we have docs#mv_polynomial.mem_supported and docs#mv_polynomial.supported_eq_range_rename, where docs#mv_polynomial.supported is the image of an inclusion from a polynomial ring with less variables to the polynomial ring of interest.

Junyan Xu (May 01 2022 at 05:14):

This would be a more literal translation but also more cumbersome:

import data.mv_polynomial.supported
import field_theory.is_alg_closed.algebraic_closure
open mv_polynomial

abbreviation Qbar := algebraic_closure 
variables (f : mv_polynomial bool Qbar)
(nondeg : ¬  (g  f) (v : bool), g  supported Qbar ({v} : set bool)  g  supported Qbar ( : set bool))

(and I'm a bit puzzled why I need to write : set bool.

Kevin Buzzard (May 01 2022 at 12:19):

You need set bool because right now the {} constructor seems to be super-ambiguous -- I think Lean is open to the idea of there existing some {v} : set X or {v} : finset bool or whatever. At least this is my mental model -- needing to have to explicitly write { ... } : set X is a common idiom and this is how I've always explained it to myself.

Junyan Xu (May 01 2022 at 14:57):

Yes I found I have to write : set X in a lot of cases, but I thought it should be fine if Lean expects a set X at the position. As a recent example, here I don't need to write {i*a} : multiset α. And docs#mv_polynomial.supported has type signature

noncomputable def mv_polynomial.supported
{σ : Type u_1} (R : Type u) [comm_semiring R] (s : set σ) :
subalgebra R (mv_polynomial σ R)

so Lean indeed expects a s : set σ here.

Ingmar Velien (May 06 2022 at 16:58):

Junyan Xu said:

I think what he wants is (hf₂ : ∀ g : mv_polynomial σ K, g ∣ f → vars g = ⊥ ∨ vars g = ⊤)

Yes, I want this. But actually I don't want to have to program it. Actually, I would like to translate the following mathematical formulation word for word, one to one.
Let PQ[X,Y]P\in\overline{\mathbb{Q}}[X,Y] be a polynomial over Q\overline{\mathbb{Q}} that has no factor that is a univariate polynomial over Q\overline{\mathbb{Q}}.
And I want to define that polynomial PP as a variable, not in a procedure.
Actually, I want to use the set {X,Y}\{X,Y\} of the variables.
I want to translate the formulation from Lean directly one to on into mathematical language (Because I want to check the proof).

Eric Wieser (May 06 2022 at 17:15):

What do you mean by wanting PP "in a variable, not in a procedure"?

Eric Wieser (May 06 2022 at 17:23):

Can you give an example of something that was said above where PP was "in a procedure"?

Ingmar Velien (May 06 2022 at 17:32):

I would prefer
variable P : (mv_polynomial ...),
not
example P : (mv_polynomial ...) ...
nodeg (P : (mv_polynomial ...) ...
lemma P : (mv_polynomial ...) ...

Eric Wieser (May 06 2022 at 17:37):

Only the first of those is valid syntax...

Eric Wieser (May 06 2022 at 17:38):

Note that these two statements mean exactly the same thing

variables (P : polynomial R)

example : P + P = 2 * P := sorry
example (P : polynomial R) : P + P = 2 * P := sorry

Eric Wieser (May 06 2022 at 17:41):

You might want to have a read of https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#variables-and-sections to clear things up

Eric Wieser (May 06 2022 at 17:42):

Although I would strongly recommend reading the preceding chapters too

Ingmar Velien (May 06 2022 at 19:40):

I guess the def command needs an action after :=, but now we need to formulate a property (¬¬∃ ...). How can my P be defined in the def command?
And how can I introduce the variables X and Y of the polynomial?

Eric Wieser (May 06 2022 at 19:45):

Ingmar Velien said:

I guess the def command needs an action after :=, but now we need to formulate a property (¬¬∃ ...).

What do you mean by "formulate a property"?

  1. Give a short name for a large proposition, such as

    def is_even (n : nat) : Prop := n % 2 = 0
    
  2. Use a property as a hypothesis in a a lemma, such as

    example (n : nat) (hn : n % 2 = 0) : n ≠ 1 := sorry
    example (n : nat) (hn : is_even n) : n ≠ 1 := sorry
    
  3. Prove a property is true, such as

    example : 0 % 2 = 0 := sorry
    example : is_even 0 := sorry
    

Ingmar Velien (May 06 2022 at 20:02):

Junyan Xu said:

This would be a more literal translation but also more cumbersome:

import data.mv_polynomial.supported
import field_theory.is_alg_closed.algebraic_closure
open mv_polynomial

abbreviation Qbar := algebraic_closure 
variables (f : mv_polynomial bool Qbar)
(nondeg : ¬  (g  f) (v : bool), g  supported Qbar ({v} : set bool)  g  supported Qbar ( : set bool))

(and I'm a bit puzzled why I need to write : set bool.

Fine, that works. I'm hoping nondeg is my polynomial P.
And how to introduce the polynomial variables X and Y?

Eric Wieser (May 06 2022 at 20:13):

f is your polynomial P, I think

Eric Wieser (May 06 2022 at 20:14):

nonneg is the statement name for the proof that f satisfies the properties you asked for

Eric Wieser (May 06 2022 at 20:14):

X is spelt mv_polynomial.X tt, Y is spelt mv_polynomial.Y tt

Ingmar Velien (May 06 2022 at 20:56):

I guess I read from the Lean commands: f Q[X0,X1]\in\overline{\mathbb{Q}}[X_0,X_1], where XX is an arbitrary, non-specified designator.
I guess nondeg is a new variable. If nondeg isn't a polynomial, I guess it's a statement, not a proof, right?
Is f the polynomial with the property that is stated in nondeg?

Ah, mv_polynomial.X works fine. Thanks.

Eric Wieser (May 06 2022 at 21:00):

In (nondeg : ¬ ∃ (g ∣ f), ...), the ¬ ∃ (g ∣ f), ...part is the statement, and nonneg is the name you give to its proof

Eric Wieser (May 06 2022 at 21:01):

Eg, if you'd write in your maths proof "using our hypothesis that f is nondegenerate", you'd write nondeg in the lean proof.

Eric Wieser (May 06 2022 at 21:02):

Is f the polynomial with the property that is stated in [the type of] nondeg?

Yes!

Ingmar Velien (May 06 2022 at 21:18):

But nondeg is my precondition, not my hypothesis. Do I need a different Lean code?

Eric Wieser (May 06 2022 at 21:54):

In lean those are the same thing, so I think you're just using different meanings of the word. Perhaps you're using "hypothesis" to mean "thing you're trying to prove"? Lean calls that the "goal"

Eric Wieser (May 06 2022 at 21:55):

"precondition" is a correct interpretation of what nondeg is though, so your lean code should be fine

Ingmar Velien (May 15 2022 at 15:24):

I want to use as few unknown/new commands as possible.

1.)
The theorem "unique_factorization_monoid.of_exists_unique_irreducible_factors" is already one part I need. But where am I wrong in the following?

import data.mv_polynomial
import field_theory.is_alg_closed.algebraic_closure
import ring_theory.polynomial
import ring_theory.unique_factorization_domain

lemma Mylemma {α : Type*} [cancel_comm_monoid_with_zero α]
(eif :  (a : α), a  0  ( (f : multiset α), ( (b : α), b  f  irreducible b)  associated f.prod a))
(uif :  (f g : multiset α), ( (x : α), x  f  irreducible x)  ( (x : α), x  g  irreducible x)  associated f.prod g.prod  multiset.rel associated f g) : unique_factorization_monoid α :=
unique_factorization_monoid.of_exists_unique_irreducible_factors α

2.)
I use P_XY : (mv_variable (fin 2) (algebraic_closure ℚ)).
How can I use in Lean the fact that Q[X]Q[X,Y]\overline{\mathbb{Q}}[X]\subseteq\overline{\mathbb{Q}}[X,Y] and Q[Y]Q[X,Y]\overline{\mathbb{Q}}[Y]\subseteq\overline{\mathbb{Q}}[X,Y]?

Junyan Xu (May 15 2022 at 15:54):

1) Seems there are some confusion going on here. unique_factorization_monoid.of_exists_unique_irreducible_factorssays that if α is a type with a cancel_comm_monoid_with_zero structure on it, and if α together with the structure satisfies eif (every nonzero element is associated to a product of irreducible elements) and uif (if two products of irreducibles are associated then there exists a 1-1 correspondence between the irreducibles such that the corresponding elements are associated), then α is a unique_factorization_monoid. Your Mylemma simply copies its statement. Notice this requires proof in mathlib because docs#unique_factorization_monoid is defined using wf_dvd_monoid and irreducible_iff_prime in mathlib. However, if you work with polynomial rings over a field, there is no need to invoke unique_factorization_monoid.of_exists_unique_irreducible_factors, since Lean already knows that all polynomial rings over a commutative unique factorization domain is a unique factorization domain via the typeclass inference mechanism (docs#mv_polynomial.unique_factorization_monoid). When you apply a theorem using unique_factorization_monoid α as an argument (i.e. hypothesis), Lean will automatically fill in that argument.

2) Qbar[X], Qbar[Y], Qbar[X,Y] are three different polynomial rings with different underlying types, so it makes no sense to talk about inclusion between them. The correct way to consider Qbar[X] as a subset (even better, subalgebra) of Qbar[X,Y] is through docs#mv_polynomial.supported; Qbar[X] is already realized as a subalgebra of Qbar[X,Y] as mv_polynomial.supported Qbar ({0} : set (fin 2)), and Qbar[Y] as mv_polynomial.supported Qbar ({1} : set (fin 2)).

Kevin Buzzard (May 15 2022 at 15:55):

I want to use as few unknown/new commands as possible.

What do you mean by "command" here? Command has a formal meaning, but you don't really use any commands in a proof; I suspect you might mean something else. Can you give examples of what you think a command is?

Q[X]Q[X,Y]\overline{\mathbb{Q}}[X]\subseteq\overline{\mathbb{Q}}[X,Y]

In Lean this is not meaningful because in Lean k[X]k[X] represents a type, not a set, and distinct types are disjoint. There is an injective map from k[X]k[X] to k[X,Y]k[X,Y]. Your question is difficult to parse because you are asking it in mathematical language. Translating a mathematical question into a formal question involves making decisions about how precisely to formalise the objects you're talking about. So my question to you is how you are defining Q[X]\overline{\mathbb{Q}}[X] and Q[X,Y]\overline{\mathbb{Q}}[X,Y], and once you tell me that, I can tell you how to get the injective map.

Junyan Xu (May 15 2022 at 16:23):

import ring_theory.unique_factorization_domain

lemma Mylemma {α : Type*} [cancel_comm_monoid_with_zero α]
(eif :  (a : α), a  0  ( (f : multiset α), ( (b : α), b  f  irreducible b)  associated f.prod a))
(uif :  (f g : multiset α), ( (x : α), x  f  irreducible x)  ( (x : α), x  g  irreducible x)  associated f.prod g.prod  multiset.rel associated f g) : unique_factorization_monoid α :=
unique_factorization_monoid.of_exists_unique_irreducible_factors eif uif

and you need to provide the eif and uif arguments here, not α. Arguments in {} [] brackets are implicit and need not be supplied; if you want to supply them, you need to write @unique_factorization_monoid.of_exists_unique_irreducible_factors α _ eif uif.

(Strangely, adding the other three imports slow things down a lot for me, and that's why didn't notice the problem earlier and why I removed them here.)

Ingmar Velien (May 15 2022 at 16:25):

1) mv_polynomial is a unique_factorization_monoid. One part of my simple lemma about irreducible polynomial factors from my original question on the top of this discussion should state exactly the statement of eif. How can I formulate and prove that in Lean?

2) Junyan Xu already gave hints for using supported. I want to try to use this.

Kevin Buzzard (May 15 2022 at 16:39):

Are you asking "how do I prove that mv_polynomial (fin 2) (algebraic_closure ℚ)) satisfies eif? Do you know about minimal working examples #mwe (link)? The best way to ask questions here is to formalise the question yourself and to ask it in code rather than in words; this solves all the problems with imprecision which I'm having with some of your earlier posts. Here is the question I'm conjecturing you're asking, this time phrased as a minimal working example:

import tactic
import ring_theory.unique_factorization_domain
import data.mv_polynomial.basic
import field_theory.is_alg_closed.algebraic_closure

@[reducible] def R := mv_polynomial (fin 2) (algebraic_closure )

example :  (a : R), a  0 
  ( (f : multiset R), ( (b : R), b  f  irreducible b)  associated f.prod a) :=
sorry

and here is the answer:

example :  (a : R), a  0 
  ( (f : multiset R), ( (b : R), b  f  irreducible b)  associated f.prod a) :=
wf_dvd_monoid.exists_factors

Ingmar Velien (May 15 2022 at 20:31):

Junyan Xu said:

The correct way to consider Qbar[X] as a subset (even better, subalgebra) of Qbar[X,Y] is through docs#mv_polynomial.supported; Qbar[X] is already realized as a subalgebra of Qbar[X,Y] as mv_polynomial.supported Qbar ({0} : set (fin 2)), and Qbar[Y] as mv_polynomial.supported Qbar ({1} : set (fin 2)).

Where I'm wrong in the following?

import data.mv_polynomial
import data.mv_polynomial.supported
import data.set
import field_theory.is_alg_closed.algebraic_closure

open mv_polynomial

def Q_XY (f : mv_polynomial (fin 2) (algebraic_closure )) : Prop :=
 g : mv_polynomial (fin 2) (algebraic_closure ),
g  f  g  supported (algebraic_closure ) ({0} : set (fin 2))
 g  supported (algebraic_closure ) ({1} : set (fin 2))

variable Q_X : mv_polynomial.supported (algebraic_closure ) ({0} : set (fin 2))
variable Q_Y : mv_polynomial.supported (algebraic_closure ) ({1} : set (fin 2))

#check Q_X  Q_XY

QXYQ_{XY} is a field extension of QXQ_X. Therefore: QXQXYQ_X\subseteq Q_{XY}.

Eric Wieser (May 15 2022 at 20:53):

That says "let Q_X be of type coe_sort S where S = mv_polynomial.supported (algebraic_closure ℚ) ({0} : set (fin 2))".

Eric Wieser (May 15 2022 at 20:53):

But what you wanted to write was "let Q_X = S", right?

Eric Wieser (May 15 2022 at 20:54):

Both sides of need to have type set _, right now neither do. It's a type error in the same way that 1 ⊆ 2 would be

Eric Wieser (May 15 2022 at 20:55):

(The error message should be telling you that)

Ingmar Velien (May 15 2022 at 21:24):

Eric Wieser said:

Both sides of need to have type set _, right now neither do. It's a type error in the same way that 1 ⊆ 2 would be

But how can I correct that?
By that?:

variable Q_X : set (mv_polynomial.supported (algebraic_closure ) ({0} : set (fin 2)))

Isn't a subalgebra a subset of an algebra? Isn't a subfield a subset of a field? How can I apply these properties from abstract algebra?

Yaël Dillies (May 15 2022 at 21:31):

Ingmar, do you believe that ℕ ⊆ ℝ?

Kevin Buzzard (May 15 2022 at 22:07):

(deleted)

Kevin Buzzard (May 15 2022 at 22:08):

A type can never be a subset of anything. If "X is a subset of Y" makes sense in Lean's type theory then X and Y have to be terms not types.

Kevin Buzzard (May 15 2022 at 22:09):

Furthermore X and Y must both be terms of type set A, the type of subsets of a type A.

Kevin Buzzard (May 15 2022 at 22:10):

In Lean there's an injective map from nat to int, one is not a subset of the other because neither of them are sets

Eric Wieser (May 15 2022 at 22:19):

Ingmar Velien said:

But how can I correct that?
By that?:

variable Q_X : set (mv_polynomial.supported (algebraic_closure ) ({0} : set (fin 2)))

Isn't a subalgebra a subset of an algebra? Isn't a subfield a subset of a field? How can I apply these properties from abstract algebra?

I still think you're getting confused about the difference between types and terms, and between : and :=.

Do you understand how to use #check? Do you know how to read its output?

import field_theory.is_alg_closed.algebraic_closure
import data.mv_polynomial.supported

variable Q_X : set (mv_polynomial.supported (algebraic_closure ) ({0} : set (fin 2)))

#check Q_X
-- Q_X :
--   set ↥(mv_polynomial.supported (algebraic_closure ℚ) {0})

#check mv_polynomial.supported (algebraic_closure ) ({0} : set (fin 2))
-- mv_polynomial.supported (algebraic_closure ℚ) {0} :
--   subalgebra (algebraic_closure ℚ) (mv_polynomial (fin 2) (algebraic_closure ℚ))

The first one is what you're doing, but you want the second

Eric Wieser (May 15 2022 at 22:21):

If you write variable S_X : ({1, 2, 3} : set ℕ), that doesn't mean "Let S_X be the set {1, 2, 3}", that means "Let S_X be one of the elements of that set".

If you write variable S_X : set ({1, 2, 3} : set ℕ) (like you tried above with Q_X), that means "Let S_X be a set of where each element is in {1, 2, 3}", aka "one of the subsets of {1, 2, 3}", but written in a very unusual way.

Kevin Buzzard (May 15 2022 at 22:22):

If you want R to be a unique factorisation domain then R has to be a type, so then you have to move away from the idea of "subset" and replace it with the idea of "injective ring homomorphism". This is the reality of formalisation and it reflects what is actually going on in formalised mathematics. Yael's example above: in set theory the naturals are defined as finite ordinals and the reals are defined as equivalence classes of Cauchy sequences so it really is not true that the naturals are a subset of the reals, even though it "feels true". The same is going on here. Polynomials in one variable are internally represented in some way, polynomials in two variables are internally represented in a different way, and one really is not a subset of the other. But the injective ring homomorphism is all you need.

Kevin Buzzard (May 15 2022 at 22:27):

Alternatively you can work with subrings, but then you have to remember that a subring is not a ring because a subring is a term and a ring is a type.

Ingmar Velien (May 16 2022 at 20:14):

Could you please correct and complete the Lean formulations made here?

Ingmar Velien (May 17 2022 at 15:59):

Kevin Buzzard said:

Q[X]Q[X,Y]\overline{\mathbb{Q}}[X]\subseteq\overline{\mathbb{Q}}[X,Y]

...
Translating a mathematical question into a formal question involves making decisions about how precisely to formalise the objects you're talking about. So my question to you is how you are defining Q[X]\overline{\mathbb{Q}}[X] and Q[X,Y]\overline{\mathbb{Q}}[X,Y], and once you tell me that, I can tell you how to get the injective map.

Q[X]\overline{\mathbb{Q}}[X] is obtained from Q\overline{\mathbb{Q}} by adjoining the indeterminate XX.
Q[X,Y]\overline{\mathbb{Q}}[X,Y] is obtained from Q[X]\overline{\mathbb{Q}}[X] by adjoining the indeterminate YY or, alternatively, from Q\overline{\mathbb{Q}} by adjoining the indeterminates XX and YY.

Actually, I just want to define a polynomial P(X,Y)P(X,Y) over Q\overline{\mathbb{Q}} of the two indeterminates XX and YY with degreeX0degreeY0\text{degree}_X\neq 0 \land\text{degree}_Y\neq 0.

Kevin Buzzard (May 17 2022 at 16:38):

You gave two definitions of Qbar[X,Y] and they are mathematially equivalent but they are not equal, so your question is not well-defined. Furthermore when I say "how are you defining them" I don't mean "type some LaTeX" I mean "give a #mwe". You need to be writing Lean code, not LaTeX. This is not informal mathematics, formalisation requires a very high degree of precision, much higher than you are used to in normal LaTeX-based mathematics.


Last updated: Dec 20 2023 at 11:08 UTC