Generalizing `Polynomial.Splits` to rings

Stream: mathlib4

[Thomas Browning]

I'm thinking about generalizing Polynomial.Splits to rings. The motivation is that if $f(x)$ splits in a number field $\mathcal O_K$, then we might want to look at the roots of $f(x)$ in $\mathcal O_K$ and how they relate to the roots of $f(x)$ in $\mathcal O_K/\mathfrak p$.

One option would be to simply redefine f.Splits to be (f.map i).roots.card = (f.map i).natDegree (which is equivalent by docs#Polynomial.splits_iff_card_roots). Thoughts?

[Kenny Lau]

roots requires Domain

[Kenny Lau]

does the polynomial 2 split in Z?

[Kenny Lau]

for reference the current definition is:

variable [CommRing K] [Field L] [Field F]
variable (i : K →+* L)
/-- A polynomial `Splits` iff it is zero or all of its irreducible factors have `degree` 1. -/
def Splits (f : K[X]) : Prop :=
  f.map i = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ f.map i → degree g = 1

[Kenny Lau]

what if we just modify this minimally, say change degree g = 1 to degree g <= 1?

[Kenny Lau]

(over fields, irreducible polynomial cannot have degree 0)

[Thomas Browning]

Interesting, I'll play around with this!

[Chris Hughes]

I think I regret the decision to include a homomorphism as part of the definition of splits by the way. And it could have been defined as the monoid closure of degree le 1 polynomials.

[Kenny Lau]

well it was 6 years ago

[Kenny Lau]

an eternity in lean timeframe

[Thomas Browning]

For the time being, would it make sense to introduce a separate predicate Polynomial.Factors (product of polynomials of degree <=1), build out some API, and then redefine splits in terms of that?

[Kenny Lau]

I think Chris is saying that he wants to define it as a submonoid instead of a predicate

[Kenny Lau]

without necessarily saying whether it's better (and I also don't know)

[Junyan Xu]

There's a splitting algebra for a monic polynomial over any commutative ring (the construction in https://arxiv.org/abs/1504.00973 was also used to define AlgebraicClosure (see AlgebraicClosure.spanCoeffs)). The definition suggested by Chris makes sure that the polynomial splits over the splitting algebra, so I'm in favor of it.

[Kenny Lau]

if we agree to only ever talk about monic polynomials then we can also stick to the submonoid generated by X-a...

[Junyan Xu]

Indeed, if $ac=0$ you have $(aX+b)(cX+d)=(ad+bc)X+bd$ which we probably don't want ...

[Aaron Liu]

in (Z/6Z)[X], X*(X+1) = (X+3)*(X+4) and X = (2X+3) * (3X+2)

[Thomas Browning]

Junyan Xu said:

Indeed, if $ac=0$ you have $(aX+b)(cX+d)=(ad+bc)X+bd$ which we probably don't want ...

What's the point being made here? I don't think this causes issues for Chris' definition?

[Thomas Browning]

Kenny Lau said:

I think Chris is saying that he wants to define it as a submonoid instead of a predicate

The one nice thing about a predicate is that you can use dot-notation and write f.Factors as opposed to f ∈ factors R (or something like that).

[Kenny Lau]

well without a specified behaviour (what do we want?) over rings that are not domains, it's a bit hard to judge which definition is better

[Thomas Browning]

But do you have an example where the irreducible divisor definition (with degree <= 1) gives a different answer than the submonoid closure definition (of polynomials of degree <= 1)?

[Junyan Xu]

What's the point being made here?

One can imagine that a quadratic polynomial can be written as a product of three factors but not two. I think in general it's safer to take the monoid generated by X-r and all constants. This would also bring it closer to the roots definition, since general linear polynomials may not have a root but monic ones (X-r) do have.

[Kenny Lau]

Thomas Browning said:

But do you have an example where the irreducible divisor definition (with degree <= 1) gives a different answer than the submonoid closure definition (of polynomials of degree <= 1)?

R=Z/6Z
2x = (3x^2+3x+1)*(2x)
3x^2+3x+1 is irreducible

[Aaron Liu]

surely we want monomials to split?

[Kenny Lau]

can we prove or disprove that x^n is splitting under the irreducible divisor definition (with deg <= 1)?

[Aaron Liu]

over Z/6Z the irreducible factors of the polynomial X^n in (Z/6Z)[X] are all deg <= 1

[Kenny Lau]

i think i have a counterexample

[Aaron Liu]

what is it

[Kenny Lau]

char p, ε^2 = 0, (x^2+ε)^p = x^(2p)

[Aaron Liu]

are you saying take the base ring to be (Z/pZ)[X]/(X^2)

[Kenny Lau]

yes

[Aaron Liu]

alright I'll try that

