Documentation

Mathlib.Algebra.Tropical.Basic

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

def Tropical (R : Type u) :

The tropicalization of a type R.

Equations

Tropical R = 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.

Equations

Tropical.trop = id

def Tropical.untrop {R : Type u} :

Tropical R → R

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

Equations

Tropical.untrop = id

theorem Tropical.trop_injective {R : Type u} :

Function.Injective Tropical.trop

theorem Tropical.untrop_injective {R : Type u} :

Function.Injective Tropical.untrop

@[simp]

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

Tropical.trop x = Tropical.trop y ↔ x = y

@[simp]

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

Tropical.untrop x = Tropical.untrop y ↔ x = y

@[simp]

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

Tropical.trop (Tropical.untrop x) = x

@[simp]

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

Tropical.untrop (Tropical.trop x) = x

theorem Tropical.leftInverse_trop {R : Type u} :

Function.LeftInverse Tropical.trop Tropical.untrop

theorem Tropical.rightInverse_trop {R : Type u} :

Function.RightInverse Tropical.trop Tropical.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.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem Tropical.tropEquiv_coe_fn {R : Type u} :

↑Tropical.tropEquiv = Tropical.trop

@[simp]

theorem Tropical.tropEquiv_symm_coe_fn {R : Type u} :

↑(Equiv.symm Tropical.tropEquiv) = Tropical.untrop

theorem Tropical.trop_eq_iff_eq_untrop {R : Type u} {x : R} {y : Tropical R} :

Tropical.trop x = y ↔ x = Tropical.untrop y

theorem Tropical.untrop_eq_iff_eq_trop {R : Type u} {x : Tropical R} {y : R} :

Tropical.untrop x = y ↔ x = Tropical.trop y

theorem Tropical.injective_trop {R : Type u} :

Function.Injective Tropical.trop

theorem Tropical.injective_untrop {R : Type u} :

Function.Injective Tropical.untrop

theorem Tropical.surjective_trop {R : Type u} :

Function.Surjective Tropical.trop

theorem Tropical.surjective_untrop {R : Type u} :

Function.Surjective Tropical.untrop

instance Tropical.instInhabitedTropical {R : Type u} [inst : Inhabited R] :

Inhabited (Tropical R)

Equations

Tropical.instInhabitedTropical = { default := Tropical.trop default }

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

F X

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

Equations

Tropical.tropRec h X = h (Tropical.untrop X)

instance Tropical.instDecidableEqTropical {R : Type u} [inst : DecidableEq R] :

DecidableEq (Tropical R)

Equations

Tropical.instDecidableEqTropical x x = decidable_of_iff (Tropical.untrop x = Tropical.untrop x) (_ : Tropical.untrop x = Tropical.untrop x ↔ x = x)

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

LE (Tropical R)

Equations

Tropical.instLETropical = { le := fun x y => Tropical.untrop x ≤ Tropical.untrop y }

@[simp]

theorem Tropical.untrop_le_iff {R : Type u} [inst : LE R] {x : Tropical R} {y : Tropical R} :

Tropical.untrop x ≤ Tropical.untrop y ↔ x ≤ y

instance Tropical.decidableLE {R : Type u} [inst : LE R] [inst : DecidableRel fun x x_1 => x ≤ x_1] :

DecidableRel fun x x_1 => x ≤ x_1

Equations

Tropical.decidableLE x y = inst (Tropical.untrop x) (Tropical.untrop y)

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

LT (Tropical R)

Equations

Tropical.instLTTropical = { lt := fun x y => Tropical.untrop x < Tropical.untrop y }

@[simp]

theorem Tropical.untrop_lt_iff {R : Type u} [inst : LT R] {x : Tropical R} {y : Tropical R} :

Tropical.untrop x < Tropical.untrop y ↔ x < y

instance Tropical.decidableLT {R : Type u} [inst : LT R] [inst : DecidableRel fun x x_1 => x < x_1] :

DecidableRel fun x x_1 => x < x_1

