feat(Algebra/Category/ModuleCat): refactor Monoidal.lean to use PresheafOfModulesOfCommRing (#43193)

Co-authored-by: Brian-Nugent <bnugent@uw.edu>

Author: Brian-Nugent

Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean

@@ -5,15 +5,15 @@ Authors: Dagur Asgeirsson, Jack McKoen, Joël Riou
 -/
 module
 
-public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
+public import Mathlib.Algebra.Category.ModuleCat.Presheaf.OfCommRing
 public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
 
 /-!
 # The monoidal category structure on presheaves of modules
 
 Given a presheaf of commutative rings `R : Cᵒᵖ ⥤ CommRingCat`, we construct
 the monoidal category structure on the category of presheaves of modules
-`PresheafOfModules (R ⋙ forget₂ _ _)`. The tensor product `M₁ ⊗ M₂` is defined
+`PresheafOfModulesOfCommRing R`. The tensor product `M₁ ⊗ M₂` is defined
 as the presheaf of modules which sends `X : Cᵒᵖ` to `M₁.obj X ⊗ M₂.obj X`.
 
 ## Notes
@@ -31,14 +31,11 @@ universe v u v₁ u₁
 
 variable {C : Type*} [Category* C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
 
-instance (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ _ RingCat).obj X) :=
-  inferInstanceAs (CommRing (R.obj X))
-
-namespace PresheafOfModules
+namespace PresheafOfModulesOfCommRing
 
 namespace Monoidal
 
-variable (M₁ M₂ M₃ M₄ : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
+variable (M₁ M₂ M₃ M₄ : PresheafOfModulesOfCommRing.{u} R)
 
 set_option backward.isDefEq.respectTransparency false in
 /-- Auxiliary definition for `tensorObj`. -/
@@ -47,62 +44,57 @@ noncomputable def tensorObjMap {X Y : Cᵒᵖ} (f : X ⟶ Y) : M₁.obj X ⊗ M
   ModuleCat.MonoidalCategory.tensorLift (fun m₁ m₂ ↦ M₁.map f m₁ ⊗ₜ M₂.map f m₂)
     (by
       intro m₁ m₁' m₂
-      dsimp +instances
+      dsimp
       rw [map_add, TensorProduct.add_tmul])
     (by intro a m₁ m₂; dsimp; erw [M₁.map_smul]; rfl)
     (by
       intro m₁ m₂ m₂'
-      dsimp +instances
+      dsimp
       rw [map_add, TensorProduct.tmul_add])
     (by intro a m₁ m₂; dsimp; erw [M₂.map_smul, TensorProduct.tmul_smul (r := R.map f a)]; rfl)
 
-set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The tensor product of two presheaves of modules. -/
 @[simps obj]
-noncomputable def tensorObj : PresheafOfModules (R ⋙ forget₂ _ _) where
-  obj X := M₁.obj X ⊗ M₂.obj X
-  map f := tensorObjMap M₁ M₂ f
-  map_id X := ModuleCat.MonoidalCategory.tensor_ext (by
-    intro m₁ m₂
-    dsimp [tensorObjMap]
-    simp
-    rfl) -- `ModuleCat.restrictScalarsId'App_inv_apply` doesn't get picked up due to type mismatch
-  map_comp f g := ModuleCat.MonoidalCategory.tensor_ext (by
-    intro m₁ m₂
-    dsimp [tensorObjMap]
-    simp +instances)
+noncomputable def tensorObj : PresheafOfModulesOfCommRing R :=
+  mk (fun X ↦ M₁.obj X ⊗ M₂.obj X)
+    (fun f ↦ tensorObjMap M₁ M₂ f)
+    (fun X ↦ ModuleCat.MonoidalCategory.tensor_ext (by
+      intro m₁ m₂
+      dsimp [tensorObjMap]
+      simp))
+    (fun f g ↦ ModuleCat.MonoidalCategory.tensor_ext (by
+      intro m₁ m₂
+      dsimp [tensorObjMap]
+      simp +instances))
 
 variable {M₁ M₂ M₃ M₄}
 
 @[simp]
 lemma tensorObj_map_tmul {X Y : Cᵒᵖ} (f : X ⟶ Y) (m₁ : M₁.obj X) (m₂ : M₂.obj X) :
     DFunLike.coe (α := (M₁.obj X ⊗ M₂.obj X :))
       (β := fun _ ↦ (ModuleCat.restrictScalars (R.map f).hom).obj (M₁.obj Y ⊗ M₂.obj Y))
-      (ModuleCat.Hom.hom (R := ↑(R.obj X)) ((tensorObj M₁ M₂).map f)) (m₁ ⊗ₜ[R.obj X] m₂) =
+      (ModuleCat.Hom.hom ((tensorObj M₁ M₂).map f)) (m₁ ⊗ₜ[R.obj X] m₂) =
     M₁.map f m₁ ⊗ₜ[R.obj Y] M₂.map f m₂ := rfl
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The tensor product of two morphisms of presheaves of modules. -/
 @[simps]
-noncomputable def tensorHom (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄) : tensorObj M₁ M₃ ⟶ tensorObj M₂ M₄ where
-  app X := f.app X ⊗ₘ g.app X
-  naturality {X Y} φ := ModuleCat.MonoidalCategory.tensor_ext (fun m₁ m₃ ↦ by
-    dsimp
-    rw [tensorObj_map_tmul]
-    -- Need `erw` because of the type mismatch in `map` and the tensor product.
-    erw [ModuleCat.MonoidalCategory.tensorHom_tmul, tensorObj_map_tmul]
-    rw [naturality_apply, naturality_apply]
-    simp)
+noncomputable def tensorHom (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄) :
+    tensorObj M₁ M₃ ⟶ tensorObj M₂ M₄ :=
+  homMk (fun X ↦ f.app' X ⊗ₘ g.app' X)
+    (fun φ ↦ ModuleCat.MonoidalCategory.tensor_ext (fun m₁ m₃ ↦ by
+      dsimp
+      rw [tensorObj_map_tmul, ModuleCat.MonoidalCategory.tensorHom_tmul, tensorObj_map_tmul,
+        naturality_apply, naturality_apply]))
 
 end Monoidal
 
 open Monoidal
 
-open ModuleCat.MonoidalCategory in
 noncomputable instance monoidalCategoryStruct :
-    MonoidalCategoryStruct (PresheafOfModules.{u} (R ⋙ forget₂ _ _)) where
+    MonoidalCategoryStruct (PresheafOfModulesOfCommRing.{u} R) where
   tensorObj := tensorObj
   whiskerLeft _ _ _ g := tensorHom (𝟙 _) g
   whiskerRight f _ := tensorHom f (𝟙 _)
@@ -113,16 +105,18 @@ noncomputable instance monoidalCategoryStruct :
   leftUnitor M := Iso.symm (isoMk (fun _ ↦ (λ_ _).symm) (fun X Y f ↦ by
     ext m
     dsimp [CommRingCat.forgetToRingCat_obj]
-    erw [leftUnitor_inv_apply, leftUnitor_inv_apply, tensorObj_map_tmul, (R.map f).hom.map_one]
+    erw [ModuleCat.MonoidalCategory.leftUnitor_inv_apply,
+      ModuleCat.MonoidalCategory.leftUnitor_inv_apply, tensorObj_map_tmul, (R.map f).hom.map_one]
     rfl))
   rightUnitor M := Iso.symm (isoMk (fun _ ↦ (ρ_ _).symm) (fun X Y f ↦ by
     ext m
     dsimp [CommRingCat.forgetToRingCat_obj]
-    erw [rightUnitor_inv_apply, rightUnitor_inv_apply, tensorObj_map_tmul, (R.map f).hom.map_one]
+    erw [ModuleCat.MonoidalCategory.rightUnitor_inv_apply,
+      ModuleCat.MonoidalCategory.rightUnitor_inv_apply, tensorObj_map_tmul, (R.map f).hom.map_one]
     rfl))
 
 noncomputable instance monoidalCategory :
-    MonoidalCategory (PresheafOfModules.{u} (R ⋙ forget₂ _ _)) where
+    MonoidalCategory (PresheafOfModulesOfCommRing.{u} R) where
   tensorHom_def _ _ := by ext1; apply tensorHom_def
   id_tensorHom_id _ _ := by ext1; apply id_tensorHom_id
   tensorHom_comp_tensorHom _ _ _ _ := by ext1; apply tensorHom_comp_tensorHom
@@ -141,9 +135,9 @@ noncomputable instance monoidalCategory :
 open BraidedCategory
 
 noncomputable instance symmetricCategory :
-    SymmetricCategory (PresheafOfModules.{u} (R ⋙ forget₂ _ _)) where
+    SymmetricCategory (PresheafOfModulesOfCommRing.{u} R) where
   braiding M₁ M₂ :=
-    isoMk (fun X ↦ braiding (C := ModuleCat (R.obj X)) (M₁.obj X) (M₂.obj X))
+    isoMk (fun X ↦ braiding (M₁.obj X) (M₂.obj X))
       (fun _ _ f ↦ ModuleCat.MonoidalCategory.tensor_ext (fun _ _ ↦ rfl))
   braiding_naturality_right _ _ _ _ := by
     ext : 1
@@ -163,84 +157,83 @@ noncomputable instance symmetricCategory :
 
 section
 
-variable (M₁ M₂ M₃ M₄ : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
+variable (M₁ M₂ M₃ M₄ : PresheafOfModulesOfCommRing.{u} R)
 
 lemma tensorObj_obj (X : Cᵒᵖ) :
-    (M₁ ⊗ M₂).obj X =
-      MonoidalCategory.tensorObj (C := ModuleCat (R.obj X)) (M₁.obj X) (M₂.obj X) := rfl
+    (M₁ ⊗ M₂).obj X = MonoidalCategory.tensorObj (M₁.obj X) (M₂.obj X) := rfl
 
 attribute [local simp] tensorObj_obj
 
 variable {M₂ M₃} in
 @[simp]
 lemma whiskerLeft_app (f : M₂ ⟶ M₃) (X : Cᵒᵖ) :
-    dsimp% (M₁ ◁ f).app X = whiskerLeft (C := ModuleCat (R.obj X)) (M₁.obj X) (f.app X) :=
-  rfl
+    dsimp% (M₁ ◁ f).app' X = whiskerLeft (M₁.obj X) (f.app' X) := rfl
 
 variable {M₁ M₂} in
 @[simp]
-lemma whiskerRight_app (f : M₁ ⟶ M₂) (M₃ : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) (X : Cᵒᵖ) :
-    dsimp% (f ▷ M₃).app X = whiskerRight (C := ModuleCat (R.obj X)) (f.app X) (M₃.obj X) := rfl
+lemma whiskerRight_app (f : M₁ ⟶ M₂) (M₃ : PresheafOfModulesOfCommRing.{u} R)
+    (X : Cᵒᵖ) :
+    dsimp% (f ▷ M₃).app' X = whiskerRight (f.app' X) (M₃.obj X) := rfl
 
 variable {M₁ M₂ M₃ M₄} in
 @[simp]
 lemma tensorHom_app (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄) (X : Cᵒᵖ) :
-    dsimp% (f ⊗ₘ g).app X =
-      MonoidalCategory.tensorHom (C := ModuleCat (R.obj X)) (f.app X) (g.app X) := rfl
+    dsimp% (f ⊗ₘ g).app' X =
+      MonoidalCategory.tensorHom (f.app' X) (g.app' X) := rfl
 
 @[simp]
 lemma leftUnitor_hom_app (X : Cᵒᵖ) :
-    dsimp% (λ_ M₁).hom.app X = (leftUnitor (C := ModuleCat (R.obj X)) (M₁.obj X)).hom :=
+    dsimp% (λ_ M₁).hom.app' X = (leftUnitor (M₁.obj X)).hom :=
   rfl
 
 @[simp]
 lemma leftUnitor_inv_app (X : Cᵒᵖ) :
-    dsimp% (λ_ M₁).inv.app X = (leftUnitor (C := ModuleCat (R.obj X)) (M₁.obj X)).inv := by
+    dsimp% (λ_ M₁).inv.app' X = (leftUnitor (M₁.obj X)).inv := by
   rfl
 
 @[simp]
 lemma rightUnitor_hom_app (X : Cᵒᵖ) :
-    dsimp% (ρ_ M₁).hom.app X = (rightUnitor (C := ModuleCat (R.obj X)) (M₁.obj X)).hom :=
+    dsimp% (ρ_ M₁).hom.app' X = (rightUnitor (M₁.obj X)).hom :=
   rfl
 
 @[simp]
 lemma rightUnitor_inv_app (X : Cᵒᵖ) :
-    dsimp% (ρ_ M₁).inv.app X = (rightUnitor (C := ModuleCat (R.obj X)) (M₁.obj X)).inv :=
+    dsimp% (ρ_ M₁).inv.app' X = (rightUnitor (M₁.obj X)).inv :=
   rfl
 
 @[simp]
 lemma associator_hom_app (X : Cᵒᵖ) :
-    (α_ M₁ M₂ M₃).hom.app X =
-      (associator (C := ModuleCat (R.obj X)) (M₁.obj X) (M₂.obj X) (M₃.obj X)).hom :=
+    (α_ M₁ M₂ M₃).hom.app' X =
+      (associator (M₁.obj X) (M₂.obj X) (M₃.obj X)).hom :=
   rfl
 
 @[simp]
 lemma associator_inv_app (X : Cᵒᵖ) :
-    (α_ M₁ M₂ M₃).inv.app X =
-      (associator (C := ModuleCat (R.obj X)) (M₁.obj X) (M₂.obj X) (M₃.obj X)).inv :=
+    (α_ M₁ M₂ M₃).inv.app' X =
+      (associator (M₁.obj X) (M₂.obj X) (M₃.obj X)).inv :=
   rfl
 
 @[simp]
 lemma braiding_hom_app (X : Cᵒᵖ) :
-    dsimp% (braiding M₁ M₂).hom.app X =
-      (braiding (C := ModuleCat (R.obj X)) (M₁.obj X) (M₂.obj X)).hom := by
+    dsimp% (braiding M₁ M₂).hom.app' X =
+      (braiding (M₁.obj X) (M₂.obj X)).hom := by
   rfl
 
 @[simp]
 lemma braiding_inv_app (X : Cᵒᵖ) :
-    dsimp% (braiding M₁ M₂).inv.app X =
-      (braiding (C := ModuleCat (R.obj X)) (M₁.obj X) (M₂.obj X)).inv := rfl
+    dsimp% (braiding M₁ M₂).inv.app' X =
+      (braiding (M₁.obj X) (M₂.obj X)).inv := rfl
 
 end
 
-instance (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) :
+instance (F : PresheafOfModulesOfCommRing.{u} R) :
     PreservesColimitsOfSize.{u, u} (tensorLeft F) where
-  preservesColimitsOfShape := ⟨⟨fun hc ↦ ⟨evaluationJointlyReflectsColimits _ _
+  preservesColimitsOfShape := ⟨⟨fun hc ↦ ⟨PresheafOfModules.evaluationJointlyReflectsColimits _ _
       (fun X ↦ isColimitOfPreserves (tensorLeft (show ModuleCat (R.obj X) from F.obj X))
-        (isColimitOfPreserves (evaluation _ X) hc))⟩⟩⟩
+        (isColimitOfPreserves (PresheafOfModules.evaluation _ X) hc))⟩⟩⟩
 
