contentIdeal

Stream: mathlib4

[Fabrizio Barroero]

In #25333 I wanted to add a couple of theorems like

theorem isPrimitive_of_span_coeffs_eq_top {p : R[X]} (h : Ideal.span (p.coeffs.toSet) = ⊤) :
    IsPrimitive p

in the file Mathlib/RingTheory/Polynomial/Content.
It occurred to me that for some people Ideal.span (p.coeffs.toSet) is actually the definition of content of a polynomial and this makes a lot of sense when there is no GCD, for instance in a Dedekind Domain.

I am therefore thinking that it might be a good idea to define

def contentIdeal (p : R[X]) := Ideal.span (p.coeffs.toSet)

and prove stuff about it.

First, I would like to know people's opinions about it.

Second, in case there is some interest, I would like to know whether this should be added to the current Mathlib/RingTheory/Polynomial/Content file, which is centered around the content with the NormalizedGCDMonoid R hypothesis, or it is better to create a new file, e.g. Mathlib/RingTheory/Polynomial/ContentIdeal.

[Johan Commelin]

@Fabrizio Barroero Good idea. I like both the new definition, and the idea to put it in a new file.

[Fabrizio Barroero]

Thanks.
#25333 is ready for review.

[Antoine Chambert-Loir]

Note that the contentIdeal has weak algebraic properties in general. For example, it is in general not multiplicative.

[Fabrizio Barroero]

Yes indeed. But, as far as I know, it is the only way to express some sort of primitivity when one does not have unique factorization

[Junyan Xu]

Multiplicativity fails in general but there's the Dedekind--Mertens lemma

[Kenny Lau]

what obscure corner of computability theory did you go to to access that paper :upside_down:

[Antoine Chambert-Loir]

Well, Thierry Coquand has marvelous insights into commutative algebra.

[Antoine Chambert-Loir]

@Fabrizio Barroero , can you add as a TODO the statement of the Dedekind-Mertens lemma with a link to Coquand's paper ? (Does Mathlib have Prüfer rings?)

[Junyan Xu]

what obscure corner of computability theory did you go to to access that paper

Computability theory? I recall I saw the lemma (even before I worked on #10327) so I googled in an attempt to find a reference, and Coquand's note popped up among the first results.

[Fabrizio Barroero]

More theorems about this can be found in #25960

[Antoine Chambert-Loir]

This paper (in French) gives a nice summary of properties of the content ideal.
http://www-math.univ-poitiers.fr/~ducos/Travaux/Gauss-Joyal.pdf

[Fabrizio Barroero]

Antoine Chambert-Loir said:

This paper (in French) gives a nice summary of properties of the content ideal.
http://www-math.univ-poitiers.fr/~ducos/Travaux/Gauss-Joyal.pdf

Thanks! That's an interesting note. I might formalise some of the things in there.