Working with polynomial factorizations

Stream: Is there code for X?

[Heather Macbeth]

Do we have the tools to prove a fact like this? On paper I would say "split all the polynomials as products of linear factors; apply unique factorization; match up and play pigeonhole".

import ring_theory.polynomial.homogeneous
import field_theory.is_alg_closed.basic

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

example {A B q c : mv_polynomial (fin 2) K} (hA : A.is_homogeneous 1) (hB : B.is_homogeneous 2)
  (hq : q.is_homogeneous 2) (hc : c.is_homogeneous 3) (H : B * q = A * c) :
  ∃ x : mv_polynomial (fin 2) K, x.is_homogeneous 1 ∧ x ∣ q ∧ x ∣ c :=
sorry

(I was trying an exercise about the resultant (page 33 here) and this was the part that was hardest to Lean.)

[Heather Macbeth]

Assume any appropriate nondegeneracy hypotheses.

[Johan Commelin]

We do not yet know that mv_polynomial is a UFD, right?

[Kevin Buzzard]

I think we do for finitely many unknowns

[Heather Macbeth]

Independent of that, do we have the factorization into linear factors of (1) a 1-variable polynomial; (2) a 2-variable homogeneous polynomial ? (Assuming an algebraically closed field in each case.)

[Heather Macbeth]

Or, say, do we know that a linear polynomial is irreducible?

[Eric Rodriguez]

we have docs#polynomial.irreducible_of_degree_eq_one; not sure about mv_polynomial

[Heather Macbeth]

Separately, why is ring_theory.polynomial.homogeneous not in the subfolder ring_theory.mv_polynomial?

[Heather Macbeth]

Kevin Buzzard said:

I think we do for finitely many unknowns

@Kevin Buzzard I didn't see even this, where is it?

[Riccardo Brasca]

https://leanprover-community.github.io/mathlib_docs/ring_theory/polynomial/basic.html#polynomial.unique_factorization_monoid

[Riccardo Brasca]

(I am with my phone)

[Riccardo Brasca]

This does not literally say that, but I am pretty sure we have all the isos needed to prove the theorem by induction

[Riccardo Brasca]

In one variable everything is in https://leanprover-community.github.io/mathlib_docs/field_theory/splitting_field.html

[Heather Macbeth]

I also wondered if this lemma existed? If not, where should it live?

import ring_theory.mv_polynomial.basic

open mv_polynomial
variables {σ R : Type*} [comm_semiring R]

example {p q : mv_polynomial σ R} {x : σ → R} (h : eval x p = 0) (hpq : p ∣ q) :
  eval x q = 0 :=
begin
  obtain ⟨r, rfl⟩ := hpq,
  simp [h],
end

[Kevin Buzzard]

Heather Macbeth said:

Kevin Buzzard said:

I think we do for finitely many unknowns

Kevin Buzzard I didn't see even this, where is it?

Yeah I can't find it: I think I was conflating it with polynomials in finitely many variables over a Noetherian ring being Noetherian. Note that a crucial part of this argument is the fact that if you're isomorphic to a Noetherian ring then you are a Noetherian ring, something which we can't prove automatically but which follows easily from the fact that a homomorphic image of a Noetherian ring is Noetherian. However the same trick does not work with UFDs! If R is a UFD then there can be injections R->S and surjections R->S to non-UFDs S (even if S is an integral domain) so we need a transfer lemma. Here's everything apart from that:

import data.mv_polynomial.equiv
import ring_theory.unique_factorization_domain
import ring_theory.polynomial.basic

variables (R : Type*) [comm_ring R] [is_domain R] [unique_factorization_monoid R]

#check @polynomial.unique_factorization_monoid

lemma transfer_fact {R S : Type*} [comm_ring R] [comm_ring S]
  [is_domain R] [is_domain S] (e : R ≃+* S) [unique_factorization_monoid R] :
unique_factorization_monoid S := sorry -- aargh

example (n : ℕ)  : unique_factorization_monoid (mv_polynomial (fin n) R) :=
begin
  induction n with d hd,
  { exact transfer_fact ((mv_polynomial.is_empty_alg_equiv R (fin 0)).to_ring_equiv.symm) },
  { suffices : unique_factorization_monoid (polynomial (mv_polynomial (fin d) R)),
    { resetI,
      exact transfer_fact (mv_polynomial.fin_succ_equiv R d).to_ring_equiv.symm },
    resetI,
    exact polynomial.unique_factorization_monoid }
end

[Kevin Buzzard]

@Mario Carneiro @Scott Morrison here's a good example (after many years of waiting for one!):

import ring_theory.unique_factorization_domain

lemma ring_equiv.unique_factorization_monoid {R S : Type*} [comm_ring R] [comm_ring S]
  [is_domain R] [is_domain S] (e : R ≃+* S) [unique_factorization_monoid R] :
unique_factorization_monoid S :=
{ well_founded_dvd_not_unit := sorry, -- well_founded dvd_not_unit
  irreducible_iff_prime := sorry -- irreducible iff prime
}

One of the goals is transferring well-foundedness over an isomorphism of partial orders, the other is transferring irreducibility and primality over rings.

[Scott Morrison]

The hard-mode challenge here is to arrange so that the proof is by transport along e.

