Simple lemma about irreducible polynomial factors

Stream: maths

[Eric Wieser]

You asked this on stackexchange too, right?

[Eric Wieser]

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]

What does $\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]

$\overline{\mathbb{Q}}[X]$ is a ring extension of $\overline{\mathbb{Q}}$. It contains $\overline{\mathbb{Q}}:\ \$ $\overline{\mathbb{Q}}[X]$ is the set of the univariate $X$-containing polynomials and the constant polynomials over $\overline{\mathbb{Q}}$. $\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 $X$ and $Y$.

[Eric Wieser]

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]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

Searching for mv_polynomial will take you to docs#mv_polynomial

[Ingmar Velien]

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

[Eric Wieser]

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]

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

[Ingmar Velien]

mv_polynomial is the polynomial, not the ring that contains it. I could reformulate my lemma without $\overline{\mathbb{Q}}[X,Y]$, $\overline{\mathbb{Q}}[X]$, $\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 $\overline{\mathbb{Q}}(X,Y)$.)
How can I declare a ring extension and a ring extension by adjunction?
Should $X$ and $Y$ be declared as variables therefore?
Is a ring implemented as a set?
How can the setminus be used?

[Johan Commelin]

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)\in\overline{\mathbb{Q}}[X,Y]\setminus\overline{\mathbb{Q}}$ doesn't have factors $p_X(X)\in\overline{\mathbb{Q}}[X]\setminus\overline{\mathbb{Q}}$ and doesn't have factors $p_Y(Y)\in\overline{\mathbb{Q}}[Y]\setminus\overline{\mathbb{Q}}$.
There are an $n\in\mathbb{N}_+$ and $\overline{\mathbb{Q}}$-irredcucible $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)=0$ is splitting into the equations $P_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]

You say

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

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

[Johan Commelin]

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

[Eric Wieser]

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 $\frac{1}{2}$

[Eric Wieser]

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

[Ingmar Velien]

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

[Junyan Xu]

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]

(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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

You want all divisors to be non-one-variable

[Junyan Xu]

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

[Johan Commelin]

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

[Ingmar Velien]

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]

@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]

Let $X,Y$ indeterminates.
How can I define the set $σ=\{X,Y\}$ ?
How can I define a polynomial P over $\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]

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]

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]

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]

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

[Ingmar Velien]

Oh yes, that works. Fine. Thanks.

[Johan Commelin]

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]

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 $K$, 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,Y$ indeterminates. How is the set $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]

inductive S : Type
| X
| Y

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Eric Wieser]

... 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]

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]

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

[Eric Wieser]

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]

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

[Eric Wieser]

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]

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

[Jireh Loreaux]

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]

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]

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]

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]

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]

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 $P\in\overline{\mathbb{Q}}[X,Y]$ be a polynomial over $\overline{\mathbb{Q}}$ that has no factor that is a univariate polynomial over $\overline{\mathbb{Q}}$.
And I want to define that polynomial $P$ as a variable, not in a procedure.
Actually, I want to use the set $\{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]

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

[Eric Wieser]

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

[Ingmar Velien]

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

[Eric Wieser]

Only the first of those is valid syntax...

[Eric Wieser]

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]

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]

Although I would strongly recommend reading the preceding chapters too

[Ingmar Velien]

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]

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]

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]

f is your polynomial P, I think

[Eric Wieser]

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

[Eric Wieser]

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

[Ingmar Velien]

I guess I read from the Lean commands: f $\in\overline{\mathbb{Q}}[X_0,X_1]$, where $X$ 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]

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

[Eric Wieser]

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]

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

Yes!

[Ingmar Velien]

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

[Eric Wieser]

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]

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

[Ingmar Velien]

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 $\overline{\mathbb{Q}}[X]\subseteq\overline{\mathbb{Q}}[X,Y]$ and $\overline{\mathbb{Q}}[Y]\subseteq\overline{\mathbb{Q}}[X,Y]$?

[Junyan Xu]

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]

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?

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

In Lean this is not meaningful because in Lean $k[X]$ represents a type, not a set, and distinct types are disjoint. There is an injective map from $k[X]$ to $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 $\overline{\mathbb{Q}}[X]$ and $\overline{\mathbb{Q}}[X,Y]$, and once you tell me that, I can tell you how to get the injective map.

[Junyan Xu]

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]

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]

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]

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

$Q_{XY}$ is a field extension of $Q_X$. Therefore: $Q_X\subseteq Q_{XY}$.

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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]

(The error message should be telling you that)

[Ingmar Velien]

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]

Ingmar, do you believe that ℕ ⊆ ℝ?

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Ingmar Velien]

Kevin Buzzard said:

$\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 $\overline{\mathbb{Q}}[X]$ and $\overline{\mathbb{Q}}[X,Y]$, and once you tell me that, I can tell you how to get the injective map.

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

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

[Kevin Buzzard]

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.