NYLL
Module

PresheafPullbackMonoidal.lean

Nyll.SchemeTheory.Modules.PresheafPullbackMonoidal
55 declarations indexed from sourceView source ↗

Module documentation

Monoidal pullback of module presheaves

Restriction of scalars, free module presheaves, and free representables provide the tensor and unit comparisons for module-presheaf pullback. Preservation of finite products on the base category makes these pullback comparisons invertible.

Imports6
  • Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
  • Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
  • Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal
  • Mathlib.CategoryTheory.Monoidal.FunctorCategory
  • Mathlib.Tactic.CategoryTheory.Reassoc
  • Mathlib.Tactic.Ext
Imported by14

Declarations

instance

commRingAt

L32 ↗
PresheafOfModules.PullbackMonoidal.commRingAt
Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
Lean source · statement
instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X)
instance

moduleAt

L37 ↗
PresheafOfModules.PullbackMonoidal.moduleAt
Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
Lean source · statement
instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X)
abbrev

ringCatHom

L49 ↗
PresheafOfModules.ringCatHom
Documentation

The morphism of underlying ring presheaves induced by the commutative-ring presheaf morphism.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
section restrictScalars
variable {C : Type u₁} [Category.{v₁} C] {R S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ R)
Lean source · statement
abbrev ringCatHom : S ⋙ forget₂ CommRingCat RingCat ⟶ R ⋙ forget₂ CommRingCat RingCat
abbrev

restrictScalarsAt

L53 ↗
PresheafOfModules.restrictScalarsAt
Documentation

Restriction of scalars along the component ring homomorphism at U.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
section restrictScalars
variable {C : Type u₁} [Category.{v₁} C] {R S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ R)
Lean source · statement
abbrev restrictScalarsAt (U : Cᵒᵖ) : ModuleCat.{u} (R.obj U) ⥤ ModuleCat.{u} (S.obj U)
def

restrictScalarsε

L61 ↗
PresheafOfModules.restrictScalarsε
Documentation

The tensor-unit comparison for restriction of scalars on module presheaves.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
section restrictScalars
variable {C : Type u₁} [Category.{v₁} C] {R S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ R)
Lean source · full declaration
def restrictScalarsε :
    𝟙_ (PresheafOfModules.{u} (S ⋙ forget₂ _ _)) ⟶
      (restrictScalars (ringCatHom φ)).obj (𝟙_ (PresheafOfModules.{u} (R ⋙ forget₂ _ _))) where
  app U := ε (restrictScalarsAt φ U)
  naturality {U V} i := by
    refine ModuleCat.hom_ext (LinearMap.ext fun (s : S.obj U) => ?_)
    change ε (restrictScalarsAt φ V) (S.map i s) = R.map i (ε (restrictScalarsAt φ U) s)
    erw [ModuleCat.restrictScalars_η, ModuleCat.restrictScalars_η]
    exact ConcreteCategory.congr_hom (φ.naturality i) s
def

restrictScalarsμ

L72 ↗
PresheafOfModules.restrictScalarsμ
Documentation

The tensor-product comparison for restriction of scalars on module presheaves.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
section restrictScalars
variable {C : Type u₁} [Category.{v₁} C] {R S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ R)
Lean source · full declaration
def restrictScalarsμ (M N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) :
    (restrictScalars (ringCatHom φ)).obj M ⊗ (restrictScalars (ringCatHom φ)).obj N ⟶
      (restrictScalars (ringCatHom φ)).obj (M ⊗ N) where
  app U := μ (restrictScalarsAt φ U) (M.obj U) (N.obj U)
  naturality {U V} i := by
    apply ModuleCat.MonoidalCategory.tensor_ext
    intro m n
    have hS := PresheafOfModulesOfCommRing.Monoidal.tensorObj_map_tmul
      (M₁ := (restrictScalars (ringCatHom φ)).obj M)
      (M₂ := (restrictScalars (ringCatHom φ)).obj N) i m n
    have hR := PresheafOfModulesOfCommRing.Monoidal.tensorObj_map_tmul
      (M₁ := M) (M₂ := N) i m n
    have hU := ModuleCat.restrictScalars_μ_tmul (φ.app U).hom (M.obj U) (N.obj U) m n
    have hV := ModuleCat.restrictScalars_μ_tmul (φ.app V).hom (M.obj V) (N.obj V)
      (M.map i m) (N.map i n)
    exact ((congrArg (μ (restrictScalarsAt φ V) (M.obj V) (N.obj V)) hS).trans hV).trans
      ((congrArg ((M ⊗ N).map i) hU).trans hR).symm