[Kevin Buzzard]

Mario -- $\mathbb{Z}\to\mathbb{Z}[\sqrt{-5}]$ is an injection from a UFD to an integral domain non-UFD, and $\mathbb{Z}[X]\to\mathbb{Z}[\sqrt{-5}]$ (send $X$ to $\sqrt{-5}$ ) is a surjection from a UFD to an integral domain non-UFD, so your trick doesn't get us out of trouble.

[Scott Morrison]

Noting that

example {α : Type} [ring α] {β : Type} (e : α ≃ β) : ring β :=
by transport using e.

is already real Lean code. The challenge is to "upgrade" transport so that it can take advantage of e : R ≃+* S.

[Kevin Buzzard]

The game is to try and get from "R a UFD implies R[X] a UFD" (which we have) to "R a UFD implies mv_polynomial (some fintype) R is a UFD"

[Mario Carneiro]

My trick factors down to the subterms though. Do we know that "irreducible", "prime", "dvd_not_unit" and "well_founded" are preserved under relevant morphisms? I would imagine that at least some of those aren't just invariant under ring equivs, but we should have the theorem in any case

[Heather Macbeth]

Heather Macbeth said:

(I was trying an exercise about the resultant (page 33 here) and this was the part that was hardest to Lean.)

Anyway, that was an instructive exercise but I think I've done all I care to ... here's the branch if anyone else is inspired to take over :-) branch#resultant-quadratic-cubic

[Kevin Buzzard]

Here's unit and irreducible: are the names correct?

import ring_theory.unique_factorization_domain

lemma mul_equiv.is_unit {R S : Type*} [monoid R] [monoid S]
  (e : R ≃* S) (r : R) (h : is_unit r) : is_unit (e r) :=
is_unit.map e h

lemma mul_equiv.is_unit_iff {R S : Type*} [monoid R] [monoid S]
  (e : R ≃* S) (r : R) : is_unit r ↔ is_unit (e r) :=
⟨is_unit.map e, λ s, by { convert is_unit.map e.symm s, simp }⟩

lemma mul_equiv.irreducible {R S : Type*} [monoid R] [monoid S]
  (e : R ≃* S) (r : R) [h : irreducible r] : irreducible (e r) :=
{ not_unit' := λ h1, irreducible.not_unit h ((e.is_unit_iff r).2 h1),
  is_unit_or_is_unit' := begin
    intros a b hr,
    apply_fun e.symm at hr,
    rw [mul_equiv.symm_apply_apply, map_mul] at hr,
    obtain (ha | hb) := irreducible.is_unit_or_is_unit' (e.symm a) (e.symm b) hr,
    { left, rwa e.symm.is_unit_iff a },
    { right, rwa e.symm.is_unit_iff b },
  end }

lemma mul_equiv.irreducible_iff {R S : Type*} [monoid R] [monoid S]
  (e : R ≃* S) (r : R) : irreducible r ↔ irreducible (e r) :=
⟨λ h, by exactI e.irreducible r,
 λ h, by { resetI, convert e.symm.irreducible (e r), rw e.symm_apply_apply, }⟩

for prime I'm not sure if we have isomorphisms of monoids with 0. For well_founded we need isomorphisms of partial orders -- do we have those?

[Mario Carneiro]

I don't think we need mul_equiv.is_unit, I guess this is just for dot-notation?

[Kevin Buzzard]

oh yeah I was just getting the hang of it at that point :-)

[Mario Carneiro]

Is irreducible normally used as an instance argument? I would expect it to be a regular hypothesis here

[Yaël Dillies]

It should be stated using docs#mul_equiv_class

[Kevin Buzzard]

You're talking about isomorphisms of monoids with zero or the transfer lemmas? Presumably the former?

[Mario Carneiro]

It would be nice if mul_equiv.irreducible was true in greater generality, but I guess someone can tell me that it's false (in either direction) for ring homs

[Mario Carneiro]

For well_founded I believe we already have the theorem

[Kevin Buzzard]

yeah, Z -> Q and Z -> Z/3Z both send the irreducible 2 to the unit 2 and irreducibles can't be units

[Mario Carneiro]

what about the other direction? A non-irreducible being sent to an irreducible

[Kevin Buzzard]

ooh that might be OK

[Kevin Buzzard]

oh curses, 6 is not irreducible in Z but it's irreducible in Z[1/2]

[Kevin Buzzard]

What about if the ring hom is a surjection?

[Mario Carneiro]

How is 6 irreducible in Z[1/2]? Isn't it still 2*3?

[Kevin Buzzard]

nope, XY is not irreducible in $\mathbb{C}[X,Y]$ but you can map that onto $\mathbb{C}[Y]$ by sending $X$ to 1.

[Eric Rodriguez]

Mario Carneiro said:

How is 6 irreducible in Z[1/2]? Isn't it still 2*3?

2 is a unit

[Kevin Buzzard]

3 = -1 * -3 but 3 is still irreducible in the integers

[Mario Carneiro]

Oh I thought you meant half-integers

[Kevin Buzzard]

oh that's not a ring

[Kevin Buzzard]

I'm doing fancy localisation

[Mario Carneiro]