-instance (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) :
+instance (F : PresheafOfModulesOfCommRing.{u} R) :
     PreservesColimitsOfSize.{u, u} (tensorRight F) :=
   preservesColimits_of_natIso (tensorLeftIsoTensorRight F)
 
-end PresheafOfModules
+end PresheafOfModulesOfCommRing

Mathlib/Algebra/Category/ModuleCat/Presheaf/OfCommRing.lean

@@ -73,6 +73,10 @@ abbrev isoMk {M₁ M₂ : PresheafOfModulesOfCommRing.{v} R}
         (app X).hom ≫ M₂.map f := by cat_disch) : M₁ ≅ M₂ :=
   PresheafOfModules.isoMk app naturality
 
+/-- a family of linear maps `M₁.obj X ⟶ M₂.obj X` for all `X`. -/
+abbrev _root_.PresheafOfModules.Hom.app' {M₁ M₂ : PresheafOfModulesOfCommRing.{v} R}
+    (f : M₁ ⟶ M₂) (X : Cᵒᵖ) : M₁.obj X ⟶ M₂.obj X := f.app X
+
 /-- The free presheaf of modules of rank one over a presheaf of commutative rings. -/
 noncomputable abbrev unit (R : Cᵒᵖ ⥤ CommRingCat.{u}) :
     PresheafOfModulesOfCommRing.{u} R :=
@@ -83,6 +87,11 @@ noncomputable abbrev restrictScalars {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : R 
     PresheafOfModulesOfCommRing.{v} S ⥤ PresheafOfModulesOfCommRing.{v} R :=
   PresheafOfModules.restrictScalars (whiskerRight φ (forget₂ _ _))
 
+lemma naturality_apply {M₁ M₂ : PresheafOfModulesOfCommRing.{v} R}
+    (f : M₁ ⟶ M₂) {X Y : Cᵒᵖ} (g : X ⟶ Y) (x : M₁.obj X) :
+    (f.app' Y) ((M₁.map g) x) = (M₂.map g) ((f.app' X) x) :=
+  PresheafOfModules.naturality_apply _ _ _
+
 end Basic
 
 section PushforwardPullback