[Kenny Lau]

it might also work with just Z/4Z and then (x^2+2)^4 = x^8

[Kenny Lau]

well ^2 also works

[Aaron Liu]

Kenny Lau said:

char p, ε^2 = 0, (x^2+ε)^p = x^(2p)

Is X^2+ε irreducible

[Kenny Lau]

no clue

[Antoine Chambert-Loir]

All the intuition about irreducible polynomials comes from their main use case, which is when the ground ring is a domain. Many definitions which are equivalent in domains will be wrong over general commutative rings (and possibly even more wrong over noncommutative rings).

[Antoine Chambert-Loir]

Monic factors of degree 1 correspond to the roots, so those factors of a polynomial are well defined, but it is likely that over a non domain, a polynomial may have several factorizations in monic polynomial of degree 1.

[Antoine Chambert-Loir]

the predicate docs#Polynomial.IsRoot is defined in general, but docs#Polynomial.roots produces a docs#Multiset, hence is forced to assume that one works over a commutative domain.

[Kenny Lau]

aha, interesting, unique factorisation for monic into monic linears holds even when the domain is not UFD?

[Kenny Lau]

(proof: pass to fraction field)

[Thomas Browning]

Here's a first stab at this: #30212. It has most of the API except for the connection with the existing definition in terms of irreducible factors.

[Kenny Lau]

@Thomas Browning thanks for the effort! "semiring" came up to my mind several times, but I never brought it up because I didn't see what's the point of say x+37 which has no root in Nat...

[Kenny Lau]

I don't really know what's the point of talking about roots in semirings

[Kenny Lau]

in fact polynomials over Nat "basically" have no roots

[Thomas Browning]

Kenny Lau said:

I don't really know what's the point of talking about roots in semirings

Yeah, it doesn't make a ton of sense, although it is a free generalization (except for having to switch over to negatives in one or two places)?

[Kenny Lau]

well if you provide the API for X-Cr then you'll be fine

[Kenny Lau]

@Thomas Browning regarding aesop, I did the following test:

example {R : Type*} [Ring R] (a b c : R) : Factors (C a * (X - C b) * (X - C c) : R[X]) := by aesop

so it works well enough but actually it might need more lemmas to work "better", which should probably be another PR

[Kenny Lau]

for example when R was Int, it used some other simp lemmas to convert C a to ↑a so it doesn't work

[Kenny Lau]

and then when R is R, things like X + 1 would also not work, so you probably need extra lemmas for _one and _ofNat

[Kenny Lau]

@Thomas Browning I have proved more theorems :melt:

theorem factors_of_natDegree_eq_zero {R : Type*} [Semiring R] {f : R[X]} (hf : natDegree f = 0) :
    Factors f :=
  (natDegree_eq_zero.mp hf).choose_spec ▸ by aesop

theorem factors_X_sub_C_mul_iff {f : R[X]} {a : R} : Factors ((X - C a) * f) ↔ Factors f := by
  refine ⟨fun hf ↦ ?_, ((factors_X_sub_C _).mul ·)⟩
  by_cases hf₀ : f = 0
  · aesop
  have := hf.eq_prod_roots
  rw [leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul,
    roots_mul (mul_ne_zero (X_sub_C_ne_zero _) hf₀), roots_X_sub_C,
    Multiset.singleton_add, Multiset.map_cons, Multiset.prod_cons, mul_left_comm] at this
  rw [mul_left_cancel₀ (X_sub_C_ne_zero _) this]
  aesop

theorem factors_mul_iff {f g : R[X]} (hfg : f * g ≠ 0) : Factors (f * g) ↔ Factors f ∧ Factors g := by
  refine ⟨fun h ↦ ?_, fun ⟨hf, hg⟩ ↦ hf.mul hg⟩
  generalize hp : f * g = p at *
  generalize hn : p.natDegree = n
  induction n generalizing p f g with
  | zero =>
    have hf₀ : f ≠ 0 := by aesop
    have hg₀ : g ≠ 0 := by aesop
    rw [← hp, natDegree_mul hf₀ hg₀, Nat.add_eq_zero] at hn
    exact ⟨factors_of_natDegree_eq_zero hn.1, factors_of_natDegree_eq_zero hn.2⟩
  | succ n ih =>
    obtain ⟨a, ha⟩ := exists_root_of_factors h (degree_ne_of_natDegree_ne <| hn ▸ by aesop)
    have := dvd_iff_isRoot.mpr ha
    rw [← hp, (prime_X_sub_C a).dvd_mul] at this
    wlog hf : X - C a ∣ f with hf2
    · exact .symm <| hf2 _ ih _ ((mul_comm _ _).trans hp) hfg h hn _ ha this.symm <|
        this.resolve_left hf
    obtain ⟨f, rfl⟩ := hf
    rw [mul_assoc] at hp; subst hp
    rw [natDegree_mul (by aesop) (by aesop), natDegree_X_sub_C, add_comm, Nat.succ_inj] at hn
    have := ih (f * g) rfl (by aesop) (factors_X_sub_C_mul_iff.mp h) hn
    aesop