Equations

Tropical.decidableLT x y = inst (Tropical.untrop x) (Tropical.untrop y)

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

Preorder (Tropical R)

Equations

One or more equations did not get rendered due to their size.

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

R ≃o Tropical R

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

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem Tropical.tropOrderIso_coe_fn {R : Type u} [inst : Preorder R] :

↑(RelIso.toRelEmbedding Tropical.tropOrderIso).toEmbedding = Tropical.trop

@[simp]

theorem Tropical.tropOrderIso_symm_coe_fn {R : Type u} [inst : Preorder R] :

↑(RelIso.toRelEmbedding (OrderIso.symm Tropical.tropOrderIso)).toEmbedding = Tropical.untrop

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

Monotone Tropical.trop

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

Monotone Tropical.untrop

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

PartialOrder (Tropical R)

Equations

Tropical.instPartialOrderTropical = let src := Tropical.instPreorderTropical; PartialOrder.mk (_ : ∀ (x x_1 : Tropical R), x ≤ x_1 → x_1 ≤ x → x = x_1)

instance Tropical.instZeroTropical {R : Type u} [inst : Top R] :

Zero (Tropical R)

Equations

Tropical.instZeroTropical = { zero := Tropical.trop ⊤ }

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

Top (Tropical R)

Equations

Tropical.instTopTropical = { top := 0 }

@[simp]

theorem Tropical.untrop_zero {R : Type u} [inst : Top R] :

Tropical.untrop 0 = ⊤

@[simp]

theorem Tropical.trop_top {R : Type u} [inst : Top R] :

Tropical.trop ⊤ = 0

@[simp]

theorem Tropical.trop_coe_ne_zero {R : Type u} (x : R) :

Tropical.trop ↑x ≠ 0

@[simp]

theorem Tropical.zero_ne_trop_coe {R : Type u} (x : R) :

0 ≠ Tropical.trop ↑x

@[simp]

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

x ≤ 0

instance Tropical.instOrderTopTropicalInstLETropical {R : Type u} [inst : LE R] [inst : OrderTop R] :

OrderTop (Tropical R)

Equations

Tropical.instOrderTopTropicalInstLETropical = let src := Tropical.instTopTropical; OrderTop.mk (_ : ∀ (x : Tropical R), Tropical.untrop x ≤ ⊤)

instance Tropical.instAddTropical {R : Type u} [inst : LinearOrder R] :

Add (Tropical R)

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

Equations

Tropical.instAddTropical = { add := fun x y => Tropical.trop (min (Tropical.untrop x) (Tropical.untrop y)) }

instance Tropical.instAddCommSemigroupTropical {R : Type u} [inst : LinearOrder R] :

AddCommSemigroup (Tropical R)

Equations

Tropical.instAddCommSemigroupTropical = AddCommSemigroup.mk (_ : ∀ (x x_1 : Tropical R), x + x_1 = x_1 + x)

@[simp]

theorem Tropical.untrop_add {R : Type u} [inst : LinearOrder R] (x : Tropical R) (y : Tropical R) :

Tropical.untrop (x + y) = min (Tropical.untrop x) (Tropical.untrop y)

@[simp]

theorem Tropical.trop_min {R : Type u} [inst : LinearOrder R] (x : R) (y : R) :

Tropical.trop (min x y) = Tropical.trop x + Tropical.trop y

@[simp]

theorem Tropical.trop_inf {R : Type u} [inst : LinearOrder R] (x : R) (y : R) :

Tropical.trop (x ⊓ y) = Tropical.trop x + Tropical.trop y

theorem Tropical.trop_add_def {R : Type u} [inst : LinearOrder R] (x : Tropical R) (y : Tropical R) :

x + y = Tropical.trop (min (Tropical.untrop x) (Tropical.untrop y))

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

LinearOrder (Tropical R)

Equations

One or more equations did not get rendered due to their size.

@[simp]

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

