Tropical algebraic structures

This file defines algebraic structures of the (min-)tropical numbers, up to the tropical semiring. Some basic lemmas about conversion from the base type R to Tropical R are provided, as well as the expected implementations of tropical addition and tropical multiplication.

Main declarations

• Tropical R: The type synonym of the tropical interpretation of R. If [LinearOrder R], then addition on R is via min.
• Semiring (Tropical R): A LinearOrderedAddCommMonoidWithTop R induces a Semiring (Tropical R). If one solely has [LinearOrderedAddCommMonoid R], then the "tropicalization of R" would be Tropical (WithTop R).

Implementation notes

The tropical structure relies on Top and min. For the max-tropical numbers, use OrderDual R.

Inspiration was drawn from the implementation of Additive/Multiplicative/Opposite, where a type synonym is created with some barebones API, and quickly made irreducible.

Algebraic structures are provided with as few typeclass assumptions as possible, even though most references rely on Semiring (Tropical R) for building up the whole theory.

References followed

• https://arxiv.org/pdf/math/0408099.pdf
• https://www.mathenjeans.fr/sites/default/files/sujets/tropical_geometry_-_casagrande.pdf

@[irreducible]

def Tropical (R : Type u) : Type u

The tropicalization of a type R.

def Tropical.trop {R : Type u} : R → Tropical R

Reinterpret x : R as an element of Tropical R. See Tropical.tropEquiv for the equivalence.

def Tropical.untrop {R : Type u} : Tropical R → R

Reinterpret x : Tropical R as an element of R. See Tropical.tropEquiv for the equivalence.

theorem Tropical.trop_injective {R : Type u} : Function.Injective trop

theorem Tropical.untrop_injective {R : Type u} : Function.Injective untrop

@[simp]

theorem Tropical.trop_inj_iff {R : Type u} (x y : R) : trop x = trop y ↔ x = y

@[simp]

theorem Tropical.untrop_inj_iff {R : Type u} (x y : Tropical R) : untrop x = untrop y ↔ x = y

@[simp]

theorem Tropical.trop_untrop {R : Type u} (x : Tropical R) : trop (untrop x) = x

@[simp]

theorem Tropical.untrop_trop {R : Type u} (x : R) : untrop (trop x) = x

theorem Tropical.leftInverse_trop {R : Type u} : Function.LeftInverse trop untrop

theorem Tropical.rightInverse_trop {R : Type u} : Function.RightInverse trop untrop

def Tropical.tropEquiv {R : Type u} : R ≃ Tropical R

Reinterpret x : R as an element of Tropical R. See Tropical.tropOrderIso for the order-preserving equivalence.

@[simp]

theorem Tropical.tropEquiv_coe_fn {R : Type u} : ⇑tropEquiv = trop

@[simp]

theorem Tropical.tropEquiv_symm_coe_fn {R : Type u} : ⇑tropEquiv.symm = untrop

theorem Tropical.trop_eq_iff_eq_untrop {R : Type u} {x : R} {y : Tropical R} : trop x = y ↔ x = untrop y

theorem Tropical.untrop_eq_iff_eq_trop {R : Type u} {x : Tropical R} {y : R} : untrop x = y ↔ x = trop y

theorem Tropical.injective_trop {R : Type u} : Function.Injective trop

theorem Tropical.injective_untrop {R : Type u} : Function.Injective untrop

theorem Tropical.surjective_trop {R : Type u} : Function.Surjective trop

theorem Tropical.surjective_untrop {R : Type u} : Function.Surjective untrop

@[implicit_reducible]

instance Tropical.instInhabited {R : Type u} [Inhabited R] : Inhabited (Tropical R)

def Tropical.tropRec {R : Type u} {F : Tropical R → Sort v} (h : (X : R) → F (trop X)) (X : Tropical R) : F X

Recursing on an x' : Tropical R is the same as recursing on an x : R reinterpreted as a term of Tropical R via trop x.

@[implicit_reducible]

instance Tropical.instDecidableEq {R : Type u} [DecidableEq R] : DecidableEq (Tropical R)