theorem Factors.of_dvd {f g : R[X]} (hg : Factors g) (hg₀ : g ≠ 0) (hfg : f ∣ g) : Factors f := by
  obtain ⟨g, rfl⟩ := hfg
  exact ((factors_mul_iff hg₀).mp hg).1

theorem Factors.of_irreducible {f : R[X]} (hf : Factors f) (irr : Irreducible f) :
    natDegree f ≤ 1 := by
  by_contra hn
  apply hn
  obtain ⟨a, ha⟩ := exists_root_of_factors hf (degree_ne_of_natDegree_ne (mt (· ▸ zero_le_one) hn))
  obtain ⟨f, rfl⟩ := dvd_iff_isRoot.mpr ha
  have := (of_irreducible_mul irr).resolve_left (not_isUnit_X_sub_C _)
  rw [natDegree_mul (X_sub_C_ne_zero _) this.ne_zero, natDegree_eq_zero_of_isUnit this]
  simp

-- Counter-example for reverse direction: `2*X+1 : ℤ[X]`
theorem Factors.splits {f : R[X]} (hf : Factors f) :
    f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → degree g ≤ 1 :=
  or_iff_not_imp_left.mpr fun hf0 _ hg hgf ↦ degree_le_of_natDegree_le <|
    (hf.of_dvd hf0 hgf).of_irreducible hg

-- Field
theorem factors_iff_splits {f : R[X]} :
    Factors f ↔ f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → degree g ≤ 1 := by
  refine ⟨(·.splits), ?_⟩
  rintro (rfl | hf)
  · aesop
  generalize hn : natDegree f = n
  induction n using Nat.strongRec generalizing f with
  | ind n ih =>
    by_cases irr : Irreducible f
    · exact factors_of_degree_le_one (hf irr dvd_rfl)
    simp only [irreducible_iff, not_and, not_forall, not_or, exists_prop] at irr
    by_cases unit : IsUnit f
    · exact factors_of_isUnit unit
    obtain ⟨f, g, rfl, huf, hug⟩ := irr unit
    by_cases hfg0 : f * g = 0
    · rw [hfg0]; aesop
    obtain ⟨hf0, hg0⟩ := mul_ne_zero_iff.mp hfg0
    rw [natDegree_mul hf0 hg0] at hn
    refine .mul (ih _ ?_ ?_ rfl) (ih _ ?_ ?_ rfl)
    · sorry
    · exact fun hp hpf ↦ hf hp (hpf.mul_right _)
    · sorry
    · exact fun hp hpg ↦ hf hp (hpg.mul_left _)

[Kenny Lau]

(R is domain unless specified)

[Thomas Browning]

Thanks! I've also pushed a version of factors_iff_splits that uses UniqueFactorizationMonoid to avoid the induction proof (at the cost of slightly heavier imports).

[Kenny Lau]

is that fine? (genuine question)

[Kenny Lau]

idk how low or high docs#Polynomial.Splits is in the import hierarchy

[Kenny Lau]

i mean it also seems to be a basic fact that k[x] is ED

[Thomas Browning]

Yeah, it doesn't use anything beyond what Splits already uses.

[Kenny Lau]

btw in the current definition of Splits (or the version in the PR) maybe we should restrict g to be monic?

[Kenny Lau]

never mind i thought i could prove something but i couldn't

[Kenny Lau]

again over (Z/2Z)[ε]/ε^2 we have (X+ε)^2 = X^2 but X doesn't divide X+ε so X is irreducible but not prime

[Kenny Lau]

being monic doesn't help with anything

[Riccardo Brasca]

In my honest opinion the theory is such a mess for nondomains that it is not worth to spend a lot of time thinking about it. Sure, we can generalize the definition and a couple of theorems for free but still...

[Kenny Lau]

@Riccardo Brasca here's a question for domains: if R is a domain and f is a monic irreducible polynomial, is f prime?

[Kenny Lau]

something tells me f in K[x] should still be irreducible...?

[Riccardo Brasca]

Give me 10 minutes, but my first reaction is "no but yes for integrally closed domains"

[Riccardo Brasca]

Kenny Lau said:

something tells me f in K[x] should still be irreducible...?

exactly, you want to use gauss lemma

[Kenny Lau]

image.png

hmm this one needs UFD...

[Riccardo Brasca]

this is gauss lemma

