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 #

@[irreducible]
def Tropical (R : Type u) :

The tropicalization of a type R.

Equations
Instances For
    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
    Instances For
      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
      Instances For
        @[simp]
        theorem Tropical.trop_inj_iff {R : Type u} (x : R) (y : R) :
        @[simp]
        @[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
        • Tropical.tropEquiv = { toFun := Tropical.trop, invFun := Tropical.untrop, left_inv := , right_inv := }
        Instances For
          @[simp]
          theorem Tropical.tropEquiv_coe_fn {R : Type u} :
          Tropical.tropEquiv = Tropical.trop
          @[simp]
          theorem Tropical.tropEquiv_symm_coe_fn {R : Type u} :
          Tropical.tropEquiv.symm = 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 an x' : Tropical R is the same as recursing on an x : R reinterpreted as a term of Tropical R via trop x.

          Equations
          Instances For
            Equations
            instance Tropical.instLETropical {R : Type u} [LE R] :
            Equations
            @[simp]
            instance Tropical.decidableLE {R : Type u} [LE R] [DecidableRel fun (x1 x2 : R) => x1 x2] :
            DecidableRel fun (x1 x2 : Tropical R) => x1 x2
            Equations
            instance Tropical.instLTTropical {R : Type u} [LT R] :
            Equations
            @[simp]
            theorem Tropical.untrop_lt_iff {R : Type u} [LT R] {x : Tropical R} {y : Tropical R} :
            instance Tropical.decidableLT {R : Type u} [LT R] [DecidableRel fun (x1 x2 : R) => x1 < x2] :
            DecidableRel fun (x1 x2 : Tropical R) => x1 < x2
            Equations
            Equations

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

            Equations
            • Tropical.tropOrderIso = { toEquiv := Tropical.tropEquiv, map_rel_iff' := }
            Instances For
              @[simp]
              theorem Tropical.tropOrderIso_coe_fn {R : Type u} [Preorder R] :
              Tropical.tropOrderIso = Tropical.trop
              @[simp]
              theorem Tropical.tropOrderIso_symm_coe_fn {R : Type u} [Preorder R] :
              Tropical.tropOrderIso.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
              Equations
              instance Tropical.instZeroTropical {R : Type u} [Top R] :
              Equations
              instance Tropical.instTopTropical {R : Type u} [Top R] :
              Equations
              • Tropical.instTopTropical = { top := 0 }
              @[simp]
              @[simp]
              theorem Tropical.trop_top {R : Type u} [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} [LE R] [OrderTop R] (x : Tropical R) :
              x 0
              instance Tropical.instOrderTop {R : Type u} [LE R] [OrderTop R] :
              Equations
              instance Tropical.instAdd {R : Type u} [LinearOrder R] :

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

              Equations
              Equations
              @[simp]
              theorem Tropical.trop_min {R : Type u} [LinearOrder R] (x : R) (y : R) :
              @[simp]
              theorem Tropical.trop_inf {R : Type u} [LinearOrder R] (x : R) (y : R) :
              Equations
              • Tropical.instLinearOrderTropical = LinearOrder.mk Tropical.decidableLE decidableEqOfDecidableLE decidableLTOfDecidableLE
              @[simp]
              theorem Tropical.min_eq_add {R : Type u} [LinearOrder R] :
              min = fun (x1 x2 : Tropical R) => x1 + x2
              @[simp]
              theorem Tropical.inf_eq_add {R : Type u} [LinearOrder R] :
              (fun (x1 x2 : Tropical R) => x1 x2) = fun (x1 x2 : Tropical R) => x1 + x2
              @[simp]
              theorem Tropical.add_eq_left {R : Type u} [LinearOrder R] ⦃x : Tropical R ⦃y : Tropical R (h : x y) :
              x + y = x
              @[simp]
              theorem Tropical.add_eq_right {R : Type u} [LinearOrder R] ⦃x : Tropical R ⦃y : Tropical R (h : y x) :
              x + y = y
              theorem Tropical.add_eq_left_iff {R : Type u} [LinearOrder R] {x : Tropical R} {y : Tropical R} :
              x + y = x x y
              theorem Tropical.add_eq_right_iff {R : Type u} [LinearOrder R] {x : Tropical R} {y : Tropical R} :
              x + y = y y x
              theorem Tropical.add_self {R : Type u} [LinearOrder R] (x : Tropical R) :
              x + x = x
              theorem Tropical.add_eq_iff {R : Type u} [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} [LinearOrder R] {a : Tropical (WithTop R)} {b : Tropical (WithTop R)} :
              a + b = 0 a = 0 b = 0
              Equations
              instance Tropical.instMulOfAdd {R : Type u} [Add R] :

              Tropical multiplication is the addition in the underlying R.

              Equations
              @[simp]
              theorem Tropical.trop_add {R : Type u} [Add R] (x : R) (y : R) :
              @[simp]
              instance Tropical.instOneTropical {R : Type u} [Zero R] :
              Equations
              @[simp]
              theorem Tropical.trop_zero {R : Type u} [Zero R] :
              @[simp]
              theorem Tropical.untrop_one {R : Type u} [Zero R] :
              Equations
              instance Tropical.instInvOfNeg {R : Type u} [Neg R] :
              Equations
              instance Tropical.instDivOfSub {R : Type u} [Sub R] :
              Equations
              @[simp]
              Equations
              Equations
              instance Tropical.instPowOfSMul {R : Type u} {α : Type u_1} [SMul α R] :
              Pow (Tropical R) α
              Equations
              @[simp]
              theorem Tropical.untrop_pow {R : Type u} {α : Type u_1} [SMul α R] (x : Tropical R) (n : α) :
              @[simp]
              theorem Tropical.trop_smul {R : Type u} {α : Type u_1} [SMul α R] (x : R) (n : α) :
              Equations
              Equations
              @[simp]
              theorem Tropical.trop_nsmul {R : Type u} [AddMonoid R] (x : R) (n : ) :
              Equations
              Equations
              Equations
              @[simp]
              theorem Tropical.untrop_zpow {R : Type u} [AddGroup R] (x : Tropical R) (n : ) :
              @[simp]
              theorem Tropical.trop_zsmul {R : Type u} [AddGroup R] (x : R) (n : ) :
              instance Tropical.covariant_mul {R : Type u} [LE R] [Add R] [CovariantClass R R (fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] :
              CovariantClass (Tropical R) (Tropical R) (fun (x1 x2 : Tropical R) => x1 * x2) fun (x1 x2 : Tropical R) => x1 x2
              Equations
              • =
              instance Tropical.covariant_swap_mul {R : Type u} [LE R] [Add R] [CovariantClass R R (Function.swap fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] :
              CovariantClass (Tropical R) (Tropical R) (Function.swap fun (x1 x2 : Tropical R) => x1 * x2) fun (x1 x2 : Tropical R) => x1 x2
              Equations
              • =
              instance Tropical.covariant_add {R : Type u} [LinearOrder R] :
              CovariantClass (Tropical R) (Tropical R) (fun (x1 x2 : Tropical R) => x1 + x2) fun (x1 x2 : Tropical R) => x1 x2
              Equations
              • =
              instance Tropical.covariant_mul_lt {R : Type u} [LT R] [Add R] [CovariantClass R R (fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 < x2] :
              CovariantClass (Tropical R) (Tropical R) (fun (x1 x2 : Tropical R) => x1 * x2) fun (x1 x2 : Tropical R) => x1 < x2
              Equations
              • =
              instance Tropical.covariant_swap_mul_lt {R : Type u} [Preorder R] [Add R] [CovariantClass R R (Function.swap fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 < x2] :
              CovariantClass (Tropical R) (Tropical R) (Function.swap fun (x1 x2 : Tropical R) => x1 * x2) fun (x1 x2 : Tropical R) => x1 < x2
              Equations
              • =
              instance Tropical.instDistribTropical {R : Type u} [LinearOrder R] [Add R] [CovariantClass R R (fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] [CovariantClass R R (Function.swap fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] :
              Equations
              @[simp]
              theorem Tropical.add_pow {R : Type u} [LinearOrder R] [AddMonoid R] [CovariantClass R R (fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] [CovariantClass R R (Function.swap fun (x1 x2 : R) => x1 + x2) fun (x1 x2 : R) => x1 x2] (x : Tropical R) (y : Tropical R) (n : ) :
              (x + y) ^ n = x ^ n + y ^ n
              Equations
              @[simp]
              theorem Tropical.succ_nsmul {R : Type u_1} [LinearOrder R] [OrderTop R] (x : Tropical R) (n : ) :
              (n + 1) x = x
              theorem Tropical.mul_eq_zero_iff {R : Type u_1} [LinearOrderedAddCommMonoid R] {a : Tropical (WithTop R)} {b : Tropical (WithTop R)} :
              a * b = 0 a = 0 b = 0