NYLL
Module

SheafificationMonoidal.lean

Nyll.SchemeTheory.Modules.SheafificationMonoidal
12 declarations indexed from sourceView source ↗

Module documentation

Tensor compatibility of module sheafification equivalences

For a locally bijective morphism of ring presheaves, the module-presheaf morphisms whose underlying additive presheaf maps are sheafification equivalences form a monoidal morphism property. The proof uses the internal-Hom adjunction and the sheafification adjunction.

Imports5
Imported by33

Declarations

abbrev

PMod

L53 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf.PresheafOfModules.IsMonoidalW.PMod
Documentation

The category of module presheaves over the given commutative-ring presheaf.

Source context 13 commands

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

section ProofImplementation
namespace
  AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace IsMonoidalW
open _root_.PresheafOfModules
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

L55 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf.PresheafOfModules.IsMonoidalW.W
Source context 13 commands

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

section ProofImplementation
namespace
  AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace IsMonoidalW
open _root_.PresheafOfModules
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

L60 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf.PresheafOfModules.IsMonoidalW.shf
Documentation

The module-sheafification functor along the locally bijective ring-presheaf morphism.

Source context 13 commands

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

section ProofImplementation
namespace
  AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace IsMonoidalW
open _root_.PresheafOfModules
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

L64 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf.PresheafOfModules.IsMonoidalW.inc
Documentation

The functor forgetting the sheaf condition and restricting scalars along the ring-presheaf morphism.

Source context 13 commands

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

section ProofImplementation
namespace
  AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace IsMonoidalW
open _root_.PresheafOfModules
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

L68 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf.PresheafOfModules.IsMonoidalW.adj
Documentation

The adjunction between module sheafification and the underlying module-presheaf functor.

Source context 13 commands

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

section ProofImplementation
namespace
  AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace IsMonoidalW
open _root_.PresheafOfModules
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)

L70 ↗
Source context 13 commands

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

section ProofImplementation
namespace
  AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace IsMonoidalW
open _root_.PresheafOfModules
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)

L71 ↗
Source context 13 commands

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

section ProofImplementation
namespace
  AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace IsMonoidalW
open _root_.PresheafOfModules
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 α).Full
lemma

W_eq

L73 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf.PresheafOfModules.IsMonoidalW.W_eq
Source context 13 commands

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

section ProofImplementation
namespace
  AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace IsMonoidalW
open _root_.PresheafOfModules
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
lemma W_eq : W (J := J) 𝒪 = (MorphismProperty.isomorphisms _).inverseImage (shf 𝒪 R α)
lemma

isIso_unit_app_of_isSheaf

L76 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf.PresheafOfModules.IsMonoidalW.isIso_unit_app_of_isSheaf
Source context 13 commands

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

section ProofImplementation
namespace
  AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace IsMonoidalW
open _root_.PresheafOfModules
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
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

L83 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf.PresheafOfModules.IsMonoidalW.isIso_shf_map_unit_whiskerRight
Source context 13 commands

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

section ProofImplementation
namespace
  AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace IsMonoidalW
open _root_.PresheafOfModules
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
lemma isIso_shf_map_unit_whiskerRight (d d' : PMod 𝒪) :
    IsIso ((shf 𝒪 R α).map (((adj 𝒪 R α).unit.app d) ▷ d'))
lemma

W_whiskerRight

L92 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf.PresheafOfModules.IsMonoidalW.W_whiskerRight
Source context 14 commands

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

section ProofImplementation
namespace
  AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace IsMonoidalW
open _root_.PresheafOfModules
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}]
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

L117 ↗
PresheafOfModules.isMonoidal_inverseImage_W_toPresheaf
Source context 8 commands

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

section ProofImplementation
namespace
  AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isMonoidal_inverseImage_W_toPresheaf
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
open PresheafOfModules.IsMonoidalW in
Lean source · full declaration
theorem _root_.PresheafOfModules.isMonoidal_inverseImage_W_toPresheaf {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.