[Kenny Lau]

yeah but it needs UFD

[Kenny Lau]

Riccardo Brasca said:

Give me 10 minutes, but my first reaction is "no but yes for integrally closed domains"

aha k[t^2,t^3] with X^2-t^2

[Kenny Lau]

let p := (X-t)t^2 = t^2X - t^3
let q := (X+t)t^2 = t^2X + t^3
X^2-t^2 divides pq but not p or q

[Riccardo Brasca]

I think the simplest example comes from number theory (at least the easiest for me...). We need $R$ not a UFD, and the classical example is $\mathbb{Z}[\sqrt{-3}]$. The easiest way to see that is not a UFD is to see that it is not integrally closed (that is the real point): just take the element $\frac{-1+\sqrt{-3}}{2}$, whose minimal polynomial is $x^2+x+1$. Now, $x^2+x+1$ has no roots in $R$ so it is irreducible. Now, take the polynomial $x^4+x^2+1=(x^2+\sqrt{-3}x - 1)(x^2-\sqrt{-3}x - 1)=(x^2+x+1)(x^2-x+1)$ to show that $x^2+x+1$ is not prime.

[Riccardo Brasca]

The idea is rather simple: take $z$ in $\operatorname{Frac}(R)$ but not $R$ whose minimal polynomial $P$ has integers coefficients. Now consider the numbers $z$, $\bar z$, $-z$ and $-\bar z$ and the polynomial $(x-z)(x+z)(x-\bar z)(x+\bar z)$. On one hand this is $PQ$, where $Q$ is the minimal polynomial of $-z$, that is still with integers coefficients, but on the other hand it is $(x^2-2\operatorname{Im}(z)z-|z|^2)(x^2+2\operatorname{Im}(z)z-|z|^2) \in R[x]$.

[Kenny Lau]

is there a non-trivial ring with ac=0 and abc=1?

[Riccardo Brasca]

Ah if you even drop commutativity then everything becomes surely a huge mess

[Kenny Lau]

