NYLL
Module

SheafOfModules_MonoidalV2.lean

Nyll.AlgebraicCurves.Foundations.Algebra.SheafOfModules_MonoidalV2
22 declarations indexed from sourceView source ↗

Module documentation

Tensor and internal hom comparisons for module sheaves

Relates tensor products and internal hom constructions for sheaves of modules.

Imports2
Imported by17

Declarations

def

toPresheafHom

L39 ↗
PresheafOfModules.InternalHom.toPresheafHom
Source context 8 commands

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

section InlinedTheorems
section LinkageInlined_5b3a613b
universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
noncomputable section
namespace PresheafOfModules
namespace InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
Lean source · full declaration
def toPresheafHom (X : Cᵒᵖ) (φ : naturalFamilies F N X) :
    (presheafHom F.presheaf N.presheaf).obj X where
  app Y := AddCommGrpCat.ofHom (φ.1 Y.unop.hom.op).toAddMonoidHom
  naturality {Y Y'} k := by
    ext x
    change φ.1 Y'.unop.hom.op (F.map k.unop.left.op x) = N.map k.unop.left.op (φ.1 Y.unop.hom.op x)
    rw [φ.2 Y.unop.hom.op k.unop.left.op x]
    exact congr_app φ (by rw [← op_comp, Over.w]) _
abbrev

appAt

L49 ↗
PresheafOfModules.InternalHom.appAt
Source context 9 commands

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

section InlinedTheorems
section LinkageInlined_5b3a613b
universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
noncomputable section
namespace PresheafOfModules
namespace InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · statement
abbrev appAt {X : Cᵒᵖ} (s : (presheafHom F.presheaf N.presheaf).obj X) (Y : (Over X.unop)ᵒᵖ)
    (x : F.obj (Opposite.op Y.unop.left)) : N.obj (Opposite.op Y.unop.left)
lemma

appAt_toPresheafHom

L53 ↗
PresheafOfModules.InternalHom.appAt_toPresheafHom
Source context 9 commands

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

section InlinedTheorems
section LinkageInlined_5b3a613b
universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
noncomputable section
namespace PresheafOfModules
namespace InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · statement
lemma appAt_toPresheafHom (X : Cᵒᵖ) (φ : naturalFamilies F N X) (Y : (Over
  X.unop)ᵒᵖ)
    (x : F.obj (Opposite.op Y.unop.left)) :
    appAt (toPresheafHom F N X φ) Y x = φ.1 Y.unop.hom.op x
def

linearSub

L58 ↗
PresheafOfModules.InternalHom.linearSub
Source context 9 commands

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

section InlinedTheorems
section LinkageInlined_5b3a613b
universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
noncomputable section
namespace PresheafOfModules
namespace InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · full declaration
def linearSub : Subfunctor (presheafHom F.presheaf N.presheaf) where
  obj X := { s | ∀ (Y : (Over X.unop)ᵒᵖ) (r : R.obj (Opposite.op Y.unop.left))
    (x : F.obj (Opposite.op Y.unop.left)), appAt s Y (r • x) = r • appAt s Y x }
  map h _ hs Y r x := hs (Opposite.op ((Over.map h.unop).obj Y.unop)) r x
def

ofPresheafHom

L63 ↗
PresheafOfModules.InternalHom.ofPresheafHom
Source context 9 commands

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

section InlinedTheorems
section LinkageInlined_5b3a613b
universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
noncomputable section
namespace PresheafOfModules
namespace InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · statement
def ofPresheafHom (X : Cᵒᵖ) (s : (linearSub F N).obj X) : naturalFamilies
  F N X
lemma

ofPresheafHom_app

L75 ↗
PresheafOfModules.InternalHom.ofPresheafHom_app
Source context 9 commands

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

section InlinedTheorems
section LinkageInlined_5b3a613b
universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
noncomputable section
namespace PresheafOfModules
namespace InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · statement
lemma ofPresheafHom_app (X : Cᵒᵖ) (s : (linearSub F N).obj X) {Y : Cᵒᵖ} (f : X ⟶ Y)
    (x : F.obj Y) :
    (ofPresheafHom F N X s).1 f x = appAt s.1 (Opposite.op (Over.mk f.unop)) x
def

equivLinearSub

L79 ↗
PresheafOfModules.InternalHom.equivLinearSub
Source context 9 commands

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

section InlinedTheorems
section LinkageInlined_5b3a613b
universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
noncomputable section
namespace PresheafOfModules
namespace InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · full declaration
def equivLinearSub (X : Cᵒᵖ) : naturalFamilies F N X ≃ (linearSub F N).obj
  X where
  toFun φ := ⟨toPresheafHom F N X φ, fun Y r x => (φ.1 Y.unop.hom.op).map_smul r x⟩
  invFun s := ofPresheafHom F N X s
  left_inv φ := by
    apply naturalFamilies_ext; intro Y f x; rfl
  right_inv s := by rfl
def

isoLinearSub

L87 ↗
PresheafOfModules.InternalHom.isoLinearSub
Source context 9 commands

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

section InlinedTheorems
section LinkageInlined_5b3a613b
universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
noncomputable section
namespace PresheafOfModules
namespace InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · statement
def isoLinearSub :
    InternalHom.presheaf F N ⋙ forget AddCommGrpCat ≅ (linearSub F N).toFunctor
lemma

linearSub_local

L93 ↗
PresheafOfModules.InternalHom.linearSub_local
Source context 10 commands

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

section InlinedTheorems
section LinkageInlined_5b3a613b
universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
noncomputable section
namespace PresheafOfModules
namespace InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
variable {F N}
Lean source · statement
lemma linearSub_local {J : GrothendieckTopology C}
    (hNsep : Presieve.IsSeparated J (N.presheaf ⋙ forget AddCommGrpCat))
    (X : Cᵒᵖ) (s : (presheafHom F.presheaf N.presheaf).obj X)
    (hs : (linearSub F N).sieveOfSection s ∈ J X.unop) : s ∈ (linearSub F N).obj X
theorem

isSheaf_ihomObj_loc

L123 ↗
PresheafOfModules.isSheaf_ihomObj_loc
Source context 4 commands

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

section InlinedTheorems
section LinkageInlined_5b3a613b
universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
Lean source · statement
theorem PresheafOfModules.isSheaf_ihomObj_loc {C : Type u} [Category.{u} C]
    {R : Cᵒᵖ ⥤ CommRingCat.{u}} (F N : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
    {J : GrothendieckTopology C} (hN : Presheaf.IsSheaf J N.presheaf) :
    Presheaf.IsSheaf J (PresheafOfModules.ihomObj F N).presheaf
abbrev

PMod

L157 ↗
PresheafOfModules.IsMonoidalW.PMod
Source context 7 commands

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

section InlinedTheorems
section LinkageInlined_68107509
universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace PresheafOfModules.IsMonoidalW
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (R : Sheaf J RingCat.{u})
  (α : 𝒪 ⋙ forget₂ CommRingCat RingCat ⟶ R.obj)
  [Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
abbrev PMod
abbrev

W

L159 ↗
PresheafOfModules.IsMonoidalW.W
Source context 7 commands

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

section InlinedTheorems
section LinkageInlined_68107509
universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace PresheafOfModules.IsMonoidalW
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (R : Sheaf J RingCat.{u})
  (α : 𝒪 ⋙ forget₂ CommRingCat RingCat ⟶ R.obj)
  [Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
abbrev W : MorphismProperty (PMod 𝒪)
abbrev

shf

L163 ↗
PresheafOfModules.IsMonoidalW.shf
Source context 7 commands

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

section InlinedTheorems
section LinkageInlined_68107509
universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace PresheafOfModules.IsMonoidalW
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (R : Sheaf J RingCat.{u})
  (α : 𝒪 ⋙ forget₂ CommRingCat RingCat ⟶ R.obj)
  [Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
abbrev shf : PMod 𝒪 ⥤ SheafOfModules.{u} R
abbrev

inc

L165 ↗
PresheafOfModules.IsMonoidalW.inc
Source context 7 commands

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

section InlinedTheorems
section LinkageInlined_68107509
universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace PresheafOfModules.IsMonoidalW
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (R : Sheaf J RingCat.{u})
  (α : 𝒪 ⋙ forget₂ CommRingCat RingCat ⟶ R.obj)
  [Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
abbrev inc : SheafOfModules.{u} R ⥤ PMod 𝒪
abbrev

adj

L168 ↗
PresheafOfModules.IsMonoidalW.adj
Source context 7 commands

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

section InlinedTheorems
section LinkageInlined_68107509
universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace PresheafOfModules.IsMonoidalW
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (R : Sheaf J RingCat.{u})
  (α : 𝒪 ⋙ forget₂ CommRingCat RingCat ⟶ R.obj)
  [Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
abbrev adj : shf 𝒪 R α ⊣ inc 𝒪 R α
instance

(anonymous instance)

L170 ↗
Source context 7 commands

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

section InlinedTheorems
section LinkageInlined_68107509
universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace PresheafOfModules.IsMonoidalW
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (R : Sheaf J RingCat.{u})
  (α : 𝒪 ⋙ forget₂ CommRingCat RingCat ⟶ R.obj)
  [Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
instance : (inc 𝒪 R α).Faithful
instance

(anonymous instance)

L171 ↗
Source context 8 commands

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

section InlinedTheorems
section LinkageInlined_68107509
universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace PresheafOfModules.IsMonoidalW
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (R : Sheaf J RingCat.{u})
  (α : 𝒪 ⋙ forget₂ CommRingCat RingCat ⟶ R.obj)
  [Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
private local instance : (inc 𝒪 R α).Faithful := (adj 𝒪 R α).fullyFaithfulROfIsIsoCounit.faithful
Lean source · statement
instance : (inc 𝒪 R α).Full
lemma

W_eq

L173 ↗
PresheafOfModules.IsMonoidalW.W_eq
Source context 9 commands

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

section InlinedTheorems
section LinkageInlined_68107509
universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace PresheafOfModules.IsMonoidalW
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (R : Sheaf J RingCat.{u})
  (α : 𝒪 ⋙ forget₂ CommRingCat RingCat ⟶ R.obj)
  [Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
private local instance : (inc 𝒪 R α).Faithful := (adj 𝒪 R α).fullyFaithfulROfIsIsoCounit.faithful
private local instance : (inc 𝒪 R α).Full := (adj 𝒪 R α).fullyFaithfulROfIsIsoCounit.full
Lean source · statement
lemma W_eq : W (J := J) 𝒪 = (MorphismProperty.isomorphisms _).inverseImage (shf 𝒪 R α)
lemma

isIso_unit_app_of_isSheaf

L176 ↗
PresheafOfModules.IsMonoidalW.isIso_unit_app_of_isSheaf
Source context 9 commands

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

section InlinedTheorems
section LinkageInlined_68107509
universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace PresheafOfModules.IsMonoidalW
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (R : Sheaf J RingCat.{u})
  (α : 𝒪 ⋙ forget₂ CommRingCat RingCat ⟶ R.obj)
  [Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
private local instance : (inc 𝒪 R α).Faithful := (adj 𝒪 R α).fullyFaithfulROfIsIsoCounit.faithful
private local instance : (inc 𝒪 R α).Full := (adj 𝒪 R α).fullyFaithfulROfIsIsoCounit.full
Lean source · statement
lemma isIso_unit_app_of_isSheaf (N : PMod 𝒪) (hN : Presheaf.IsSheaf J N.presheaf) :
    IsIso ((adj 𝒪 R α).unit.app N)
lemma

isIso_shf_map_unit_whiskerRight

L183 ↗
PresheafOfModules.IsMonoidalW.isIso_shf_map_unit_whiskerRight
Source context 9 commands

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

section InlinedTheorems
section LinkageInlined_68107509
universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace PresheafOfModules.IsMonoidalW
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (R : Sheaf J RingCat.{u})
  (α : 𝒪 ⋙ forget₂ CommRingCat RingCat ⟶ R.obj)
  [Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
private local instance : (inc 𝒪 R α).Faithful := (adj 𝒪 R α).fullyFaithfulROfIsIsoCounit.faithful
private local instance : (inc 𝒪 R α).Full := (adj 𝒪 R α).fullyFaithfulROfIsIsoCounit.full
Lean source · statement
lemma isIso_shf_map_unit_whiskerRight (d d' : PMod 𝒪) :
    IsIso ((shf 𝒪 R α).map (((adj 𝒪 R α).unit.app d) ▷ d'))
lemma

W_whiskerRight

L192 ↗
PresheafOfModules.IsMonoidalW.W_whiskerRight
Source context 10 commands

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

section InlinedTheorems
section LinkageInlined_68107509
universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace PresheafOfModules.IsMonoidalW
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (R : Sheaf J RingCat.{u})
  (α : 𝒪 ⋙ forget₂ CommRingCat RingCat ⟶ R.obj)
  [Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
private local instance : (inc 𝒪 R α).Faithful := (adj 𝒪 R α).fullyFaithfulROfIsIsoCounit.faithful
private local instance : (inc 𝒪 R α).Full := (adj 𝒪 R α).fullyFaithfulROfIsIsoCounit.full
include R α in
Lean source · statement
lemma W_whiskerRight {d₁ d₂ : PMod 𝒪} (g : d₁ ⟶ d₂) (hg : W (J := J) 𝒪 g) (d' : PMod 𝒪) :
    W (J := J) 𝒪 (g ▷ d')
theorem

isMonoidal_inverseImage_W_toPresheaf_loc

L217 ↗
PresheafOfModules.isMonoidal_inverseImage_W_toPresheaf_loc
Source context 5 commands

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

section InlinedTheorems
section LinkageInlined_68107509
universe u
open CategoryTheory MonoidalCategory Limits
open PresheafOfModules.IsMonoidalW in
Lean source · full declaration
theorem PresheafOfModules.isMonoidal_inverseImage_W_toPresheaf_loc {C : Type u}
  [Category.{u} C] {J : GrothendieckTopology C}
    (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (R : Sheaf J RingCat.{u})
    (α : 𝒪 ⋙ forget₂ CommRingCat RingCat ⟶ R.obj)
    [Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
    [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}] :
    ((J.W (A := AddCommGrpCat.{u})).inverseImage
      (PresheafOfModules.toPresheaf (𝒪 ⋙ forget₂ CommRingCat RingCat))).IsMonoidal where
  whiskerRight g hg d' := W_whiskerRight 𝒪 R α g hg d'
  whiskerLeft d g₁ g₂ g hg :=
    ((W (J := J) 𝒪).arrow_mk_iso_iff (Arrow.isoMk' (g ▷ d) (d ◁ g) (β_ g₁ d) (β_ g₂ d)
      (BraidedCategory.braiding_naturality_left g d).symm)).1 (W_whiskerRight 𝒪 R α g hg d)

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