From 70cd00bc20ad304f2ac0886b2291b44261787607 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Tue, 14 May 2019 01:42:01 +1000
Subject: [PATCH] =?UTF-8?q?feat(Top.presheaf=5F=E2=84=82):=20presheaves=20?=
 =?UTF-8?q?of=20functions=20to=20topological=20commutative=20rings=20(#976?=
 =?UTF-8?q?)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* feat(category_theory/colimits): missing simp lemmas

* feat(category_theory): functor.map_nat_iso

* define `functor.map_nat_iso`, and relate to whiskering
* rename `functor.on_iso` to `functor.map_iso`
* add some missing lemmas about whiskering

* fix(category_theory): presheaves, unbundled and bundled, and pushforwards

* restoring `(opens X)ᵒᵖ`

* various changes from working on stalks

* rename `nbhds` to `open_nhds`

* fix introduced typo

* typo

* compactify a proof

* rename `presheaf` to `presheaf_on_space`

* fix(category_theory): turn `has_limits` classes into structures

* naming instances to avoid collisions

* breaking up instances.topological_spaces

* fixing all the other pi-type typclasses

* fix import

* oops

* fix import

* missed one

* typo

* WIP

* oops

* the presheaf of continuous functions to ℂ

* restoring eq_to_hom simp lemmas

* removing unnecessary simp lemma

* remove another superfluous lemma

* removing the nat_trans and vcomp notations; use \hom and \gg

* a simpler proposal

* getting rid of vcomp

* fix

* splitting files

* renaming

* update notation

* fix

* cleanup

* use iso_whisker_right instead of map_nat_iso

* proofs magically got easier?

* improve some proofs

* moving instances

* remove crap

* tidy

* minimise imports

* chore(travis): disable the check for minimal imports

* Update src/algebraic_geometry/presheafed_space.lean

Co-Authored-By: semorrison <scott@tqft.net>

* writing `op_induction` tactic, and improving proofs

* squeeze_simping

* cleanup

* rearranging

* cleanup

* cleaning up

* cleaning up

* move

* Update src/category_theory/instances/Top/presheaf_of_functions.lean

Co-Authored-By: Floris van Doorn <fpvdoorn@gmail.com>

* fixes in response to review
---
 .../instances/CommRing/basic.lean             |  2 +
 .../instances/Top/default.lean                |  2 +-
 src/category_theory/instances/Top/opens.lean  |  5 ++
 .../instances/Top/presheaf_of_functions.lean  | 74 +++++++++++++++++
 .../instances/TopCommRing/basic.lean          | 83 +++++++++++++++++++
 .../instances/TopCommRing/default.lean        |  1 +
 6 files changed, 166 insertions(+), 1 deletion(-)
 create mode 100644 src/category_theory/instances/Top/presheaf_of_functions.lean
 create mode 100644 src/category_theory/instances/TopCommRing/basic.lean
 create mode 100644 src/category_theory/instances/TopCommRing/default.lean

diff --git a/src/category_theory/instances/CommRing/basic.lean b/src/category_theory/instances/CommRing/basic.lean
index a32ac9cc487b0..1ff3904d92664 100644
--- a/src/category_theory/instances/CommRing/basic.lean
+++ b/src/category_theory/instances/CommRing/basic.lean
@@ -42,6 +42,8 @@ instance : category CommRing :=
 namespace CommRing
 variables {R S T : CommRing.{u}}
 
+def of (α : Type u) [comm_ring α] : CommRing := ⟨α, by apply_instance⟩
+
 @[simp] lemma id_val : subtype.val (𝟙 R) = id := rfl
 @[simp] lemma comp_val (f : R ⟶ S) (g : S ⟶ T) :
   (f ≫ g).val = g.val ∘ f.val := rfl
diff --git a/src/category_theory/instances/Top/default.lean b/src/category_theory/instances/Top/default.lean
index 83f516161f1d0..6e1df55a9d699 100644
--- a/src/category_theory/instances/Top/default.lean
+++ b/src/category_theory/instances/Top/default.lean
@@ -6,4 +6,4 @@ import category_theory.instances.Top.basic
 import category_theory.instances.Top.limits
 import category_theory.instances.Top.adjunctions
 import category_theory.instances.Top.open_nhds
-import category_theory.instances.Top.presheaf
+import category_theory.instances.Top.presheaf_of_functions
diff --git a/src/category_theory/instances/Top/opens.lean b/src/category_theory/instances/Top/opens.lean
index a93cb40a157a6..5a26ac4d93f1b 100644
--- a/src/category_theory/instances/Top/opens.lean
+++ b/src/category_theory/instances/Top/opens.lean
@@ -25,6 +25,11 @@ instance opens_category : category.{u+1} (opens X) :=
   id   := λ X, ⟨ ⟨ le_refl X ⟩ ⟩,
   comp := λ X Y Z f g, ⟨ ⟨ le_trans f.down.down g.down.down ⟩ ⟩ }
 
