Lemma about splitting of homogeneous polynomial equations into irreducible equations

Question

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

Answer 1

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.