@[implicit_reducible]

instance Tropical.instLETropical {R : Type u} [LE R] : LE (Tropical R)

@[simp]

theorem Tropical.untrop_le_iff {R : Type u} [LE R] {x y : Tropical R} : untrop x ≤ untrop y ↔ x ≤ y

@[implicit_reducible]

instance Tropical.decidableLE {R : Type u} [LE R] [DecidableLE R] : DecidableLE (Tropical R)

@[implicit_reducible]

instance Tropical.instLTTropical {R : Type u} [LT R] : LT (Tropical R)

@[simp]

theorem Tropical.untrop_lt_iff {R : Type u} [LT R] {x y : Tropical R} : untrop x < untrop y ↔ x < y

@[implicit_reducible]

instance Tropical.decidableLT {R : Type u} [LT R] [DecidableLT R] : DecidableLT (Tropical R)

@[implicit_reducible]

instance Tropical.instPreorderTropical {R : Type u} [Preorder R] : Preorder (Tropical R)

def Tropical.tropOrderIso {R : Type u} [Preorder R] : R ≃o Tropical R

Reinterpret x : R as an element of Tropical R, preserving the order.

@[simp]

theorem Tropical.tropOrderIso_coe_fn {R : Type u} [Preorder R] : ⇑tropOrderIso = trop

@[simp]

theorem Tropical.tropOrderIso_symm_coe_fn {R : Type u} [Preorder R] : ⇑tropOrderIso.symm = untrop

theorem Tropical.trop_monotone {R : Type u} [Preorder R] : Monotone trop

theorem Tropical.untrop_monotone {R : Type u} [Preorder R] : Monotone untrop

@[implicit_reducible]

instance Tropical.instPartialOrderTropical {R : Type u} [PartialOrder R] : PartialOrder (Tropical R)

@[implicit_reducible]

instance Tropical.instZeroTropical {R : Type u} [Top R] : Zero (Tropical R)

@[implicit_reducible]

instance Tropical.instTopTropical {R : Type u} [Top R] : Top (Tropical R)

@[simp]

theorem Tropical.untrop_zero {R : Type u} [Top R] : untrop 0 = ⊤

@[simp]

theorem Tropical.trop_top {R : Type u} [Top R] : trop ⊤ = 0

@[simp]

theorem Tropical.trop_coe_ne_zero {R : Type u} (x : R) : trop ↑x ≠ 0

@[simp]

theorem Tropical.zero_ne_trop_coe {R : Type u} (x : R) : 0 ≠ trop ↑x

@[simp]

theorem Tropical.le_zero {R : Type u} [LE R] [OrderTop R] (x : Tropical R) : x ≤ 0

@[implicit_reducible]

instance Tropical.instOrderTop {R : Type u} [LE R] [OrderTop R] : OrderTop (Tropical R)

@[implicit_reducible]

instance Tropical.instAdd {R : Type u} [LinearOrder R] : Add (Tropical R)

Tropical addition is the minimum of two underlying elements of R.

@[implicit_reducible]

instance Tropical.instAddCommSemigroupTropical {R : Type u} [LinearOrder R] : AddCommSemigroup (Tropical R)

@[simp]

theorem Tropical.untrop_add {R : Type u} [LinearOrder R] (x y : Tropical R) : untrop (x + y) = min (untrop x) (untrop y)

@[simp]

theorem Tropical.trop_min {R : Type u} [LinearOrder R] (x y : R) : trop (min x y) = trop x + trop y

@[simp]

theorem Tropical.trop_inf {R : Type u} [LinearOrder R] (x y : R) : trop (min x y) = trop x + trop y

theorem Tropical.trop_add_def {R : Type u} [LinearOrder R] (x y : Tropical R) : x + y = trop (min (untrop x) (untrop y))

@[implicit_reducible]

instance Tropical.instLinearOrderTropical {R : Type u} [LinearOrder R] : LinearOrder (Tropical R)

@[simp]