Tropical.untrop (x ⊔ y) = Tropical.untrop x ⊔ Tropical.untrop y

@[simp]

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

Tropical.untrop (max x y) = max (Tropical.untrop x) (Tropical.untrop y)

@[simp]

theorem Tropical.min_eq_add {R : Type u} [inst : LinearOrder R] :

min = fun x x_1 => x + x_1

@[simp]

theorem Tropical.inf_eq_add {R : Type u} [inst : LinearOrder R] :

(fun x x_1 => x ⊓ x_1) = fun x x_1 => x + x_1

theorem Tropical.trop_max_def {R : Type u} [inst : LinearOrder R] (x : Tropical R) (y : Tropical R) :

max x y = Tropical.trop (max (Tropical.untrop x) (Tropical.untrop y))

theorem Tropical.trop_sup_def {R : Type u} [inst : LinearOrder R] (x : Tropical R) (y : Tropical R) :

x ⊔ y = Tropical.trop (Tropical.untrop x ⊔ Tropical.untrop y)

@[simp]

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

x + y = x

@[simp]

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

x + y = y

theorem Tropical.add_eq_left_iff {R : Type u} [inst : LinearOrder R] {x : Tropical R} {y : Tropical R} :

x + y = x ↔ x ≤ y

theorem Tropical.add_eq_right_iff {R : Type u} [inst : LinearOrder R] {x : Tropical R} {y : Tropical R} :

x + y = y ↔ y ≤ x

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

x + x = x

@[simp]

theorem Tropical.bit0 {R : Type u} [inst : LinearOrder R] (x : Tropical R) :

bit0 x = x

theorem Tropical.add_eq_iff {R : Type u} [inst : LinearOrder R] {x : Tropical R} {y : Tropical R} {z : Tropical R} :

x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x

@[simp]

theorem Tropical.add_eq_zero_iff {R : Type u} [inst : LinearOrder R] {a : Tropical (WithTop R)} {b : Tropical (WithTop R)} :

a + b = 0 ↔ a = 0 ∧ b = 0

instance Tropical.instAddCommMonoidTropical {R : Type u} [inst : LinearOrder R] [inst : OrderTop R] :

AddCommMonoid (Tropical R)

Equations

Tropical.instAddCommMonoidTropical = let src := Tropical.instZeroTropical; let src_1 := Tropical.instAddCommSemigroupTropical; AddCommMonoid.mk (_ : ∀ (a b : Tropical R), a + b = b + a)

instance Tropical.instMulTropical {R : Type u} [inst : Add R] :

Mul (Tropical R)

Tropical multiplication is the addition in the underlying R.

Equations

Tropical.instMulTropical = { mul := fun x y => Tropical.trop (Tropical.untrop x + Tropical.untrop y) }

@[simp]

theorem Tropical.trop_add {R : Type u} [inst : Add R] (x : R) (y : R) :

Tropical.trop (x + y) = Tropical.trop x * Tropical.trop y

@[simp]

theorem Tropical.untrop_mul {R : Type u} [inst : Add R] (x : Tropical R) (y : Tropical R) :

Tropical.untrop (x * y) = Tropical.untrop x + Tropical.untrop y

theorem Tropical.trop_mul_def {R : Type u} [inst : Add R] (x : Tropical R) (y : Tropical R) :

x * y = Tropical.trop (Tropical.untrop x + Tropical.untrop y)

instance Tropical.instOneTropical {R : Type u} [inst : Zero R] :

One (Tropical R)

Equations

Tropical.instOneTropical = { one := Tropical.trop 0 }

@[simp]

theorem Tropical.trop_zero {R : Type u} [inst : Zero R] :

Tropical.trop 0 = 1

@[simp]

theorem Tropical.untrop_one {R : Type u} [inst : Zero R] :

Tropical.untrop 1 = 0

instance Tropical.instAddMonoidWithOneTropical {R : Type u} [inst : LinearOrder R] [inst : OrderTop R] [inst : Zero R] :

