Tropical polynomials

Stream: new members

[Linus Sommer]

Hello all,
I want to define tropical polynomials with the greater goal of formalizing some tropical geometry.

I have seen that the tropical semiring is formalized in in Algebra/Tropical/Basic.lean. Is this the correct object?

    { instAddMonoidWithOneTropical,
    instDistribTropical,
    instAddCommMonoidTropical,
    instCommMonoidTropical with
    zero_mul := fun _ => untrop_injective (by simp [top_add])
    mul_zero := fun _ => untrop_injective (by simp [add_top]) }

(Line 557 to 563)

If it is the correct object, could you please guide me on how to use it to define a polynomial ring? I have noticed that there are polynomial-related modules in both "Algebra" and "Data." Could you please clarify which one I should use for my purpose?

[Eric Wieser]

Are you asking for a Polynomial over a tropical ring, or does "tropical polynomial" mean something different?

[Eric Wieser]

If so, I believe you can use docs#Tropical as (Tropical R)[X] for some ring R, after open scoped Polynomial for the notation

[Eric Wieser]

If so, I believe you can use docs#Tropical as (Tropical R)[X] for some ring R, after open scoped Polynomial for the notation

[Linus Sommer]

Thank you Eric, I was asking about polynomials over a tropical ring.

[Alex J. Best]

Working out which ring R you want to use may be tricky though!
As for different polynomial modules, they should just contain different theorems about the same definition of polynomial. So you should use whatever you need from both.

[Linus Sommer]

Unfortunately I get the following error: unknown namespace 'Polynomial'.

My code looks like this:

import Mathlib.Algebra.Tropical.Basic
variable {R : Type*}

open Tropical

open scoped Polynomial
#check (Tropical R)[X]

[Linus Sommer]

If I do this

import Mathlib.Algebra.Tropical.Basic
import Mathlib.Data.Polynomial.Basic

variable {R : Type*}

open Tropical

open scoped Polynomial
#check (Tropical R)[X]

I get the following error: failed to synthesize instance Semiring (Tropical R)

[Linus Sommer]

@Alex J. Best I was planing on using the extended reals .

[Kevin Buzzard]

variable {R : Type*} means "let $R$ be a set", and if $R$ is just a set then Tropical R is also just a set, and you can't take polynomials over a set.

[Kevin Buzzard]

I don't know what you're doing but if you really want to work with an arbitrary R then you should assume it's something like a totally ordered additive commutative monoid with a maximal element; then Tropical R will be a semiring which is probably the minimal sensible thing you need in order to make polynomials over it.

[Kevin Buzzard]

import Mathlib.Algebra.Tropical.Basic
import Mathlib.Data.Polynomial.Basic

variable {R : Type*} [LinearOrderedAddCommMonoidWithTop R]

open Tropical

open scoped Polynomial
#check (Tropical R)[X]

works.

[Kevin Buzzard]