Strictly speaking we're talking about monoids here, although I don't know that this makes a difference

[Kevin Buzzard]

Right, but all my rings are monoids

[Kevin Buzzard]

I'm just better at thinking about rings because I'd never heard of monoids 5 years ago ;-)

[Adam Topaz]

Something can probably be said for local ring morphisms in the sense of docs#is_local_ring_hom

[Adam Topaz]

That excludes the localization counterexamples mentioned above.

[Eric Rodriguez]

docs#of_irreducible_map

[Adam Topaz]

Nice! I suppose we also have that ring equivs are local?

[Kevin Buzzard]

Until today that was my favourite transfer example.

[Eric Rodriguez]

docs#is_local_ring_hom_equiv

[Eric Rodriguez]

this stuff should get some fun_like love I think :b

[Kevin Buzzard]

So the Mario excuse to avoid having to write a proper transport tactic is either to say "you haven't specified the problem well enough" or to say "there's no point having a tactic which proves that if X and Y are homeo and X is compact then Y is compact, because a continuous image of compact is compact and that's in your API so just use that".

My one desperate retort to this over the years has been "aah well what about local rings -- if R is local and isomorphic to S then S is local, and being local doesn't transfer along injections or surjections (because the zero ring!) so now please write me a transport tactic". However the modified workaround is this: like preprime (1 or prime) you define a pre-local ring to be either a local ring or the zero ring! Now prelocality does transfer along surjections, and nonzeroness transports along injections, and put the two together and you can deduce that localness transfers along bijections! This was a really annoying observation. But with Heather's brilliant UFD move the ball is firmly back in Mario's court ;-)

[Kevin Buzzard]

Eric Rodriguez said:

docs#is_local_ring_hom_equiv

That's not it. We're looking for "R equiv S and R local implies S local" and I've just sketched a cool way to do it :-)

[Kevin Buzzard]

I can't find morphisms of monoids with zero and I'm assuming that that a monoid morphism (mul_hom) of monoids with 0 doesn't automatically send 0 to 0, so perhaps this is a good time to go to bed.

[Eric Rodriguez]

I think @Yaël Dillies added docs#monoid_with_zero_hom recently

[Yaël Dillies]

To clarify, it's the right object, but no it's not mine.

[Eric Rodriguez]

oopsies, sorry!

[Yaël Dillies]

What I added was docs#order_monoid_with_zero_hom

[Yaël Dillies]

The goal being #3292

[Yaël Dillies]

You can't be blamed because after having defined dozens of homs I myself had to check :sweat_smile:

[Eric Rodriguez]

it's very annoying f 0 = f(0 * a) = f 0 * f adoesn't imply that f 0 = 0 :/

[Eric Rodriguez]

I guess you need cancellation, but anyways that's a tangent

[Kevin Buzzard]

Oh OK great! But we don't have monoid_with_zero_equiv?

[Yaël Dillies]

It's mul_equiv again

[Yaël Dillies]

The pattern is that an isomorphism respects many more properties than originally requested

[Kevin Buzzard]

Yes I got it. Thanks.

[Yaël Dillies]

There must be something like docs#mul_hom.monoid_with_zero_hom or something on one of my branches which does exactly this strengthening, Eric.

[Kevin Buzzard]

The proof is $0_1=0_1\times 0_2=0_2$ so the zero is unique

[Eric Rodriguez]

but for that you need some t such that f t = 0, right?

[Kevin Buzzard]

yeah I mean for the equivs. I'm showing that a monoid-isomorphism of monoids with 0 is a monoid-with-zero isomorphism.

[Yaël Dillies]

Nope, just a 0 in the domain.

[Mario Carneiro]

Kevin Buzzard said:

So the Mario excuse to avoid having to write a proper transport tactic is either to say "you haven't specified the problem well enough" or to say "there's no point having a tactic which proves that if X and Y are homeo and X is compact then Y is compact, because a continuous image of compact is compact and that's in your API so just use that".

My one desperate retort to this over the years has been "aah well what about local rings -- if R is local and isomorphic to S then S is local, and being local doesn't transfer along injections or surjections (because the zero ring!) so now please write me a transport tactic". However the modified workaround is this: like preprime (1 or prime) you define a pre-local ring to be either a local ring or the zero ring! Now prelocality does transfer along surjections, and nonzeroness transports along injections, and put the two together and you can deduce that localness transfers along bijections! This was a really annoying observation. But with Heather's brilliant UFD move the ball is firmly back in Mario's court ;-)

I wouldn't call it an "excuse" so much as a framework for proving equiv lemmas. The fact that often you can make use of something weaker than an equiv is a side benefit but even without that the main point is that every notion in the library should have a theorem proving it is invariant under (suitable kinds of) equivs (or something weaker), and so every transport lemma is only applying these lemmas to each immediate subterm, so they are generally quite short proofs.

[Kevin Buzzard]

Was mul_equiv.irreducible above a short proof? It was mildly annoying. And the well_founded one scares me a bit.

[Mario Carneiro]

The issue is that these proofs do tend to vary in structure a bit depending on what the suitable kind of equiv is or how high-order they are, which makes writing a general tactic difficult

[Kevin Buzzard]

