Ordered AddTorsors

This file defines ordered vector addition and proves some properties. A motivating example is given by the additive action of ℤ on subsets of reals that are closed under integer translation. The order compatibility allows for a treatment of the R((z))-module structure on (z ^ s) V((z)) for an R-module V, using the formalism of Hahn series.

Implementation notes

We write our conditions as Prop-valued mixins.

Definitions

• OrderedVAdd : inequalities are preserved by translation.
• CancelVAdd : the vector addition version of cancellative addition
• OrderedCancelVAdd : inequalities are preserved and reflected by translation.

Instances

• OrderedAddCommMonoid.toOrderedVAdd
• OrderedVAdd.toCovariantClassLeft
• OrderedCancelVAdd.toCancelVAdd
• OrderedCancelAddCommMonoid.toOrderedCancelVAdd
• OrderedCancelVAdd.toContravariantClassLeft

TODO

• OrderedAddTorsor : An additive torsor over an additive commutative group with compatible order.
• Set.vAddAntidiagonal
• (lex) prod instances
• Pi instances
• vAddAntidiagonal.finite_of_isPWO
• Finset.vAddAntidiagonal

class OrderedVAdd (G : Type u_3) (P : Type u_4) [LE G] [LE P] [VAdd G P] : Prop

An ordered vector addition is a bi-monotone vector addition.

• vadd_le_vadd_left : ∀ (a b : P), a ≤ b → ∀ (c : G), c +ᵥ a ≤ c +ᵥ b
• vadd_le_vadd_right : ∀ (c d : G), c ≤ d → ∀ (a : P), c +ᵥ a ≤ d +ᵥ a

theorem OrderedVAdd.vadd_le_vadd_left {G : Type u_3} {P : Type u_4} [LE G] [LE P] [VAdd G P] [self : OrderedVAdd G P] (a : P) (b : P) : a ≤ b → ∀ (c : G), c +ᵥ a ≤ c +ᵥ b

theorem OrderedVAdd.vadd_le_vadd_right {G : Type u_3} {P : Type u_4} [LE G] [LE P] [VAdd G P] [self : OrderedVAdd G P] (c : G) (d : G) : c ≤ d → ∀ (a : P), c +ᵥ a ≤ d +ᵥ a

instance OrderedAddCommMonoid.toOrderedVAdd {G : Type u_1} [OrderedAddCommMonoid G] : OrderedVAdd G G

Equations

• ⋯ = ⋯

instance OrderedVAdd.toCovariantClassLeft {G : Type u_1} {P : Type u_2} [LE G] [LE P] [VAdd G P] [OrderedVAdd G P] : CovariantClass G P (fun (x : G) (x_1 : P) => x +ᵥ x_1) fun (x x_1 : P) => x ≤ x_1

Equations

• ⋯ = ⋯

class CancelVAdd (G : Type u_3) (P : Type u_4) [LE G] [LE P] [VAdd G P] : Prop

A vector addition is cancellative if it is pointwise injective on the left and right.

• left_cancel : ∀ (a : G) (b c : P), a +ᵥ b = a +ᵥ c → b = c
• right_cancel : ∀ (a b : G) (c : P), a +ᵥ c = b +ᵥ c → a = b

theorem CancelVAdd.left_cancel {G : Type u_3} {P : Type u_4} [LE G] [LE P] [VAdd G P] [self : CancelVAdd G P] (a : G) (b : P) (c : P) : a +ᵥ b = a +ᵥ c → b = c

theorem CancelVAdd.right_cancel {G : Type u_3} {P : Type u_4} [LE G] [LE P] [VAdd G P] [self : CancelVAdd G P] (a : G) (b : G) (c : P) : a +ᵥ c = b +ᵥ c → a = b

class OrderedCancelVAdd (G : Type u_3) (P : Type u_4) [LE G] [LE P] [VAdd G P] extends OrderedVAdd : Prop

An ordered cancellative vector addition is an ordered vector addition that is cancellative.

• vadd_le_vadd_left : ∀ (a b : P), a ≤ b → ∀ (c : G), c +ᵥ a ≤ c +ᵥ b
• vadd_le_vadd_right : ∀ (c d : G), c ≤ d → ∀ (a : P), c +ᵥ a ≤ d +ᵥ a
• le_of_vadd_le_vadd_left : ∀ (a : G) (b c : P), a +ᵥ b ≤ a +ᵥ c → b ≤ c
• le_of_vadd_le_vadd_right : ∀ (a b : G) (c : P), a +ᵥ c ≤ b +ᵥ c → a ≤ b

theorem OrderedCancelVAdd.le_of_vadd_le_vadd_left {G : Type u_3} {P : Type u_4} [LE G] [LE P] [VAdd G P] [self : OrderedCancelVAdd G P] (a : G) (b : P) (c : P) : a +ᵥ b ≤ a +ᵥ c → b ≤ c

theorem OrderedCancelVAdd.le_of_vadd_le_vadd_right {G : Type u_3} {P : Type u_4} [LE G] [LE P] [VAdd G P] [self : OrderedCancelVAdd G P] (a : G) (b : G) (c : P) : a +ᵥ c ≤ b +ᵥ c → a ≤ b

instance OrderedCancelVAdd.toCancelVAdd {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [VAdd G P] [OrderedCancelVAdd G P] : CancelVAdd G P

Equations

• ⋯ = ⋯

instance OrderedCancelAddCommMonoid.toOrderedCancelVAdd {G : Type u_1} [OrderedCancelAddCommMonoid G] : OrderedCancelVAdd G G

Equations

• ⋯ = ⋯

theorem VAdd.vadd_lt_vadd_of_le_of_lt {G : Type u_1} {P : Type u_2} [LE G] [Preorder P] [VAdd G P] [OrderedCancelVAdd G P] {a : G} {b : G} {c : P} {d : P} (h₁ : a ≤ b) (h₂ : c < d) : a +ᵥ c < b +ᵥ d

theorem VAdd.vadd_lt_vadd_of_lt_of_le {G : Type u_1} {P : Type u_2} [Preorder G] [Preorder P] [VAdd G P] [OrderedCancelVAdd G P] {a : G} {b : G} {c : P} {d : P} (h₁ : a < b) (h₂ : c ≤ d) : a +ᵥ c < b +ᵥ d

@[instance 200]

instance OrderedCancelVAdd.toContravariantClassLeLeft {G : Type u_1} {P : Type u_2} [LE G] [LE P] [VAdd G P] [OrderedCancelVAdd G P] : ContravariantClass G P (fun (x : G) (x_1 : P) => x +ᵥ x_1) fun (x x_1 : P) => x ≤ x_1

Equations

• ⋯ = ⋯