feat(category_theory): Top, nbhd x, CommRing

category_theory/category.lean

@@ -23,7 +23,7 @@ namespace category_theory
 
 universes u v
 
-/- 
+/-
 The propositional fields of `category` are annotated with the auto_param `obviously`, which is
 defined here as a [`replacer` tactic](https://github.com/leanprover/mathlib/blob/master/docs/tactics.md#def_replacer).
 We then immediately set up `obviously` to call `tidy`. Later, this can be replaced with more
@@ -34,7 +34,7 @@ def_replacer obviously
 
 /--
 The typeclass `category C` describes morphisms associated to objects of type `C`.
-The universe levels of the objects and morphisms are unconstrained, and will often need to be 
+The universe levels of the objects and morphisms are unconstrained, and will often need to be
 specified explicitly, as `category.{u v} C`. (See also `large_category` and `small_category`.)
 -/
 class category (obj : Type u) : Type (max u (v+1)) :=
@@ -57,7 +57,7 @@ restate_axiom category.assoc'
 attribute [simp] category.id_comp category.comp_id category.assoc
 
 /--
-A `large_category` has objects in one universe level higher than the universe level of the morphisms. 
+A `large_category` has objects in one universe level higher than the universe level of the morphisms.
 It is useful for examples such as the category of types, or the category of groups, etc.
 -/
 abbreviation large_category (C : Type (u+1)) : Type (u+1) := category.{u+1 u} C
@@ -66,26 +66,40 @@ A `small_category` has objects and morphisms in the same universe level.
 -/
 abbreviation small_category (C : Type u)     : Type (u+1) := category.{u u} C
 
+/-- `concrete_category c h _ _` constructs a concrete category from a class `c` and a morphism
+predicate `hom`. `c` is usually a type class like `topological_space` and `hom` is `continuous`. -/
+structure concrete_category {C : Type u → Type v}
+  (hom : out_param $ ∀{α β : Type u}, C α → C β → (α → β) → Prop) :=
+(hom_id : ∀{α} (ia : C α), hom ia ia id)
+(hom_comp : ∀{α β γ} (ia : C α) (ib : C β) (ic : C γ) {f g}, hom ia ib f → hom ib ic g → hom ia ic (g ∘ f))
+attribute [class] concrete_category
+
+instance {C : Type u → Type v} (hom : ∀{α β : Type u}, C α → C β → (α → β) → Prop)
+  [h : concrete_category @hom] : category (sigma C) :=
+{ hom   := λa b, subtype (hom a.2 b.2),
+  id    := λa, ⟨@id a.1, h.hom_id a.2⟩,
+  comp  := λa b c f g, ⟨g.1 ∘ f.1, h.hom_comp a.2 b.2 c.2 f.2 g.2⟩ }
+
 section
 variables {C : Type u} [𝒞 : category.{u v} C] {X Y Z : C}
 include 𝒞
 
-class epi  (f : X ⟶ Y) : Prop := 
+class epi  (f : X ⟶ Y) : Prop :=
 (left_cancellation : Π {Z : C} (g h : Y ⟶ Z) (w : f ≫ g = f ≫ h), g = h)
 class mono (f : X ⟶ Y) : Prop :=
 (right_cancellation : Π {Z : C} (g h : Z ⟶ X) (w : g ≫ f = h ≫ f), g = h)
 
-@[simp] lemma cancel_epi  (f : X ⟶ Y) [epi f]  (g h : Y ⟶ Z) : (f ≫ g = f ≫ h) ↔ g = h := 
+@[simp] lemma cancel_epi  (f : X ⟶ Y) [epi f]  (g h : Y ⟶ Z) : (f ≫ g = f ≫ h) ↔ g = h :=
 ⟨ λ p, epi.left_cancellation g h p, begin intro a, subst a end ⟩
-@[simp] lemma cancel_mono (f : X ⟶ Y) [mono f] (g h : Z ⟶ X) : (g ≫ f = h ≫ f) ↔ g = h := 
+@[simp] lemma cancel_mono (f : X ⟶ Y) [mono f] (g h : Z ⟶ X) : (g ≫ f = h ≫ f) ↔ g = h :=
 ⟨ λ p, mono.right_cancellation g h p, begin intro a, subst a end ⟩
 end
 
 section
 variable (C : Type u)
 variable [small_category C]
 
-instance : large_category (ulift.{(u+1)} C) := 
+instance : large_category (ulift.{(u+1)} C) :=
 { hom  := λ X Y, (X.down ⟶ Y.down),
   id   := λ X, 𝟙 X.down,
   comp := λ _ _ _ f g, f ≫ g }

category_theory/examples/measurable_space.lean

@@ -0,0 +1,29 @@
+/- Copyright (c) 2018 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl
+
+Basic setup for measurable spaces.
+-/
+
+import category_theory.examples.topological_spaces
+import category_theory.types
+import analysis.measure_theory.borel_space
+
+open category_theory
+universes u v
+
+namespace category_theory.examples
+
+@[reducible] def Meas : Type (u+1) := sigma measurable_space
+
+namespace Meas
+
+instance : concrete_category @measurable := ⟨@measurable_id, @measurable.comp⟩
+
+end Meas
+
+def Borel : Top ⥤ Meas :=
+concrete_functor @continuous @measurable
+  @measure_theory.borel @measure_theory.measurable_of_continuous
+
+end category_theory.examples

category_theory/examples/rings.lean

@@ -0,0 +1,42 @@
+/- Copyright (c) 2018 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, Johannes Hölzl
+
+Introduce CommRing -- the category of commutative rings.
+
+Currently only the basic setup.
+-/
+
+import category_theory.functor
+import algebra.ring
+import analysis.topology.topological_structures
+
+open category_theory
+
+namespace category_theory.examples
+
+@[reducible] def {u} CommRing : Type (u + 1) := Σ α : Type u, comm_ring α
+
+@[reducible] def is_comm_ring_hom {α β} [comm_ring α] [comm_ring β] (f : α → β) : Prop :=
+is_ring_hom f
+
+instance : concrete_category @is_comm_ring_hom :=
+⟨by introsI α ia; exact is_ring_hom.id,
+  by introsI α β γ ia ib ic f g hf hg; exact is_ring_hom.comp f g⟩
+
+instance : large_category CommRing := infer_instance
+
+instance (R : CommRing) : comm_ring R.1 := R.2
+
+instance (R S : CommRing) (f : category.hom R S) : is_ring_hom f.1 := f.2
+
+@[simp] lemma comm_ring_hom.map_mul (R S : CommRing) (f : category.hom R S) (x y : R.1) :
+  f.1 (x * y) = (f.1 x) * (f.1 y) :=
+by rw f.2.map_mul
+@[simp] lemma comm_ring_hom.map_add (R S : CommRing) (f : category.hom R S) (x y : R.1) :
+  f.1 (x + y) = (f.1 x) + (f.1 y) :=
+by rw f.2.map_add
+@[simp] lemma comm_ring_hom.map_one (R S : CommRing) (f : category.hom R S) : f.1 1 = 1 :=
+by rw f.2.map_one
+
+end category_theory.examples

category_theory/examples/topological_spaces.lean

@@ -0,0 +1,49 @@
+-- Copyright (c) 2017 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Patrick Massot, Scott Morrison
+
+import category_theory.full_subcategory
+import analysis.topology.topological_space
+import analysis.topology.continuity
+
+open category_theory
+universe u
+
+namespace category_theory.examples
+
+@[reducible] def Top : Type (u + 1) := Σ α : Type u, topological_space α
+
+namespace Top
+instance : concrete_category @continuous := ⟨@continuous_id, @continuous.comp⟩
+
+instance : large_category Top := infer_instance
+
+instance (X : Top) : topological_space X.1 := X.2
+
+end Top
+
+structure open_set (α : Type u) [X : topological_space α] : Type u :=
+(s : set α)
+(is_open : topological_space.is_open X s)
+
+variables {α : Type*} [topological_space α]
+
+namespace open_set
+instance : has_coe (open_set α) (set α) := { coe := λ U, U.s }
+
+instance : has_subset (open_set α) :=
+{ subset := λ U V, U.s ⊆ V.s }
+
+instance : preorder (open_set α) := by refine { le := (⊆), .. } ; tidy
+
+instance open_sets : small_category (open_set α) := by apply_instance
+
+instance : has_mem α (open_set α) :=
+{ mem := λ a V, a ∈ V.s }
+
+def nbhd (x : α) := { U : open_set α // x ∈ U }
+def nbhds (x : α) : small_category (nbhd x) := begin unfold nbhd, apply_instance end
+
+end open_set
+
+end category_theory.examples

category_theory/functor.lean

@@ -9,7 +9,7 @@ Defines a functor between categories.
 by the underlying function on objects, the name is capitalised.)
 
 Introduces notations
-  `C ⥤ D` for the type of all functors from `C` to `D`. 
+  `C ⥤ D` for the type of all functors from `C` to `D`.
     (I would like a better arrow here, unfortunately ⇒ (`\functor`) is taken by core.)
   `F X` (a coercion) for a functor `F` acting on an object `X`.
 -/
@@ -19,7 +19,7 @@ import tactic.tidy
 
 namespace category_theory
 
-universes u₁ v₁ u₂ v₂ u₃ v₃
+universes u v u₁ v₁ u₂ v₂ u₃ v₃
 
 /--
 `functor C D` represents a functor between categories `C` and `D`.
@@ -53,18 +53,18 @@ instance : has_coe_to_fun (C ⥤ D) :=
 
 def map (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) : (F X) ⟶ (F Y) := F.map' f
 
-@[simp] lemma map_id (F : C ⥤ D) (X : C) : F.map (𝟙 X) = 𝟙 (F X) := 
+@[simp] lemma map_id (F : C ⥤ D) (X : C) : F.map (𝟙 X) = 𝟙 (F X) :=
 begin unfold functor.map, erw F.map_id', refl end
-@[simp] lemma map_comp (F : C ⥤ D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : 
-  F.map (f ≫ g) = F.map f ≫ F.map g := 
+@[simp] lemma map_comp (F : C ⥤ D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+  F.map (f ≫ g) = F.map f ≫ F.map g :=
 begin unfold functor.map, erw F.map_comp' end
 
 -- We define a refl lemma 'refolding' the coercion,
 -- and two lemmas for the coercion applied to an explicit structure.
 @[simp] lemma obj_eq_coe {F : C ⥤ D} (X : C) : F.obj X = F X := by unfold_coes
-@[simp] lemma mk_obj (o : C → D) (m mi mc) (X : C) : 
+@[simp] lemma mk_obj (o : C → D) (m mi mc) (X : C) :
   ({ functor . obj := o, map' := m, map_id' := mi, map_comp' := mc } : C ⥤ D) X = o X := rfl
-@[simp] lemma mk_map (o : C → D) (m mi mc) {X Y : C} (f : X ⟶ Y) : 
+@[simp] lemma mk_map (o : C → D) (m mi mc) {X Y : C} (f : X ⟶ Y) :
   functor.map { functor . obj := o, map' := m, map_id' := mi, map_comp' := mc } f = m f := rfl
 end
 
@@ -84,8 +84,8 @@ variable {C}
 end
 
 section
-variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] 
-          {D : Type u₂} [𝒟 : category.{u₂ v₂} D] 
+variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C]
+          {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
           {E : Type u₃} [ℰ : category.{u₃ v₃} E]
 include 𝒞 𝒟 ℰ
 
@@ -99,9 +99,23 @@ def comp (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E :=
 infixr ` ⋙ `:80 := comp
 
 @[simp] lemma comp_obj (F : C ⥤ D) (G : D ⥤ E) (X : C) : (F ⋙ G) X = G (F X) := rfl
-@[simp] lemma comp_map (F : C ⥤ D) (G : D ⥤ E) (X Y : C) (f : X ⟶ Y) : 
+@[simp] lemma comp_map (F : C ⥤ D) (G : D ⥤ E) (X Y : C) (f : X ⟶ Y) :
   (F ⋙ G).map f = G.map (F.map f) := rfl
 end
 
 end functor
+
+def concrete_functor
+  {C : Type u → Type v} (hC : ∀{α β}, C α → C β → (α → β) → Prop) [concrete_category @hC]
+  {D : Type u → Type v} (hD : ∀{α β}, D α → D β → (α → β) → Prop) [concrete_category @hD]
+  (m : ∀{α}, C α → D α) (h : ∀{α β} (ia : C α) (ib : C β) {f}, hC ia ib f → hD (m ia) (m ib) f) :
+  sigma C ⥤ sigma D :=
+begin
+  /- Uh, we have a problem when obviously fails! -/
+  refine @category_theory.functor.mk (sigma C) _ (sigma D) _ (sigma.map id @m) _ _ _,
+  /- change sigma.map to use projections instead of case -/
+  { rintros ⟨a, ia⟩ ⟨b, ib⟩ ⟨f, hf⟩, exact ⟨f, h ia ib hf⟩ },
+  obviously
+end
+
 end category_theory

category_theory/types.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Stephen Morgan, Scott Morrison
 
-import category_theory.functor_category
+import category_theory.functor_category category_theory.embedding
 
 namespace category_theory
 
@@ -13,22 +13,22 @@ instance types : large_category (Type u) :=
   id      := λ a, id,
   comp    := λ _ _ _ f g, g ∘ f }
 
-@[simp] lemma types_hom {α β : Type u} : (α ⟶ β) = (α → β) := rfl  
+@[simp] lemma types_hom {α β : Type u} : (α ⟶ β) = (α → β) := rfl
 @[simp] lemma types_id {α : Type u} (a : α) : (𝟙 α : α → α) a = a := rfl
 @[simp] lemma types_comp {α β γ : Type u} (f : α → β) (g : β → γ) (a : α) : (((f : α ⟶ β) ≫ (g : β ⟶ γ)) : α ⟶ γ) a = g (f a) := rfl
 
 namespace functor_to_types
-variables {C : Type u} [𝒞 : category.{u v} C] (F G H : C ⥤ (Type w)) {X Y Z : C} 
+variables {C : Type u} [𝒞 : category.{u v} C] (F G H : C ⥤ (Type w)) {X Y Z : C}
 include 𝒞
-variables (σ : F ⟹ G) (τ : G ⟹ H) 
+variables (σ : F ⟹ G) (τ : G ⟹ H)
 
 @[simp] lemma map_comp (f : X ⟶ Y) (g : Y ⟶ Z) (a : F X) : (F.map (f ≫ g)) a = (F.map g) ((F.map f) a) :=
 by simp
 
-@[simp] lemma map_id (a : F X) : (F.map (𝟙 X)) a = a := 
+@[simp] lemma map_id (a : F X) : (F.map (𝟙 X)) a = a :=
 by simp
 
-lemma naturality (f : X ⟶ Y) (x : F X) : σ Y ((F.map f) x) = (G.map f) (σ X x) := 
+lemma naturality (f : X ⟶ Y) (x : F X) : σ Y ((F.map f) x) = (G.map f) (σ X x) :=
 congr_fun (σ.naturality f) x
 
 @[simp] lemma vcomp (x : F X) : (σ ⊟ τ) X x = τ X (σ X x) := rfl
@@ -39,8 +39,18 @@ variables {D : Type u'} [𝒟 : category.{u' v'} D] (I J : D ⥤ C) (ρ : I ⟹
 
 end functor_to_types
 
-definition ulift_functor : (Type u) ⥤ (Type (max u v)) := 
+def ulift_functor : (Type u) ⥤ (Type (max u v)) :=
 { obj      := λ X, ulift.{v} X,
   map'     := λ X Y f, λ x : ulift.{v} X, ulift.up (f x.down) }
 
+section forget
+variables (C : Type u → Type v) {hom : ∀α β, C α → C β → (α → β) → Prop} [i : concrete_category hom]
+include i
+
+def forget : sigma C ⥤ Type u := { obj  := sigma.fst, map' := λa b h, h.1 }
+
+instance forget.faithful : faithful (forget C) := {}
+
+end forget
+
 end category_theory