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 α : Type u_2

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

• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b
• top : α
• le_top (a : α) : a ≤ ⊤
• top_add' (x : α) : ⊤ + x = ⊤

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

class LinearOrderedAddCommGroupWithTop (α : Type u_2) extends LinearOrderedAddCommMonoidWithTop α, SubNegMonoid α, Nontrivial α : Type u_2

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

• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b
• top : α
• le_top (a : α) : a ≤ ⊤
• top_add' (x : α) : ⊤ + x = ⊤
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : LinearOrderedAddCommGroupWithTop.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : LinearOrderedAddCommGroupWithTop.zsmul (↑n.succ) a = LinearOrderedAddCommGroupWithTop.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : LinearOrderedAddCommGroupWithTop.zsmul (Int.negSucc n) a = -LinearOrderedAddCommGroupWithTop.zsmul (↑n.succ) a
• exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
• neg_top : -⊤ = ⊤
• add_neg_cancel (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 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 ⋯ ⋯ ⋯

theorem LinearOrderedAddCommGroupWithTop.injective_add_left_of_ne_top {α : Type u_1} [LinearOrderedAddCommGroupWithTop α] (b : α) (h : b ≠ ⊤) : Function.Injective fun (x : α) => x + b

theorem LinearOrderedAddCommGroupWithTop.injective_add_right_of_ne_top {α : Type u_1} [LinearOrderedAddCommGroupWithTop α] (b : α) (h : b ≠ ⊤) : Function.Injective fun (x : α) => b + x

theorem LinearOrderedAddCommGroupWithTop.strictMono_add_left_of_ne_top {α : Type u_1} [LinearOrderedAddCommGroupWithTop α] (b : α) (h : b ≠ ⊤) : StrictMono fun (x : α) => x + b

theorem LinearOrderedAddCommGroupWithTop.strictMono_add_right_of_ne_top {α : Type u_1} [LinearOrderedAddCommGroupWithTop α] (b : α) (h : b ≠ ⊤) : StrictMono fun (x : α) => b + x

theorem LinearOrderedAddCommGroupWithTop.sub_pos {α : Type u_1} [LinearOrderedAddCommGroupWithTop α] (a b : α) : 0 < a - b ↔ b < a ∨ b = ⊤