Polynomials: `Irreducible (p.map f) → Irreducible p`

Stream: maths

[Snir Broshi]

import Mathlib
open Polynomial

theorem irreducible_of_irreducible_map
    {R R' : Type*} [Semiring R] [Semiring R'] (p : R[X]) (f : R →+* R') :
    Irreducible (p.map f) → Irreducible p := by
  sorry

What are the weakest assumptions needed to make this true?
I expected this to be true just by adding f.Injective and possibly CommRing, but such a statement doesn't exist in Mathlib. Does anyone have a counterexample?

---

There's docs#Polynomial.Monic.irreducible_of_irreducible_map which adds p.Monic and:

[CommRing R] [IsDomain R] [CommRing R'] [IsDomain R']

---

There's docs#Polynomial.IsPrimitive.irreducible_of_irreducible_map_of_injective which adds p.IsPrimitive and f.Injective and:

[CommRing R] [CommRing R'] [IsDomain R']

[Johan Commelin]

Consider $\Z \to \mathbb{Q}$ and $2X$.

[Riccardo Brasca]

This has already been discussed, and the conclusion was that it seems difficult to do better than what we currently have.

[Riccardo Brasca]

@Jiang Jiedong you wrote some nice counterexample, didn't you?

[Kenny Lau]

The only issue seems to be mapping nonunits to units, which is fixed by IsLocalHom I would suppose. (e.g. it is true for integral extensions)

So the following should be true:

import Mathlib

open Polynomial

example {A B : Type*} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B]
    (f : A →+* B) [IsLocalHom f] (hf : Function.Injective f)
    {p : A[X]} (hfp : Irreducible (p.map f)) : Irreducible p :=
  sorry

[Jiang Jiedong]

@Riccardo Brasca had a discussion with me about whether irreducibility is preserved by a surjective local homomorphism. It is related to the opposite direction of your original statement. The example is as follows.

Consider the additive monoids M = ℕ ⊕ ℕ, N = ℕ,
with a surjective local (additive) hom f : M →+ N sending (m, n) to 2m + n.
It is local because the only add unit in N is 0, with preimage {(0, 0)} also an add unit.
Then x = (1, 0) is irreducible in M, but f x = 2 = 1 + 1 is not irreducible in N.

By taking the MonoidAlgebra, this could be upgraded into a counterexample in terms of rings.

[Kenny Lau]

proof:

import Mathlib

open Polynomial

theorem Polynomial.isLocalHom_map {A B : Type*} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B]
    {f : A →+* B} [IsLocalHom f] (hf : Function.Injective f) :
    IsLocalHom (mapRingHom f) := by
  refine ⟨fun p (hfp : IsUnit (p.map f)) ↦ ?_⟩
  rw [isUnit_iff] at hfp ⊢
  obtain ⟨fx, hfx, hfxp⟩ := hfp
  have hp0 : p.natDegree = 0 := (natDegree_map_eq_of_injective hf p).symm.trans <| by simp [← hfxp]
  obtain ⟨x, rfl⟩ := natDegree_eq_zero.mp hp0
  obtain rfl := by simpa using hfxp
  exact ⟨x, isUnit_of_map_unit f x hfx, rfl⟩

example {A B : Type*} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B]
    (f : A →+* B) [IsLocalHom f] (hf : Function.Injective f)
    {p : A[X]} (hfp : Irreducible (p.map f)) : Irreducible p :=
  have := isLocalHom_map hf
  .of_map (f := mapRingHom f) hfp

[Snir Broshi]

Cool! Didn't know IsLocalHom (neither in mathlib nor in math), and now I'm wondering what else is true for local homs, e.g.:

example {A B : Type*} [CommRing A] [IsDomain A] [NormalizedGCDMonoid A]
    [CommRing B] [IsDomain B] [NormalizedGCDMonoid B]
    (f : A →+* B) [IsLocalHom f] (hf : Function.Injective f)
    {p q : A[X]} : gcd (p.map f) (q.map f) = (gcd p q).map f := by
  -- or maybe just `Associated`
  sorry

example {A B : Type*} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B]
    (f : A →+* B) [IsLocalHom f] (hf : Function.Injective f)
    {p q : A[X]} (h : IsCoprime (p.map f) (q.map f)) : IsCoprime p q := by
  sorry

