# Zulip Chat Archive

## 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,
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 (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
```

Thank you for your help.

#### 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 `Polynomial`

s 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
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 (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