of course I don't mean excuse in a serious way, I'm just giving an irreverent summary of the situation. I do find it fascinating that it's taken years to find this good example.

[Mario Carneiro]

The proof of mul_equiv.irreducible does look worse than it should be

[Kevin Buzzard]

It's an annoying condition!

[Mario Carneiro]

most likely you need to be using more theorems like or.map or something

[Kevin Buzzard]

I'm doing mul_equiv.prime now I've realised mul_equivs send 0 to 0

[Kevin Buzzard]

docs#or.map

[Kevin Buzzard]

hey! I've been duped!

[Bhavik Mehta]

docs#or.imp

[Kevin Buzzard]

import data.mv_polynomial.equiv
import ring_theory.unique_factorization_domain
import ring_theory.polynomial.basic
/-!

irred iff prime stuff

-/
lemma mul_equiv.is_unit_iff {R S : Type*} [monoid R] [monoid S]
  (e : R ≃* S) (r : R) : is_unit r ↔ is_unit (e r) :=
⟨is_unit.map e, λ s, by { convert is_unit.map e.symm s, simp }⟩

lemma mul_equiv.irreducible {R S : Type*} [monoid R] [monoid S]
  (e : R ≃* S) (r : R) [h : irreducible r] : irreducible (e r) :=
{ not_unit' := λ h1, irreducible.not_unit h ((e.is_unit_iff r).2 h1),
  is_unit_or_is_unit' := begin
    intros a b hr,
    apply_fun e.symm at hr,
    rw [mul_equiv.symm_apply_apply, map_mul] at hr,
    obtain (ha | hb) := irreducible.is_unit_or_is_unit' (e.symm a) (e.symm b) hr,
    { left, rwa e.symm.is_unit_iff a },
    { right, rwa e.symm.is_unit_iff b },
  end }

lemma mul_equiv.irreducible_iff {R S : Type*} [monoid R] [monoid S]
  (e : R ≃* S) (r : R) : irreducible r ↔ irreducible (e r) :=
⟨λ h, by exactI e.irreducible r,
 λ h, by { resetI, convert e.symm.irreducible (e r), rw e.symm_apply_apply, }⟩

lemma mul_equiv.prime {R S : Type*} [comm_monoid_with_zero R] [comm_monoid_with_zero S]
  (e : R ≃* S) {r : R} (hr : prime r) : prime (e r) :=
⟨ λ h, hr.1 (by { convert map_zero e.symm, rw [← h, mul_equiv.symm_apply_apply], }),
  λ h, hr.2.1 $ (e.is_unit_iff r).2 h,
  begin
    rintro a b h,
    replace h := e.symm.to_monoid_hom.map_dvd h,
    simp only [mul_equiv.coe_to_monoid_hom, mul_equiv.symm_apply_apply, map_mul] at h,
    refine (hr.2.2 _ _ h).imp _ _,
    { intro h, convert e.to_monoid_hom.map_dvd h, simp },
    { intro h, convert e.to_monoid_hom.map_dvd h, simp },
  end⟩

lemma mul_equiv.prime_iff {R S : Type*} [comm_monoid_with_zero R] [comm_monoid_with_zero S]
  (e : R ≃* S) (r : R) : prime r ↔ prime (e r) :=
⟨e.prime, λ h, by {convert e.symm.prime h, simp }⟩

/-

well-founded dvd not unit stuff

-/

lemma mul_equiv.dvd_not_unit {R S : Type*} [comm_monoid_with_zero R] [comm_monoid_with_zero S]
  (e : R ≃* S) {a b : R} (hd : dvd_not_unit a b) : dvd_not_unit (e a) (e b) :=
⟨ λ h, hd.1 (by { convert map_zero e.symm, rw [← h, mul_equiv.symm_apply_apply], }),
  begin
    obtain ⟨c, hc, rfl⟩ := hd.2,
    exact ⟨e c, λ h, hc ((e.is_unit_iff c).2 h), e.map_mul _ _⟩,
  end⟩

lemma mul_equiv.dvd_not_unit_iff {R S : Type*} [comm_monoid_with_zero R] [comm_monoid_with_zero S]
  (e : R ≃* S) {a b : R} : dvd_not_unit a b ↔ dvd_not_unit (e a) (e b) :=
⟨e.dvd_not_unit, λ h, by {convert e.symm.dvd_not_unit h; simp }⟩

/-

where is my tactic which does this?

-/

lemma ring_equiv.unique_factorization_monoid {R S : Type*} [comm_ring R] [comm_ring S]
  [is_domain R] [is_domain S] (e : R ≃+* S) [hR : unique_factorization_monoid R] :
