reorganising category_theory/instances/rings.lean

src/category_theory/instances/CommRing/adjunctions.lean

@@ -0,0 +1,61 @@
+/- Copyright (c) 2019 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, Johannes Hölzl
+
+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 category_theory.adjunction
+import data.mv_polynomial
+
+universe u
+
+open mv_polynomial
+open category_theory
+open category_theory.instances
+
+namespace category_theory.instances.CommRing
+
+local attribute [instance, priority 0] subtype.fintype set_fintype classical.prop_decidable
+
+noncomputable def polynomial_ring : Type u ⥤ CommRing.{u} :=
+{ obj := λ α, ⟨mv_polynomial α ℤ, by apply_instance⟩,
+  map := λ α β f, ⟨eval₂ C (X ∘ f), by apply_instance⟩,
+  map_id' := λ α, subtype.ext.mpr $ funext $ eval₂_eta,
+  map_comp' := λ α β γ f g, subtype.ext.mpr $ funext $ λ p,
+  by apply mv_polynomial.induction_on p; intros;
+    simp only [*, eval₂_add, eval₂_mul, eval₂_C, eval₂_X, comp_val,
+      eq_self_iff_true, function.comp_app, types_comp] at * }
+
+@[simp] lemma polynomial_ring_obj_α {α : Type u} :
+  (polynomial_ring.obj α).α = mv_polynomial α ℤ := rfl
+
+@[simp] lemma polynomial_ring_map_val {α β : Type u} {f : α → β} :
+  (polynomial_ring.map f).val = eval₂ C (X ∘ f) := rfl
+
+noncomputable def adj : adjunction polynomial_ring (forget : CommRing ⥤ Type u) :=
+adjunction.mk_of_hom_equiv _ _
+{ hom_equiv := λ α R,
+  { to_fun := λ f, f ∘ X,
+    inv_fun := λ f, ⟨eval₂ int.cast f, by apply_instance⟩,
+    left_inv := λ f, subtype.ext.mpr $ funext $ λ p,
+    begin
+      have H0 := λ n, (congr (int.eq_cast' (f.val ∘ C)) (rfl : n = n)).symm,
+      have H1 := λ p₁ p₂, (@is_ring_hom.map_add _ _ _ _ f.val f.2 p₁ p₂).symm,
+      have H2 := λ p₁ p₂, (@is_ring_hom.map_mul _ _ _ _ f.val f.2 p₁ p₂).symm,
+      apply mv_polynomial.induction_on p; intros;
+      simp only [*, eval₂_add, eval₂_mul, eval₂_C, eval₂_X,
+        eq_self_iff_true, function.comp_app, hom_coe_app] at *
+    end,
+    right_inv := by tidy },
+  hom_equiv_naturality_left_symm' := λ X' X Y f g, subtype.ext.mpr $ funext $ λ p,
+  begin
+    apply mv_polynomial.induction_on p; intros;
+    simp only [*, eval₂_mul, eval₂_add, eval₂_C, eval₂_X,
+      comp_val, equiv.coe_fn_symm_mk, hom_coe_app, polynomial_ring_map_val,
+      eq_self_iff_true, function.comp_app, add_right_inj, types_comp] at *
+  end }
+
+end category_theory.instances.CommRing

src/category_theory/instances/rings.lean → src/category_theory/instances/CommRing/basic.lean

@@ -3,15 +3,12 @@ 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.instances.monoids
 import category_theory.fully_faithful
-import category_theory.adjunction
-import data.mv_polynomial
 import algebra.ring
+import data.int.basic
 
 universes u v
 
@@ -28,7 +25,7 @@ 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
+instance Ring.hom_is_ring_hom {R S : Ring} (f : R ⟶ S) : is_ring_hom (f : R → S) := f.2
 
 /-- The category of commutative rings. -/
 @[reducible] def CommRing : Type (u+1) := bundled comm_ring
@@ -91,50 +88,6 @@ instance forget_to_CommMon.faithful : faithful (forget_to_CommMon) := {}
 
 example : faithful (forget_to_CommMon ⋙ CommMon.forget_to_Mon) := by apply_instance
 
-section
-open mv_polynomial
-local attribute [instance, priority 0] subtype.fintype set_fintype classical.prop_decidable
-
-noncomputable def polynomial : Type u ⥤ CommRing.{u} :=
-{ obj := λ α, ⟨mv_polynomial α ℤ, by apply_instance⟩,
-  map := λ α β f, ⟨eval₂ C (X ∘ f), by apply_instance⟩,
-  map_id' := λ α, subtype.ext.mpr $ funext $ eval₂_eta,
-  map_comp' := λ α β γ f g, subtype.ext.mpr $ funext $ λ p,
-  by apply mv_polynomial.induction_on p; intros;
-    simp only [*, eval₂_add, eval₂_mul, eval₂_C, eval₂_X, comp_val,
-      eq_self_iff_true, function.comp_app, types_comp] at * }
-
-@[simp] lemma polynomial_obj_α {α : Type u} :
-  (polynomial.obj α).α = mv_polynomial α ℤ := rfl
-
-@[simp] lemma polynomial_map_val {α β : Type u} {f : α → β} :
-  (CommRing.polynomial.map f).val = eval₂ C (X ∘ f) := rfl
-
-noncomputable def adj : adjunction polynomial (forget : CommRing ⥤ Type u) :=
-adjunction.mk_of_hom_equiv _ _
-{ hom_equiv := λ α R,
-  { to_fun := λ f, f ∘ X,
-    inv_fun := λ f, ⟨eval₂ int.cast f, by apply_instance⟩,
-    left_inv := λ f, subtype.ext.mpr $ funext $ λ p,
-    begin
-      have H0 := λ n, (congr (int.eq_cast' (f.val ∘ C)) (rfl : n = n)).symm,
-      have H1 := λ p₁ p₂, (@is_ring_hom.map_add _ _ _ _ f.val f.2 p₁ p₂).symm,
-      have H2 := λ p₁ p₂, (@is_ring_hom.map_mul _ _ _ _ f.val f.2 p₁ p₂).symm,
-      apply mv_polynomial.induction_on p; intros;
-      simp only [*, eval₂_add, eval₂_mul, eval₂_C, eval₂_X,
-        eq_self_iff_true, function.comp_app, hom_coe_app] at *
-    end,
-    right_inv := by tidy },
-  hom_equiv_naturality_left_symm' := λ X' X Y f g, subtype.ext.mpr $ funext $ λ p,
-  begin
-    apply mv_polynomial.induction_on p; intros;
-    simp only [*, eval₂_mul, eval₂_add, eval₂_C, eval₂_X,
-      comp_val, equiv.coe_fn_symm_mk, hom_coe_app, polynomial_map_val,
-      eq_self_iff_true, function.comp_app, add_right_inj, types_comp] at *
-  end }
-
-end
-
 end CommRing
 
 end category_theory.instances

src/category_theory/instances/CommRing/default.lean

@@ -0,0 +1,8 @@
+/-
+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.CommRing.basic
+import category_theory.instances.CommRing.adjunctions