refactor(algebra.abs): Introduce has_pos_part and has_neg_part cl…

…asses (#10420)

refactor(algebra.abs): Introduce `has_pos_part` and `has_neg_part` classes

src/algebra/abs.lean

@@ -10,9 +10,19 @@ Authors: Christopher Hoskin
 This file defines a notational class `has_abs` which adds the unary operator `abs` and the notation
 `|.|`. The concept of an absolute value occurs in lattice ordered groups and in GL and GM spaces.
 
+Mathematical structures possessing an absolute value often also possess a unique decomposition of
+elements into "positive" and "negative" parts which are in some sense "disjoint" (e.g. the Jordan
+decomposition of a measure). This file also defines `has_pos_part` and `has_neg_part` classes
+which add unary operators `pos` and `neg`, representing the maps taking an element to its positive
+and negative part respectively along with the notation ⁺ and ⁻.
+
 ## Notations
 
-The notation `|.|` is introduced for the absolute value.
+The following notation is introduced:
+
+* `|.|` for the absolute value;
+* `.⁺` for the positive part;
+* `.⁻` for the negative part.
 
 ## Tags
 
@@ -26,4 +36,16 @@ Absolute value is a unary operator with properties similar to the absolute value
 class has_abs (α : Type*) := (abs : α → α)
 export has_abs (abs)
 
+/--
+The positive part of an element admiting a decomposition into positive and negative parts.
+-/
+class has_pos_part (α : Type*) := (pos : α → α)
+
+/--
+The negative part of an element admiting a decomposition into positive and negative parts.
+-/
+class has_neg_part (α : Type*) := (neg : α → α)
+
 notation `|`a`|` := abs a
+postfix `⁺`:1000 := has_pos_part.pos
+postfix `⁻`:1000 := has_neg_part.neg

src/algebra/lattice_ordered_group.lean

@@ -125,26 +125,35 @@ calc a⊓b * (a ⊔ b) = a ⊓ b * ((a * b) * (b⁻¹ ⊔ a⁻¹)) :
 
 namespace lattice_ordered_comm_group
 
--- Bourbaki A.VI.12 Definition 4
 /--
+Let `α` be a lattice ordered commutative group with identity `1`. For an element `a` of type `α`,
+the element `a ⊔ 1` is said to be the *positive component* of `a`, denoted `a⁺`.
+-/
+@[to_additive /-"
 Let `α` be a lattice ordered commutative group with identity `0`. For an element `a` of type `α`,
 the element `a ⊔ 0` is said to be the *positive component* of `a`, denoted `a⁺`.
--/
-@[to_additive pos
-  "Let `α` be a lattice ordered commutative group with identity `0`. For an element `a` of type `α`,
-  the element `a ⊔ 0` is said to be the *positive component* of `a`, denoted `a⁺`."]
-def mpos (a : α) : α :=  a ⊔ 1
-postfix `⁺`:1000 := mpos
+"-/,
+priority 100
+] -- see Note [lower instance priority]
+instance has_one_lattice_has_pos_part : has_pos_part (α)  := ⟨λa, a ⊔ 1⟩
+
+@[to_additive pos_part_def]
+lemma m_pos_part_def (a : α) : a⁺ = a ⊔ 1 := rfl
 
 /--
+Let `α` be a lattice ordered commutative group with identity `1`. For an element `a` of type `α`,
+the element `(-a) ⊔ 1` is said to be the *negative component* of `a`, denoted `a⁻`.
+-/
+@[to_additive /-"
 Let `α` be a lattice ordered commutative group with identity `0`. For an element `a` of type `α`,
 the element `(-a) ⊔ 0` is said to be the *negative component* of `a`, denoted `a⁻`.
--/
-@[to_additive neg
-  "Let `α` be a lattice ordered commutative group with identity `0`. For an element `a` of type `α`,
-  the element `(-a) ⊔ 0` is said to be the *negative component* of `a`, denoted `a⁻`."]
-def mneg (a : α) : α := a⁻¹ ⊔ 1
-postfix `⁻`:1000 := mneg
+"-/,
+priority 100
+] -- see Note [lower instance priority]
+instance has_one_lattice_has_neg_part : has_neg_part (α)  := ⟨λa, a⁻¹ ⊔ 1⟩
+
+@[to_additive neg_part_def]
+lemma m_neg_part_def (a : α) : a⁻ = a⁻¹ ⊔ 1 := rfl
 
 /--
 Let `α` be a lattice ordered commutative group and let `a` be an element in `α` with absolute value
@@ -194,9 +203,9 @@ lemma m_le_neg (a : α) : a⁻¹ ≤ a⁻ := le_sup_left
 /--
 Let `α` be a lattice ordered commutative group and let `a` be an element in `α`. Then the negative
 component `a⁻` of `a` is equal to the positive component `(-a)⁺` of `-a`.
--/
+"-/
 @[to_additive]
-lemma neg_eq_pos_inv (a : α) : a⁻ = (a⁻¹)⁺ := by { unfold mneg, unfold mpos}
+lemma neg_eq_pos_inv (a : α) : a⁻ = (a⁻¹)⁺ := by rw [ m_neg_part_def, m_pos_part_def]
 
 /--
 Let `α` be a lattice ordered commutative group and let `a` be an element in `α`. Then the positive
@@ -228,10 +237,7 @@ $$a⁻ = -(a ⊓ 0).$$
 -/
 @[to_additive]
 lemma neg_eq_inv_inf_one [covariant_class α α (*) (≤)] (a : α) : a⁻ = (a ⊓ 1)⁻¹ :=
-begin
-  unfold lattice_ordered_comm_group.mneg,
-  rw [← inv_inj, inv_sup_eq_inv_inf_inv, inv_inv, inv_inv, one_inv],
-end
+by rw [m_neg_part_def, ← inv_inj, inv_sup_eq_inv_inf_inv, inv_inv, inv_inv, one_inv]
 
 -- Bourbaki A.VI.12  Prop 9 a)
 /--
@@ -244,9 +250,7 @@ lemma pos_inv_neg [covariant_class α α (*) (≤)] (a : α) : a = a⁺ / a⁻ :
 begin
   rw div_eq_mul_inv,
   apply eq_mul_inv_of_mul_eq,
-  unfold lattice_ordered_comm_group.mneg,
-  rw [mul_sup_eq_mul_sup_mul, mul_one, mul_right_inv, sup_comm],
-  unfold lattice_ordered_comm_group.mpos,
+  rw [m_neg_part_def, mul_sup_eq_mul_sup_mul, mul_one, mul_right_inv, sup_comm, m_pos_part_def],
 end
 
 -- Hack to work around rewrite not working if lhs is a variable
@@ -467,7 +471,7 @@ equal to its positive component `a⁺`.
 @[to_additive pos_pos_id]
 lemma m_pos_pos_id (a : α) (h : 1 ≤ a): a⁺ = a :=
 begin
-  unfold lattice_ordered_comm_group.mpos,
+  rw m_pos_part_def,
   apply sup_of_le_left h,
 end