unique_factorization_monoid S :=
{ well_founded_dvd_not_unit :=
  let i : (dvd_not_unit : S → S → Prop) ↪r (dvd_not_unit : R → R → Prop) :=
  { to_fun := e.symm,
    inj' := equiv_like.injective e.symm,
    map_rel_iff' := λ a b, e.symm.to_mul_equiv.dvd_not_unit_iff.symm }
  in rel_embedding.well_founded i hR.well_founded_dvd_not_unit,
  irreducible_iff_prime := λ a, begin
    rw [e.symm.to_mul_equiv.irreducible_iff,e.symm.to_mul_equiv.prime_iff],
    apply unique_factorization_monoid.irreducible_iff_prime,
  end }

example (R : Type*) [comm_ring R] [is_domain R] [unique_factorization_monoid R] (n : ℕ)  :
unique_factorization_monoid (mv_polynomial (fin n) R) :=
begin
  induction n with d hd,
  { exact (mv_polynomial.is_empty_alg_equiv R (fin 0)).to_ring_equiv.symm.unique_factorization_monoid },
  { suffices : unique_factorization_monoid (polynomial (mv_polynomial (fin d) R)),
    { resetI,
      exact (mv_polynomial.fin_succ_equiv R d).to_ring_equiv.symm.unique_factorization_monoid },
    resetI,
    exact polynomial.unique_factorization_monoid }
end

@Heather Macbeth we've got it now :-)

[Kevin Buzzard]

(I have no idea why I had to increase my deterministic timeout to 10^6 but it compiles for me)

[Heather Macbeth]

Excellent! Remember I have a long list of demands, I also want to split a homogeneous polynomial in 2 variables over an algebraically closed field as a product of linear factors.

[Heather Macbeth]

(Maybe @Jujian Zhang is on the way to this?)

[Kevin Buzzard]

My instinct is to dehomogenise, factor and rehomogenise but that doesn't sound at all nice...

[Heather Macbeth]

I'm a bit rusty here, can a homogeneous polynomial have a non-homogeneous factor?

[Alex J. Best]

We have a bunch of homogenization stuff in flt-regular for doing precisely this sort of thing, explicitly factoring x^n - y^n using the dehomogonized version. So most of the lemmata for that strategy should be already there. Maybe the only thing we don’t have is that dehomogenization (e.g. evaluate some variable at 1) is inverse to homogenization

[Alex J. Best]

I tried to set it up in a way where that would be nice though, in that homogenization doesn’t change the set of variables, so statements like dehomogenize and then rehomogenize is the identity should be literal equalities without changing rings, but we just never needed dehomogenizing yet I think

[Heather Macbeth]

That does look nice! I'll look forward to it being in mathlib!

https://github.com/leanprover-community/flt-regular/blob/master/src/ring_theory/polynomial/homogenization.lean
for anyone else wanting to find it.

[Junyan Xu]

Full generality, using two lemmas above :)
Using this equivalent definition makes it unnecessary to deal with irreducible and well-foundedness.

import ring_theory.unique_factorization_domain

lemma mul_equiv.is_unit_iff {R S : Type*} [monoid R] [monoid S]
  (e : R ≃* S) (r : R) : is_unit r ↔ is_unit (e r) :=
⟨is_unit.map e, λ s, by { convert is_unit.map e.symm s, simp }⟩

lemma mul_equiv.prime {R S : Type*} [comm_monoid_with_zero R] [comm_monoid_with_zero S]
  (e : R ≃* S) {r : R} (hr : prime r) : prime (e r) :=
⟨ λ h, hr.1 (by { convert map_zero e.symm, rw [← h, mul_equiv.symm_apply_apply], }),
  λ h, hr.2.1 $ (e.is_unit_iff r).2 h,
  begin
    rintro a b h,
    replace h := e.symm.to_monoid_hom.map_dvd h,
    simp only [mul_equiv.coe_to_monoid_hom, mul_equiv.symm_apply_apply, map_mul] at h,
    refine (hr.2.2 _ _ h).imp _ _,
    { intro h, convert e.to_monoid_hom.map_dvd h, simp },
    { intro h, convert e.to_monoid_hom.map_dvd h, simp },
  end⟩

lemma mul_equiv.unique_factorization_monoid {R S : Type*}
  [cancel_comm_monoid_with_zero R] [cancel_comm_monoid_with_zero S] (e : R ≃* S)
  (hR : unique_factorization_monoid R) : unique_factorization_monoid S :=
begin
  rw unique_factorization_monoid.iff_exists_prime_factors at hR ⊢,
  intros a ha, rcases hR (e.symm a) (λ h, ha (by {convert ← map_zero e, simp [←h]})) with ⟨w,hp,u,h⟩,
  use w.map e, split,
  { intros b hb, rw multiset.mem_map at hb,
    rcases hb with ⟨c,hc,he⟩, rw ← he, exact e.prime (hp c hc) },
  { use units.map e.to_monoid_hom u,
    erw [multiset.prod_hom, ← e.map_mul, h], simp },
end

[Damiano Testa]

Heather, regarding homogeneity of factors, factors of a homogeneous polynomial must be homogeneous, if the coefficients lie in an integral domain.

If $f$ and $g$ are polynomials with coefficients in an integral domain whose product is homogeneous, they they are homogeneous. Indeed, write $f=f_0+f_1$ with $f_0$ containing the sum of all the terms of minimum degree of $f$ and similarly $g=g_0+g_1$. The product $fg$ contains the homogeneous part $f_0g_0$, having degree less than or equal to the degree of $fg$. The degree of $f_0g_0$ is strictly smaller than the degree of $fg$ if at least one of $f_0$ or $g_0$ has degree strictly smaller than their corresponding polynomials. Thus, if the product is homogeneous, both $f$ and $g$ must be homogeneous.