instance

restrictScalars_laxMonoidal

L90 ↗
PresheafOfModules.restrictScalars_laxMonoidal
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
section restrictScalars
variable {C : Type u₁} [Category.{v₁} C] {R S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ R)
Lean source · full declaration
instance restrictScalars_laxMonoidal :
    (restrictScalars (ringCatHom φ)).LaxMonoidal where
  ε := restrictScalarsε φ
  μ M N := restrictScalarsμ φ M N
  μ_natural_left f N := by
    ext1 U
    simp only [comp_app, PresheafOfModulesOfCommRing.whiskerRight_app, restrictScalars_map_app]
    exact μ_natural_left (restrictScalarsAt φ U) (f.app U) (N.obj U)
  μ_natural_right M f := by
    ext1 U
    simp only [comp_app, PresheafOfModulesOfCommRing.whiskerLeft_app, restrictScalars_map_app]
    exact μ_natural_right (restrictScalarsAt φ U) (M.obj U) (f.app U)
  associativity M N P := by
    ext1 U
    simp only [comp_app, PresheafOfModulesOfCommRing.whiskerRight_app,
      PresheafOfModulesOfCommRing.whiskerLeft_app, restrictScalars_map_app,
      PresheafOfModulesOfCommRing.associator_hom_app]
    exact associativity (restrictScalarsAt φ U) (M.obj U) (N.obj U) (P.obj U)
  left_unitality M := by
    ext1 U
    simp only [comp_app, PresheafOfModulesOfCommRing.whiskerRight_app, restrictScalars_map_app,
      PresheafOfModulesOfCommRing.leftUnitor_hom_app]
    exact left_unitality (restrictScalarsAt φ U) (M.obj U)
  right_unitality M := by
    ext1 U
    simp only [comp_app, PresheafOfModulesOfCommRing.whiskerLeft_app, restrictScalars_map_app,
      PresheafOfModulesOfCommRing.rightUnitor_hom_app]
    exact right_unitality (restrictScalarsAt φ U) (M.obj U)
instance

pushforward_laxMonoidal

L126 ↗
PresheafOfModules.pushforward_laxMonoidal
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
section pushforward
variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D)
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
Lean source · statement
instance pushforward_laxMonoidal :
    (pushforward (R := R ⋙ forget₂ _ _) (ringCatHom φ)).LaxMonoidal
instance

pullback_oplaxMonoidal

L131 ↗
PresheafOfModules.pullback_oplaxMonoidal
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
section pushforward
variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D)
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
Lean source · statement
instance pullback_oplaxMonoidal
    [(pushforward (R := R ⋙ forget₂ _ _) (ringCatHom φ)).IsRightAdjoint] :
    (pullback (R := R ⋙ forget₂ _ _) (ringCatHom φ)).OplaxMonoidal
lemma

isIso_app_of_isColimit

L142 ↗
CategoryTheory.Limits.isIso_app_of_isColimit
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace CategoryTheory.Limits
Lean source · statement
lemma isIso_app_of_isColimit {𝒜 : Type*} [Category 𝒜] {ℬ : Type*} [Category ℬ]
    {J : Type*} [Category J] {H₁ H₂ : 𝒜 ⥤ ℬ} (τ : H₁ ⟶ H₂) {K : J ⥤ 𝒜} {c : Cocone K}
    (hc : IsColimit c) [PreservesColimit K H₁] [PreservesColimit K H₂]
    (h : ∀ j, IsIso (τ.app (K.obj j))) : IsIso (τ.app c.pt)
