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 ofR
. If[LinearOrder R]
, then addition onR
is viamin
.Semiring (Tropical R)
: ALinearOrderedAddCommMonoidWithTop R
induces aSemiring (Tropical R)
. If one solely has[LinearOrderedAddCommMonoid R]
, then the "tropicalization ofR
" would beTropical (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
Reinterpret x : R
as an element of Tropical R
.
See Tropical.tropEquiv
for the equivalence.
Equations
- Tropical.trop = id
Instances For
Reinterpret x : Tropical R
as an element of R
.
See Tropical.tropEquiv
for the equivalence.
Equations
- Tropical.untrop = id
Instances For
Reinterpret x : R
as an element of Tropical R
.
See Tropical.tropOrderIso
for the order-preserving equivalence.
Equations
- Tropical.tropEquiv = { toFun := Tropical.trop, invFun := Tropical.untrop, left_inv := ⋯, right_inv := ⋯ }
Instances For
Equations
- Tropical.instInhabited = { default := Tropical.trop default }
Recursing on an 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)
Instances For
Equations
- x✝.instDecidableEq x = decidable_of_iff (Tropical.untrop x✝ = Tropical.untrop x) ⋯
Equations
- Tropical.instLETropical = { le := fun (x y : Tropical R) => Tropical.untrop x ≤ Tropical.untrop y }
Equations
- x.decidableLE y = inst (Tropical.untrop x) (Tropical.untrop y)
Equations
- Tropical.instLTTropical = { lt := fun (x y : Tropical R) => Tropical.untrop x < Tropical.untrop y }
Equations
- x.decidableLT y = inst (Tropical.untrop x) (Tropical.untrop y)
Equations
- Tropical.instPreorderTropical = Preorder.mk ⋯ ⋯ ⋯
Equations
- Tropical.instPartialOrderTropical = PartialOrder.mk ⋯
Equations
- Tropical.instZeroTropical = { zero := Tropical.trop ⊤ }
Equations
- Tropical.instOrderTop = OrderTop.mk ⋯
Tropical addition is the minimum of two underlying elements of R
.
Equations
- Tropical.instAdd = { add := fun (x y : Tropical R) => Tropical.trop (min (Tropical.untrop x) (Tropical.untrop y)) }
Equations
- Tropical.instAddCommSemigroupTropical = AddCommSemigroup.mk ⋯
Equations
- Tropical.instLinearOrderTropical = LinearOrder.mk ⋯ Tropical.decidableLE decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯
Equations
- Tropical.instAddCommMonoidTropical = AddCommMonoid.mk ⋯
Tropical multiplication is the addition in the underlying R
.
Equations
- Tropical.instMulOfAdd = { mul := fun (x y : Tropical R) => Tropical.trop (Tropical.untrop x + Tropical.untrop y) }
Equations
- Tropical.instOneTropical = { one := Tropical.trop 0 }
Equations
- Tropical.instAddMonoidWithOneTropical = AddMonoidWithOne.mk ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- Tropical.instInvOfNeg = { inv := fun (x : Tropical R) => Tropical.trop (-Tropical.untrop x) }
Equations
- Tropical.instDivOfSub = { div := fun (x y : Tropical R) => Tropical.trop (Tropical.untrop x - Tropical.untrop y) }
Equations
- Tropical.instSemigroupTropical = Semigroup.mk ⋯
Equations
- Tropical.instCommSemigroupTropical = CommSemigroup.mk ⋯
Equations
- Tropical.instPowOfSMul = { pow := fun (x : Tropical R) (n : α) => Tropical.trop (n • Tropical.untrop x) }
Equations
- Tropical.instMulOneClassTropical = MulOneClass.mk ⋯ ⋯
Equations
- Tropical.instCommMonoidTropical = CommMonoid.mk ⋯
Equations
- Tropical.instCommGroupOfAddCommGroup = CommGroup.mk ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- Tropical.instDistribTropical = Distrib.mk ⋯ ⋯
Equations
- Tropical.instCommSemiring = CommSemiring.mk ⋯
Equations
- ⋯ = ⋯