The integral domain assumption is used to see that $f_0g_0$ is non-zero.

[Heather Macbeth]

@Damiano Testa Nice, thanks! That would simplify the argument a lot.

[Heather Macbeth]

So @Kevin Buzzard @Junyan Xu are you going to PR the UFD instance? :)

[Junyan Xu]

I have limited time to address PR reviews, so it would be ideal if someone else (maybe you) PR it :)

I'm trying to deduce the infinite(ly many variable) case from the finite case, and it seems we don't have this map_var in mathlib right? If so then many lemmas I need (composition, injectivity, joint surjectivity from finsets) are probably also not there.

noncomputable def map_var {R : Type*} {σ τ : Type*} [comm_semiring R] (f : σ → τ) :
  mv_polynomial σ R →+* mv_polynomial τ R := eval₂_hom C (X ∘ f)

[Junyan Xu]

Hmm, I read every file under data.mv_polynomial and in the third-to-last file I discovered that it's called docs#mv_polynomial.rename (and the desired lemmas are there!)
Didn't expect even docs#mv_polynomial.exists_finset_rename is there (seems it's only applied to docs#mv_polynomial.eq_zero_or_eq_zero_of_mul_eq_zero)

[Johan Commelin]

We even know it's monadic in σ (-;

[Junyan Xu]

It has now been established that a polynomial ring of arbitrary number of variables over a UFD is itself a UFD: https://gist.github.com/alreadydone/31f1ee37aba285115cdb365d3fcdfd6a#file-mv_polynomial_ufd-lean-L128

[Riccardo Brasca]

Do you mind PRing it?

[Junyan Xu]

If someone wants to PR please feel free to do so! If no one does it I'll PR in a few days (declarations need to go into multiple files).

[Junyan Xu]

This is the first time I use something less general to prove something strictly more general. I guess this is an appropriate occasion to mark the less general stuff private.

[Johan Commelin]

I think it should be called _aux, because private has been causing mysterious bugs lately.

[Alex J. Best]

In this case I don't think you need to worry. It seems like most of the private issues come from tactics applying private lemmas in other files, not from using a private lemma immediately after it is defined (and it might be fixed now anyways)

[Junyan Xu]

PR opened at #12866

[Heather Macbeth]

Nice!

Does this argument of Damiano now imply that the homogeneous multivariable polynomials form a unique factorization monoid?

[Junyan Xu]

I think yes. Any submonoid of a cancel_comm_monoid_with_zero that contains zero is again a cancel_comm_monoid_with_zero. Damiano's argument shows that that the homogeneous polynomials in a multivariate polynomial ring over an integral domain is a saturated submonoid (if xy is in the submonoid then x and y are also). However, it seems that the weaker property, that if xy and x are in the submonoid then y is also, already implies that dvd, is_unit, prime, irreducible are all the same in the submonoid as in the whole polynomial ring, so we can transfer wf_dvd_domain and irreducible_iff_prime properties to the submonoid, so the submonoid is also a unique_factorization_monoid.

Now, by existence of factorization into primes the submonoid (which remains prime in the whole ring) and uniqueness in the whole polynomial ring, and since all units are homogeneous of degree 0 in a polynomial ring over a domain, we see that the factors of a homogeneous polynomial must be homogeneous, so the weaker property implies the stronger saturatedness. A weird argument!

[Junyan Xu]

Hmm, I made some errors: with the weaker condition, primeness in the whole ring implies primeness in the submonoid, but not vice versa.

[Junyan Xu]

I've successfully shown that a saturated submonoid of a unique_factorization_monoid containing 0 is itself a unique_factorization_monoid:

submonoid.ufm :
  ∀ {α : Type u_2} [_inst_1 : cancel_comm_monoid_with_zero α] (s : submonoid α) [hmem : fact (0 ∈ s)],
    (∀ ⦃a b : α⦄, b ∈ s → a ∣ b → a ∈ s) →
    unique_factorization_monoid α → unique_factorization_monoid ↥s

https://gist.github.com/alreadydone/869f2810d6b9a31eb2d4632e8df26c68

[Junyan Xu]

Hmm, as currently stated, this is a vacuous statement, since everything divides 0 so everything must belong to the submonoid. The correct condition should be ∀ ⦃a b : α⦄, b ∈ s → b ≠ 0 → a ∣ b → a ∈ s. Without b ≠ 0, this condition isn't satisfied by the homogeneous polynomials over a domain.

[Junyan Xu]

I managed to formalize Damiano's argument at what I think is appropriate generality for mathlib; here I show that factors of a nonzero homogeneous element in an algebra without zero divisors graded by a linear_ordered_cancel_add_comm_monoid are also homogeneous:
https://gist.github.com/alreadydone/6f26faa1bde01d1f7785a08bf83a6a28

[Heather Macbeth]

@Junyan Xu, awesome!

[Heather Macbeth]

I see you got the UFM part working too?

[Junyan Xu]

Thanks! I realize that we seem to be missing the graded_algebra instance on mv_polynomial.homogeneous_submodule σ R so my result can't be directly applied to mv_polynomial yet. I'm trying to construct one now; it seems everything necessary is in ring_theory.polynomial.homogeneous.

[Junyan Xu]