AddMonoidWithOne (Tropical R)

Equations

Tropical.instAddMonoidWithOneTropical = let src := Tropical.instOneTropical; let src_1 := Tropical.instAddCommMonoidTropical; AddMonoidWithOne.mk

instance Tropical.instNontrivialTropicalWithTop {R : Type u} [inst : Zero R] :

Nontrivial (Tropical (WithTop R))

Equations

@Tropical.instNontrivialTropicalWithTop = @Tropical.instNontrivialTropicalWithTop.proof_1

instance Tropical.instInvTropical {R : Type u} [inst : Neg R] :

Inv (Tropical R)

Equations

Tropical.instInvTropical = { inv := fun x => Tropical.trop (-Tropical.untrop x) }

@[simp]

theorem Tropical.untrop_inv {R : Type u} [inst : Neg R] (x : Tropical R) :

Tropical.untrop x⁻¹ = -Tropical.untrop x

instance Tropical.instDivTropical {R : Type u} [inst : Sub R] :

Div (Tropical R)

Equations

Tropical.instDivTropical = { div := fun x y => Tropical.trop (Tropical.untrop x - Tropical.untrop y) }

@[simp]

theorem Tropical.untrop_div {R : Type u} [inst : Sub R] (x : Tropical R) (y : Tropical R) :

Tropical.untrop (x / y) = Tropical.untrop x - Tropical.untrop y

instance Tropical.instSemigroupTropical {R : Type u} [inst : AddSemigroup R] :

Semigroup (Tropical R)

Equations

Tropical.instSemigroupTropical = Semigroup.mk (_ : ∀ (x x_1 x_2 : Tropical R), x * x_1 * x_2 = x * (x_1 * x_2))

instance Tropical.instCommSemigroupTropical {R : Type u} [inst : AddCommSemigroup R] :

CommSemigroup (Tropical R)

Equations

Tropical.instCommSemigroupTropical = let src := Tropical.instSemigroupTropical; CommSemigroup.mk (_ : ∀ (x x_1 : Tropical R), x * x_1 = x_1 * x)

instance Tropical.instPowTropical {R : Type u} {α : Type u_1} [inst : SMul α R] :

Pow (Tropical R) α

Equations

Tropical.instPowTropical = { pow := fun x n => Tropical.trop (n • Tropical.untrop x) }

@[simp]

theorem Tropical.untrop_pow {R : Type u} {α : Type u_1} [inst : SMul α R] (x : Tropical R) (n : α) :

Tropical.untrop (x ^ n) = n • Tropical.untrop x

@[simp]

theorem Tropical.trop_smul {R : Type u} {α : Type u_1} [inst : SMul α R] (x : R) (n : α) :

Tropical.trop (n • x) = Tropical.trop x ^ n

instance Tropical.instMulOneClassTropical {R : Type u} [inst : AddZeroClass R] :

MulOneClass (Tropical R)

Equations

Tropical.instMulOneClassTropical = MulOneClass.mk (_ : ∀ (x : Tropical R), 1 * x = x) (_ : ∀ (x : Tropical R), x * 1 = x)

instance Tropical.instMonoidTropical {R : Type u} [inst : AddMonoid R] :

Monoid (Tropical R)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem Tropical.trop_nsmul {R : Type u} [inst : AddMonoid R] (x : R) (n : ℕ) :

Tropical.trop (n • x) = Tropical.trop x ^ n

instance Tropical.instCommMonoidTropical {R : Type u} [inst : AddCommMonoid R] :

CommMonoid (Tropical R)

Equations

Tropical.instCommMonoidTropical = let src := Tropical.instMonoidTropical; let src_1 := Tropical.instCommSemigroupTropical; CommMonoid.mk (_ : ∀ (a b : Tropical R), a * b = b * a)

instance Tropical.instGroupTropical {R : Type u} [inst : AddGroup R] :

Group (Tropical R)

Equations