(I feel like there's some smart linear transformations over infinite dimension vector space that would work)

[Kenny Lau]

yeah ok let

• a(x0, x1, ...) = (0, x0, 0, x1, ...)
• b(x0, x1, ...) = (x1, x2, ...)
• c(x0, x1, ...) = (x0, x2, x4, ...)

(use the reverse composition order, i.e. do a and then do b and then do c)

[Riccardo Brasca]

yes, with functions ℕ → ℕ is immediate (it's what you did, but just play with indexes)

[Kenny Lau]

in some sense R[x] is also the "wrong object" to consider (like mathlib's elliptic curve over commring)

[Kenny Lau]

do we have the correct R<x>?

[Kenny Lau]

how does it even work? does XaX = XbX imply a=b?

[Riccardo Brasca]

What do you mean? For one variable noncommutative polynomials are just polynomials

[Riccardo Brasca]

R is alwyas in the center

[Kenny Lau]

I mean the one where aX and Xa are different, does this have a name?

[Riccardo Brasca]

in general we have docs#FreeAlgebra

[Kenny Lau]

Riccardo Brasca said:

in general we have docs#FreeAlgebra

image.png

[Aaron Liu]

maybe you want the quotient of the free ring on Option R by all the relations in R

[Riccardo Brasca]

yes, because algebras are over commsemiring

[Aaron Liu]

no but that would have an extra one

[Aaron Liu]

hmmmm

[Kenny Lau]

Aaron Liu said:

no but that would have an extra one

it's fine we have a relation [1] = 1

[Kenny Lau]

your construction will work

[Kenny Lau]

free semiring, even

[Aaron Liu]

I guess

[Riccardo Brasca]

you can always take the huge free algebra over ℤ (generated by the variables and the elements of R) and quotient out by the relation on R

[Aaron Liu]

of course

[Kenny Lau]

indeed, i was more asking if it's in mathlib

[Kenny Lau]

and does it have any use

[Aaron Liu]

we have docs#FreeNonUnitalNonAssocAlgebra

[Aaron Liu]

I don't know if we have free extensions of a noncommutative ring

[Kenny Lau]

it seems like R is still in the center there (even tho R is not even commutative)

[Kenny Lau]

anyway, let's go back to the main context, the reason i asked that is i'm wondering whether this is true:

[Kenny Lau]

theorem Factors.natDegree_le_one_of_irreducible {R : Type*} [Semiring R]
    {f : R[X]} (hf : Factors f) (h : Irreducible f) : natDegree f ≤ 1 := by

[Aaron Liu]

are you writing R[X] to mean the (semi)ring with the universal property that (R[X] →+* S) ≃ ((R →+* S) × S) for any (semi)ring S

[Aaron Liu]

or is it just docs#Polynomial

[Aaron Liu]

I'm guessing it's just docs#Polynomial

[Kenny Lau]

yes polynomial

[Kenny Lau]

it's for #30212

[Riccardo Brasca]

Kenny Lau said:

theorem Factors.natDegree_le_one_of_irreducible {R : Type*} [Semiring R]
    {f : R[X]} (hf : Factors f) (h : Irreducible f) : natDegree f ≤ 1 := by

This looks true to me at least over CommRing: if P is c(x - a_1)...(x-a_n) you have that x-a_1 divides P and it is not a unit (see Polynomial.isUnit_iff_coeff_isUnit_isNilpotent), so c(x - a_2)...(x-a_n) must be a unit. This implies that c is nilpotent and in particular the constant term is also nilpotent so not a unit.

[Kenny Lau]

yes the PR contains a proof for CommSemiring and i'm wonder if I can generalise it to Semiring

[Kevin Buzzard]

But why do you care? Where are the applications? This thread started off with something which has a clear application. Factorization isn't really a thing away from commutative domains, it's a pathological thing outside that domain (as you already know).

[Kenny Lau]

yeah it's probably fine

[Antoine Chambert-Loir]

Kenny Lau said:

I mean the one where aX and Xa are different, does this have a name?

There is docs#SkewMonoidAlgebra.

[Kenny Lau]

it seems like aX = Xa there?

[Antoine Chambert-Loir]

That should be $Xa = \sigma(a) X$.

[Antoine Chambert-Loir]

The semiring structure comes very late in the file, with docs#SkewMonoidAlgebra.instNonUnitalSemiring that involves an action of the monoid on the scalars.

[Kenny Lau]

i guess that's a more useful instance (though still not "free")

[Aaron Liu]

not free enough

[Antoine Chambert-Loir]

Then you have the free associative algebra on a set, but that's just the algebra on the word monoid of that set.

[Andrew Yang]

Do we really want $2x + 1$ to not be split in $\mathbb{Z}[X]$? I imagine having the nontrivial fact that splits in Q => splits in Z easily available would be useful, which is not true under the current definition.

[Thomas Browning]

Junyan Xu said:

One can imagine that a quadratic polynomial can be written as a product of three factors but not two. I think in general it's safer to take the monoid generated by X-r and all constants. This would also bring it closer to the roots definition, since general linear polynomials may not have a root but monic ones (X-r) do have.

I guess the motivation was the connection with having roots.

[Thomas Browning]

In particular, for my ANT applications, I would prefer "f splits/factors in this ring" to mean "f has roots in this ring"

[Thomas Browning]

Or another way of saying this is that there is some advantage to having a predicate that distinguishes these cases of "roots in the ring" vs "roots in the field of fractions"

[Johan Commelin]

Yeah, this sounds like a place where we want to have two similar-but-slightly-distinct predicates?

[Thomas Browning]

Is there an immediate use case for the "product of degree <= 1" definition? If not, could we hold off on on introducing it until it's needed?

(E.g., even if you've got a polynomial like 2x+1, if you care about it being a "product of degree <= 1", then you probably care about it's roots in the field of fractions, so the field of fractions is probably already in the picture, and you can just say that the polynomial factors after mapping to the field of fractions).

[Thomas Browning]

Here are the first couple PRs: #30869 and #30870 (mostly targeting occurrences of Polynomial.Splits (RingHom.id k) for now.

[Riccardo Brasca]

I am assigning both of them to myself, but I will not have time during the weekend, so anyone should feel free to review!

[Riccardo Brasca]

Do we really want to replace Splits by Factors everywhere? I agree it's sometimes better, but the "Splits" seems a more standard terminology.

[Kenny Lau]

Thomas Browning said:

For the time being, would it make sense to introduce a separate predicate Polynomial.Factors (product of polynomials of degree <=1), build out some API, and then redefine splits in terms of that?

I thought it was a temporary measure

[Riccardo Brasca]

If the point is redefining Splits using Factors, what is the point of of refactoring current declaration that use Splits to use Factors?

[Thomas Browning]

Yeah, this is something I'm not altogether sure about. I think at least for the instances of Splits (RingHom.id F), it definitely makes sense to split over.

[Thomas Browning]

Kenny Lau said:

Thomas Browning said:

For the time being, would it make sense to introduce a separate predicate Polynomial.Factors (product of polynomials of degree <=1), build out some API, and then redefine splits in terms of that?

I thought it was a temporary measure

From this perspective (where we're trying to fix suboptimal design decisions in Splits), the idea would be to get rid of Splits entirely, and then rename Factors to Splits, I guess?

[Kenny Lau]

aha, interesting

[Riccardo Brasca]

But the current approach doesn't seem sustainable, we would end up with a lot of deprecated declarations coming from the "limbo" period.

[Riccardo Brasca]

It seems better to redefine splits on terms of factors, fixing the api and not touching any declaration that only uses splits

[Riccardo Brasca]

Anyway we should think a bit before doing a lot of work

[Kenny Lau]

@Thomas Browning will a lot of code break if we just replace Splits right now by Factors map?

[Kenny Lau]

it's a bit tricky here because they don't have the same type (Splits eats a map as input)

[Thomas Browning]

Riccardo Brasca said:

It seems better to redefine splits on terms of factors, fixing the api and not touching any declaration that only uses splits

Well, Splits is already defined in terms of Factors at this point.

[Thomas Browning]

Kenny Lau said:

it's a bit tricky here because they don't have the same type (Splits eats a map as input)

Yeah, you could try to pull off the band-aid all at once, but it would be a massive refactor where everything breaks.

[Kenny Lau]

but if Splits is already defined using Factors then it wouldn't break right?

[Thomas Browning]

Piecemeal switching to Factors would be easier in this regard, but it does have this issue of deprecated definitions that Reccardo points out.

[Kenny Lau]

ok, yeah, it is a lot of files:

Mathlib.Algebra.Polynomial.Splits
Mathlib.Algebra.CubicDiscriminant
Mathlib.FieldTheory.Separable
Mathlib.RingTheory.Adjoin.Field
Mathlib.FieldTheory.SplittingField.IsSplittingField
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.FieldTheory.Extension
Mathlib.FieldTheory.Normal.Defs
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.FieldTheory.SplittingField.Construction
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Mathlib.FieldTheory.Normal.Basic
Mathlib.FieldTheory.Normal.Closure
Mathlib.FieldTheory.PrimitiveElement
Mathlib.FieldTheory.Galois.Basic
Mathlib.FieldTheory.IsSepClosed
Mathlib.FieldTheory.SeparableDegree
Mathlib.RingTheory.Trace.Basic
Mathlib.RingTheory.Polynomial.Vieta
Mathlib.Topology.Algebra.Polynomial
Mathlib.FieldTheory.PolynomialGaloisGroup

[Kenny Lau]

but from another perspective, it's "only" 234 declarations that need changing...

[Thomas Browning]

Hmm, if people are happy to review such a large diff (easily > 1000 lines, I think), then this is an option...

[Kenny Lau]

let's see what Riccardo thinks first

[Riccardo Brasca]

I am talking specifically about #30870. For example, it modifies X_pow_sub_C_splits_of_isPrimitiveRoot from

theorem X_pow_sub_C_splits_of_isPrimitiveRoot
    (X ^ n - C a).Splits (RingHom.id _)

to

theorem X_pow_sub_C_factors_of_isPrimitiveRoot
    {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {α a : K} (e : α ^ n = a) :
    (X ^ n - C a).Factors

And I am not sure this is good: we are creating a new declaration, X_pow_sub_C_factors_of_isPrimitiveRoot, that will be removed soon to get back to X_pow_sub_C_splits_of_isPrimitiveRoot? Then why not keeping X_pow_sub_C_splits_of_isPrimitiveRoot?

[Riccardo Brasca]

But I may have misunderstood the plan.

[Kenny Lau]

I see, so we should change the statement but keep the name for now?

[Riccardo Brasca]

I mean, Factors works better over rings, but it's equivalent over fields, so why bothering? X_pow_sub_C_factors_of_isPrimitiveRoot is still about fields.

[Riccardo Brasca]

anyway I am closing my laptop now, happy Halloween!

[Andrew Yang]

The ring hom in Splits is really annoying and we should get rid of it regardless. And I think the easiest way to achieve this is to gradually replace it with factors.

[Kenny Lau]

yes but I thought we also want to replace the name with "Splits" after all that

[Thomas Browning]

Riccardo Brasca said:

And I am not sure this is good: we are creating a new declaration, X_pow_sub_C_factors_of_isPrimitiveRoot, that will be removed soon to get back to X_pow_sub_C_splits_of_isPrimitiveRoot? Then why not keeping X_pow_sub_C_splits_of_isPrimitiveRoot?

Well, if we do the shift gradually, then it wouldn't be super soon, maybe a couple months?

[Thomas Browning]

Kenny Lau said:

I see, so we should change the statement but keep the name for now?

It is worth considering this option since it allows for gradual replacement while avoiding the deprecation mess (the only downside being the slight mismatch between the name and statement in the short-term).

[Thomas Browning]

Just to keep the ball rolling here, it seems like there are a few decisions to be made:
A) Ultimately have two predicates, one with a ring hom (Splits) and one without a ring hom (Factors).
B) Ultimately have just one predicate, without a ring hom (Splits, since that is the more standard name).

It seems like there is consensus for B? Then the question would be how to achieve this refactor. Here are some options:
C) Slowly refactor mathlib (both theorem statements and theorem names) to be in terms of Factors instead of Splits until Splits can be deprecated. Then Splits is deleted and Factors is renamed to Splits. This is the approach of #30870.
D) Same as C, but just refactor theorem statements, keeping theorem names in terms of Splits to avoid the need for aliases.
E) Pull off the bandaid all at once by immediately removing the ring hom from Splits and refactoring every subsequent usage of Splits.

