## Stream: new members

### Topic: Tropical polynomials

#### Linus Sommer (Sep 09 2023 at 13:41):

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,
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 (Sep 09 2023 at 13:54):

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

#### Eric Wieser (Sep 09 2023 at 14:00):

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 (Sep 09 2023 at 14:00):

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 (Sep 09 2023 at 14:24):

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

#### Alex J. Best (Sep 09 2023 at 14:27):

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 (Sep 09 2023 at 14:32):

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 (Sep 09 2023 at 14:32):

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 (Sep 09 2023 at 14:34):

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

#### Kevin Buzzard (Sep 09 2023 at 14:37):

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 (Sep 09 2023 at 14:39):

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 (Sep 09 2023 at 14:39):

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 (Sep 09 2023 at 14:43):

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 (Sep 09 2023 at 14:49):

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 (Sep 09 2023 at 17:34):

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

#### Linus Sommer (Sep 10 2023 at 09:42):

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


#### Damiano Testa (Sep 10 2023 at 09:46):

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 (Sep 10 2023 at 09:53):

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 (Sep 10 2023 at 10:44):

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

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 (Sep 10 2023 at 12:03):

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 (Sep 10 2023 at 14:56):

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)


Last updated: Dec 20 2023 at 11:08 UTC