Documentation

Mathlib.Algebra.Order.AddGroupWithTop

Linearly ordered commutative additive groups and monoids with a top element adjoined #

This file sets up a special class of linearly ordered commutative additive monoids that show up as the target of so-called “valuations” in algebraic number theory.

Usually, in the informal literature, these objects are constructed by taking a linearly ordered commutative additive group Γ and formally adjoining a top element: Γ ∪ {⊤}.

The disadvantage is that a type such as ENNReal is not of that form, whereas it is a very common target for valuations. The solutions is to use a typeclass, and that is exactly what we do in this file.

source
class LinearOrderedAddCommMonoidWithTop (α : Type u_2) extends LinearOrderedAddCommMonoid , OrderTop , OrderedAddCommMonoid , LinearOrder , AddCommMonoid , PartialOrder , AddMonoid , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add , Min , Max , Ord , Preorder , LE , LT , Top :
Type u_2

A linearly ordered commutative monoid with an additively absorbing ⊤ element. Instances should include number systems with an infinite element adjoined.

    Instances
      source
      theorem LinearOrderedAddCommMonoidWithTop.top_add' {α : Type u_2} [self : LinearOrderedAddCommMonoidWithTop α] (x : α) :
      ⊤ + x = ⊤

      In a LinearOrderedAddCommMonoidWithTop, the ⊤ element is invariant under addition.

      source
      class LinearOrderedAddCommGroupWithTop (α : Type u_2) extends LinearOrderedAddCommMonoidWithTop , SubNegMonoid , Nontrivial , LinearOrderedAddCommMonoid , OrderTop , OrderedAddCommMonoid , LinearOrder , AddCommMonoid , PartialOrder , AddMonoid , AddCommSemigroup , Neg , Sub , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add , Min , Max , Ord , Preorder , LE , LT , Top :
      Type u_2

      A linearly ordered commutative group with an additively absorbing ⊤ element. Instances should include number systems with an infinite element adjoined.

        Instances
          source
          theorem LinearOrderedAddCommGroupWithTop.neg_top {α : Type u_2} [self : LinearOrderedAddCommGroupWithTop α] :
          -⊤ = ⊤
          source
          theorem LinearOrderedAddCommGroupWithTop.add_neg_cancel {α : Type u_2} [self : LinearOrderedAddCommGroupWithTop α] (a : α) :
          a ≠ ⊤ → a + -a = 0
          source
          instance WithTop.linearOrderedAddCommMonoidWithTop {α : Type u_1} [LinearOrderedAddCommMonoid α] :
          LinearOrderedAddCommMonoidWithTop (WithTop α)
          Equations
          source
          @[simp]
          theorem top_add {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (a : α) :
          ⊤ + a = ⊤
          source
          @[simp]
          theorem add_top {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (a : α) :
          a + ⊤ = ⊤
          source
          instance WithTop.LinearOrderedAddCommGroup.instNeg {α : Type u_1} [LinearOrderedAddCommGroup α] :
          Neg (WithTop α)
          Equations
          • WithTop.LinearOrderedAddCommGroup.instNeg = { neg := Option.map fun (a : α) => -a }
          source
          def WithTop.LinearOrderedAddCommGroup.sub {α : Type u_1} [LinearOrderedAddCommGroup α] :
          WithTop α → WithTop α → WithTop α

          If α has subtraction, we can extend the subtraction to WithTop α, by setting x - ⊤ = ⊤ and ⊤ - x = ⊤. This definition is only registered as an instance on linearly ordered additive commutative groups, to avoid conflicting with the instance WithTop.instSub on types with a bottom element.

          Equations
          Instances For
            source
            instance WithTop.LinearOrderedAddCommGroup.instSub {α : Type u_1} [LinearOrderedAddCommGroup α] :
            Sub (WithTop α)
            Equations
            • WithTop.LinearOrderedAddCommGroup.instSub = { sub := WithTop.LinearOrderedAddCommGroup.sub }
            source
            @[simp]
            theorem WithTop.LinearOrderedAddCommGroup.coe_neg {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) :
            ↑(-a) = -↑a
            source
            @[simp]
            theorem WithTop.LinearOrderedAddCommGroup.neg_top {α : Type u_1} [LinearOrderedAddCommGroup α] :
            -⊤ = ⊤
            source
            @[simp]
            theorem WithTop.LinearOrderedAddCommGroup.coe_sub {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} :
            ↑(a - b) = ↑a - ↑b
            source
            @[simp]
            theorem WithTop.LinearOrderedAddCommGroup.top_sub {α : Type u_1} [LinearOrderedAddCommGroup α] {a : WithTop α} :
            ⊤ - a = ⊤
            source
            @[simp]
            theorem WithTop.LinearOrderedAddCommGroup.sub_top {α : Type u_1} [LinearOrderedAddCommGroup α] {a : WithTop α} :
            a - ⊤ = ⊤
            source
            @[simp]
            theorem WithTop.LinearOrderedAddCommGroup.sub_eq_top_iff {α : Type u_1} [LinearOrderedAddCommGroup α] {a : WithTop α} {b : WithTop α} :
            a - b = ⊤ ↔ a = ⊤ ∨ b = ⊤
            source
            instance WithTop.LinearOrderedAddCommGroup.instLinearOrderedAddCommGroupWithTop {α : Type u_1} [LinearOrderedAddCommGroup α] :
            LinearOrderedAddCommGroupWithTop (WithTop α)
            Equations