This also works (now we don't introduce any new sets at all):

import Mathlib.Algebra.Tropical.Basic
import Mathlib.Data.Polynomial.Basic
import Mathlib.Data.Real.ENNReal

open Tropical ENNReal

open scoped Polynomial

#check (Tropical ℝ≥0∞)[X]

[Alex J. Best]

I spent some time playing with the different options, I think if you want to use WithTop R you can make it work.
The main difficulties are, you can't use negation directly (as there is no negative of the top element), tactics aren't working very well with this type and numerals, so if you want to calculate explicitly you have to awkwardly move back to the reals sometimes.

import Mathlib.Algebra.Tropical.Basic
import Mathlib.Data.Real.EReal
import Mathlib.Data.Polynomial.Eval
import Mathlib.Algebra.Group.OrderSynonym

-- check that we can treat nonnegative reals with infinity as a semiring
#synth Semiring (Tropical (WithTop ℝ))

open Polynomial Tropical
-- check that X^2 + 7 * X does the right thing tropically (min (X + X) (X + 7))
-- min (2 * 4) (4 + 3) = 7
-- min (2 * 0) (0 + 3) = 0

example : (X^2 + C (trop 3) * X : (Tropical (WithTop ℝ))[X]).eval (trop 4) = trop 7 := by
  simp
  rw [trop_add_def, pow_two, trop_mul_def, trop_mul_def, untrop_trop, untrop_trop, untrop_trop, untrop_trop]
  congr
  norm_num
  have : (7 : ℝ) ≤ (8 : ℝ) := by norm_num
  apply_fun ((↑) : ℝ → WithTop ℝ) at this
  norm_num [-WithTop.coe_le_coe] at this
  assumption
  exact WithTop.coe_mono

example : (X^2 + C (trop 3) * X : (Tropical (WithTop ℝ))[X]).eval (trop 0) = trop 0 := by
  simp
  rw [trop_add_def, untrop_trop, untrop_one,  ← trop_zero]
  congr
  norm_num
  have : (0 : ℝ) ≤ (3 : ℝ) := by norm_num
  apply_fun ((↑) : ℝ → WithTop ℝ) at this
  norm_num [-WithTop.coe_zero, -WithTop.coe_nonneg, -WithTop.coe_le_coe] at this
  assumption
  exact WithTop.coe_mono

[Linus Sommer]

@Kevin Buzzard @Alex J. Best thank you for your input I will experiment with your recommendations!

[Linus Sommer]

Hello,
How can I change the variables such that R has the type CommSemiring and f is a polynomial over R?
And how can I change the definition such that I pass something of type CommSemiring and get (Tropical R)[X]?

import Mathlib.Algebra.Tropical.Basic
import Mathlib.Data.Polynomial.Basic
import Mathlib.Data.Real.ENNReal

open Tropical ENNReal
open scoped Polynomial

universe f
variable {R : Type*} [LinearOrderedAddCommMonoidWithTop R]
variable {f : Type*} [R[X]]

def TropicalPolynomialring : R :=
  (Tropical R)[X]

#check TropicalPolynomialring ENNReal
-- (Tropical ℝ≥0∞)[X] : Type

Thank you for your help.

[Damiano Testa]

This gives you R as a CommSemiring and f as a polynomial with coefficients in R:

open Polynomial
variable {R} [CommSemiring R] (f : R[X])

[Damiano Testa]

I am not sure that I understand correctly your other question, but if R is a CommSemiring, there is not Semiring instance on Tropical R and hence you cannot take Polynomials of Tropical R. This however works:

def TropicalPolynomialring (R) [LinearOrderedAddCommMonoidWithTop R] := (Tropical R)[X]

[Damiano Testa]

Linus, I do not know what your actual goal is, but I suspect that the definition that I wrote above may not be such a good idea.

• First, it is longer to type TropicalPolynomialring R than (Tropical R)[X].
• Second, each new definition involves proving (trivial) properties about it, so that it merges well into the existing lemmas. Recycling the already defined Tropical R might save you some boilerplate.
• Third, with a def you are creating a copy of (Tropical R)[X] that carries none of the instances of the source:

import Mathlib.Algebra.Tropical.Basic
import Mathlib.Data.Polynomial.Basic

open Polynomial
variable (R) [LinearOrderedAddCommMonoidWithTop R]

def TropicalPolynomialringDef := (Tropical R)[X]
#synth Semiring (TropicalPolynomialringDef R)  -- failed

abbrev TropicalPolynomialring := (Tropical R)[X]
#synth Semiring (TropicalPolynomialring R)  -- finds `semiring`

So, I suspect that, at best, you may want an abbrev, but likely it might be better to work directly with the given name (Tropical R)[X]. Possibly, you may want to introduce notation for Tropical, but maybe even that is unclear.

I hope that this helps!

[Kevin Buzzard]

And how can I change the definition such that I pass something of type CommSemiring and get (Tropical R)[X]?

Tropical R is the same underlying type (i.e. set) as R but with a different algebraic structure, so if R is a CommSemiring then Tropical R has no reason to be (addition on Tropical R is coming from an order on R, but you didn't give R an order).

[Yakov Pechersky]

Linus, you might be interested in the (mathlib3) code I never PRed here: https://github.com/leanprover-community/mathlib/compare/master...pechersky/tropical-polynomial-again (or another branch https://github.com/leanprover-community/mathlib/compare/master...pechersky/tropical-polynomial)
with declarations like

lemma trop_eval_monotone_left [linear_ordered_add_comm_monoid_with_top S]
  (p : polynomial (tropical S)) :
  monotone (λ x, eval x p)

def _root_.polynomial.eval_tropical (p : polynomial (tropical (with_top R))) (hp : p ≠ 0) (x : R) :
  R :=

lemma concave_on_eval_tropical (p : polynomial (tropical (with_top R))) (hp : p ≠ 0) :
  concave_on' R set.univ (p.eval_tropical hp)