more instances

src/order/filter/filter_product.lean

@@ -2,10 +2,12 @@
 Copyright (c) 2019 Abhimanyu Pallavi Sudhir. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abhimanyu Pallavi Sudhir
-"Filterproducts" (ultraproducts on general filters), ultraproducts.
+"Filterproducts" (ultraproducts on general filters), ultraproducts and 
+the construction of the hyperreals.
 -/
 
 import order.filter.basic
+import .misc_dependencies
 
 universes u v
 variables {α : Type u} (β : Type v) (φ : filter α)
@@ -15,7 +17,7 @@ namespace filter
 
 /-- Two sequences are bigly equal iff the kernel of their difference is in φ -/
 def bigly_equal : setoid (α → β) := 
-⟨ λ a b, {n | a n = b n} ∈ φ,
+⟨ λ a b, {n | a n = b n} ∈ φ.sets,
   λ a, by simp only [eq_self_iff_true, (set.univ_def).symm, univ_sets], 
   λ a b ab, by simpa only [eq_comm], 
   λ a b c ab bc, sets_of_superset φ (inter_sets φ ab bc) (λ n r, eq.trans r.1 r.2)⟩
@@ -35,24 +37,24 @@ def of (b : β): β* := of_seq (function.const α b)
 
 /-- Lift function to filter product -/
 def lift (f : β → β) : β* → β* :=
-λ x, quotient.lift_on' x (λ a, (of_seq $ λ n, f (a n) : β*)) $
+  λ x, quotient.lift_on' x (λ a, (of_seq $ λ n, f (a n) : β*)) $
   λ a b h, quotient.sound' $ show _ ∈ _, by filter_upwards [h] λ i hi, congr_arg _ hi
 
 /-- Lift binary operation to filter product -/
 def lift₂ (f : β → β → β) : β* → β* → β* :=
-λ x y, quotient.lift_on₂' x y (λ a b, (of_seq $ λ n, f (a n) (b n) : β*)) $
+  λ x y, quotient.lift_on₂' x y (λ a b, (of_seq $ λ n, f (a n) (b n) : β*)) $
   λ a₁ a₂ b₁ b₂ h1 h2, quotient.sound' $ show _ ∈ _,
   by filter_upwards [h1, h2] λ i hi1 hi2, congr (congr_arg _ hi1) hi2
 
 /-- Lift properties to filter product -/
 def lift_rel (R : β → Prop) : β* → Prop :=
-λ x, quotient.lift_on' x (λ a, {i : α | R (a i)} ∈ φ) $ λ a b h, propext 
+  λ x, quotient.lift_on' x (λ a, {i : α | R (a i)} ∈ φ.sets) $ λ a b h, propext 
   ⟨ λ ha, by filter_upwards [h, ha] λ i hi hia, by simpa [hi.symm],
     λ hb, by filter_upwards [h, hb] λ i hi hib, by simpa [hi.symm.symm] ⟩
 
 /-- Lift binary relations to filter product -/
 def lift_rel₂ (R : β → β → Prop) : β* → β* → Prop :=
-λ x y, quotient.lift_on₂' x y (λ a b, {i : α | R (a i) (b i)} ∈ φ) $
+  λ x y, quotient.lift_on₂' x y (λ a b, {i : α | R (a i) (b i)} ∈ φ.sets) $
   λ a₁ a₂ b₁ b₂ h₁ h₂, propext 
   ⟨ λ ha, by filter_upwards [h₁, h₂, ha] λ i hi1 hi2 hia, by simpa [hi1.symm, hi2.symm],
     λ hb, by filter_upwards [h₁, h₂, hb] λ i hi1 hi2 hib, by simpa [hi1.symm.symm, hi2.symm.symm] ⟩
@@ -63,14 +65,25 @@ instance [has_add β] : has_add β* := { add := lift₂ has_add.add }
 
 instance [has_zero β] : has_zero β* := { zero := of 0 }
 
