# Lemma about splitting of homogeneous polynomial equations into irreducible equations

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 correctly written?
3. How can I let Lean check if the lemma is true?
4. How can I let Lean check if the lemma is well formulated?
5. How can I let check Lean if the lemma is efficiently written?

Until now, I use the Lean web editor at https://leanprover-community.github.io/lean-web-editor.

I already know the Lean structures ring and irreducible. But how can I write a ring of two indeterminates?

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.

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 removed [lean-web-editor] tag, as I don't think the behavior is different from lean.
– Couchy
Apr 16, 2022 at 16:46
• @Couchy Please read the note in the tag info. The tag was added because there are two different online URLs and currently they are using different versions of Lean. Apr 16, 2022 at 17:04
• I don't particularly think that tag is worth having. The difference between the two web editors is no different than between the two versions (3.4.2, unmaintained, vs community version) of lean3.
– Eric
Apr 16, 2022 at 19:27
• Now I've read that Lean 4 doesn't contain the mathlib library and we therefore should use Lean 3 if we want to make mathematics. I don't know if this information from late last year is still up to date.
– IV_
Apr 17, 2022 at 0:02
• I'm not in a position to give a full answer, but is mv_polynomial (fin 2) ℚ what you mean by $\overline{\mathbb{Q}}[X,Y]$? This gives you the polynomials in X and Y with rational coefficients. I'm not familiar with what the overbar means in your notation, so have ignored it.
– Eric
Apr 17, 2022 at 5:26

Here is a full formalization of the statement (note that I generalized from $$\mathbb{Q}$$ to an arbitrary field K, and from $$\{X,Y\}$$ to an arbitrary finite set of variables):

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

lemma IV_ {σ K : Type*} [fintype σ] [field K] (f : mv_polynomial σ K)
/- σ is a finite "set of variables". -/
(hf₁ : vars f ≠ ⊥)
/- vars f is the (finite) set of variables appearing in f. -/
(hf₂ : ∀ g : mv_polynomial σ K, g ∣ f → vars g = ⊥ ∨ vars g = ⊤) :
/- ⊥ is the empty set and ⊤ is the set of all variables. -/
∃ P : multiset (mv_polynomial σ K),
(∀ p ∈ P, irreducible p) ∧
(∀ p ∈ P, vars p = ⊤) ∧
P.prod = f :=
sorry


with a complete proof (with mathlib at commit eb22ba4f6e):

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

open mv_polynomial

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 IV_ {σ K : Type*} [fintype σ] [field K] (f : mv_polynomial σ K)
/- σ is a finite "set of variables". -/
(hf₁ : vars f ≠ ⊥)
/- vars f is the (finite) set of variables appearing in f. -/
(hf₂ : ∀ g : mv_polynomial σ K, g ∣ f → vars g = ⊥ ∨ vars g = ⊤) :
/- ⊥ is the empty set and ⊤ is the set of all variables. -/
∃ P : multiset (mv_polynomial σ K),
(∀ p ∈ P, irreducible p) ∧
(∀ p ∈ P, vars p = ⊤) ∧
P.prod = f :=
begin
/- decomposition into irreducible 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 },
refine ⟨P, hi, _, rfl⟩,
{ /- 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


Thanks to @jmc for writing down an initial formalization on Zulip.

• @IV_ The first block of code needs the same import and open commands as in the second block to work. I edited the post to add them. Apr 19, 2022 at 23:49
• The proof seems too complicated in comparison to the very simple mathematical proof.
– IV_
Apr 22, 2022 at 19:35
• Lean gives the result "No messages." That shows that all formulations are correct according to the Lean language. But how can we see if the proof is mathematically correct and effective?
– IV_
Apr 22, 2022 at 19:37
• The de Bruijn factor cs.ru.nl/~freek/factor is a price you have to pay when formalizing math; it depends on how complete the library (in this case the is_unit lemma and the factorization without multiplying by a unit are missing) and how intelligent automation is (look forward to more progress in AI which also learns from formalized math libraries!). However, once you formalize the definitions and statement and Lean checks the proof, then Lean guarantees that the statement is true, but it doesn't guarantee the definition and statement reflect what you have in mind. Apr 24, 2022 at 6:28
• … Usually, the best way to catch errors in formalizing definitions and statements is to prove facts about the definitions and to use the statements in other proofs. Apr 24, 2022 at 6:30