theorem Tropical.untrop_sup {R : Type u} [LinearOrder R] (x y : Tropical R) : untrop (max x y) = max (untrop x) (untrop y)

@[simp]

theorem Tropical.untrop_max {R : Type u} [LinearOrder R] (x y : Tropical R) : untrop (max x y) = max (untrop x) (untrop y)

@[simp]

theorem Tropical.min_eq_add {R : Type u} [LinearOrder R] : min = fun (x1 x2 : Tropical R) => x1 + x2

@[simp]

theorem Tropical.inf_eq_add {R : Type u} [LinearOrder R] : (fun (x1 x2 : Tropical R) => min x1 x2) = fun (x1 x2 : Tropical R) => x1 + x2

theorem Tropical.trop_max_def {R : Type u} [LinearOrder R] (x y : Tropical R) : max x y = trop (max (untrop x) (untrop y))

theorem Tropical.trop_sup_def {R : Type u} [LinearOrder R] (x y : Tropical R) : max x y = trop (max (untrop x) (untrop y))

@[simp]

theorem Tropical.add_eq_left {R : Type u} [LinearOrder R] ⦃x y : Tropical R⦄ (h : x ≤ y) : x + y = x

@[simp]

theorem Tropical.add_eq_right {R : Type u} [LinearOrder R] ⦃x y : Tropical R⦄ (h : y ≤ x) : x + y = y

theorem Tropical.add_eq_left_iff {R : Type u} [LinearOrder R] {x y : Tropical R} : x + y = x ↔ x ≤ y

theorem Tropical.add_eq_right_iff {R : Type u} [LinearOrder R] {x y : Tropical R} : x + y = y ↔ y ≤ x

theorem Tropical.add_self {R : Type u} [LinearOrder R] (x : Tropical R) : x + x = x

theorem Tropical.add_eq_iff {R : Type u} [LinearOrder R] {x y z : Tropical R} : x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x

@[simp]

theorem Tropical.add_eq_zero_iff {R : Type u} [LinearOrder R] {a b : Tropical (WithTop R)} : a + b = 0 ↔ a = 0 ∧ b = 0

@[implicit_reducible]

instance Tropical.instAddCommMonoidTropical {R : Type u} [LinearOrder R] [OrderTop R] : AddCommMonoid (Tropical R)

@[implicit_reducible]

instance Tropical.instMulOfAdd {R : Type u} [Add R] : Mul (Tropical R)

Tropical multiplication is the addition in the underlying R.

@[simp]

theorem Tropical.trop_add {R : Type u} [Add R] (x y : R) : trop (x + y) = trop x * trop y

@[simp]

theorem Tropical.untrop_mul {R : Type u} [Add R] (x y : Tropical R) : untrop (x * y) = untrop x + untrop y

theorem Tropical.trop_mul_def {R : Type u} [Add R] (x y : Tropical R) : x * y = trop (untrop x + untrop y)

@[implicit_reducible]

instance Tropical.instOneTropical {R : Type u} [Zero R] : One (Tropical R)

@[simp]

theorem Tropical.trop_zero {R : Type u} [Zero R] : trop 0 = 1

@[simp]

theorem Tropical.untrop_one {R : Type u} [Zero R] : untrop 1 = 0

@[implicit_reducible]

instance Tropical.instAddMonoidWithOneTropical {R : Type u} [LinearOrder R] [OrderTop R] [Zero R] : AddMonoidWithOne (Tropical R)

instance Tropical.instNontrivialWithTopOfZero {R : Type u} [Zero R] : Nontrivial (Tropical (WithTop R))

@[implicit_reducible]

instance Tropical.instInvOfNeg {R : Type u} [Neg R] : Inv (Tropical R)

@[simp]

theorem Tropical.untrop_inv {R : Type u} [Neg R] (x : Tropical R) : untrop x⁻¹ = -untrop x

@[implicit_reducible]

instance Tropical.instDivOfSub {R : Type u} [Sub R] : Div (Tropical R)

@[simp]

theorem Tropical.untrop_div {R : Type u} [Sub R] (x y : Tropical R) : untrop (x / y) = untrop x - untrop y