Yes I made the UFM part work with the appropriate nonzero assumption, so you can concatenate the two gists. I'm not sure how useful the UFM instance is though; I used the UFM instance to show that being prime in the homogeneous submonoid is the same as being prime in the whole ring, but the irreducible_iff equivalence doesn't rely on UFM and may be good enough for applications.

[Heather Macbeth]

Well, so here was my original motivation:

import ring_theory.polynomial.homogeneous
import field_theory.is_alg_closed.basic

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

example {A B q c : mv_polynomial (fin 2) K} (hA : A.is_homogeneous 1) (hB : B.is_homogeneous 2)
  (hq : q.is_homogeneous 2) (hc : c.is_homogeneous 3) (H : B * q = A * c) :
  ∃ x : mv_polynomial (fin 2) K, x.is_homogeneous 1 ∧ x ∣ q ∧ x ∣ c :=
sorry

[Heather Macbeth]

It certainly feels like it should reduce to some factorization argument, but I don't have a theory about what the exact shortest path is.

[Junyan Xu]

I think you would only need that the mv_polynomial in two variables is UFD if you use the dehomogenize-factor-homogenize approach suggested by Kevin. However it might be easier to show that every homogeneous polynomial has a linear homogeneous factor (over alg_closed field), and to iterate this process it's most convenient to use the saturatedness I just showed to deduce the other factor is also homogeneous, so eventually we factorize B,q,A,c into products of multisets of linear factors. It's easy to show linear factors are irreducible (total_degree of a product of polynomials over an integral domain is the sum of total_degrees, so one of the factors must be degree 0, hence a constant and a unit). Then you use 2+3>2+2=1+3 to show that no matter how you permute the elements, the multisets of factors of q and c must overlap up to associates, so you get a (homogeneous) linear factor that divides both.

[Junyan Xu]

It turns out there are already two PRs #8913 and #10119 (latest activity 23 days ago by @Jujian Zhang) providing the graded_algebra instance.

[Jujian Zhang]

I just cleaned up #10119, it should be usable now if you need it

[Jake Levinson]

Heather Macbeth said:

It certainly feels like it should reduce to some factorization argument, but I don't have a theory about what the exact shortest path is.

What about something like: factor q into linear factors x_1 x_2, then use that linear factors are prime? (Most of the discussion above seemed to be about irreducible, but primeness seems like what is actually needed). So x_1 divides A or c. If it doesn't divide c, then factor x_1 out of A leaving a scalar, then cancel the x_1, so now x_2 | c.

[Jake Levinson]

This avoids all the pigeonhole principle / multiset overlap messiness.

[Jake Levinson]

In fact it's enough (in this toy example) to just obtain some linear factor of q, since then the leftover factor is automatically also of degree 1.

[Heather Macbeth]

@Jake Levinson Are you at all tempted to do it for me? :)

[Jake Levinson]

Hmm, I just tried running it and got

invalid import: field_theory.is_alg_closed.basic
could not resolve import: field_theory.is_alg_closed.basic

I think my Lean install might be out of date.

[Kevin Buzzard]

If you've got leanproject installed then you can just use it to get bang up to date fully compiled lean and mathlib, although exactly what you type depends on whether you're working with mathlib itself or with another project having mathlib as a dependency. If you're working in mathlib then git pull followed by leanproject get-cache should get you up to date.

[Junyan Xu]

I was trying to construct the monoid iso (homogenization/dehomogenization) between R[x] and the submonoid of homogeneous polynomials in R[x,y] not divisible by y, so as to transfer factorization into linear polynomials in R[x] to factorization into linear homogeneous polynomials in R[x,y], for a domain R. The submonoid in R[x,y] is simply the meet (intersection) of the complement of the prime ideal (y) and set_like.homogeneous_submonoid (homogeneous_submodule (fin 2) R). However, I was stuck at the first step: showing that y is a prime element. I tried to use canonical isomorphisms to reduce it to docs#polynomial.prime_X, but encountered some inexplicable issues, most recently a typeclass issue:

import ring_theory.polynomial.homogeneous
import ring_theory.polynomial.basic

namespace mv_polynomial
open_locale polynomial

variables {R σ : Type*} [comm_ring R] [is_domain R] (n : ℕ)

lemma prime_X (n : σ) : prime (X n : mv_polynomial σ R) :=
begin
  classical,
  let := sum_alg_equiv R punit ({n}ᶜ : set σ), let := this.to_mul_equiv,
/-
failed to synthesize type class instance for
R : Type u_1,
σ : Type u_2,
_inst_1 : comm_ring R,
_inst_2 : is_domain R,
n : σ,
_inst : Π (a : Prop), decidable a,
this : mv_polynomial (punit ⊕ ↥{n}ᶜ) R ≃ₐ[R] mv_polynomial punit (mv_polynomial ↥{n}ᶜ R) :=
  sum_alg_equiv R punit ↥{n}ᶜ
⊢ algebra R (mv_polynomial punit (mv_polynomial ↥{n}ᶜ R))
-/
end

It's really weird that we already have the alg_equiv this in the context, but Lean complains it can't find the algebra instance on the target!
Unfortunately I didn't have time to look into this further lately.

[Jake Levinson]