+def to_Top (X : Top.{u}) : opens X ⥤ Top :=
+{ obj := λ U, ⟨U.val, infer_instance⟩,
+  map := λ U V i, ⟨λ x, ⟨x.1, i.down.down x.2⟩,
+    (embedding.continuous_iff embedding_subtype_val).2 continuous_induced_dom⟩ }
+
 /-- `opens.map f` gives the functor from open sets in Y to open set in X,
     given by taking preimages under f. -/
 def map (f : X ⟶ Y) : opens Y ⥤ opens X :=
diff --git a/src/category_theory/instances/Top/presheaf_of_functions.lean b/src/category_theory/instances/Top/presheaf_of_functions.lean
new file mode 100644
index 0000000000000..8bf2c6b03411d
--- /dev/null
+++ b/src/category_theory/instances/Top/presheaf_of_functions.lean
@@ -0,0 +1,74 @@
+import category_theory.instances.Top.presheaf
+import category_theory.instances.TopCommRing.basic
+import category_theory.yoneda
+import ring_theory.subring
+import topology.algebra.continuous_functions
+
+universes v u
+
+open category_theory
+open category_theory.instances
+open topological_space
+
+namespace category_theory.instances.Top
+
+variables (X : Top.{v})
+
+def presheaf_to_Top (T : Top.{v}) : X.presheaf (Type v) :=
+(opens.to_Top X).op ⋙ (yoneda.obj T)
+
+-- TODO upgrade the result to TopCommRing?
+def continuous_functions (X : Top.{v}ᵒᵖ) (R : TopCommRing.{v}) : CommRing.{v} :=
+{ α := unop X ⟶ TopCommRing.forget_to_Top.obj R,
+  str := _root_.continuous_comm_ring }
+
+namespace continuous_functions
+@[simp] lemma one (X : Top.{v}ᵒᵖ) (R : TopCommRing.{v}) (x) :
+  (monoid.one ↥(continuous_functions X R)).val x = 1 := rfl
+@[simp] lemma add (X : Top.{v}ᵒᵖ) (R : TopCommRing.{v}) (f g : continuous_functions X R) (x) :
+  (comm_ring.add f g).val x = f.1 x + g.1 x := rfl
+@[simp] lemma mul (X : Top.{v}ᵒᵖ) (R : TopCommRing.{v}) (f g : continuous_functions X R) (x) :
+  (ring.mul f g).val x = f.1 x * g.1 x := rfl
+
+def pullback {X Y : Topᵒᵖ} (f : X ⟶ Y) (R : TopCommRing) :
+  continuous_functions X R ⟶ continuous_functions Y R :=
+{ val := λ g, f.unop ≫ g,
+  property :=
+  { map_one := rfl,
+    map_add := by tidy,
+    map_mul := by tidy } }
+
+local attribute [extensionality] subtype.eq
+
+def map (X : Topᵒᵖ) {R S : TopCommRing} (φ : R ⟶ S) :
+  continuous_functions X R ⟶ continuous_functions X S :=
+{ val := λ g, g ≫ (TopCommRing.forget_to_Top.map φ),
+  property :=
+  { map_one := begin ext1, ext1, simp only [one], exact φ.2.1.map_one end,
+    map_add := λ x y,
+    begin ext1, ext1, simp only [function.comp_app, add], apply φ.2.1.map_add end,
+    map_mul := λ x y,
+    begin ext1, ext1, simp only [function.comp_app, mul], apply φ.2.1.map_mul end } }
+end continuous_functions
+
+def CommRing_yoneda : TopCommRing ⥤ (Topᵒᵖ ⥤ CommRing) :=
+{ obj := λ R,
+  { obj := λ X, continuous_functions X R,
+    map := λ X Y f, continuous_functions.pullback f R },
+  map := λ R S φ,
+  { app := λ X, continuous_functions.map X φ } }
+
+def presheaf_to_TopCommRing (T : TopCommRing.{v}) :
+  X.presheaf CommRing.{v} :=
+(opens.to_Top X).op ⋙ (CommRing_yoneda.obj T)
+
+noncomputable def presheaf_ℚ (Y : Top) : Y.presheaf CommRing :=
+presheaf_to_TopCommRing Y (TopCommRing.of ℚ)
+
+noncomputable def presheaf_ℝ (Y : Top) : Y.presheaf CommRing :=
+presheaf_to_TopCommRing Y (TopCommRing.of ℝ)
+
+noncomputable def presheaf_ℂ (Y : Top) : Y.presheaf CommRing :=
+presheaf_to_TopCommRing Y (TopCommRing.of ℂ)
+
+end category_theory.instances.Top
diff --git a/src/category_theory/instances/TopCommRing/basic.lean b/src/category_theory/instances/TopCommRing/basic.lean
new file mode 100644
index 0000000000000..8c89b62fdf3fe
--- /dev/null
+++ b/src/category_theory/instances/TopCommRing/basic.lean
@@ -0,0 +1,83 @@
+import category_theory.instances.CommRing.basic
+import category_theory.instances.Top.basic
+import topology.instances.complex
+
+universes u
+
+open category_theory
+
+namespace category_theory.instances
+
+structure TopCommRing :=
+(α : Type u)
+[is_comm_ring : comm_ring α]
+[is_topological_space : topological_space α]
+[is_topological_ring : topological_ring α]
+
+instance : has_coe_to_sort TopCommRing :=
+{ S := Type u, coe := TopCommRing.α }
+
+instance TopCommRing_comm_ring (R : TopCommRing) : comm_ring R := R.is_comm_ring
+instance TopCommRing_topological_space (R : TopCommRing) : topological_space R := R.is_topological_space
+instance TopCommRing_topological_ring (R : TopCommRing) : topological_ring R := R.is_topological_ring
+
+instance TopCommRing_category : category TopCommRing :=
+{ hom   := λ R S, {f : R → S // is_ring_hom f ∧ continuous f },
+  id    := λ R, ⟨id, by obviously⟩,
+  comp  := λ R S T f g, ⟨g.val ∘ f.val,
+    begin -- TODO automate
+      cases f, cases g, cases f_property, cases g_property, split,
+      dsimp, resetI, apply_instance,
+      dsimp, apply continuous.comp ; assumption
+    end⟩ }.
+
+namespace TopCommRing
+
+def of (X : Type u) [comm_ring X] [topological_space X] [topological_ring X] : TopCommRing :=
+{ α := X }
+
+noncomputable example : TopCommRing := TopCommRing.of ℚ
+noncomputable example : TopCommRing := TopCommRing.of ℝ
+noncomputable example : TopCommRing := TopCommRing.of ℂ
+
+/-- The forgetful functor to CommRing. -/
+def forget_to_CommRing : TopCommRing ⥤ CommRing :=
+{ obj := λ R, { α := R, str := instances.TopCommRing_comm_ring R },
+  map := λ R S f, ⟨ f.1, f.2.left ⟩ }
+
+instance forget_to_CommRing_faithful : faithful (forget_to_CommRing) := by tidy
+
+instance forget_to_CommRing_topological_space (R : TopCommRing) : topological_space (forget_to_CommRing.obj R) :=
+R.is_topological_space
+
+/-- The forgetful functor to Top. -/
+def forget_to_Top : TopCommRing ⥤ Top :=
+{ obj := λ R, { α := R, str := instances.TopCommRing_topological_space R },
+  map := λ R S f, ⟨ f.1, f.2.right ⟩ }
+
+instance forget_to_Top_faithful : faithful (forget_to_Top) := by tidy
+
+instance forget_to_Top_comm_ring (R : TopCommRing) : comm_ring (forget_to_Top.obj R) :=
+R.is_comm_ring
+instance forget_to_Top_topological_ring (R : TopCommRing) : topological_ring (forget_to_Top.obj R) :=
+R.is_topological_ring
+
+def forget : TopCommRing ⥤ (Type u) :=
+{ obj := λ R, R,
+  map := λ R S f, f.1 }
+
+instance forget_faithful : faithful (forget) := by tidy
+
+instance forget_topological_space (R : TopCommRing) : topological_space (forget.obj R) :=
+R.is_topological_space
+instance forget_comm_ring (R : TopCommRing) : comm_ring (forget.obj R) :=
+R.is_comm_ring
+instance forget_topological_ring (R : TopCommRing) : topological_ring (forget.obj R) :=
+R.is_topological_ring
+
+def forget_to_Type_via_Top : forget_to_Top ⋙ category_theory.forget ≅ forget := iso.refl _
+def forget_to_Type_via_CommRing : forget_to_Top ⋙ category_theory.forget ≅ forget := iso.refl _
+
+end TopCommRing
+
+end category_theory.instances
diff --git a/src/category_theory/instances/TopCommRing/default.lean b/src/category_theory/instances/TopCommRing/default.lean
new file mode 100644
index 0000000000000..e4c0ff49fedbf
--- /dev/null
+++ b/src/category_theory/instances/TopCommRing/default.lean
@@ -0,0 +1 @@
+import category_theory.instances.TopCommRing.basic