mathlib3 documentation

algebra.tropical.basic

Tropical algebraic structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.trop {R : Type u} :

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

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

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]
@[simp]
@[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
@[simp]
def tropical.trop_rec {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
@[protected, instance]
def tropical.has_le {R : Type u} [has_le R] :
Equations
@[simp]
@[protected, instance]
Equations
@[protected, instance]
def tropical.has_lt {R : Type u} [has_lt R] :
Equations
@[simp]
theorem tropical.untrop_lt_iff {R : Type u} [has_lt R] {x y : tropical R} :
@[protected, instance]
Equations

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

Equations
@[protected, instance]
Equations
@[protected, instance]
def tropical.has_top {R : Type u} [has_top R] :
Equations
@[simp]
@[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} [has_le R] [order_top R] (x : tropical R) :
x 0
@[protected, instance]
Equations
@[protected, instance]

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

Equations
@[simp]
theorem tropical.trop_inf {R : Type u} [linear_order R] (x y : 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
theorem tropical.add_eq_left_iff {R : Type u} [linear_order R] {x y : tropical R} :
x + y = x x y
theorem tropical.add_eq_right_iff {R : Type u} [linear_order R] {x y : tropical R} :
x + y = y y x
@[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
@[protected, instance]
Equations
@[protected, instance]
def tropical.has_mul {R : Type u} [has_add R] :

Tropical multiplication is the addition in the underlying R.

Equations
@[simp]
theorem tropical.trop_add {R : Type u} [has_add R] (x y : R) :
@[simp]
@[protected, instance]
def tropical.has_one {R : Type u} [has_zero R] :
Equations
@[simp]
theorem tropical.trop_zero {R : Type u} [has_zero R] :
@[simp]
theorem tropical.untrop_one {R : Type u} [has_zero R] :
@[protected, instance]
@[protected, instance]
def tropical.has_inv {R : Type u} [has_neg R] :
Equations
@[protected, instance]
def tropical.has_div {R : Type u} [has_sub R] :
Equations
@[simp]
@[protected, instance]
Equations
@[protected, instance]
def tropical.has_pow {R : Type u} {α : Type u_1} [has_smul α R] :
Equations
@[simp]
theorem tropical.untrop_pow {R : Type u} {α : Type u_1} [has_smul α R] (x : tropical R) (n : α) :
@[simp]
theorem tropical.trop_smul {R : Type u} {α : Type u_1} [has_smul α R] (x : R) (n : α) :
@[protected, instance]
Equations
@[protected, instance]
def tropical.monoid {R : Type u} [add_monoid R] :
Equations
@[simp]
theorem tropical.trop_nsmul {R : Type u} [add_monoid R] (x : R) (n : ) :
@[protected, instance]
def tropical.group {R : Type u} [add_group R] :
Equations
@[simp]
theorem tropical.untrop_zpow {R : Type u} [add_group R] (x : tropical R) (n : ) :
@[simp]
theorem tropical.trop_zsmul {R : Type u} [add_group R] (x : R) (n : ) :
@[simp]
@[simp]
theorem tropical.succ_nsmul {R : Type u_1} [linear_order R] [order_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