Tropical.instGroupTropical = let src := Tropical.instMonoidTropical; Group.mk (_ : ∀ (x : Tropical R), x⁻¹ * x = 1)

instance Tropical.instCommGroupTropical {R : Type u} [inst : AddCommGroup R] :

CommGroup (Tropical R)

Equations

Tropical.instCommGroupTropical = let src := Tropical.instGroupTropical; CommGroup.mk (_ : ∀ (x x_1 : Tropical R), x * x_1 = x_1 * x)

@[simp]

theorem Tropical.untrop_zpow {R : Type u} [inst : AddGroup R] (x : Tropical R) (n : ℤ) :

Tropical.untrop (x ^ n) = n • Tropical.untrop x

@[simp]

theorem Tropical.trop_zsmul {R : Type u} [inst : AddGroup R] (x : R) (n : ℤ) :

Tropical.trop (n • x) = Tropical.trop x ^ n

instance Tropical.covariant_mul {R : Type u} [inst : LE R] [inst : Add R] [inst : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

CovariantClass (Tropical R) (Tropical R) (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

@Tropical.covariant_mul = @Tropical.covariant_mul.proof_1

instance Tropical.covariant_swap_mul {R : Type u} [inst : LE R] [inst : Add R] [inst : CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

CovariantClass (Tropical R) (Tropical R) (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

@Tropical.covariant_swap_mul = @Tropical.covariant_swap_mul.proof_1

instance Tropical.covariant_add {R : Type u} [inst : LinearOrder R] :

CovariantClass (Tropical R) (Tropical R) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

@Tropical.covariant_add = @Tropical.covariant_add.proof_1

instance Tropical.covariant_mul_lt {R : Type u} [inst : LT R] [inst : Add R] [inst : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

CovariantClass (Tropical R) (Tropical R) (fun x x_1 => x * x_1) fun x x_1 => x < x_1

Equations

@Tropical.covariant_mul_lt = @Tropical.covariant_mul_lt.proof_1

instance Tropical.covariant_swap_mul_lt {R : Type u} [inst : Preorder R] [inst : Add R] [inst : CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

CovariantClass (Tropical R) (Tropical R) (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1

Equations

@Tropical.covariant_swap_mul_lt = @Tropical.covariant_swap_mul_lt.proof_1

instance Tropical.instDistribTropical {R : Type u} [inst : LinearOrder R] [inst : Add R] [inst : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

Distrib (Tropical R)

Equations

Tropical.instDistribTropical = Distrib.mk (_ : ∀ (x x_1 x_2 : Tropical R), x * (x_1 + x_2) = x * x_1 + x * x_2) (_ : ∀ (x x_1 x_2 : Tropical R), (x + x_1) * x_2 = x * x_2 + x_1 * x_2)

@[simp]

theorem Tropical.add_pow {R : Type u} [inst : LinearOrder R] [inst : AddMonoid R] [inst : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (x : Tropical R) (y : Tropical R) (n : ℕ) :

(x + y) ^ n = x ^ n + y ^ n

instance Tropical.instCommSemiringTropical {R : Type u} [inst : LinearOrderedAddCommMonoidWithTop R] :

CommSemiring (Tropical R)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem Tropical.succ_nsmul {R : Type u_1} [inst : LinearOrder R] [inst : OrderTop R] (x : Tropical R) (n : ℕ) :

(n + 1) • x = x

theorem Tropical.mul_eq_zero_iff {R : Type u_1} [inst : LinearOrderedAddCommMonoid R] {a : Tropical (WithTop R)} {b : Tropical (WithTop R)} :

a * b = 0 ↔ a = 0 ∨ b = 0

instance Tropical.instNoZeroDivisorsTropicalWithTopInstMulTropicalAddToAddToAddZeroClassToAddMonoidToAddCommMonoidInstZeroTropicalTop {R : Type u_1} [inst : LinearOrderedAddCommMonoid R] :

NoZeroDivisors (Tropical (WithTop R))

Equations

One or more equations did not get rendered due to their size.