Thoughts on these options, or other suggestions?

[Thomas Browning]

Personally I'm leaning towards (D) at this point since it seems least painful, but I would be happy to give (E) a shot if there's strong support and fast review.

[Riccardo Brasca]

I think B) is much better than A).

Concerning the strategy: the main problem is the ring hom, right? In the sense that we cannot just change the definition of Splits, we really need to change its type.

[Thomas Browning]

Yes, the definition is already changed as much as it can be without changing its type.

[Riccardo Brasca]

In D) what happens to the ring hom?

[Thomas Browning]

The definition of Splits would remain unchanged (with the ring hom) for the time being, but every subsequent theorem would eventually be restated in terms of Factors (ditching the ring homs).

[Thomas Browning]

(D) is just #30870 but without the renaming and aliases

[Thomas Browning]

(The disadvantage of (D) is that in the short-term, you now have a bunch of theorems in mathlib whose name says "splits" but whose statement says "factors").

[Riccardo Brasca]

Do you think that getting rid of the ring hom is a lot of work? I guess that 90% of the time Splits is used with the identity

[Riccardo Brasca]

I have the impression that nobody likes the ring hom

[Riccardo Brasca]

Riccardo Brasca said:

Do you think that getting rid of the ring hom is a lot of work? I guess that 90% of the time Splits is used with the identity

