chore(category_theory): move all instances (e.g. Top, CommRing, Meas) into the root namespace (#1074)

* splitting adjunction.lean

* chore(CommRing/adjunctions): refactor proofs

* remove unnecessary assumptions

* add helpful doc-string

* cleanup

* chore(category_theory): move all instances (e.g. Top, CommRing, Meas) to the root namespace

* minor

* breaking things, haven't finished yet

* deterministic timeout

* unfold_coes to the rescue

* one more int.cast

* yet another int.cast

* fix merge

* minor

* merge

* fix imports

* fix merge

* fix imports/namespaces

* more namespace fixes

* fixes

* delete stray file

Author: kim-em

docs/tutorial/category_theory/calculating_colimits_in_Top.lean

@@ -1,4 +1,4 @@
-import category_theory.instances.Top.limits
+import topology.Top.limits
 import category_theory.limits.shapes
 import topology.instances.real
 
@@ -7,7 +7,6 @@ import topology.instances.real
 noncomputable theory
 
 open category_theory
-open category_theory.instances
 open category_theory.limits
 
 def R : Top := Top.of ℝ

src/category_theory/instances/CommRing/adjunctions.lean renamed to src/algebra/CommRing/adjunctions.lean

@@ -6,22 +6,21 @@ Multivariable polynomials on a type is the left adjoint of the
 forgetful functor from commutative rings to types.
 -/
 
-import category_theory.instances.CommRing.basic
+import algebra.CommRing.basic
 import category_theory.adjunction.basic
 import data.mv_polynomial
 
 universe u
 
 open mv_polynomial
 open category_theory
-open category_theory.instances
 
-namespace category_theory.instances.CommRing
+namespace CommRing
 
 local attribute [instance, priority 0] classical.prop_decidable
 
 noncomputable def polynomial_ring : Type u ⥤ CommRing.{u} :=
-{ obj := λ α, ⟨mv_polynomial α ℤ, by apply_instance⟩,
+{ obj := λ α, ⟨mv_polynomial α ℤ⟩,
   map := λ α β f, ⟨rename f, by apply_instance⟩ }
 
 @[simp] lemma polynomial_ring_obj_α {α : Type u} :
@@ -30,15 +29,14 @@ noncomputable def polynomial_ring : Type u ⥤ CommRing.{u} :=
 @[simp] lemma polynomial_ring_map_val {α β : Type u} {f : α → β} :
   (polynomial_ring.map f).val = rename f := rfl
 
-noncomputable def adj : polynomial_ring ⊣ (forget : CommRing.{u} ⥤ Type u) :=
+noncomputable def adj : polynomial_ring ⊣ (forget : CommRing ⥤ Type u) :=
 adjunction.mk_of_hom_equiv
 { hom_equiv := λ α R,
   { to_fun    := λ f, f ∘ X,
     inv_fun   := λ f, ⟨eval₂ (λ n : ℤ, (n : R)) f, by { unfold_coes, apply_instance }⟩,
-    left_inv  := λ f, CommRing.hom.ext $ @eval₂_hom_X _ _ _ _ _ _ f _,
+    left_inv  := λ f, bundled.hom_ext (@eval₂_hom_X _ _ _ _ _ _ f.val _),
     right_inv := λ x, by { ext1, unfold_coes, simp only [function.comp_app, eval₂_X] } },
   hom_equiv_naturality_left_symm' :=
-  λ X X' Y f g, by { ext1, dsimp, apply eval₂_cast_comp }
-}.
+  λ X X' Y f g, by { ext1, dsimp, apply eval₂_cast_comp } }.
 
-end category_theory.instances.CommRing
+end CommRing

src/category_theory/instances/CommRing/basic.lean renamed to src/algebra/CommRing/basic.lean

@@ -5,7 +5,7 @@ Authors: Scott Morrison, Johannes Hölzl
 Introduce CommRing -- the category of commutative rings.
 -/
 
-import category_theory.instances.Mon.basic
+import algebra.Mon.basic
 import category_theory.fully_faithful
 import algebra.ring
 import data.int.basic
@@ -14,85 +14,78 @@ universes u v
 
 open category_theory
 
-namespace category_theory.instances
-
 /-- The category of rings. -/
 @[reducible] def Ring : Type (u+1) := bundled ring
 
+/-- The category of commutative rings. -/
+@[reducible] def CommRing : Type (u+1) := bundled comm_ring
+
+namespace Ring
+
 instance (x : Ring) : ring x := x.str
 
 instance concrete_is_ring_hom : concrete_category @is_ring_hom :=
 ⟨by introsI α ia; apply_instance,
   by introsI α β γ ia ib ic f g hf hg; apply_instance⟩
 
-instance Ring.hom_is_ring_hom {R S : Ring} (f : R ⟶ S) : is_ring_hom (f : R → S) := f.2
+def of (α : Type u) [ring α] : Ring := ⟨α⟩
 
-/-- The category of commutative rings. -/
-@[reducible] def CommRing : Type (u+1) := bundled comm_ring
+abbreviation forget : Ring.{u} ⥤ Type u := forget
 
-instance (x : CommRing) : comm_ring x := x.str
+instance hom_is_ring_hom {R S : Ring} (f : R ⟶ S) : is_ring_hom (f : R → S) := f.2
 
--- Here we don't use the `concrete` machinery,
--- because it would require introducing a useless synonym for `is_ring_hom`.
-instance : category CommRing :=
-{ hom := λ R S, { f : R → S // is_ring_hom f },
-  id := λ R, ⟨ id, by resetI; apply_instance ⟩,
-  comp := λ R S T g h, ⟨ h.1 ∘ g.1, begin haveI := g.2, haveI := h.2, apply_instance end ⟩ }
+end Ring
 
 namespace CommRing
-variables {R S T : CommRing.{u}}
 
-def of (α : Type u) [comm_ring α] : CommRing := ⟨α, by apply_instance⟩
+instance (x : CommRing) : comm_ring x := x.str
 
-@[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
+@[reducible] def is_comm_ring_hom {α β} [comm_ring α] [comm_ring β] (f : α → β) : Prop :=
+is_ring_hom f
 
-instance hom_coe : has_coe_to_fun (R ⟶ S) :=
-{ F := λ f, R → S,
-  coe := λ f, f.1 }
+instance concrete_is_comm_ring_hom : concrete_category @is_comm_ring_hom :=
+⟨by introsI α ia; apply_instance,
+  by introsI α β γ ia ib ic f g hf hg; apply_instance⟩
 
-@[extensionality] lemma hom.ext  {f g : R ⟶ S} : (∀ x : R, f x = g x) → f = g :=
-λ w, subtype.ext.2 $ funext w
+def of (α : Type u) [comm_ring α] : CommRing := ⟨α⟩
 
-@[simp] lemma hom_coe_app (val : R → S) (prop) (r : R) : (⟨val, prop⟩ : R ⟶ S) r = val r := rfl
+abbreviation forget : CommRing.{u} ⥤ Type u := forget
 
-instance hom_is_ring_hom (f : R ⟶ S) : is_ring_hom (f : R → S) := f.2
+instance hom_is_ring_hom {R S : CommRing} (f : R ⟶ S) : is_ring_hom (f : R → S) := f.2
 
-def Int : CommRing := ⟨ℤ, infer_instance⟩
+variables {R S T : CommRing.{u}}
 
-def Int.cast {R : CommRing} : Int ⟶ R := { val := int.cast, property := by apply_instance }
+-- TODO need to kill these
+@[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
+
+-- TODO rename the next three lemmas?
+def Int.cast {R : CommRing} : CommRing.of ℤ ⟶ R := { val := int.cast, property := by apply_instance }
 
-def Int.hom_unique {R : CommRing} : unique (Int ⟶ R) :=
+def Int.hom_unique {R : CommRing} : unique (CommRing.of ℤ ⟶ R) :=
 { default := Int.cast,
   uniq := λ f, subtype.ext.mpr $ funext $ int.eq_cast f f.2.map_one f.2.map_add }
 
-/-- The forgetful functor commutative rings to Type. -/
-def forget : CommRing.{u} ⥤ Type u :=
-{ obj := λ R, R,
-  map := λ _ _ f, f }
-
 instance forget.faithful : faithful (forget) := {}
 
 instance forget_comm_ring (R : CommRing) : comm_ring (forget.obj R) := R.str
 instance forget_is_ring_hom {R S : CommRing} (f : R ⟶ S) : is_ring_hom (forget.map f) := f.property
 
 /-- The functor from commutative rings to rings. -/
 def to_Ring : CommRing.{u} ⥤ Ring.{u} :=
-{ obj := λ X, { α := X.1, str := by apply_instance },
+{ obj := λ X, { α := X.1 },
   map := λ X Y f, ⟨ f, by apply_instance ⟩ }
 
 instance to_Ring.faithful : faithful (to_Ring) := {}
 
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
 def forget_to_CommMon : CommRing.{u} ⥤ CommMon.{u} :=
-{ obj := λ X, { α := X.1, str := by apply_instance },
+{ obj := λ X, { α := X.1 },
   map := λ X Y f, ⟨ f, by apply_instance ⟩ }
 
 instance forget_to_CommMon.faithful : faithful (forget_to_CommMon) := {}
 
 example : faithful (forget_to_CommMon ⋙ CommMon.forget_to_Mon) := by apply_instance
 
 end CommRing
-
-end category_theory.instances

src/category_theory/instances/CommRing/colimits.lean renamed to src/algebra/CommRing/colimits.lean

@@ -1,10 +1,12 @@
-import category_theory.instances.CommRing.basic
+-- Copyright (c) 2019 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+import algebra.CommRing.basic
 import category_theory.limits.limits
 
 universes u v
 
 open category_theory
-open category_theory.instances
 open category_theory.limits
 
 -- [ROBOT VOICE]:
@@ -34,7 +36,7 @@ comm_ring.left_distrib : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), a
 comm_ring.right_distrib : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
 -/
 
-namespace category_theory.instances.CommRing.colimits
+namespace CommRing.colimits
 
 variables {J : Type v} [small_category J] (F : J ⥤ CommRing.{v})
 
@@ -430,4 +432,4 @@ instance has_colimits_CommRing : @has_colimits CommRing.{v} infer_instance :=
     { cocone := colimit_cocone F,
       is_colimit := colimit_is_colimit F } } }
 
-end category_theory.instances.CommRing.colimits
+end CommRing.colimits

src/category_theory/instances/CommRing/default.lean renamed to src/algebra/CommRing/default.lean

@@ -4,6 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 
-import category_theory.instances.CommRing.basic
-import category_theory.instances.CommRing.adjunctions
-import category_theory.instances.CommRing.colimits
+import algebra.CommRing.basic
+import algebra.CommRing.adjunctions
+import algebra.CommRing.colimits

src/category_theory/instances/CommRing/limits.lean renamed to src/algebra/CommRing/limits.lean

@@ -2,26 +2,24 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Scott Morrison
 
-import category_theory.instances.CommRing.basic
+import algebra.CommRing.basic
 import category_theory.limits.types
 import category_theory.limits.preserves
 import ring_theory.subring
 import algebra.pi_instances
 
 open category_theory
-open category_theory.instances
+open category_theory.limits
 
 universe u
 
-namespace category_theory.instances.CommRing
-
-open category_theory.limits
+namespace CommRing
 
 variables {J : Type u} [small_category J]
 
-instance (F : J ⥤ CommRing.{u}) (j) : comm_ring ((F ⋙ CommRing.forget).obj j) :=
+instance comm_ring_obj (F : J ⥤ CommRing.{u}) (j) : comm_ring ((F ⋙ CommRing.forget).obj j) :=
 by { dsimp, apply_instance }
-instance (F : J ⥤ CommRing.{u}) (j j') (f : j ⟶ j') : is_ring_hom ((F ⋙ CommRing.forget).map f) :=
+instance is_ring_hom_map (F : J ⥤ CommRing.{u}) (j j') (f : j ⟶ j') : is_ring_hom ((F ⋙ CommRing.forget).map f) :=
 by { dsimp, apply_instance }
 
 instance sections_submonoid (F : J ⥤ CommRing.{u}) : is_submonoid (F ⋙ forget).sections :=
@@ -112,4 +110,4 @@ instance forget_preserves_limits : preserves_limits (forget : CommRing.{u} ⥤ T
     by exactI preserves_limit_of_preserves_limit_cone
       (limit.is_limit F) (limit.is_limit (F ⋙ forget)) } }
 
-end category_theory.instances.CommRing
+end CommRing

src/category_theory/instances/Mon/basic.lean renamed to src/algebra/Mon/basic.lean

@@ -13,21 +13,29 @@ universes u v
 
 open category_theory
 
-namespace category_theory.instances
-
 /-- The category of monoids and monoid morphisms. -/
 @[reducible] def Mon : Type (u+1) := bundled monoid
 
+/-- The category of commutative monoids and monoid morphisms. -/
+@[reducible] def CommMon : Type (u+1) := bundled comm_monoid
+
+namespace Mon
+
 instance (x : Mon) : monoid x := x.str
 
 instance concrete_is_monoid_hom : concrete_category @is_monoid_hom :=
 ⟨by introsI α ia; apply_instance,
   by introsI α β γ ia ib ic f g hf hg; apply_instance⟩
 
-instance Mon_hom_is_monoid_hom {R S : Mon} (f : R ⟶ S) : is_monoid_hom (f : R → S) := f.2
+def of (X : Type u) [monoid X] : Mon := ⟨X⟩
 
-/-- The category of commutative monoids and monoid morphisms. -/
-@[reducible] def CommMon : Type (u+1) := bundled comm_monoid
+abbreviation forget : Mon.{u} ⥤ Type u := forget
+
+instance hom_is_monoid_hom {R S : Mon} (f : R ⟶ S) : is_monoid_hom (f : R → S) := f.2
+
+end Mon
+
+namespace CommMon
 
 instance (x : CommMon) : comm_monoid x := x.str
 
@@ -38,10 +46,13 @@ instance concrete_is_comm_monoid_hom : concrete_category @is_comm_monoid_hom :=
 ⟨by introsI α ia; apply_instance,
   by introsI α β γ ia ib ic f g hf hg; apply_instance⟩
 
-instance CommMon_hom_is_comm_monoid_hom {R S : CommMon} (f : R ⟶ S) :
+def of (X : Type u) [comm_monoid X] : CommMon := ⟨X⟩
+
+abbreviation forget : CommMon.{u} ⥤ Type u := forget
+
+instance hom_is_comm_monoid_hom {R S : CommMon} (f : R ⟶ S) :
   is_comm_monoid_hom (f : R → S) := f.2
 
-namespace CommMon
 /-- The forgetful functor from commutative monoids to monoids. -/
 def forget_to_Mon : CommMon ⥤ Mon :=
 concrete_functor
@@ -51,5 +62,3 @@ concrete_functor
 instance : faithful (forget_to_Mon) := {}
 
 end CommMon
-
-end category_theory.instances

src/category_theory/instances/Mon/colimits.lean renamed to src/algebra/Mon/colimits.lean

@@ -1,10 +1,9 @@
-import category_theory.instances.Mon.basic
+import algebra.Mon.basic
 import category_theory.limits.limits
 
 universes v
 
 open category_theory
-open category_theory.instances
 open category_theory.limits
 
 /-
@@ -28,7 +27,7 @@ colimits of commutative rings.
 A slightly bolder claim is that we could do this with tactics, as well.
 -/
 
-namespace category_theory.instances.Mon.colimits
+namespace Mon.colimits
 
 variables {J : Type v} [small_category J] (F : J ⥤ Mon.{v})
 
@@ -234,4 +233,4 @@ instance has_colimits_Mon : @has_colimits Mon.{v} infer_instance :=
     { cocone := colimit_cocone F,
       is_colimit := colimit_is_colimit F } } }
 
-end category_theory.instances.Mon.colimits
+end Mon.colimits

src/category_theory/instances/Mon/default.lean renamed to src/algebra/Mon/default.lean

@@ -4,5 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 
-import category_theory.instances.Mon.basic
-import category_theory.instances.Mon.colimits
+import algebra.Mon.basic
+import algebra.Mon.colimits

src/algebraic_geometry/presheafed_space.lean

@@ -1,13 +1,12 @@
 -- Copyright (c) 2019 Scott Morrison. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Scott Morrison
-import category_theory.instances.Top.presheaf
+import topology.Top.presheaf
 
 universes v u
 
 open category_theory
-open category_theory.instances
-open category_theory.instances.Top
+open Top
 open topological_space
 open opposite
 

src/algebraic_geometry/stalks.lean

@@ -2,12 +2,11 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Scott Morrison
 import algebraic_geometry.presheafed_space
-import category_theory.instances.Top.stalks
+import topology.Top.stalks
 
 universes v u v' u'
 
 open category_theory
-open category_theory.instances
 open category_theory.limits
 open algebraic_geometry
 open topological_space
@@ -17,7 +16,7 @@ include 𝒞
 
 local attribute [tidy] tactic.op_induction'
 
-open category_theory.instances.Top.presheaf
+open Top.presheaf
 
 namespace algebraic_geometry.PresheafedSpace