mathlib documentation

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 has_top and min. For the max-tropical numbers, use order_dual 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) :
Type u

The tropicalization of a type R.

Equations
def tropical.trop {R : Type u} :
R → tropical R

Reinterpret x : R as an element of tropical R. See tropical.trop_equiv for the equivalence.

Equations
def tropical.untrop {R : Type u} :
tropical R → R

Reinterpret x : tropical R as an element of R. See tropical.trop_equiv for the equivalence.

Equations
@[simp]
theorem tropical.trop_inj_iff {R : Type u} (x y : R) :
@[simp]
theorem tropical.untrop_inj_iff {R : Type u} (x y : tropical R) :
@[simp]
theorem tropical.trop_untrop {R : Type u} (x : tropical R) :
@[simp]
theorem tropical.untrop_trop {R : Type u} (x : R) :
def tropical.trop_equiv {R : Type u} :

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

Equations
theorem tropical.trop_eq_iff_eq_untrop {R : Type u} {x : R} {y : tropical R} :
theorem tropical.untrop_eq_iff_eq_trop {R : Type u} {x : tropical R} {y : R} :
@[instance]
def tropical.inhabited {R : Type u} [inhabited R] :
Equations
@[simp]
def tropical.trop_rec {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
@[simp]
theorem tropical.untrop_le_iff {R : Type u} [preorder R] {x y : tropical R} :
def tropical.trop_order_iso {R : Type u} [preorder R] :

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

Equations
@[instance]
def tropical.has_zero {R : Type u} [has_top R] :
Equations
@[instance]
def tropical.has_top {R : Type u} [has_top R] :
Equations
@[simp]
theorem tropical.untrop_zero {R : Type u} [has_top R] :
@[simp]
theorem tropical.trop_top {R : Type u} [has_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} [order_top R] (x : tropical R) :
x 0
def tropical.add {R : Type u} [linear_order R] (x y : tropical R) :

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

Equations
@[simp]
theorem tropical.untrop_add {R : Type u} [linear_order R] (x y : tropical R) :
@[simp]
theorem tropical.add_eq_left {R : Type u} [linear_order R] ⦃x y : tropical R⦄ (h : x y) :
x + y = x
@[simp]
theorem tropical.add_eq_right {R : Type u} [linear_order R] ⦃x y : tropical R⦄ (h : y x) :
x + y = y
@[simp]
theorem tropical.add_self {R : Type u} [linear_order R] (x : tropical R) :
x + x = x
@[simp]
theorem tropical.bit0 {R : Type u} [linear_order R] (x : tropical R) :
bit0 x = x
theorem tropical.add_eq_iff {R : Type u} [linear_order 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} [linear_order R] {a b : tropical (with_top R)} :
a + b = 0 a = 0 b = 0
def tropical.mul {R : Type u} [has_add R] (x y : tropical R) :

Tropical multiplication is the addition in the underlying R.

Equations
@[instance]
def tropical.has_mul {R : Type u} [has_add R] :
Equations
@[simp]
theorem tropical.untrop_mul {R : Type u} [has_add R] (x y : tropical R) :
theorem tropical.trop_mul_def {R : Type u} [has_add R] (x y : tropical R) :
@[instance]
def tropical.has_one {R : Type u} [has_zero R] :
Equations
@[instance]
def tropical.nontrivial {R : Type u} [has_zero R] :
@[instance]
def tropical.has_inv {R : Type u} [has_neg R] :
Equations
@[simp]
@[instance]
def tropical.has_div {R : Type u} [has_sub R] :
Equations
@[simp]
theorem tropical.untrop_div {R : Type u} [has_sub R] (x y : tropical R) :
@[simp]
theorem tropical.untrop_one {R : Type u} [add_monoid R] :
@[simp]
theorem tropical.untrop_pow {R : Type u} [add_monoid R] (x : tropical R) (n : ) :
@[simp]
theorem tropical.trop_nsmul {R : Type u} [add_monoid R] (x : R) (n : ) :
@[instance]
def tropical.group {R : Type u} [add_group R] :
Equations
@[simp]
theorem tropical.add_pow {R : Type u} [linear_order R] [add_monoid R] [covariant_class R R has_add.add has_le.le] [covariant_class R R (function.swap has_add.add) has_le.le] (x y : tropical R) (n : ) :
(x + y) ^ n = x ^ n + y ^ n
@[instance]
Equations
@[simp]
theorem tropical.succ_nsmul {R : Type u} [linear_ordered_add_comm_monoid_with_top R] (x : tropical R) (n : ) :
(n + 1) x = x
@[simp]
theorem tropical.mul_eq_zero_iff {R : Type u_1} [linear_ordered_add_comm_monoid R] {a b : tropical (with_top R)} :
a * b = 0 a = 0 b = 0