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 #

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 #

def Tropical (R : Type u) :

The tropicalization of a type R.

Equations
def Tropical.trop {R : Type u} :
RTropical 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 RR

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

Equations
  • Tropical.untrop = id
@[simp]
theorem Tropical.trop_inj_iff {R : Type u} (x : R) (y : R) :
@[simp]
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

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
Equations
def Tropical.tropRec {R : Type u} {F : Tropical RSort 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
instance Tropical.instLETropical {R : Type u} [inst : LE R] :
Equations
@[simp]
theorem Tropical.untrop_le_iff {R : Type u} [inst : LE R] {x : Tropical R} {y : Tropical R} :
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
instance Tropical.instLTTropical {R : Type u} [inst : LT R] :
Equations
@[simp]
theorem Tropical.untrop_lt_iff {R : Type u} [inst : LT R] {x : Tropical R} {y : Tropical R} :
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
Equations
  • One or more equations did not get rendered due to their size.
def Tropical.tropOrderIso {R : Type u} [inst : Preorder 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
Equations
  • Tropical.instPartialOrderTropical = let src := Tropical.instPreorderTropical; PartialOrder.mk (_ : ∀ (x x_1 : Tropical R), x x_1x_1 xx = x_1)
instance Tropical.instZeroTropical {R : Type u} [inst : Top R] :
Equations
instance Tropical.instTopTropical {R : Type u} [inst : Top R] :
Equations
  • Tropical.instTopTropical = { top := 0 }
@[simp]
theorem Tropical.untrop_zero {R : Type u} [inst : Top R] :
@[simp]
theorem Tropical.trop_top {R : Type u} [inst : Top R] :
@[simp]
theorem Tropical.trop_coe_ne_zero {R : Type u} (x : R) :
@[simp]
theorem Tropical.zero_ne_trop_coe {R : Type u} (x : R) :
@[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] :
Equations
instance Tropical.instAddTropical {R : Type u} [inst : LinearOrder R] :

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

Equations
Equations
@[simp]
theorem Tropical.untrop_add {R : Type u} [inst : LinearOrder R] (x : Tropical R) (y : Tropical R) :
@[simp]
theorem Tropical.trop_min {R : Type u} [inst : LinearOrder R] (x : R) (y : R) :
@[simp]
theorem Tropical.trop_inf {R : Type u} [inst : LinearOrder R] (x : R) (y : R) :
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Tropical.untrop_max {R : Type u} [inst : LinearOrder R] (x : Tropical R) (y : Tropical R) :
@[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
@[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
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] :

Tropical multiplication is the addition in the underlying R.

Equations
@[simp]
theorem Tropical.trop_add {R : Type u} [inst : Add R] (x : R) (y : R) :
@[simp]
theorem Tropical.untrop_mul {R : Type u} [inst : Add R] (x : Tropical R) (y : Tropical R) :
instance Tropical.instOneTropical {R : Type u} [inst : Zero R] :
Equations
@[simp]
theorem Tropical.trop_zero {R : Type u} [inst : Zero R] :
@[simp]
theorem Tropical.untrop_one {R : Type u} [inst : Zero R] :
instance Tropical.instAddMonoidWithOneTropical {R : Type u} [inst : LinearOrder R] [inst : OrderTop R] [inst : Zero R] :
Equations
  • Tropical.instAddMonoidWithOneTropical = let src := Tropical.instOneTropical; let src_1 := Tropical.instAddCommMonoidTropical; AddMonoidWithOne.mk
instance Tropical.instInvTropical {R : Type u} [inst : Neg R] :
Equations
@[simp]
instance Tropical.instDivTropical {R : Type u} [inst : Sub R] :
Equations
@[simp]
theorem Tropical.untrop_div {R : Type u} [inst : Sub R] (x : Tropical R) (y : Tropical R) :
Equations
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
@[simp]
theorem Tropical.untrop_pow {R : Type u} {α : Type u_1} [inst : SMul α R] (x : Tropical R) (n : α) :
@[simp]
theorem Tropical.trop_smul {R : Type u} {α : Type u_1} [inst : SMul α R] (x : R) (n : α) :
Equations
instance Tropical.instMonoidTropical {R : Type u} [inst : AddMonoid 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 : ) :
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] :
Equations
  • Tropical.instGroupTropical = let src := Tropical.instMonoidTropical; Group.mk (_ : ∀ (x : Tropical R), x⁻¹ * x = 1)
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 : ) :
@[simp]
theorem Tropical.trop_zsmul {R : Type u} [inst : AddGroup R] (x : R) (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
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
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
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
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
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] :
Equations
@[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
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