Actually not at all

[Thomas Browning]

Yeah, might only be 25%, although I think a lot of that is API for Splits as well as Splits encouraging unnecessarily relative API (i.e., docs#IsAlgClosed.splits_domain shouldn't really exist, but it does since you can't just write IsAlgClosed.splits.map).

[Thomas Browning]

Actually, here's a reason to not try to do the refactor all at once: The type difference between Splits and Factors means that they will naturally have different API, so switching over all at once would include refactoring the Splits API at which point the mega-PR would be a mess of new and deleted declarations. It seems simpler to develop the correct API for Factors, switch mathlib over from Splits to Factors using this API, and then rename Factors to Splits.

[Riccardo Brasca]

I thought a little bit about this, and unfortunately I don't see a 100% clean way of doing things, so we have to accept a compromise. Maybe you launch a poll

[Thomas Browning]

/poll What is the best way to remove the ring hom from Polynomial.Splits?
Slowly refactor mathlib (both theorem statements and theorem names) to be in terms of Factors instead of Splits until Splits can be deprecated. Then Splits is deleted and Factors is renamed to Splits.
Same as above, but just refactor theorem statements, keeping theorem names in terms of Splits to avoid the need for aliases.
Pull off the bandaid all at once by immediately removing the ring hom from Splits and refactoring the Splits API every subsequent usage of Splits.

[Snir Broshi]

I'm not sure if this is exactly what the 3rd option means, but this is what I vote for:

• In a single PR, unfold every use of Splits and rename Factors to Splits. This means replacing every p.Splits f with (p.map f).Splits. Maybe this can even be done by a script.
  This keeps the theorems defeq to their previous version, and avoiding name changes is justified by the theorems still containing Splits.

• Refactors can come later, e.g. removing occurrences of p.map (RingHom.Id) introduced by the previous PR.

[Ruben Van de Velde]

I'd like to avoid massive unreviewable PRs; no strong opinion on the names in the intermediate period

[Snir Broshi]

The PR should be at most +300/-300, which I think is on the low side when it comes to mathlib based on refactors I've seen (though I'm not a reviewer, idk how hard it is)

[Thomas Browning]

Well, there are over 400 usages of Splits, so that's at least +400/-400, not counting all the proofs that will break.

[Snir Broshi]

Thomas Browning said:

Well, there are over 400 usages of Splits, so that's at least +400/-400, not counting all the proofs that will break.