-instance [has_neg β] : has_neg β* :=
-{ neg := lift has_neg.neg }
+instance [has_neg β] : has_neg β* := { neg := lift has_neg.neg }
 
 instance [add_semigroup β] : add_semigroup β* :=
 { add_assoc := λ x y z, quotient.induction_on₃' x y z $ λ a b c, quotient.sound' $
-    show {n | _ + _ + _ = _ + (_ + _)} ∈ _, by simp only [add_assoc, eq_self_iff_true]; exact φ.univ_sets, 
+    show {n | _+_+_ = _+(_+_)} ∈ _, by simp only [add_assoc, eq_self_iff_true]; exact φ.2, 
   ..filter_product.has_add }
 
+instance [add_left_cancel_semigroup β] : add_left_cancel_semigroup β* :=
+{ add_left_cancel := λ x y z, quotient.induction_on₃' x y z $ λ a b c h,
+    have h' : _ := quotient.exact' h, quotient.sound' $ 
+    by filter_upwards [h'] λ i, add_left_cancel,
+  ..filter_product.add_semigroup }
+
+instance [add_right_cancel_semigroup β] : add_right_cancel_semigroup β* :=
+{ add_right_cancel := λ x y z, quotient.induction_on₃' x y z $ λ a b c h,
+    have h' : _ := quotient.exact' h, quotient.sound' $ 
+    by filter_upwards [h'] λ i, add_right_cancel,
+  ..filter_product.add_semigroup }
+
 instance [add_monoid β] : add_monoid β* :=
 { zero_add := λ x, quotient.induction_on' x 
     (λ a, quotient.sound'(by simp only [zero_add]; apply (setoid.iseqv _).1)),
@@ -98,17 +111,15 @@ instance [add_comm_group β] : add_comm_group β* :=
 { ..filter_product.add_comm_monoid, 
   ..filter_product.add_group }
 
-instance [has_mul β] : has_mul β* :=
-{ mul := lift₂ has_mul.mul }
+instance [has_mul β] : has_mul β* := { mul := lift₂ has_mul.mul }
 
 instance [has_one β] : has_one β* := { one := of 1 }
 
-instance [has_inv β] : has_inv β* :=
-{ inv := lift has_inv.inv }
+instance [has_inv β] : has_inv β* := { inv := lift has_inv.inv }
 
 instance [semigroup β] : semigroup β* :=
 { mul_assoc := λ x y z, quotient.induction_on₃' x y z $ λ a b c, quotient.sound' $
-    show {n | _ * _ * _ = _ * (_ * _)} ∈ _, by simp only [mul_assoc, eq_self_iff_true]; exact φ.2, 
+    show {n | _*_*_ = _*(_*_)} ∈ _, by simp only [mul_assoc, eq_self_iff_true]; exact φ.2, 
   ..filter_product.has_mul }
 
 instance [monoid β] : monoid β* :=
@@ -214,8 +225,8 @@ instance [preorder β] : preorder β* :=
 { le_refl := λ x, quotient.induction_on' x $ λ a, show _ ∈ _, 
     by simp only [le_refl, (set.univ_def).symm, univ_sets],
   le_trans := λ x y z, quotient.induction_on₃' x y z $ λ a b c hab hbc, 
-    by filter_upwards [hab, hbc] λ i hiab hibc, le_trans hiab hibc, 
-  ..filter_product.has_le }
+    by filter_upwards [hab, hbc] λ i, le_trans, 
+  ..filter_product.has_le}
 
 instance [partial_order β] : partial_order β* :=
 { le_antisymm := λ x y, quotient.induction_on₂' x y $ λ a b hab hba, quotient.sound' $ 
@@ -239,11 +250,11 @@ begin
   exact NT rs
 end
 
-theorem of_seq_fun (f g : α → β) (h : β → β) (H : {n : α | f n = h (g n) } ∈ φ) : 
-  of_seq f = (lift h) (@of_seq _ _ φ g) := quotient.sound' H
+theorem of_seq_fun (f g : α → β) (h : β → β) (H : {n : α | f n = h (g n) } ∈ φ.sets) : 
+of_seq f = (lift h) (@of_seq _ _ φ g) := quotient.sound' H
 
-theorem of_seq_fun₂ (f g₁ g₂ : α → β) (h : β → β → β) (H : {n : α | f n = h (g₁ n) (g₂ n) } ∈ φ) : 
-  of_seq f = (lift₂ h) (@of_seq _ _ φ g₁) (@of_seq _ _ φ g₂) := quotient.sound' H
+theorem of_seq_fun₂ (f g₁ g₂ : α → β) (h : β → β → β) (H : {n : α | f n = h (g₁ n) (g₂ n) } ∈ φ.sets) : 
+of_seq f = (lift₂ h) (@of_seq _ _ φ g₁) (@of_seq _ _ φ g₂) := quotient.sound' H
 
 @[simp] lemma of_seq_zero [has_zero β] (f : α → β) : of_seq 0 = (0 : β*) := rfl
 
@@ -261,13 +272,17 @@ lemma of_eq_coe (x : β) : of x = (↑x : β*) := rfl
 
 @[simp] lemma of_id (x : β) : of x = (x : β*) := rfl
 
-lemma of_eq (x y : β) (NT : φ ≠ ⊥) : x = y ↔ of x = (of y : β*) := ⟨λ h, by rw h, by apply of_inj NT⟩
+lemma of_eq (x y : β) (NT : φ ≠ ⊥) : x = y ↔ of x = (of y : β*) := 
+⟨λ h, by rw h, by apply of_inj NT⟩
 
-lemma of_ne (x y : β) (NT : φ ≠ ⊥) : x ≠ y ↔ of x ≠ (of y : β*) := by show ¬ x = y ↔ of x ≠ of y; rwa [of_eq]
+lemma of_ne (x y : β) (NT : φ ≠ ⊥) : x ≠ y ↔ of x ≠ (of y : β*) := 
+by show ¬ x = y ↔ of x ≠ of y; rwa [of_eq]
 
-lemma of_eq_zero [has_zero β] (NT : φ ≠ ⊥) (x : β) : x = 0 ↔ of x = (0 : β*) := of_eq _ _ NT
+lemma of_eq_zero [has_zero β] (NT : φ ≠ ⊥) (x : β) : x = 0 ↔ of x = (0 : β*) := 
+of_eq _ _ NT
 
-lemma of_ne_zero [has_zero β] (NT : φ ≠ ⊥) (x : β) : x ≠ 0 ↔ of x ≠ (0 : β*) := of_ne _ _ NT
+lemma of_ne_zero [has_zero β] (NT : φ ≠ ⊥) (x : β) : x ≠ 0 ↔ of x ≠ (0 : β*) :=
+of_ne _ _ NT
 
 @[simp] lemma of_zero [has_zero β] : of 0 = (0 : β*) := rfl
 
@@ -281,31 +296,31 @@ lemma of_ne_zero [has_zero β] (NT : φ ≠ ⊥) (x : β) : x ≠ 0 ↔ of x ≠
 
 @[simp] lemma of_inv [has_inv β] (x : β) : of (x⁻¹) = (of x : β*)⁻¹ := rfl
 
-lemma of_rel_of_rel (R : β → Prop) (x : β) : 
+lemma of_rel_of_rel {R : β → Prop} {x : β} : 
   R x → (lift_rel R) (of x : β*) := 
 λ hx, by show {i | R x} ∈ _; simp only [hx]; exact univ_mem_sets  
 
-lemma of_rel (R : β → Prop) (x : β) (NT: φ ≠ ⊥) : 
+lemma of_rel {R : β → Prop} {x : β} (NT: φ ≠ ⊥) : 
   R x ↔ (lift_rel R) (of x : β*) :=
-⟨ of_rel_of_rel _ _, 
+⟨ of_rel_of_rel, 
   λ hxy, by change {i | R x} ∈ _ at hxy; by_contra h;
   simp only [h, set.set_of_false, empty_in_sets_eq_bot] at hxy;
   exact NT hxy ⟩
 
-lemma of_rel_of_rel₂ (R : β → β → Prop) (x y : β) : 
+lemma of_rel_of_rel₂ {R : β → β → Prop} {x y : β} : 
   R x y → (lift_rel₂ R) (of x) (of y : β*) :=
 λ hxy, by show {i | R x y} ∈ _; simp only [hxy]; exact univ_mem_sets  
 
-lemma of_rel₂ (R : β → β → Prop) (x y : β) (NT: φ ≠ ⊥) : 
+lemma of_rel₂ {R : β → β → Prop} {x y : β} (NT: φ ≠ ⊥) : 
   R x y ↔ (lift_rel₂ R) (of x) (of y : β*) :=
-⟨ of_rel_of_rel₂ _ _ _, 
+⟨ of_rel_of_rel₂,
   λ hxy, by change {i | R x y} ∈ _ at hxy; by_contra h;
   simp only [h, set.set_of_false, empty_in_sets_eq_bot] at hxy;
   exact NT hxy ⟩
 
-lemma of_le_of_le [has_le β] (x y : β) : x ≤ y → of x ≤ (of y : β*) := of_rel_of_rel₂ _ _ _
+lemma of_le_of_le [has_le β] {x y : β} : x ≤ y → of x ≤ (of y : β*) := of_rel_of_rel₂
 
-lemma of_le [has_le β] (x y : β) (NT: φ ≠ ⊥) : x ≤ y ↔ of x ≤ (of y : β*) := of_rel₂ _ _ _ NT
+lemma of_le [has_le β] {x y : β} (NT: φ ≠ ⊥) : x ≤ y ↔ of x ≤ (of y : β*) := of_rel₂ NT
 
 lemma lt_def [K : preorder β] (U : is_ultrafilter φ) (x y : β*) : 
   (x < y) ↔ @lift_rel₂ _ _ φ K.lt x y := 
@@ -323,12 +338,12 @@ lemma lt_def' [K : preorder β] (U : is_ultrafilter φ) :
   filter_product.preorder.lt = @lift_rel₂ _ _ φ K.lt := 
 by ext x y; exact lt_def U x y
 
-lemma of_lt_of_lt [preorder β] (U : is_ultrafilter φ) (x y : β) : 
+lemma of_lt_of_lt [preorder β] (U : is_ultrafilter φ) {x y : β} : 
   x < y → of x < (of y : β*) := 
 by rw lt_def U; apply of_rel_of_rel₂
 
-lemma of_lt [preorder β] (x y : β) (U : is_ultrafilter φ) : x < y ↔ of x < (of y : β*) := 
-by rw lt_def U; exact of_rel₂ _ _ _ U.1
+lemma of_lt [preorder β] {x y : β} (U : is_ultrafilter φ) : x < y ↔ of x < (of y : β*) := 
+by rw lt_def U; exact of_rel₂ U.1
 
 instance [ordered_comm_group β] (U : is_ultrafilter φ) : ordered_comm_group β* :=
 { add_le_add_left := λ x y hxy z, by revert hxy; exact quotient.induction_on₃' x y z 
@@ -367,6 +382,12 @@ noncomputable instance [decidable_linear_ordered_comm_ring β] (U : is_ultrafilt
 noncomputable instance [discrete_linear_ordered_field β] (U : is_ultrafilter φ) : discrete_linear_ordered_field β* :=
 { ..filter_product.linear_ordered_field U, ..filter_product.decidable_linear_ordered_comm_ring U, ..filter_product.discrete_field U }
 
+instance [ordered_cancel_comm_monoid β] : ordered_cancel_comm_monoid β* :=
+{ add_le_add_left := λ x y hxy z, by revert hxy; exact quotient.induction_on₃' x y z 
+    (λ a b c hab, by filter_upwards [hab] λ i hi, by simpa),
+  le_of_add_le_add_left := λ x y z, quotient.induction_on₃' x y z $ λ x y z h, by filter_upwards [h] λ i, le_of_add_le_add_left,
+  ..filter_product.add_comm_monoid, ..filter_product.add_left_cancel_semigroup, ..filter_product.add_right_cancel_semigroup, ..filter_product.partial_order }
+
 end filter_product
 
 end filter