I'm taking a look, but I don't know this part of mathlib at all. For example, where do I find the lemma that {σ : Type} {a b c : mv_polynomial σ K} (ha : a ≠ 0) (H : a * b = a * c) : b = c?

Currently every time I try to use library_search it crashes VS Code with a memory consumption error. I don't know if this is something wrong with my installation or what.

[Jake Levinson]

@Heather Macbeth Here's the proof outline I was imagining. (I think some of these sorries might be easy to fill in, but as I mentioned I'm having trouble with Lean and VS Code at the moment, so I had limited searching ability...)

import ring_theory.polynomial.homogeneous
import field_theory.is_alg_closed.basic

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

lemma mv_polynomial.is_homogeneous.factor
  {σ : Type} {f g : mv_polynomial σ K}
  {n : ℕ} (hg : g.is_homogeneous n) (hfg : f ∣ g) :
f.is_homogeneous (f.total_degree) := sorry
-- proof: by Damiano's argument higher up the thread (look at minimum and maximum degree parts of f)

lemma mv_polynomial.prime_of_linear
  {σ : Type} (f : mv_polynomial σ K) (hf : f.is_homogeneous 1) :
prime f := sorry
-- proof: irreducibility (by degree counting) + UFD

lemma mv_polynomial.has_linear_factor
  (f : mv_polynomial (fin 2) K) {n : ℕ} (hf : f.is_homogeneous n) :
∃ x : mv_polynomial (fin 2) K, x.is_homogeneous 1 ∧ x ∣ f := sorry
-- proof: possibly annoying since it involves dehomogenizing

example {A B q c : mv_polynomial (fin 2) K} (hA : A.is_homogeneous 1) (hB : B.is_homogeneous 2)
  (hq : q.is_homogeneous 2) (hc : c.is_homogeneous 3) (H : B * q = A * c)
  (q_ne_zero : q ≠ 0) (A_ne_zero : A ≠ 0) :
  ∃ x : mv_polynomial (fin 2) K, x.is_homogeneous 1 ∧ x ∣ q ∧ x ∣ c :=
begin
  obtain ⟨x, hx, hxq⟩ := q.has_linear_factor hq,
  by_cases hxc : x ∣ c,
  { exact ⟨x, hx, hxq, hxc⟩, },

  have hxA : x ∣ A,
  { apply or.resolve_left (prime.dvd_or_dvd (x.prime_of_linear hx) _) hxc,
    rw [mul_comm, ← H],
    exact hxq.trans (dvd_mul_left _ _) },

  -- pull out factors
  obtain ⟨y, hqxy⟩ := hxq,
  obtain ⟨A', hAxA'⟩ := hxA,
  rw [hAxA', hqxy, (by ring : B * (x * y) = x * (B * y))] at H,
  rw mul_assoc at H,

  have x_ne_zero : x ≠ 0,
  { intro h, apply A_ne_zero, rw [hAxA', h, zero_mul], },
  have H' : B * y = A' * c,
  { rw ← sub_eq_zero,
    apply or.resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero _) x_ne_zero,
    rw [mul_sub, H, sub_self], },


  have hyq : y ∣ q := ⟨x, mul_comm x y ▸ hqxy⟩,

  have hy : y.is_homogeneous 1,
  { convert hq.factor hyq,
    apply @nat.add_left_cancel 1,
    apply hq.inj_right _ q_ne_zero,
    exact (hqxy.symm ▸ hx.mul (hq.factor hyq)), },

  have hA'' : A'.is_homogeneous 0,
  { convert hA.factor (⟨x, mul_comm x A' ▸ hAxA'⟩ : A' ∣ A),
    apply @nat.add_left_cancel 1,
    apply hA.inj_right _ A_ne_zero,
    exact hAxA'.symm ▸ hx.mul (hA.factor (⟨x, mul_comm x A' ▸ hAxA'⟩ : A' ∣ A)), },
  have A'_ne_zero : A' ≠ 0,
  { intro h, apply A_ne_zero, rw [hAxA', h, mul_zero], },

  have A'_inv : mv_polynomial (fin 2) K := sorry,
  have A'_mul : A'_inv * A' = 1 := sorry,
  -- inverse of a nonzero constant?

  have hyc : y ∣ c,
  { have H'' : c = y * (A'_inv * B),
    symmetry,
    calc y * (A'_inv * B) = A'_inv * (B * y)  : by ring
                      ... = A'_inv * (A' * c) : by rw H'
                      ... = (A'_inv * A') * c : by ring
                      ... = 1 * c             : by rw A'_mul
                      ... = c                 : by ring,
    exact ⟨_, H''⟩, },

  exact ⟨y, hy, hyq, hyc⟩,
end

[Junyan Xu]

Jake Levinson said:

I'm taking a look, but I don't know this part of mathlib at all. For example, where do I find the lemma that {σ : Type} {a b c : mv_polynomial σ K} (ha : a ≠ 0) (H : a * b = a * c) : b = c?

It's docs#cancel_monoid_with_zero.mul_left_cancel_of_ne_zero; the instance should be automatic for a domain or field K.

[Jake Levinson]

Thanks @Junyan Xu . I've golfed it a little more. Should I edit my post above or post a fresh version?