lemma

freeObj_map_freeMk

L176 ↗
PresheafOfModules.freeObj_map_freeMk
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
Lean source · statement
lemma freeObj_map_freeMk (T : Cᵒᵖ ⥤ Type u) {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : T.obj X) :
    (freeObj (R := R') T).map f (ModuleCat.freeMk x) = ModuleCat.freeMk (T.map f x)
def

freeεIso

L186 ↗
PresheafOfModules.freeεIso
Documentation

The isomorphism from the module-presheaf tensor unit to the free presheaf on the type-valued tensor unit.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
Lean source · statement
def freeεIso :
    𝟙_ (PresheafOfModules.{u} R') ≅ (free R').obj (𝟙_ (Cᵒᵖ ⥤ Type u))
def

freeμIso

L209 ↗
PresheafOfModules.freeμIso
Documentation

The isomorphism identifying the tensor product of free module presheaves with the free presheaf on their product.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
Lean source · statement
def freeμIso (F G : Cᵒᵖ ⥤ Type u) :
    (free R').obj F ⊗ (free R').obj G ≅ (free R').obj (F ⊗ G)
lemma

freeμIso_hom_app

L229 ↗
PresheafOfModules.freeμIso_hom_app
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
Lean source · statement
lemma freeμIso_hom_app (F G : Cᵒᵖ ⥤ Type u) (X : Cᵒᵖ) :
    (freeμIso (R := R) F G).hom.app X =
      (ModuleCat.FreeMonoidal.μIso (R.obj X) (F.obj X) (G.obj X)).hom
lemma

freeεIso_hom_app

L232 ↗
PresheafOfModules.freeεIso_hom_app
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
Lean source · statement
lemma freeεIso_hom_app (X : Cᵒᵖ) :
    (freeεIso (R := R)).hom.app X = (ModuleCat.FreeMonoidal.εIso (R.obj X)).hom
instance

free_monoidal

L235 ↗
PresheafOfModules.free_monoidal
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
Lean source · statement
instance free_monoidal : (free R').Monoidal
abbrev

pf

L290 ↗
PresheafOfModules.PullbackMonoidal.pf
Documentation

The pushforward functor on module presheaves along F and the ring-presheaf morphism.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
abbrev pf : PresheafOfModules.{u} R' ⥤ PresheafOfModules.{u} S'
abbrev

pb

L294 ↗
PresheafOfModules.PullbackMonoidal.pb
Documentation

The pullback functor on module presheaves along F and the ring-presheaf morphism.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
abbrev pb : PresheafOfModules.{u} S' ⥤ PresheafOfModules.{u} R'
abbrev

adj

L298 ↗
PresheafOfModules.PullbackMonoidal.adj
Documentation

The pullback-pushforward adjunction on module presheaves.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
abbrev adj : pb F φ ⊣ pf F φ
abbrev

gS

L301 ↗
PresheafOfModules.PullbackMonoidal.gS
Documentation

The free module presheaf on a representable presheaf on the source category.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
abbrev gS (U : C) : PresheafOfModules.{u} S'
abbrev

gR

L303 ↗
PresheafOfModules.PullbackMonoidal.gR
Documentation

The free module presheaf on a representable presheaf on the target category.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
abbrev gR (V : D) : PresheafOfModules.{u} R'
abbrev

h₂

L307 ↗
PresheafOfModules.PullbackMonoidal.h₂
Documentation

The corepresentation of pushforward maps out of a free representable by the corresponding target free representable.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
abbrev h₂ (U : C) :
    (pf F φ ⋙ coyoneda.obj (op (gS U))).CorepresentableBy (gR (F.obj U))
def

u₂

L312 ↗
PresheafOfModules.PullbackMonoidal.u₂
Documentation

The universal map into the pushforward of the corresponding target free representable.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
def u₂ (U : C) : gS U ⟶ (pf F φ).obj (gR (F.obj U))
lemma

freeYonedaEquiv_apply'

L316 ↗
PresheafOfModules.PullbackMonoidal.freeYonedaEquiv_apply'
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
omit [HasFiniteProducts C] [HasFiniteProducts D] [PreservesFiniteProducts F] in
Lean source · statement
lemma freeYonedaEquiv_apply' {M : PresheafOfModules.{u} S'} {X : C}
    (f : gS X ⟶ M) : freeYonedaEquiv f = f.app (op X) (ModuleCat.freeMk (𝟙 X))
lemma

gS_map_freeMk

L320 ↗
PresheafOfModules.PullbackMonoidal.gS_map_freeMk
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
omit [HasFiniteProducts C] [HasFiniteProducts D] [PreservesFiniteProducts F] in
Lean source · statement
lemma gS_map_freeMk {U W W' : C} (a : W ⟶ U) (b : W' ⟶ W) :
    (gS (S := S) U).map b.op (ModuleCat.freeMk a) = ModuleCat.freeMk (b ≫ a)
lemma

gR_map_freeMk

L325 ↗
PresheafOfModules.PullbackMonoidal.gR_map_freeMk
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
omit [HasFiniteProducts C] [HasFiniteProducts D] [PreservesFiniteProducts F] in
Lean source · statement
lemma gR_map_freeMk {U W W' : D} (a : W ⟶ U) (b : W' ⟶ W) :
    (gR (R := R) U).map b.op (ModuleCat.freeMk a) = ModuleCat.freeMk (b ≫ a)
lemma

free_map_app_freeMk

L330 ↗
PresheafOfModules.PullbackMonoidal.free_map_app_freeMk
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
omit [HasFiniteProducts C] [HasFiniteProducts D] [PreservesFiniteProducts F] in
Lean source · statement
lemma free_map_app_freeMk {E : Type u} [SmallCategory E] {T : Eᵒᵖ ⥤ CommRingCat.{u}}
    {P Q : Eᵒᵖ ⥤ Type u} (ψ : P ⟶ Q) (X : Eᵒᵖ) (x : P.obj X) :
    ((free (T ⋙ forget₂ CommRingCat RingCat)).map ψ).app X (ModuleCat.freeMk x) =
      (ModuleCat.freeMk (ψ.app X x) : ((free (T ⋙ forget₂ CommRingCat RingCat)).obj Q).obj X)
lemma

freeμIso_inv_app_freeMk

L337 ↗
PresheafOfModules.PullbackMonoidal.freeμIso_inv_app_freeMk
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
omit [HasFiniteProducts C] [HasFiniteProducts D] [PreservesFiniteProducts F] in
Lean source · statement
lemma freeμIso_inv_app_freeMk {E : Type u} [SmallCategory E] {T : Eᵒᵖ ⥤ CommRingCat.{u}}
    (P Q : Eᵒᵖ ⥤ Type u) (X : Eᵒᵖ) (z : (P ⊗ Q).obj X) :
    (freeμIso (R := T) P Q).inv.app X (ModuleCat.freeMk z) =
      (ModuleCat.freeMk z.1 ⊗ₜ[T.obj X] ModuleCat.freeMk z.2 :
        (((free (T ⋙ forget₂ CommRingCat RingCat)).obj P).obj X ⊗
          ((free (T ⋙ forget₂ CommRingCat RingCat)).obj Q).obj X :))
lemma

tensorHom_app_tmul

L346 ↗
PresheafOfModules.PullbackMonoidal.tensorHom_app_tmul
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
omit [HasFiniteProducts C] [HasFiniteProducts D] [PreservesFiniteProducts F] in
Lean source · full declaration
lemma tensorHom_app_tmul {E : Type u} [SmallCategory E] {T : Eᵒᵖ ⥤ CommRingCat.{u}}
    {M₁ M₂ M₃ M₄ : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)}
    (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄) (X : Eᵒᵖ) (m : M₁.obj X) (n : M₃.obj X) :
    DFunLike.coe (α := (M₁.obj X ⊗ M₃.obj X :)) (β := fun _ => (M₂.obj X ⊗ M₄.obj X :))
      ((f ⊗ₘ g).app X).hom (m ⊗ₜ[T.obj X] n) = f.app X m ⊗ₜ[T.obj X] g.app X n := by
  exact ModuleCat.MonoidalCategory.tensorHom_tmul _ _ _ _
lemma

u₂_app_freeMk

L354 ↗
PresheafOfModules.PullbackMonoidal.u₂_app_freeMk
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
omit [HasFiniteProducts C] [HasFiniteProducts D] [PreservesFiniteProducts F] in
Lean source · statement
lemma u₂_app_freeMk (U : C) {W : C} (a : W ⟶ U) :
    (u₂ F φ U).app (op W) (ModuleCat.freeMk a) =
      (ModuleCat.freeMk (F.map a) : (gR (R := R) (F.obj U)).obj (op (F.obj W)))
def

e

L368 ↗
PresheafOfModules.PullbackMonoidal.e
Documentation

The pullback comparison isomorphism for the free presheaf on a representable.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · full declaration
def e (U : C) : (pb F φ).obj (gS U) ≅ gR (F.obj U) where
  hom := ((adj F φ).homEquiv _ _).symm (u₂ F φ U)
  inv := (h₂ F φ U).homEquiv.symm ((adj F φ).unit.app (gS U))
  hom_inv_id := ((adj F φ).homEquiv _ _).injective (by
    rw [Adjunction.homEquiv_naturality_right, Equiv.apply_symm_apply]
    have := (h₂ F φ U).homEquiv_comp ((h₂ F φ U).homEquiv.symm ((adj F φ).unit.app (gS U))) (𝟙 _)
    rw [Category.id_comp, Equiv.apply_symm_apply] at this
    erw [Adjunction.homEquiv_unit, CategoryTheory.Functor.map_id, Category.comp_id]
    exact this.symm)
  inv_hom_id := (h₂ F φ U).homEquiv.injective (by
    rw [(h₂ F φ U).homEquiv_comp, Equiv.apply_symm_apply]
    change (adj F φ).unit.app (gS U) ≫ (pf F φ).map (((adj F φ).homEquiv _ _).symm (u₂ F φ U)) =
      (h₂ F φ U).homEquiv (𝟙 _)
    erw [← (adj F φ).homEquiv_unit, Equiv.apply_symm_apply]
    rfl)
lemma

unit_comp_map_e_hom

L385 ↗
PresheafOfModules.PullbackMonoidal.unit_comp_map_e_hom
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
omit [HasFiniteProducts C] [HasFiniteProducts D] [PreservesFiniteProducts F] in
Lean source · statement
lemma unit_comp_map_e_hom (U : C) :
    (adj F φ).unit.app (gS U) ≫ (pf F φ).map (e F φ U).hom = u₂ F φ U
def

yonedaTensorIso

L392 ↗
PresheafOfModules.PullbackMonoidal.yonedaTensorIso
Documentation

The Yoneda comparison identifying the product of representable presheaves with the representable of the product.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
def yonedaTensorIso {E : Type u} [SmallCategory E] [HasFiniteProducts E] (U V : E) :
    yoneda.obj U ⊗ yoneda.obj V ≅ yoneda.obj (U ⨯ V)
lemma

yonedaTensorIso_inv_app_apply

L406 ↗
PresheafOfModules.PullbackMonoidal.yonedaTensorIso_inv_app_apply
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
lemma yonedaTensorIso_inv_app_apply {E : Type u} [SmallCategory E] [HasFiniteProducts E] (U V : E)
    {W : E} (c : W ⟶ U ⨯ V) :
    (yonedaTensorIso U V).inv.app (op W) c = (c ≫ prod.fst, c ≫ prod.snd)
def

tensorUnitIso

L412 ↗
PresheafOfModules.PullbackMonoidal.tensorUnitIso
Documentation

The identification of the type-valued tensor unit with the representable of the terminal object.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
def tensorUnitIso (E : Type u) [SmallCategory E] [HasFiniteProducts E] :
    𝟙_ (Eᵒᵖ ⥤ Type u) ≅ yoneda.obj (⊤_ E)
def

j

L423 ↗
PresheafOfModules.PullbackMonoidal.j
Documentation

The tensor comparison from source free representables to the free representable of their product.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
def j (U V : C) : gS (S := S) U ⊗ gS V ≅ gS (U ⨯ V)
def

j₀

L427 ↗
PresheafOfModules.PullbackMonoidal.j₀
Documentation

The tensor-unit comparison with the source free representable of the terminal object.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
def j₀ : 𝟙_ (PresheafOfModules.{u} S') ≅ gS (S := S) (⊤_ C)
def

r

L431 ↗
PresheafOfModules.PullbackMonoidal.r
Documentation

The target free-representable tensor comparison induced by preservation of binary products.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
def r (U V : C) : gR (R := R) (F.obj (U ⨯ V)) ≅ gR (F.obj U) ⊗ gR (F.obj V)
def

r₀

L438 ↗
PresheafOfModules.PullbackMonoidal.r₀
Documentation

The target free-representable tensor-unit comparison induced by preservation of the terminal object.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
def r₀ : gR (R := R) (F.obj (⊤_ C)) ≅ 𝟙_ _
lemma

pf_μ_app_tmul

L443 ↗
PresheafOfModules.PullbackMonoidal.pf_μ_app_tmul
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
omit [HasFiniteProducts C] [HasFiniteProducts D] [PreservesFiniteProducts F] in
Lean source · full declaration
lemma pf_μ_app_tmul (M N : PresheafOfModules.{u} R') (W : C)
    (m : M.obj (op (F.obj W))) (n : N.obj (op (F.obj W))) :
    DFunLike.coe (α := (((pf F φ).obj M).obj (op W) ⊗ ((pf F φ).obj N).obj (op W) :))
      (β := fun _ => ((pf F φ).obj (M ⊗ N)).obj (op W))
      ((μ (pf F φ) M N).app (op W)).hom ((show ((pf F φ).obj M).obj (op W) from m) ⊗ₜ[S.obj (op W)]
        (show ((pf F φ).obj N).obj (op W) from n)) = m ⊗ₜ[R.obj (op (F.obj W))] n := by
  change DFunLike.coe (α := (((pf F φ).obj M).obj (op W) ⊗ ((pf F φ).obj N).obj (op W) :))
      (β := fun _ => ((pf F φ).obj (M ⊗ N)).obj (op W))
    ((μ (restrictScalars (ringCatHom (R := F.op ⋙ R) φ))
        ((pushforward₀OfCommRingCat F R).obj M) ((pushforward₀OfCommRingCat F R).obj N) ≫
      (restrictScalars (ringCatHom (R := F.op ⋙ R) φ)).map
        (μ (pushforward₀OfCommRingCat F R) M N)).app (op W)).hom ((show ((pf F φ).obj M).obj (op W)
          from m) ⊗ₜ[S.obj (op W)]
        (show ((pf F φ).obj N).obj (op W) from n)) = _
  erw [show μ (pushforward₀OfCommRingCat F R) M N = 𝟙 _ from rfl, CategoryTheory.Functor.map_id,
    Category.comp_id]
  exact ModuleCat.restrictScalars_μ_tmul (S := R.obj (op (F.obj W))) _ _ _ m n
lemma

keyL

L462 ↗
PresheafOfModules.PullbackMonoidal.keyL
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
omit [HasFiniteProducts D] [PreservesFiniteProducts F] in
Lean source · statement
lemma keyL (U V : C) :
    ((j (S := S) U V).inv ≫ ((u₂ F φ U ⊗ₘ u₂ F φ V) ≫
      μ (pf F φ) (gR (F.obj U)) (gR (F.obj V)))).app (op (U ⨯ V)) (ModuleCat.freeMk (𝟙 (U ⨯ V))) =
    (ModuleCat.freeMk (F.map prod.fst) ⊗ₜ[R.obj (op (F.obj (U ⨯ V)))]
      ModuleCat.freeMk (F.map prod.snd) :
      ((gR (R := R) (F.obj U)).obj (op (F.obj (U ⨯ V))) ⊗
        (gR (R := R) (F.obj V)).obj (op (F.obj (U ⨯ V))) :))
lemma

keyR

L481 ↗
PresheafOfModules.PullbackMonoidal.keyR
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
lemma keyR (U V : C) :
    (u₂ F φ (U ⨯ V) ≫ (pf F φ).map (r (R := R) F U V).hom).app (op (U ⨯ V))
      (ModuleCat.freeMk (𝟙 (U ⨯ V))) =
    (ModuleCat.freeMk (F.map prod.fst) ⊗ₜ[R.obj (op (F.obj (U ⨯ V)))]
      ModuleCat.freeMk (F.map prod.snd) :
      ((gR (R := R) (F.obj U)).obj (op (F.obj (U ⨯ V))) ⊗
        (gR (R := R) (F.obj V)).obj (op (F.obj (U ⨯ V))) :))
lemma

key_δ

L505 ↗
PresheafOfModules.PullbackMonoidal.key_δ
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
lemma key_δ (U V : C) :
    (j (S := S) U V).inv ≫ ((u₂ F φ U ⊗ₘ u₂ F φ V) ≫
      μ (pf F φ) (gR (F.obj U)) (gR (F.obj V))) =
      u₂ F φ (U ⨯ V) ≫ (pf F φ).map (r (R := R) F U V).hom
lemma

δ_gS_comp

L512 ↗
PresheafOfModules.PullbackMonoidal.δ_gS_comp
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
lemma δ_gS_comp (U V : C) :
    δ (pb F φ) (gS U) (gS V) ≫ ((e F φ U).hom ⊗ₘ (e F φ V).hom) =
      (pb F φ).map (j (S := S) U V).hom ≫ (e F φ (U ⨯ V)).hom ≫ (r (R := R) F U V).hom
instance

isIso_δ_gS

L525 ↗
PresheafOfModules.PullbackMonoidal.isIso_δ_gS
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
instance isIso_δ_gS (U V : C) : IsIso (δ (pb F φ) (gS U) (gS V))
lemma

isIso_app_of_freeYoneda

L534 ↗
PresheafOfModules.PullbackMonoidal.isIso_app_of_freeYoneda
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
omit [HasFiniteProducts C] [HasFiniteProducts D] [PreservesFiniteProducts F] in
Lean source · statement
lemma isIso_app_of_freeYoneda {ℬ : Type*} [Category ℬ]
    {H₁ H₂ : PresheafOfModules.{u} S' ⥤ ℬ}
    [PreservesColimitsOfSize.{u, u} H₁] [PreservesColimitsOfSize.{u, u} H₂] (τ : H₁ ⟶ H₂)
    (h : ∀ U : C, IsIso (τ.app (gS U))) (M : PresheafOfModules.{u} S') : IsIso (τ.app M)
instance

(anonymous instance)

L546 ↗
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
instance : PreservesColimitsOfSize.{u, u} (pb F φ)
instance

isIso_δ

L548 ↗
PresheafOfModules.PullbackMonoidal.isIso_δ
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
instance isIso_δ (A B : PresheafOfModules.{u} S') : IsIso (δ (pb F φ) A B)
lemma

keyL₀

L560 ↗
PresheafOfModules.PullbackMonoidal.keyL₀
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
omit [HasFiniteProducts D] [PreservesFiniteProducts F] in
Lean source · statement
lemma keyL₀ : ((j₀ (S := S)).inv ≫ ε (pf F φ)).app (op (⊤_ C))
      (ModuleCat.freeMk (𝟙 (⊤_ C))) = (1 : R.obj (op (F.obj (⊤_ C))))
lemma

keyR₀

L574 ↗
PresheafOfModules.PullbackMonoidal.keyR₀
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
lemma keyR₀ : (u₂ F φ (⊤_ C) ≫ (pf F φ).map (r₀ (R := R) F).hom).app (op (⊤_ C))
      (ModuleCat.freeMk (𝟙 (⊤_ C))) = (1 : R.obj (op (F.obj (⊤_ C))))
lemma

key_η

L587 ↗
PresheafOfModules.PullbackMonoidal.key_η
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
lemma key_η : (j₀ (S := S)).inv ≫ ε (pf F φ) = u₂ F φ (⊤_ C) ≫ (pf F φ).map (r₀ (R := R) F).hom
lemma

η_eq

L592 ↗
PresheafOfModules.PullbackMonoidal.η_eq
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
lemma η_eq : η (pb F φ) = (pb F φ).map (j₀ (S := S)).hom ≫ (e F φ (⊤_ C)).hom ≫ (r₀ (R := R) F).hom
instance

isIso_η

L601 ↗
PresheafOfModules.PullbackMonoidal.isIso_η
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
instance isIso_η : IsIso (η (pb F φ))
instance

pullback_monoidal

L603 ↗
PresheafOfModules.PullbackMonoidal.pullback_monoidal
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
namespace PullbackMonoidal

-- Match Mathlib's instance comparison for presheaf tensor products over a
-- commutative ring viewed through `forget₂ CommRingCat RingCat`.
open Opposite Functor.LaxMonoidal Functor.OplaxMonoidal
variable {C D : Type u} [SmallCategory C] [SmallCategory D]
  [HasFiniteProducts C] [HasFiniteProducts D]
  (F : C ⥤ D) [PreservesFiniteProducts F]
  {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R)
local notation "R'" => R ⋙ forget₂ CommRingCat RingCat
local notation "S'" => S ⋙ forget₂ CommRingCat RingCat
Lean source · statement
instance pullback_monoidal : (pb F φ).Monoidal
instance

pullback_monoidal'

L607 ↗
PresheafOfModules.pullback_monoidal'
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u v₁ u₁ v₂ u₂
open CategoryTheory MonoidalCategory Limits Functor.LaxMonoidal Functor.OplaxMonoidal
local instance PresheafOfModules.PullbackMonoidal.commRingAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u}) (X : Eᵒᵖ) :
    CommRing ((T ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (T.obj X))
local instance PresheafOfModules.PullbackMonoidal.moduleAt {E : Type u₁} [Category.{v₁} E]
    (T : Eᵒᵖ ⥤ CommRingCat.{u})
    (M : PresheafOfModules.{u} (T ⋙ forget₂ CommRingCat RingCat)) (X : Eᵒᵖ) :
    Module (T.obj X) (M.obj X) := (M.obj X).isModule
namespace PresheafOfModules
Lean source · statement
instance pullback_monoidal' {C D : Type u} [SmallCategory C] [SmallCategory D]
    [HasFiniteProducts C] [HasFiniteProducts D] (F : C ⥤ D) [PreservesFiniteProducts F]
    {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R) :
    (pullback (R := R ⋙ forget₂ _ _) (ringCatHom φ)).Monoidal

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.