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.

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.

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

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

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.

@[simp]

theorem LinearOrderedAddCommGroupWithTop.neg_top {α : Type u_2} [self : LinearOrderedAddCommGroupWithTop α] : -⊤ = ⊤

theorem LinearOrderedAddCommGroupWithTop.add_neg_cancel {α : Type u_2} [self : LinearOrderedAddCommGroupWithTop α] (a : α) : a ≠ ⊤ → a + -a = 0

instance WithTop.linearOrderedAddCommMonoidWithTop {α : Type u_1} [LinearOrderedAddCommMonoid α] : LinearOrderedAddCommMonoidWithTop (WithTop α)

Equations

• WithTop.linearOrderedAddCommMonoidWithTop = LinearOrderedAddCommMonoidWithTop.mk ⋯

@[simp]

theorem top_add {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (a : α) : ⊤ + a = ⊤

@[simp]

theorem add_top {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (a : α) : a + ⊤ = ⊤

instance WithTop.LinearOrderedAddCommGroup.instNeg {α : Type u_1} [LinearOrderedAddCommGroup α] : Neg (WithTop α)

Equations

• WithTop.LinearOrderedAddCommGroup.instNeg = { neg := Option.map fun (a : α) => -a }

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

• WithTop.LinearOrderedAddCommGroup.sub x none = ⊤
• WithTop.LinearOrderedAddCommGroup.sub none (some x_2) = ⊤
• WithTop.LinearOrderedAddCommGroup.sub (some x_2) (some y) = ↑(x_2 - y)

instance WithTop.LinearOrderedAddCommGroup.instSub {α : Type u_1} [LinearOrderedAddCommGroup α] : Sub (WithTop α)

Equations

• WithTop.LinearOrderedAddCommGroup.instSub = { sub := WithTop.LinearOrderedAddCommGroup.sub }

@[simp]

theorem WithTop.LinearOrderedAddCommGroup.coe_neg {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) : ↑(-a) = -↑a

@[simp]

theorem WithTop.LinearOrderedAddCommGroup.neg_top {α : Type u_1} [LinearOrderedAddCommGroup α] : -⊤ = ⊤

@[simp]

theorem WithTop.LinearOrderedAddCommGroup.coe_sub {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} : ↑(a - b) = ↑a - ↑b

@[simp]

theorem WithTop.LinearOrderedAddCommGroup.top_sub {α : Type u_1} [LinearOrderedAddCommGroup α] {a : WithTop α} : ⊤ - a = ⊤

@[simp]

theorem WithTop.LinearOrderedAddCommGroup.sub_top {α : Type u_1} [LinearOrderedAddCommGroup α] {a : WithTop α} : a - ⊤ = ⊤

@[simp]

theorem WithTop.LinearOrderedAddCommGroup.sub_eq_top_iff {α : Type u_1} [LinearOrderedAddCommGroup α] {a : WithTop α} {b : WithTop α} : a - b = ⊤ ↔ a = ⊤ ∨ b = ⊤

instance WithTop.LinearOrderedAddCommGroup.instLinearOrderedAddCommGroupWithTop {α : Type u_1} [LinearOrderedAddCommGroup α] : LinearOrderedAddCommGroupWithTop (WithTop α)

Equations

• WithTop.LinearOrderedAddCommGroup.instLinearOrderedAddCommGroupWithTop = LinearOrderedAddCommGroupWithTop.mk ⋯ zsmulRec ⋯ ⋯ ⋯ ⋯ ⋯

theorem LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a : α} (h : a ≠ ⊤) : a + -a = 0

@[simp]

theorem LinearOrderedAddCommGroupWithTop.add_eq_top {α : Type u_1} [LinearOrderedAddCommGroupWithTop α] {a : α} {b : α} : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

@[simp]

theorem LinearOrderedAddCommGroupWithTop.top_ne_zero {α : Type u_1} [LinearOrderedAddCommGroupWithTop α] : ⊤ ≠ 0

@[simp]

theorem LinearOrderedAddCommGroupWithTop.neg_eq_top {α : Type u_1} [LinearOrderedAddCommGroupWithTop α] {a : α} : -a = ⊤ ↔ a = ⊤

@[instance 100]

instance LinearOrderedAddCommGroupWithTop.toSubtractionMonoid {α : Type u_1} [LinearOrderedAddCommGroupWithTop α] : SubtractionMonoid α

Equations

• LinearOrderedAddCommGroupWithTop.toSubtractionMonoid = SubtractionMonoid.mk ⋯ ⋯ ⋯