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 #

tropical R: The type synonym of the tropical interpretation of R. If [linear_order R], then addition on R is via min.
semiring (tropical R): A linear_ordered_add_comm_monoid_with_top R induces a semiring (tropical R). If one solely has [linear_ordered_add_comm_monoid R], then the "tropicalization of R" would be tropical (with_top R).

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 #

@[irreducible]

def tropical (R : Type u) :

The tropicalization of a type R.

Equations

tropical R = R

Instances for tropical

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

tropical.trop = id

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

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 y : R) :

tropical.trop x = tropical.trop y ↔ x = y

@[simp]

theorem tropical.untrop_inj_iff {R : Type u} (x 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.left_inverse_trop {R : Type u} :

function.left_inverse tropical.trop tropical.untrop

theorem tropical.right_inverse_trop {R : Type u} :

function.right_inverse tropical.trop tropical.untrop

def tropical.trop_equiv {R : Type u} :

R ≃ tropical R

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

Equations

tropical.trop_equiv = {to_fun := tropical.trop R, inv_fun := tropical.untrop R, left_inv := _, right_inv := _}

@[simp]

theorem tropical.trop_equiv_coe_fn {R : Type u} :

⇑tropical.trop_equiv = tropical.trop

@[simp]

theorem tropical.trop_equiv_symm_coe_fn {R : Type u} :

⇑(tropical.trop_equiv.symm) = 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

@[protected, instance]

def tropical.inhabited {R : Type u} [inhabited R] :

inhabited (tropical R)

Equations

tropical.inhabited = {default := tropical.trop inhabited.default}

@[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

tropical.trop_rec h = λ (X : tropical R), h (tropical.untrop X)

@[protected, instance]

def tropical.decidable_eq {R : Type u} [decidable_eq R] :

decidable_eq (tropical R)

Equations

tropical.decidable_eq = λ (x y : tropical R), decidable_of_iff (tropical.untrop x = tropical.untrop y) _

@[protected, instance]

def tropical.has_le {R : Type u} [has_le R] :

has_le (tropical R)

Equations

tropical.has_le = {le := λ (x y : tropical R), tropical.untrop x ≤ tropical.untrop y}

@[simp]

theorem tropical.untrop_le_iff {R : Type u} [has_le R] {x y : tropical R} :

tropical.untrop x ≤ tropical.untrop y ↔ x ≤ y

@[protected, instance]

def tropical.decidable_le {R : Type u} [has_le R] [decidable_rel has_le.le] :

decidable_rel has_le.le

Equations

tropical.decidable_le = λ (x y : tropical R), _inst_2 (tropical.untrop x) (tropical.untrop y)

@[protected, instance]

def tropical.has_lt {R : Type u} [has_lt R] :

has_lt (tropical R)

Equations

tropical.has_lt = {lt := λ (x y : tropical R), tropical.untrop x < tropical.untrop y}

@[simp]

theorem tropical.untrop_lt_iff {R : Type u} [has_lt R] {x y : tropical R} :

tropical.untrop x < tropical.untrop y ↔ x < y

@[protected, instance]

def tropical.decidable_lt {R : Type u} [has_lt R] [decidable_rel has_lt.lt] :

decidable_rel has_lt.lt

Equations

tropical.decidable_lt = λ (x y : tropical R), _inst_2 (tropical.untrop x) (tropical.untrop y)

@[protected, instance]

def tropical.preorder {R : Type u} [preorder R] :

preorder (tropical R)

Equations

tropical.preorder = {le := has_le.le tropical.has_le, lt := has_lt.lt tropical.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

def tropical.trop_order_iso {R : Type u} [preorder R] :

R ≃o tropical R

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

Equations

tropical.trop_order_iso = {to_equiv := {to_fun := tropical.trop_equiv.to_fun, inv_fun := tropical.trop_equiv.inv_fun, left_inv := _, right_inv := _}, map_rel_iff' := _}

@[simp]

theorem tropical.trop_order_iso_coe_fn {R : Type u} [preorder R] :

⇑tropical.trop_order_iso = tropical.trop

@[simp]

theorem tropical.trop_order_iso_symm_coe_fn {R : Type u} [preorder R] :

⇑(tropical.trop_order_iso.symm) = tropical.untrop

theorem tropical.trop_monotone {R : Type u} [preorder R] :

monotone tropical.trop

theorem tropical.untrop_monotone {R : Type u} [preorder R] :

monotone tropical.untrop

@[protected, instance]

def tropical.partial_order {R : Type u} [partial_order R] :

partial_order (tropical R)

Equations

tropical.partial_order = {le := preorder.le tropical.preorder, lt := preorder.lt tropical.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

@[protected, instance]

def tropical.has_zero {R : Type u} [has_top R] :

has_zero (tropical R)

Equations

tropical.has_zero = {zero := tropical.trop ⊤}

@[protected, instance]

def tropical.has_top {R : Type u} [has_top R] :

has_top (tropical R)

Equations

tropical.has_top = {top := 0}

@[simp]

theorem tropical.untrop_zero {R : Type u} [has_top R] :

tropical.untrop 0 = ⊤

@[simp]

theorem tropical.trop_top {R : Type u} [has_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} [has_le R] [order_top R] (x : tropical R) :

x ≤ 0

@[protected, instance]

def tropical.order_top {R : Type u} [has_le R] [order_top R] :

order_top (tropical R)

Equations

tropical.order_top = {top := ⊤, le_top := _}

@[protected, instance]

def tropical.has_add {R : Type u} [linear_order R] :

has_add (tropical R)

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

Equations

tropical.has_add = {add := λ (x y : tropical R), tropical.trop (linear_order.min (tropical.untrop x) (tropical.untrop y))}

@[protected, instance]

def tropical.add_comm_semigroup {R : Type u} [linear_order R] :

add_comm_semigroup (tropical R)

Equations

tropical.add_comm_semigroup = {add := has_add.add tropical.has_add, add_assoc := _, add_comm := _}

@[simp]

theorem tropical.untrop_add {R : Type u} [linear_order R] (x y : tropical R) :

tropical.untrop (x + y) = linear_order.min (tropical.untrop x) (tropical.untrop y)

@[simp]

theorem tropical.trop_min {R : Type u} [linear_order R] (x y : R) :

tropical.trop (linear_order.min x y) = tropical.trop x + tropical.trop y

@[simp]

theorem tropical.trop_inf {R : Type u} [linear_order R] (x y : R) :

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

theorem tropical.trop_add_def {R : Type u} [linear_order R] (x y : tropical R) :

x + y = tropical.trop (linear_order.min (tropical.untrop x) (tropical.untrop y))

@[protected, instance]

def tropical.linear_order {R : Type u} [linear_order R] :

linear_order (tropical R)

Equations

tropical.linear_order = {le := partial_order.le tropical.partial_order, lt := partial_order.lt tropical.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := tropical.decidable_le (λ (a b : R), has_le.le.decidable a b), decidable_eq := tropical.decidable_eq (λ (a b : R), eq.decidable a b), decidable_lt := tropical.decidable_lt (λ (a b : R), has_lt.lt.decidable a b), max := λ (a b : tropical R), tropical.trop (linear_order.max (tropical.untrop a) (tropical.untrop b)), max_def := _, min := has_add.add tropical.has_add, min_def := _}

@[simp]

theorem tropical.untrop_sup {R : Type u} [linear_order R] (x y : tropical R) :

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

@[simp]

theorem tropical.untrop_max {R : Type u} [linear_order R] (x y : tropical R) :

tropical.untrop (linear_order.max x y) = linear_order.max (tropical.untrop x) (tropical.untrop y)

@[simp]

theorem tropical.min_eq_add {R : Type u} [linear_order R] :

linear_order.min = has_add.add

@[simp]

theorem tropical.inf_eq_add {R : Type u} [linear_order R] :

has_inf.inf = has_add.add

theorem tropical.trop_max_def {R : Type u} [linear_order R] (x y : tropical R) :

linear_order.max x y = tropical.trop (linear_order.max (tropical.untrop x) (tropical.untrop y))

theorem tropical.trop_sup_def {R : Type u} [linear_order R] (x y : tropical R) :

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

@[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]

def tropical.add_comm_monoid {R : Type u} [linear_order R] [order_top R] :

add_comm_monoid (tropical R)

Equations

tropical.add_comm_monoid = {add := add_comm_semigroup.add tropical.add_comm_semigroup, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default 0 add_comm_semigroup.add tropical.add_comm_monoid._proof_4 tropical.add_comm_monoid._proof_5, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

@[protected, instance]

def tropical.has_mul {R : Type u} [has_add R] :

has_mul (tropical R)

Tropical multiplication is the addition in the underlying R.

Equations

tropical.has_mul = {mul := λ (x y : tropical R), tropical.trop (tropical.untrop x + tropical.untrop y)}

@[simp]

theorem tropical.trop_add {R : Type u} [has_add R] (x y : R) :

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

@[simp]

theorem tropical.untrop_mul {R : Type u} [has_add R] (x y : tropical R) :

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

theorem tropical.trop_mul_def {R : Type u} [has_add R] (x y : tropical R) :

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

@[protected, instance]

def tropical.has_one {R : Type u} [has_zero R] :

has_one (tropical R)

Equations

tropical.has_one = {one := tropical.trop 0}

@[simp]

theorem tropical.trop_zero {R : Type u} [has_zero R] :

tropical.trop 0 = 1

@[simp]

theorem tropical.untrop_one {R : Type u} [has_zero R] :

tropical.untrop 1 = 0

@[protected, instance]

def tropical.add_monoid_with_one {R : Type u} [linear_order R] [order_top R] [has_zero R] :

add_monoid_with_one (tropical R)

Equations

tropical.add_monoid_with_one = {nat_cast := λ (n : ℕ), ite (n = 0) 0 1, add := add_comm_monoid.add tropical.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero tropical.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul tropical.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, one := 1, nat_cast_zero := _, nat_cast_succ := _}

@[protected, instance]

def tropical.nontrivial {R : Type u} [has_zero R] :

nontrivial (tropical (with_top R))

@[protected, instance]

def tropical.has_inv {R : Type u} [has_neg R] :

has_inv (tropical R)

Equations

tropical.has_inv = {inv := λ (x : tropical R), tropical.trop (-tropical.untrop x)}

@[simp]

theorem tropical.untrop_inv {R : Type u} [has_neg R] (x : tropical R) :

tropical.untrop x⁻¹ = -tropical.untrop x

@[protected, instance]

def tropical.has_div {R : Type u} [has_sub R] :

has_div (tropical R)

Equations

tropical.has_div = {div := λ (x y : tropical R), tropical.trop (tropical.untrop x - tropical.untrop y)}

@[simp]

theorem tropical.untrop_div {R : Type u} [has_sub R] (x y : tropical R) :

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

@[protected, instance]

def tropical.semigroup {R : Type u} [add_semigroup R] :

semigroup (tropical R)

Equations

tropical.semigroup = {mul := has_mul.mul tropical.has_mul, mul_assoc := _}

@[protected, instance]

def tropical.comm_semigroup {R : Type u} [add_comm_semigroup R] :

comm_semigroup (tropical R)

Equations

tropical.comm_semigroup = {mul := semigroup.mul tropical.semigroup, mul_assoc := _, mul_comm := _}

@[protected, instance]

def tropical.has_pow {R : Type u} {α : Type u_1} [has_smul α R] :

has_pow (tropical R) α

Equations

tropical.has_pow = {pow := λ (x : tropical R) (n : α), tropical.trop (n • tropical.untrop x)}

@[simp]

theorem tropical.untrop_pow {R : Type u} {α : Type u_1} [has_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} [has_smul α R] (x : R) (n : α) :

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

@[protected, instance]

def tropical.mul_one_class {R : Type u} [add_zero_class R] :

mul_one_class (tropical R)

Equations

tropical.mul_one_class = {one := 1, mul := has_mul.mul tropical.has_mul, one_mul := _, mul_one := _}

@[protected, instance]

def tropical.monoid {R : Type u} [add_monoid R] :

monoid (tropical R)

Equations

tropical.monoid = {mul := mul_one_class.mul tropical.mul_one_class, mul_assoc := _, one := mul_one_class.one tropical.mul_one_class, one_mul := _, mul_one := _, npow := λ (n : ℕ) (x : tropical R), x ^ n, npow_zero' := _, npow_succ' := _}

@[simp]

theorem tropical.trop_nsmul {R : Type u} [add_monoid R] (x : R) (n : ℕ) :

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

@[protected, instance]

def tropical.comm_monoid {R : Type u} [add_comm_monoid R] :

comm_monoid (tropical R)

Equations

tropical.comm_monoid = {mul := monoid.mul tropical.monoid, mul_assoc := _, one := monoid.one tropical.monoid, one_mul := _, mul_one := _, npow := monoid.npow tropical.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}

@[protected, instance]

def tropical.group {R : Type u} [add_group R] :

group (tropical R)

Equations

tropical.group = {mul := monoid.mul tropical.monoid, mul_assoc := _, one := monoid.one tropical.monoid, one_mul := _, mul_one := _, npow := monoid.npow tropical.monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv tropical.has_inv, div := div_inv_monoid.div._default monoid.mul tropical.group._proof_6 monoid.one tropical.group._proof_7 tropical.group._proof_8 monoid.npow tropical.group._proof_9 tropical.group._proof_10 has_inv.inv, div_eq_mul_inv := _, zpow := λ (n : ℤ) (x : tropical R), tropical.trop (n • tropical.untrop x), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}

@[protected, instance]

def tropical.comm_group {R : Type u} [add_comm_group R] :

comm_group (tropical R)

Equations

tropical.comm_group = {mul := group.mul tropical.group, mul_assoc := _, one := group.one tropical.group, one_mul := _, mul_one := _, npow := group.npow tropical.group, npow_zero' := _, npow_succ' := _, inv := group.inv tropical.group, div := group.div tropical.group, div_eq_mul_inv := _, zpow := group.zpow tropical.group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}

@[simp]

theorem tropical.untrop_zpow {R : Type u} [add_group R] (x : tropical R) (n : ℤ) :

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

@[simp]

theorem tropical.trop_zsmul {R : Type u} [add_group R] (x : R) (n : ℤ) :

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

@[protected, instance]

def tropical.covariant_mul {R : Type u} [has_le R] [has_add R] [covariant_class R R has_add.add has_le.le] :

covariant_class (tropical R) (tropical R) has_mul.mul has_le.le

@[protected, instance]

def tropical.covariant_swap_mul {R : Type u} [has_le R] [has_add R] [covariant_class R R (function.swap has_add.add) has_le.le] :

covariant_class (tropical R) (tropical R) (function.swap has_mul.mul) has_le.le

@[protected, instance]

def tropical.covariant_add {R : Type u} [linear_order R] :

covariant_class (tropical R) (tropical R) has_add.add has_le.le

@[protected, instance]

def tropical.covariant_mul_lt {R : Type u} [has_lt R] [has_add R] [covariant_class R R has_add.add has_lt.lt] :

covariant_class (tropical R) (tropical R) has_mul.mul has_lt.lt

@[protected, instance]

def tropical.covariant_swap_mul_lt {R : Type u} [preorder R] [has_add R] [covariant_class R R (function.swap has_add.add) has_lt.lt] :

covariant_class (tropical R) (tropical R) (function.swap has_mul.mul) has_lt.lt

@[protected, instance]

def tropical.distrib {R : Type u} [linear_order R] [has_add R] [covariant_class R R has_add.add has_le.le] [covariant_class R R (function.swap has_add.add) has_le.le] :

distrib (tropical R)

Equations

tropical.distrib = {mul := has_mul.mul tropical.has_mul, add := has_add.add tropical.has_add, left_distrib := _, right_distrib := _}

@[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

@[protected, instance]

def tropical.comm_semiring {R : Type u} [linear_ordered_add_comm_monoid_with_top R] :

comm_semiring (tropical R)

Equations

tropical.comm_semiring = {add := add_monoid_with_one.add tropical.add_monoid_with_one, add_assoc := _, zero := add_monoid_with_one.zero tropical.add_monoid_with_one, zero_add := _, add_zero := _, nsmul := add_monoid_with_one.nsmul tropical.add_monoid_with_one, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := distrib.mul tropical.distrib, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := add_monoid_with_one.one tropical.add_monoid_with_one, one_mul := _, mul_one := _, nat_cast := add_monoid_with_one.nat_cast tropical.add_monoid_with_one, nat_cast_zero := _, nat_cast_succ := _, npow := comm_monoid.npow tropical.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}

@[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

@[protected, instance]

def tropical.no_zero_divisors {R : Type u_1} [linear_ordered_add_comm_monoid R] :

no_zero_divisors (tropical (with_top R))