example {A B : Type*} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B]
    (f : A →+* B) [IsLocalHom f] (hf : Function.Injective f)
    {p : A[X]} (h : (p.map f).Separable) : p.Separable := by
  -- special case of the `IsCoprime` example (using `Polynomial.derivative_map`)
  sorry

[Johan Commelin]

Snir Broshi said:

Cool! Didn't know IsLocalHom (neither in mathlib nor in math)

The concept comes from morphisms of local rings. (A local ring has a unique maximal ideal, and hence a unique surjection onto a field. Morphisms of local rings should commute with that structure. Exercise: show that this concept is the same as the mathlib definition.)

[Ruben Van de Velde]

What, do you mean the solution isn't in mathlib? :)

[Johan Commelin]

I didn't make that claim :wink:

[Antoine Chambert-Loir]

(Anybody having the slightest attraction to intuitionistic logic should cry at reading the docstring of docs#IsLocalHom. Maybe that's on purpose.)

[Aaron Liu]

Antoine Chambert-Loir said:

(Anybody having the slightest attraction to intuitionistic logic should cry at reading the docstring of docs#IsLocalHom. Maybe that's on purpose.)

I don't get it

[Floris van Doorn]

It's probably this part, and the fact that the docstring is the contrapositive of the Lean statement.

Lean statement: map_nonunit (a : R) : IsUnit (f a) → IsUnit a

Docstring: A local homomorphism f : R ⟶ S will send nonunits of R to nonunits of S.

[Aaron Liu]

oh god

[Aaron Liu]

did they change the field at some point and forget to change the docstring?

[Jiang Jiedong]

Shall we fix the doc string and the name map_nonunit?

[Kevin Buzzard]

But they're the same thing! ;-)

More seriously, what are proposals for a sentence which is constructively accurate and isn't a lot more ugly?

[Fernando Chu]

Something like "f reflects units"? Pretending this is a statement about one object categories, this is a very standard usage of "reflects" :)

[Damiano Testa]

Maybe "only units map to units"?

[Kevin Buzzard]

I agree with you that for those people who know what "reflects" means, this is a good docstring. But I would argue that this word is not taught as standard in mathematics.

This sort of question has come up before: are we allowed to write a docstring which is mathematically equivalent to, but not equal to, the Lean code, and my impression is that the answer is "yes". I think that if someone wants to add a sentence about reflecting then this should be added as an extra comment, rather than removing the mathematically accurate (at least if you're not a constructivist, and mathlib is not a constructivist library) and easier-to-understand (because it doesn't mention a technical term which is essentially unheard of outside of category theory) term. But I would have no objections to an additional comment of the form "Note: this is implemented as: f reflects units".

[Christian Merten]

Fernando Chu said:

Something like "f reflects units"? Pretending this is a statement about one object categories, this is a very standard usage of "reflects" :)

Would you also like to rename IsLocalHom to ReflectsIsos? I don't think this is great. The current docstring is quite clear and if the formula was not shown in the docs, it would cause no confusion.

[Fernando Chu]

The reference to categories was a joke. The serious part was that the concept/name of a function "reflecting" properties is nice, but I agree it is very non-standard.

[Junyan Xu]

I'd use comap_isUnit for the name

[Kevin Buzzard]

but that would surely mean "an arbitrary preimage of a nonunit is a nonunit"?

[Yaël Dillies]

kern_isUnit? :speak_no_evil:

[Kenny Lau]

The exported lemma is called sUnit_of_map_unit, which is a bad name; I would just call the field isUnit_of_isUnit_apply' and export it to isUnit_of_isUnit_apply.

[Kenny Lau]

if a shorter name is sought for the field then it can be isUnit_of_map

[Ruben Van de Velde]

We don't need a separate name for the field though, do we?

[Ruben Van de Velde]

At least, I'm not seeing any of the usual reasons

[Kenny Lau]

Right, we don't need the ' version above (my apologies); but if we want a shorter name for the field then we can export it to a longer name, in which case we'll need a separate name.

[Yaël Dillies]

IsUnit.of_map would be my name

[Kenny Lau]

IsUnit.of_map actually exists already! :tada:

[Yaël Dillies]

A win for #naming :grinning_face_with_smiling_eyes: