feat(order/category/omega-complete): omega-complete partial orders form a complete category (#4397)

as discussed in #4348.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Author: 3 people

src/category_theory/limits/shapes/biproducts.lean

@@ -227,11 +227,11 @@ by simp [biproduct.ι_π, h]
 /-- Given a collection of maps into the summands, we obtain a map into the biproduct. -/
 abbreviation biproduct.lift
   {f : J → C} [has_biproduct f] {P : C} (p : Π b, P ⟶ f b) : P ⟶ ⨁ f :=
-(biproduct.is_limit f).lift (fan.mk p)
+(biproduct.is_limit f).lift (fan.mk P p)
 /-- Given a collection of maps out of the summands, we obtain a map out of the biproduct. -/
 abbreviation biproduct.desc
   {f : J → C} [has_biproduct f] {P : C} (p : Π b, f b ⟶ P) : ⨁ f ⟶ P :=
-(biproduct.is_colimit f).desc (cofan.mk p)
+(biproduct.is_colimit f).desc (cofan.mk P p)
 
 @[simp, reassoc]
 lemma biproduct.lift_π {f : J → C} [has_biproduct f] {P : C} (p : Π b, P ⟶ f b) (j : J) :
@@ -822,7 +822,7 @@ has_biproduct_of_total
   ι_π := λ j j', by simp, }
 begin
   ext,
-  simp only [comp_sum, limits.cofan.mk_π_app, limits.colimit.ι_desc_assoc, eq_self_iff_true,
+  simp only [comp_sum, limits.colimit.ι_desc_assoc, eq_self_iff_true,
     limits.colimit.ι_desc, category.comp_id],
   dsimp,
   simp only [dite_comp, finset.sum_dite_eq, finset.mem_univ, if_true, category.id_comp,

src/category_theory/limits/shapes/equalizers.lean

@@ -156,6 +156,7 @@ by rw [←s.w right, parallel_pair_map_right]
 
 /-- A fork on `f g : X ⟶ Y` is determined by the morphism `ι : P ⟶ X` satisfying `ι ≫ f = ι ≫ g`.
 -/
+@[simps]
 def fork.of_ι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : fork f g :=
 { X := P,
   π :=
@@ -170,6 +171,7 @@ def fork.of_ι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : fork f g :=
 
 /-- A cofork on `f g : X ⟶ Y` is determined by the morphism `π : Y ⟶ P` satisfying
     `f ≫ π = g ≫ π`. -/
+@[simps]
 def cofork.of_π {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : cofork f g :=
 { X := P,
   ι :=
@@ -182,15 +184,6 @@ def cofork.of_π {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : cofork f g :
       { dsimp, simp, },
     end } }
 
-@[simp] lemma fork.of_ι_app_zero {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) :
-  (fork.of_ι ι w).π.app zero = ι := rfl
-@[simp] lemma fork.of_ι_app_one {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) :
-  (fork.of_ι ι w).π.app one = ι ≫ f := rfl
-@[simp] lemma cofork.of_π_app_zero {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) :
-  (cofork.of_π π w).ι.app zero = f ≫ π := rfl
-@[simp] lemma cofork.of_π_app_one {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) :
-  (cofork.of_π π w).ι.app one = π := rfl
-
 /-- A fork `t` on the parallel pair `f g : X ⟶ Y` consists of two morphisms `t.π.app zero : t.X ⟶ X`
     and `t.π.app one : t.X ⟶ Y`. Of these, only the first one is interesting, and we give it the
     shorter name `fork.ι t`. -/

src/category_theory/limits/shapes/products.lean

@@ -26,18 +26,17 @@ abbreviation fan (f : β → C) := cone (discrete.functor f)
 abbreviation cofan (f : β → C) := cocone (discrete.functor f)
 
 /-- A fan over `f : β → C` consists of a collection of maps from an object `P` to every `f b`. -/
-def fan.mk {f : β → C} {P : C} (p : Π b, P ⟶ f b) : fan f :=
+@[simps]
+def fan.mk {f : β → C} (P : C) (p : Π b, P ⟶ f b) : fan f :=
 { X := P,
   π := { app := p } }
 
 /-- A cofan over `f : β → C` consists of a collection of maps from every `f b` to an object `P`. -/
-def cofan.mk {f : β → C} {P : C} (p : Π b, f b ⟶ P) : cofan f :=
+@[simps]
+def cofan.mk {f : β → C} (P : C) (p : Π b, f b ⟶ P) : cofan f :=
 { X := P,
   ι := { app := p } }
 
-@[simp] lemma fan.mk_π_app {f : β → C} {P : C} (p : Π b, P ⟶ f b) (b : β) : (fan.mk p).π.app b = p b := rfl
-@[simp] lemma cofan.mk_π_app {f : β → C} {P : C} (p : Π b, f b ⟶ P) (b : β) : (cofan.mk p).ι.app b = p b := rfl
-
 /-- An abbreviation for `has_limit (discrete.functor f)`. -/
 abbreviation has_product (f : β → C) := has_limit (discrete.functor f)
 
@@ -74,10 +73,10 @@ colimit.ι (discrete.functor f) b
 
 /-- A collection of morphisms `P ⟶ f b` induces a morphism `P ⟶ ∏ f`. -/
 abbreviation pi.lift {f : β → C} [has_product f] {P : C} (p : Π b, P ⟶ f b) : P ⟶ ∏ f :=
-limit.lift _ (fan.mk p)
+limit.lift _ (fan.mk P p)
 /-- A collection of morphisms `f b ⟶ P` induces a morphism `∐ f ⟶ P`. -/
 abbreviation sigma.desc {f : β → C} [has_coproduct f] {P : C} (p : Π b, f b ⟶ P) : ∐ f ⟶ P :=
-colimit.desc _ (cofan.mk p)
+colimit.desc _ (cofan.mk P p)
 
 /--
 Construct a morphism between categorical products (indexed by the same type)

src/category_theory/limits/shapes/types.lean

@@ -39,7 +39,7 @@ namespace category_theory.limits.types
 @[simp]
 lemma pi_lift_π_apply {β : Type u} (f : β → Type u) {P : Type u} (s : Π b, P ⟶ f b) (b : β) (x : P) :
   (pi.π f b : (∏ f) → f b) (@pi.lift β _ _ f _ P s x) = s b x :=
-congr_fun (limit.lift_π (fan.mk s) b) x
+congr_fun (limit.lift_π (fan.mk P s) b) x
 
 /-- A restatement of `types.map_π_apply` that uses `pi.π` and `pi.map`. -/
 @[simp]

src/order/category/omega_complete_partial_order.lean

@@ -6,6 +6,9 @@ Author: Simon Hudon
 
 import order.omega_complete_partial_order
 import order.category.Preorder
+import category_theory.limits.shapes.products
+import category_theory.limits.shapes.equalizers
+import category_theory.limits.shapes.constructions.limits_of_products_and_equalizers
 
 /-!
 # Category of types with a omega complete partial order
@@ -26,7 +29,7 @@ open category_theory
 universes u v
 
 /-- The category of types with a omega complete partial order. -/
-def ωCPO := bundled omega_complete_partial_order
+def ωCPO : Type (u+1) := bundled omega_complete_partial_order
 
 namespace ωCPO
 
@@ -47,4 +50,85 @@ instance : inhabited ωCPO := ⟨of punit⟩
 
 instance (α : ωCPO) : omega_complete_partial_order α := α.str
 
+section
+
+open category_theory.limits
+
+namespace has_products
+
+/-- The pi-type gives a cone for a product. -/
+def product {J : Type v} (f : J → ωCPO.{v}) : fan f :=
+fan.mk (of (Π j, f j)) (λ j, continuous_hom.of_mono (pi.monotone_apply j : _) (λ c, rfl))
+
+/-- The pi-type is a limit cone for the product. -/
+def is_product (J : Type v) (f : J → ωCPO) : is_limit (product f) :=
+{ lift := λ s,
+    ⟨λ t j, s.π.app j t, λ x y h j, (s.π.app j).monotone h,
+     λ x, funext (λ j, (s.π.app j).continuous x)⟩,
+  uniq' := λ s m w,
+  begin
+    ext t j,
+    change m t j = s.π.app j t,
+    rw ← w j,
+    refl,
+  end }.
+
+instance (J : Type v) (f : J → ωCPO.{v}) : has_product f :=
+has_limit.mk ⟨_, is_product _ f⟩
+
+end has_products
+
+instance omega_complete_partial_order_equalizer
+  {α β : Type*} [omega_complete_partial_order α] [omega_complete_partial_order β]
+  (f g : α →𝒄 β) : omega_complete_partial_order {a : α // f a = g a} :=
+omega_complete_partial_order.subtype _ $ λ c hc,
+begin
+  rw [f.continuous, g.continuous],
+  congr' 1,
+  ext,
+  apply hc _ ⟨_, rfl⟩,
+end
+
+namespace has_equalizers
+
+/-- The equalizer inclusion function as a `continuous_hom`. -/
+def equalizer_ι {α β : Type*} [omega_complete_partial_order α] [omega_complete_partial_order β]
+  (f g : α →𝒄 β) :
+  {a : α // f a = g a} →𝒄 α :=
+continuous_hom.of_mono (preorder_hom.subtype.val _) (λ c, rfl)
+
+/-- A construction of the equalizer fork. -/
+def equalizer {X Y : ωCPO.{v}} (f g : X ⟶ Y) :
+  fork f g :=
+@fork.of_ι _ _ _ _ _ _ (ωCPO.of {a // f a = g a}) (equalizer_ι f g)
+  (continuous_hom.ext _ _ (λ x, x.2))
+
+/-- The equalizer fork is a limit. -/
+def is_equalizer {X Y : ωCPO.{v}} (f g : X ⟶ Y) : is_limit (equalizer f g) :=
+fork.is_limit.mk' _ $ λ s,
+⟨{ to_fun := λ x, ⟨s.ι x, by apply continuous_hom.congr_fun s.condition⟩,
+    monotone' := λ x y h, s.ι.monotone h,
+    cont := λ x, subtype.ext (s.ι.continuous x) },
+  by { ext, refl },
+  λ m hm,
+  begin
+    ext,
+    apply continuous_hom.congr_fun hm,
+  end⟩
+
+end has_equalizers
+
+instance : has_products ωCPO.{v} :=
+λ J, { has_limit := λ F, has_limit_of_iso discrete.nat_iso_functor.symm }
+
+instance {X Y : ωCPO.{v}} (f g : X ⟶ Y) : has_limit (parallel_pair f g) :=
+has_limit.mk ⟨_, has_equalizers.is_equalizer f g⟩
+
+instance : has_equalizers ωCPO.{v} := has_equalizers_of_has_limit_parallel_pair _
+
+instance : has_limits ωCPO.{v} := limits_from_equalizers_and_products
+
+end
+
+
 end ωCPO

src/order/omega_complete_partial_order.lean

@@ -238,6 +238,17 @@ begin
   apply ωSup_le _ _ a,
 end
 
+/-- A subset `p : α → Prop` of the type closed under `ωSup` induces an
+`omega_complete_partial_order` on the subtype `{a : α // p a}`. -/
+def subtype {α : Type*} [omega_complete_partial_order α] (p : α → Prop)
+  (hp : ∀ (c : chain α), (∀ i ∈ c, p i) → p (ωSup c)) :
+  omega_complete_partial_order (subtype p) :=
+omega_complete_partial_order.lift
+  (preorder_hom.subtype.val p)
+  (λ c, ⟨ωSup _, hp (c.map (preorder_hom.subtype.val p)) (λ i ⟨n, q⟩, q.symm ▸ (c n).2)⟩)
+  (λ x y h, h)
+  (λ c, rfl)
+
 section continuity
 open chain
 
@@ -582,6 +593,12 @@ end old_struct
 
 namespace continuous_hom
 
+theorem congr_fun {f g : α →𝒄 β} (h : f = g) (x : α) : f x = g x :=
+congr_arg (λ h : α →𝒄 β, h x) h
+
+theorem congr_arg (f : α →𝒄 β) {x y : α} (h : x = y) : f x = f y :=
+congr_arg (λ x : α, f x) h
+
 @[mono]
 lemma monotone (f : α →𝒄 β) : monotone f :=
 continuous_hom.monotone' f
@@ -670,7 +687,7 @@ protected lemma ext (f g : α →𝒄 β) (h : ∀ x, f x = g x) : f = g :=
 by cases f; cases g; congr; ext; apply h
 
 protected lemma coe_inj (f g : α →𝒄 β) (h : (f : α → β) = g) : f = g :=
-continuous_hom.ext _ _ $ congr_fun h
+continuous_hom.ext _ _ $ _root_.congr_fun h
 
 @[simp]
 lemma comp_id (f : β →𝒄 γ) : f.comp id = f := by ext; refl

src/order/preorder_hom.lean

@@ -62,6 +62,10 @@ by { ext, refl }
 @[simp] lemma id_comp (f : preorder_hom α β) : id.comp f = f :=
 by { ext, refl }
 
+/-- `subtype.val` as a bundled monotone function.  -/
+def subtype.val (p : α → Prop) : subtype p →ₘ α :=
+⟨subtype.val, λ x y h, h⟩
+
 /-- The preorder structure of `α →ₘ β` is pointwise inequality: `f ≤ g ↔ ∀ a, f a ≤ g a`. -/
 instance : preorder (α →ₘ β) :=
 preorder.lift preorder_hom.to_fun