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 : α), min a b = if a ≤ b then a else b
• max_def : ∀ (a b : α), max 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.

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 , Neg , Sub , 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 : α), min a b = if a ≤ b then a else b
• max_def : ∀ (a b : α), max 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 : ℤ → α → α

  Multiplication by an integer. Set this to zsmulRec unless Module diamonds are possible.

• 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

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 ⋯ ⋯ ⋯ ⋯ ⋯