I counted 236 + 44 (https://loogle.lean-lang.org/?q=Polynomial.Splits + https://loogle.lean-lang.org/?q=Polynomial.Factors), what did I miss?

[Thomas Browning]

Those are theorem statements, but proofs that mention Splits will need to be changed.

[Snir Broshi]

Riccardo Brasca said:

Riccardo Brasca said:

Do you think that getting rid of the ring hom is a lot of work? I guess that 90% of the time Splits is used with the identity

Actually not at all

It looks to me like a lot of Splits usages use algebraMap, maybe we should have aSplits K similar to aroots K vs roots?

[Riccardo Brasca]

I don't think so. Just say that the relevant polynomial splits.

[Snir Broshi]

Thomas Browning said:

Those are theorem statements, but proofs that mention Splits will need to be changed.

I tried deprecating Splits locally and got 275 warnings, will that check still miss some usages?
Keep in mind that the change from p.Splits f to (p.map f).Factors is defeq so only things that expect syntactical equality (e.g. rw) might break, and even those I'm not sure will since changing everything at once should change both sides in the same way when checking for syntactical equality.

[Snir Broshi]

I removed the ringhom argument from Splits and replaced all usages of Splits with a script, and all of mathlib successfully builds except for docs#Polynomial.isSplittingField_C for some reason.
So I now have a +252/-252 change that removes the ringhom, + one sorry I need to fix, + 78 lines that exceed 100 chars that I need to break manually.
So presumably I'll be able to open a PR with +330/-252 that completes the task (of course this is just a first step before refactors). Is that okay or is the long way still preferred?

[Snir Broshi]

Fixed the sorry (the refactor made the first simp use Algebra.algebraMap_self, map_C, RingHom.id_apply instead of Algebra.algebraMap_self, splits_C for some reason) so now everything builds

[Snir Broshi]

Final score: +275/-264 (full diff), result:

def Splits (f : K[X]) : Prop :=
-  Factors (f.map i)
+  Factors f

[Thomas Browning]

Huh, that's not as bad as I thought. If this were merged, I guess the follow-up would be a PR delete Splits and renaming Factors to Splits (so that we keep the more general definition of Factors and the surrounding API).

[Thomas Browning]

I'll add this to the poll.

[Thomas Browning]

Snir Broshi said:

Final score: +275/-264 (full diff), result:

def Splits (f : K[X]) : Prop :=
-  Factors (f.map i)
+  Factors f

Can you open a PR?

[Thomas Browning]

Also, in some sense @Snir Broshi's can be done in parallel with the "switching over from Splits to Factors without changing theorem names" approach, since even after redefining Splits, we will still want to switch over to Factors API.

[Thomas Browning]

So there might not actually be a need to choose between the two.

[Thomas Browning]

(And the point is that @Snir Broshi's work would make the switch Splits to Factors easier).

[Snir Broshi]

Thomas Browning said:

Can you open a PR?

Sure, just waited for confirmation here first, thanks
Opened #31631

[Thomas Browning]

Once #31631 is merged, the question is what's the best next step. There's the slow option from the poll of slowly refactoring theorem statements to be in terms of Factors instead of Splits. But once #31631 is merged I think it's worth checking how bad the diff would be if we immediately rename Factors to Splits (deleting the current definition of Splits, but leaving the Splits file around temporarily for any API lemmas that aren't already covered in the Factors file).

[Snir Broshi]

Merged :+1:

[Thomas Browning]

#31878 is +110/-128, which seems pretty reasonable. Reviews welcome!

[Thomas Browning]

We're basically in the cleanup phase now. #31915 cleans up the lingering Splits (p.map (RingHom.id _)) from #31631. And after that, I think the only big thing left is to combine the existing Splits.lean and Factors.lean into a new-and-improved Splits.lean (mostly by deprecating the old API in Splits.lean in favor of the new API in Factors.lean).

[Thomas Browning]

The first deprecation PR is #32040, with at least a couple more to follow, I think.

[Thomas Browning]

Here's the next one: #32103

[Thomas Browning]

And here's the next one: #32284

[Thomas Browning]

And another: #32325

[Thomas Browning]

Here's another smaller one: #32409

[Thomas Browning]

And another: #32500

[Thomas Browning]

Next one: #32574 (hopefully just two or three more)

[Thomas Browning]

And another: #32752 (just one or two more!)

[Thomas Browning]

Last batch: #32818

[Thomas Browning]

So at this point Splits.lean is entirely deprecated. What's the best way to wrap this up? Move the contents of Factors.lean back into Splits.lean? If so, should Factors.lean be left around as a deprecated module or something?

[Snir Broshi]

IMO move without deprecation because Factors.lean was very short-lived, but idk what's the policy

[Johan Commelin]

@Thomas Browning Whatever you think is best. Adding a deprecated module doesn't hurt, but as Snir points out it also isn't super necessary.

[Thomas Browning]

#32946 moves the contents over with a deprecated module

[Ruben Van de Velde]

If the file was shipped in a stable release, it definitely should have a deprecation

[Ruben Van de Velde]

(And if you don't, I'll probably add one anyway)