@[implicit_reducible]

instance Tropical.instSemigroupTropical {R : Type u} [AddSemigroup R] : Semigroup (Tropical R)

@[implicit_reducible]

instance Tropical.instCommSemigroupTropical {R : Type u} [AddCommSemigroup R] : CommSemigroup (Tropical R)

@[implicit_reducible]

instance Tropical.instPowOfSMul {R : Type u} {α : Type u_1} [SMul α R] : Pow (Tropical R) α

@[simp]

theorem Tropical.untrop_pow {R : Type u} {α : Type u_1} [SMul α R] (x : Tropical R) (n : α) : untrop (x ^ n) = n • untrop x

@[simp]

theorem Tropical.trop_smul {R : Type u} {α : Type u_1} [SMul α R] (x : R) (n : α) : trop (n • x) = trop x ^ n

@[implicit_reducible]

instance Tropical.instMulOneClassTropical {R : Type u} [AddZeroClass R] : MulOneClass (Tropical R)

@[implicit_reducible]

instance Tropical.instMonoidTropical {R : Type u} [AddMonoid R] : Monoid (Tropical R)

@[simp]

theorem Tropical.trop_nsmul {R : Type u} [AddMonoid R] (x : R) (n : ℕ) : trop (n • x) = trop x ^ n

@[implicit_reducible]

instance Tropical.instCommMonoidTropical {R : Type u} [AddCommMonoid R] : CommMonoid (Tropical R)

@[implicit_reducible]

instance Tropical.instGroupTropical {R : Type u} [AddGroup R] : Group (Tropical R)

@[implicit_reducible]

instance Tropical.instCommGroupOfAddCommGroup {R : Type u} [AddCommGroup R] : CommGroup (Tropical R)

@[simp]

theorem Tropical.untrop_zpow {R : Type u} [AddGroup R] (x : Tropical R) (n : ℤ) : untrop (x ^ n) = n • untrop x

@[simp]

theorem Tropical.trop_zsmul {R : Type u} [AddGroup R] (x : R) (n : ℤ) : trop (n • x) = trop x ^ n

instance Tropical.mulLeftMono {R : Type u} [LE R] [Add R] [AddLeftMono R] : MulLeftMono (Tropical R)

instance Tropical.mulRightMono {R : Type u} [LE R] [Add R] [AddRightMono R] : MulRightMono (Tropical R)

instance Tropical.addLeftMono {R : Type u} [LinearOrder R] : AddLeftMono (Tropical R)

instance Tropical.mulLeftStrictMono {R : Type u} [LT R] [Add R] [AddLeftStrictMono R] : MulLeftStrictMono (Tropical R)

instance Tropical.mulRightStrictMono {R : Type u} [Preorder R] [Add R] [AddRightStrictMono R] : MulRightStrictMono (Tropical R)

@[implicit_reducible]

instance Tropical.instDistribTropical {R : Type u} [LinearOrder R] [Add R] [AddLeftMono R] [AddRightMono R] : Distrib (Tropical R)

@[simp]

theorem Tropical.add_pow {R : Type u} [LinearOrder R] [AddMonoid R] [AddLeftMono R] [AddRightMono R] (x y : Tropical R) (n : ℕ) : (x + y) ^ n = x ^ n + y ^ n

@[implicit_reducible]

instance Tropical.instCommSemiring {R : Type u} [LinearOrderedAddCommMonoidWithTop R] : CommSemiring (Tropical R)

@[simp]

theorem Tropical.succ_nsmul {R : Type u_1} [LinearOrder R] [OrderTop R] (x : Tropical R) (n : ℕ) : (n + 1) • x = x

theorem Tropical.mul_eq_zero_iff {R : Type u_1} [AddCommMonoid R] {a b : Tropical (WithTop R)} : a * b = 0 ↔ a = 0 ∨ b = 0

instance Tropical.instNoZeroDivisorsWithTop {R : Type u_1} [AddCommMonoid R] : NoZeroDivisors (Tropical (WithTop R))