Module

ModulesIhomSections.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesIhomSections

130 declarations indexed from sourceView source ↗

Module documentation

Internal hom sections and module morphisms

Identifies internal hom sections with natural linear families and morphisms of restricted modules.

Imports3

Imported by27

def

toPresheafHom

L40 ↗

PresheafOfModules.InternalHom.IsSheafAux.toPresheafHom

Documentation

The presheaf morphism over an object associated to a natural family of linear maps.

Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace PresheafOfModules
namespace InternalHom
namespace IsSheafAux
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

L51 ↗

PresheafOfModules.InternalHom.IsSheafAux.appAt

Documentation

The component of a presheaf morphism at an object over the chosen base.

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace PresheafOfModules
namespace InternalHom
namespace IsSheafAux
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

L55 ↗

PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace PresheafOfModules
namespace InternalHom
namespace IsSheafAux
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

L60 ↗

PresheafOfModules.InternalHom.IsSheafAux.linearSub

Documentation

The subfunctor of presheaf morphisms whose components commute with scalar multiplication.

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace PresheafOfModules
namespace InternalHom
namespace IsSheafAux
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

L66 ↗

PresheafOfModules.InternalHom.IsSheafAux.ofPresheafHom

Documentation

The natural family of linear maps associated to a section of the linear subfunctor.

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace PresheafOfModules
namespace InternalHom
namespace IsSheafAux
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

L77 ↗

PresheafOfModules.InternalHom.IsSheafAux.ofPresheafHom_app

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace PresheafOfModules
namespace InternalHom
namespace IsSheafAux
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

L82 ↗

PresheafOfModules.InternalHom.IsSheafAux.equivLinearSub

Documentation

The equivalence between natural linear families and sections of the linear subfunctor.

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace PresheafOfModules
namespace InternalHom
namespace IsSheafAux
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

L91 ↗

PresheafOfModules.InternalHom.IsSheafAux.isoLinearSub

Documentation

The natural isomorphism identifying the internal Hom presheaf with its linear subfunctor model.

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace PresheafOfModules
namespace InternalHom
namespace IsSheafAux
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

L97 ↗

PresheafOfModules.InternalHom.IsSheafAux.linearSub_local

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace PresheafOfModules
namespace InternalHom
namespace IsSheafAux
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

ihomObj_isSheaf

L129 ↗

PresheafOfModules.ihomObj_isSheaf

Source context 3 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct

Lean source · statement

theorem PresheafOfModules.ihomObj_isSheaf {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

lemma

ihom_obj_eq_ihomObj

L152 ↗

PresheafOfModules.ihom_obj_eq_ihomObj

Source context 6 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace PresheafOfModules
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N N' : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}

Lean source · statement

lemma ihom_obj_eq_ihomObj (N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) :
    (ihom F).obj N = ihomObj F N

lemma

ihom_map_app_val

L155 ↗

PresheafOfModules.ihom_map_app_val

Source context 6 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace PresheafOfModules
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N N' : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}

Lean source · statement

lemma ihom_map_app_val (ψ : N ⟶ N') {X : Cᵒᵖ} (φ : (ihomObj F N).obj X) {Y : Cᵒᵖ}
    (f : X ⟶ Y) (x : F.obj Y) :
    (((ihom F).map ψ).app X φ).1 f x = ψ.app Y (φ.1 f x)

lemma

ihom_adjunction_unit_app_val

L159 ↗

PresheafOfModules.ihom_adjunction_unit_app_val

Source context 6 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace PresheafOfModules
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N N' : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}

Lean source · full declaration

lemma ihom_adjunction_unit_app_val (G : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {X : Cᵒᵖ}
    (y : G.obj X) {Y : Cᵒᵖ} (f : X ⟶ Y) (x : F.obj Y) :
    ((((ihom.adjunction F).unit.app G).app X y) : (ihomObj F (F ⊗ G)).obj X).1 f x =
      x ⊗ₜ[R.obj Y] (show G.obj Y from G.map f y) := rfl

lemma

ihom_adjunction_counit_app

L164 ↗

PresheafOfModules.ihom_adjunction_counit_app

Source context 6 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace PresheafOfModules
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N N' : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}

Lean source · statement

lemma ihom_adjunction_counit_app (N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) :
    (ihom.adjunction F).counit.app N = uncurry' F (𝟙 (ihomObj F N))

theorem

unitIsoSelf_hom_eq

L175 ↗

CategoryTheory.MonoidalClosed.unitIsoSelf_hom_eq

Source context 5 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
namespace CategoryTheory.MonoidalClosed
variable {C : Type u'} [Category.{v'} C] [MonoidalCategory C] [MonoidalClosed C]

Lean source · statement

theorem unitIsoSelf_hom_eq (X : C) :
    (unitIsoSelf X).hom = (λ_ _).inv ≫ (ihom.ev (𝟙_ C)).app X

lemma

sheafify_map_val_app_unit

L200 ↗

SheafOfModules.sheafify_map_val_app_unit

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
section unit
variable {𝒪 h𝒪}

Lean source · statement

lemma sheafify_map_val_app_unit {P P' : PMod 𝒪} (g : P ⟶ P') (X : Cᵒᵖ) (z : P.obj X) :
    (((sheafifyFunctor 𝒪 h𝒪).map g).val.app X) (((sheafifyAdj 𝒪 h𝒪).unit.app P).app X z) =
      ((sheafifyAdj 𝒪 h𝒪).unit.app P').app X (g.app X z)

lemma

counit_val_app_unit

L206 ↗

SheafOfModules.counit_val_app_unit

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
section unit
variable {𝒪 h𝒪}

Lean source · statement

lemma counit_val_app_unit (N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪)) (X : Cᵒᵖ) (y : N.val.obj X) :
    (((sheafifyAdj 𝒪 h𝒪).counit.app N).val.app X)
      (((sheafifyAdj 𝒪 h𝒪).unit.app ((toPMod 𝒪 h𝒪).obj N)).app X y) = y

lemma

toPMod_obj_map_apply

L213 ↗

SheafOfModules.toPMod_obj_map_apply

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
section unit
variable {𝒪 h𝒪}
omit [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}] in

Lean source · statement

lemma toPMod_obj_map_apply (S : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪)) {X Y : Cᵒᵖ} (f : X ⟶ Y)
    (x : S.val.obj X) : ((toPMod 𝒪 h𝒪).obj S).map f x = S.val.map f x

abbrev

ihomModel

L221 ↗

SheafOfModules.ihomModel

Documentation

The presheaf of natural linear families underlying the internal Hom of two module sheaves.

Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))

Lean source · statement

abbrev ihomModel : PMod 𝒪

theorem

isSheaf_ihomModel

L225 ↗

SheafOfModules.isSheaf_ihomModel

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
omit [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}] in

Lean source · statement

theorem isSheaf_ihomModel : Presheaf.IsSheaf J (ihomModel 𝒪 h𝒪 M N).presheaf

theorem

ihom_obj_eq

L231 ↗

SheafOfModules.ihom_obj_eq

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

theorem ihom_obj_eq : (ihom M).obj N = (sheafifyFunctor 𝒪 h𝒪).obj (ihomModel 𝒪 h𝒪 M N)

def

ihomModelToIhom

L234 ↗

SheafOfModules.ihomModelToIhom

Documentation

The sheafification unit from the natural-family model to the internal Hom sheaf.

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]

Lean source · statement

def ihomModelToIhom : ihomModel 𝒪 h𝒪 M N ⟶ (toPMod 𝒪 h𝒪).obj ((ihom M).obj N)

instance

isIso_ihomModelToIhom

L237 ↗

SheafOfModules.isIso_ihomModelToIhom

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]

Lean source · statement

instance isIso_ihomModelToIhom : IsIso (ihomModelToIhom 𝒪 h𝒪 M N)

def

ihomModelSectionsIso

L247 ↗

SheafOfModules.ihomModelSectionsIso

Documentation

The sectionwise isomorphism from the natural-family model to its internal Hom sheaf.

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]

Lean source · statement

def ihomModelSectionsIso (X : Cᵒᵖ) :
    (ihomModel 𝒪 h𝒪 M N).obj X ≅ ((toPMod 𝒪 h𝒪).obj ((ihom M).obj N)).obj X

def

ihomSectionsEquivFamily

L252 ↗

SheafOfModules.ihomSectionsEquivFamily

Documentation

The additive equivalence between internal Hom sections and natural linear families.

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]

Lean source · statement

def ihomSectionsEquivFamily (X : Cᵒᵖ) :
    ((ihom M).obj N).val.obj X ≃+ naturalFamilies ((toPMod 𝒪 h𝒪).obj M) ((toPMod 𝒪 h𝒪).obj N) X

lemma

ihomSectionsEquivFamily_symm_apply

L259 ↗

SheafOfModules.ihomSectionsEquivFamily_symm_apply

Source context 11 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ihomSectionsEquivFamily_symm_apply (X : Cᵒᵖ)
    (φ : naturalFamilies ((toPMod 𝒪 h𝒪).obj M) ((toPMod 𝒪 h𝒪).obj N) X) :
    (ihomSectionsEquivFamily 𝒪 h𝒪 M N X).symm φ = (ihomModelToIhom 𝒪 h𝒪 M N).app X φ

lemma

ihomSectionsEquivFamily_apply

L264 ↗

SheafOfModules.ihomSectionsEquivFamily_apply

Source context 11 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ihomSectionsEquivFamily_apply (X : Cᵒᵖ) (t : ((ihom M).obj N).val.obj X) :
    ihomSectionsEquivFamily 𝒪 h𝒪 M N X t = (inv (ihomModelToIhom 𝒪 h𝒪 M N)).app X t

lemma

ihomSectionsEquivFamily_unit

L268 ↗

SheafOfModules.ihomSectionsEquivFamily_unit

Source context 11 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ihomSectionsEquivFamily_unit (X : Cᵒᵖ)
    (φ : naturalFamilies ((toPMod 𝒪 h𝒪).obj M) ((toPMod 𝒪 h𝒪).obj N) X) :
    ihomSectionsEquivFamily 𝒪 h𝒪 M N X ((ihomModelToIhom 𝒪 h𝒪 M N).app X φ) = φ

lemma

unit_ihomSectionsEquivFamily

L274 ↗

SheafOfModules.unit_ihomSectionsEquivFamily

Source context 11 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma unit_ihomSectionsEquivFamily (X : Cᵒᵖ) (t : ((ihom M).obj N).val.obj X) :
    (ihomModelToIhom 𝒪 h𝒪 M N).app X (ihomSectionsEquivFamily 𝒪 h𝒪 M N X t) = t

lemma

ihomSectionsEquivFamily_map

L279 ↗

SheafOfModules.ihomSectionsEquivFamily_map

Source context 11 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ihomSectionsEquivFamily_map {X Y : Cᵒᵖ} (f : X ⟶ Y) (t : ((ihom M).obj N).val.obj X) :
    ihomSectionsEquivFamily 𝒪 h𝒪 M N Y (((ihom M).obj N).val.map f t) =
      (ihomModel 𝒪 h𝒪 M N).map f (ihomSectionsEquivFamily 𝒪 h𝒪 M N X t)

lemma

ihomSectionsEquivFamily_map_app

L285 ↗

SheafOfModules.ihomSectionsEquivFamily_map_app

Source context 11 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ihomSectionsEquivFamily_map_app {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (t : ((ihom M).obj N).val.obj X)
    (g : Y ⟶ Z) (m : M.val.obj Z) :
    (ihomSectionsEquivFamily 𝒪 h𝒪 M N Y (((ihom M).obj N).val.map f t)).1 g m =
      (ihomSectionsEquivFamily 𝒪 h𝒪 M N X t).1 (f ≫ g) m

def

ihomEval

L296 ↗

SheafOfModules.ihomEval

Documentation

Evaluation of an internal Hom section on a module section at the identity restriction.

Source context 11 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)

Lean source · statement

def ihomEval (X : Cᵒᵖ) (m : M.val.obj X) (t : ((ihom M).obj N).val.obj X) : N.val.obj X

lemma

ihomEval_def

L302 ↗

SheafOfModules.ihomEval_def

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ihomEval_def (X : Cᵒᵖ) (m : M.val.obj X) (t : ((ihom M).obj N).val.obj X) :
    ihomEval 𝒪 h𝒪 M N X m t = (ihomSectionsEquivFamily 𝒪 h𝒪 M N X t).1 (𝟙 X) m

lemma

ihomSectionsEquivFamily_app_eq_ihomEval

L306 ↗

SheafOfModules.ihomSectionsEquivFamily_app_eq_ihomEval

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ihomSectionsEquivFamily_app_eq_ihomEval {X Y : Cᵒᵖ} (f : X ⟶ Y)
    (t : ((ihom M).obj N).val.obj X) (m : M.val.obj Y) :
    (ihomSectionsEquivFamily 𝒪 h𝒪 M N X t).1 f m =
      ihomEval 𝒪 h𝒪 M N Y m (((ihom M).obj N).val.map f t)

lemma

ihomEval_unit_app

L314 ↗

SheafOfModules.ihomEval_unit_app

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ihomEval_unit_app (X : Cᵒᵖ) (m : M.val.obj X)
    (φ : naturalFamilies ((toPMod 𝒪 h𝒪).obj M) ((toPMod 𝒪 h𝒪).obj N) X) :
    ihomEval 𝒪 h𝒪 M N X m ((ihomModelToIhom 𝒪 h𝒪 M N).app X φ) = φ.1 (𝟙 X) m

lemma

map_ihomEval

L322 ↗

SheafOfModules.map_ihomEval

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma map_ihomEval {X Y : Cᵒᵖ} (f : X ⟶ Y) (m : M.val.obj X) (t : ((ihom M).obj N).val.obj X) :
    N.val.map f (ihomEval 𝒪 h𝒪 M N X m t) =
      ihomEval 𝒪 h𝒪 M N Y (M.val.map f m) (((ihom M).obj N).val.map f t)

lemma

ihom_sections_ext

L330 ↗

SheafOfModules.ihom_sections_ext

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ihom_sections_ext {X : Cᵒᵖ} {t t' : ((ihom M).obj N).val.obj X}
    (h : ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (m : M.val.obj Y),
      ihomEval 𝒪 h𝒪 M N Y m (((ihom M).obj N).val.map f t) =
        ihomEval 𝒪 h𝒪 M N Y m (((ihom M).obj N).val.map f t')) : t = t'

lemma

ihomEval_add_right

L341 ↗

SheafOfModules.ihomEval_add_right

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ihomEval_add_right (X : Cᵒᵖ) (m : M.val.obj X) (t t' : ((ihom M).obj N).val.obj X) :
    ihomEval 𝒪 h𝒪 M N X m (t + t') = ihomEval 𝒪 h𝒪 M N X m t + ihomEval 𝒪 h𝒪 M N X m t'

lemma

ihomEval_add_left

L346 ↗

SheafOfModules.ihomEval_add_left

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ihomEval_add_left (X : Cᵒᵖ) (m m' : M.val.obj X) (t : ((ihom M).obj N).val.obj X) :
    ihomEval 𝒪 h𝒪 M N X (m + m') t = ihomEval 𝒪 h𝒪 M N X m t + ihomEval 𝒪 h𝒪 M N X m' t

lemma

ihomEval_smul_left

L351 ↗

SheafOfModules.ihomEval_smul_left

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ihomEval_smul_left (X : Cᵒᵖ) (r : 𝒪.obj X) (m : M.val.obj X)
    (t : ((ihom M).obj N).val.obj X) :
    ihomEval 𝒪 h𝒪 M N X (r • m) t = r • ihomEval 𝒪 h𝒪 M N X m t

lemma

ihomEval_smul_right

L357 ↗

SheafOfModules.ihomEval_smul_right

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ihomEval_smul_right (X : Cᵒᵖ) (r : 𝒪.obj X) (m : M.val.obj X)
    (t : ((ihom M).obj N).val.obj X) :
    ihomEval 𝒪 h𝒪 M N X m (r • t) = r • ihomEval 𝒪 h𝒪 M N X m t

def

sheafifyTensorIso

L374 ↗

SheafOfModules.sheafifyTensorIso

Documentation

The comparison isomorphism from the sheafified presheaf tensor product to the tensor product of sheaves.

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))

Lean source · statement

def sheafifyTensorIso : (sheafifyFunctor 𝒪 h𝒪).obj ((toPMod 𝒪 h𝒪).obj M ⊗ (toPMod 𝒪 h𝒪).obj P) ≅
    M ⊗ P

lemma

sheafifyTensorIso_hom_naturality

L381 ↗

SheafOfModules.sheafifyTensorIso_hom_naturality

Source context 15 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma sheafifyTensorIso_hom_naturality {M' P' : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪)}
    (f : M ⟶ M') (g : P ⟶ P') :
    (sheafifyFunctor 𝒪 h𝒪).map ((toPMod 𝒪 h𝒪).map f ⊗ₘ (toPMod 𝒪 h𝒪).map g) ≫
      (sheafifyTensorIso 𝒪 h𝒪 M' P').hom = (sheafifyTensorIso 𝒪 h𝒪 M P).hom ≫ (f ⊗ₘ g)

def

sheafifyTensorNatIso

L394 ↗

SheafOfModules.sheafifyTensorNatIso

Documentation

The natural tensor comparison isomorphism for sheafification and passage to underlying presheaves.

Source context 14 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in

Lean source · statement

def sheafifyTensorNatIso :
    toPMod 𝒪 h𝒪 ⋙ (tensorLeft ((toPMod 𝒪 h𝒪).obj M) ⋙ sheafifyFunctor 𝒪 h𝒪) ≅ tensorLeft M ⋙ 𝟭 _

lemma

sheafifyTensorNatIso_hom_app

L405 ↗

SheafOfModules.sheafifyTensorNatIso_hom_app

Source context 15 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma sheafifyTensorNatIso_hom_app :
    (sheafifyTensorNatIso 𝒪 h𝒪 M).hom.app P = (sheafifyTensorIso 𝒪 h𝒪 M P).hom

def

unitIhomNatIso

L409 ↗

SheafOfModules.unitIhomNatIso

Documentation

The natural isomorphism identifying internal Hom presheaves with their sheafifications.

Source context 14 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in

Lean source · statement

def unitIhomNatIso : 𝟭 _ ⋙ (toPMod 𝒪 h𝒪 ⋙ ihom ((toPMod 𝒪 h𝒪).obj M)) ≅
    (toPMod 𝒪 h𝒪 ⋙ ihom ((toPMod 𝒪 h𝒪).obj M) ⋙ sheafifyFunctor 𝒪 h𝒪) ⋙ toPMod 𝒪 h𝒪

lemma

unitIhomNatIso_hom_app

L415 ↗

SheafOfModules.unitIhomNatIso_hom_app

Source context 15 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma unitIhomNatIso_hom_app : (unitIhomNatIso 𝒪 h𝒪 M).hom.app N = ihomModelToIhom 𝒪 h𝒪 M N

theorem

ihom_adjunction_eq

L418 ↗

SheafOfModules.ihom_adjunction_eq

Source context 15 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

theorem ihom_adjunction_eq : ihom.adjunction M =
    (((ihom.adjunction ((toPMod 𝒪 h𝒪).obj M)).comp (sheafifyAdj 𝒪 h𝒪)).restrictFullyFaithful
      (Functor.FullyFaithful.ofFullyFaithful (toPMod 𝒪 h𝒪)) (Functor.FullyFaithful.id _)
      (sheafifyTensorNatIso 𝒪 h𝒪 M) (unitIhomNatIso 𝒪 h𝒪 M))

def

tmulSection

L425 ↗

SheafOfModules.tmulSection

Documentation

The tensor product of two sheaf sections, obtained from their presheaf tensor and the sheafification unit.

Source context 14 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in

Lean source · statement

def tmulSection (X : Cᵒᵖ) (m : M.val.obj X) (p : P.val.obj X) : (M ⊗ P).val.obj X

lemma

tmulSection_def

L433 ↗

SheafOfModules.tmulSection_def

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma tmulSection_def (X : Cᵒᵖ) (m : M.val.obj X) (p : P.val.obj X) :
    tmulSection 𝒪 h𝒪 M P X m p = (sheafifyTensorIso 𝒪 h𝒪 M P).hom.val.app X
      (((sheafifyAdj 𝒪 h𝒪).unit.app ((toPMod 𝒪 h𝒪).obj M ⊗ (toPMod 𝒪 h𝒪).obj P)).app X
        (m ⊗ₜ[𝒪.obj X] p))

lemma

tensorHom_val_app_tmulSection

L439 ↗

SheafOfModules.tensorHom_val_app_tmulSection

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma tensorHom_val_app_tmulSection {M' P' : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪)}
    (f : M ⟶ M') (g : P ⟶ P') (X : Cᵒᵖ) (m : M.val.obj X) (p : P.val.obj X) :
    (f ⊗ₘ g).val.app X (tmulSection 𝒪 h𝒪 M P X m p) =
      tmulSection 𝒪 h𝒪 M' P' X (f.val.app X m) (g.val.app X p)

lemma

whiskerLeft_val_app_tmulSection

L451 ↗

SheafOfModules.whiskerLeft_val_app_tmulSection

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma whiskerLeft_val_app_tmulSection {P' : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪)} (g : P ⟶ P')
    (X : Cᵒᵖ) (m : M.val.obj X) (p : P.val.obj X) :
    (M ◁ g).val.app X (tmulSection 𝒪 h𝒪 M P X m p) =
      tmulSection 𝒪 h𝒪 M P' X m (g.val.app X p)

lemma

whiskerRight_val_app_tmulSection

L458 ↗

SheafOfModules.whiskerRight_val_app_tmulSection

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma whiskerRight_val_app_tmulSection {M' : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪)} (f : M ⟶ M')
    (X : Cᵒᵖ) (m : M.val.obj X) (p : P.val.obj X) :
    (f ▷ P).val.app X (tmulSection 𝒪 h𝒪 M P X m p) =
      tmulSection 𝒪 h𝒪 M' P X (f.val.app X m) p

lemma

map_tmulSection

L465 ↗

SheafOfModules.map_tmulSection

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma map_tmulSection {X Y : Cᵒᵖ} (f : X ⟶ Y) (m : M.val.obj X) (p : P.val.obj X) :
    (M ⊗ P).val.map f (tmulSection 𝒪 h𝒪 M P X m p) =
      tmulSection 𝒪 h𝒪 M P Y (M.val.map f m) (P.val.map f p)

lemma

tmulSection_add_left

L476 ↗

SheafOfModules.tmulSection_add_left

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma tmulSection_add_left (X : Cᵒᵖ) (m m' : M.val.obj X) (p : P.val.obj X) :
    tmulSection 𝒪 h𝒪 M P X (m + m') p =
      tmulSection 𝒪 h𝒪 M P X m p + tmulSection 𝒪 h𝒪 M P X m' p

lemma

tmulSection_add_right

L486 ↗

SheafOfModules.tmulSection_add_right

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma tmulSection_add_right (X : Cᵒᵖ) (m : M.val.obj X) (p p' : P.val.obj X) :
    tmulSection 𝒪 h𝒪 M P X m (p + p') =
      tmulSection 𝒪 h𝒪 M P X m p + tmulSection 𝒪 h𝒪 M P X m p'

lemma

tmulSection_smul_left

L496 ↗

SheafOfModules.tmulSection_smul_left

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma tmulSection_smul_left (X : Cᵒᵖ) (r : 𝒪.obj X) (m : M.val.obj X) (p : P.val.obj X) :
    tmulSection 𝒪 h𝒪 M P X (r • m) p = r • tmulSection 𝒪 h𝒪 M P X m p

lemma

tmulSection_smul_right

L505 ↗

SheafOfModules.tmulSection_smul_right

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma tmulSection_smul_right (X : Cᵒᵖ) (r : 𝒪.obj X) (m : M.val.obj X) (p : P.val.obj X) :
    tmulSection 𝒪 h𝒪 M P X m (r • p) = r • tmulSection 𝒪 h𝒪 M P X m p

lemma

toPMod_map_curry

L514 ↗

SheafOfModules.toPMod_map_curry

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma toPMod_map_curry (θ : M ⊗ P ⟶ N) :
    (toPMod 𝒪 h𝒪).map (MonoidalClosed.curry θ) =
      ((ihom.adjunction ((toPMod 𝒪 h𝒪).obj M)).comp (sheafifyAdj 𝒪 h𝒪)).unit.app
          ((toPMod 𝒪 h𝒪).obj P) ≫
        (toPMod 𝒪 h𝒪 ⋙ ihom ((toPMod 𝒪 h𝒪).obj M)).map ((sheafifyTensorNatIso 𝒪 h𝒪 M).hom.app P) ≫
        (toPMod 𝒪 h𝒪 ⋙ ihom ((toPMod 𝒪 h𝒪).obj M)).map ((𝟭 _).map θ) ≫
        (unitIhomNatIso 𝒪 h𝒪 M).hom.app N

theorem

ihomSectionsEquivFamily_curry_app

L530 ↗

SheafOfModules.ihomSectionsEquivFamily_curry_app

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

theorem ihomSectionsEquivFamily_curry_app (θ : M ⊗ P ⟶ N) (X : Cᵒᵖ) (p : P.val.obj X) {Y : Cᵒᵖ}
    (f : X ⟶ Y) (x : M.val.obj Y) :
    (ihomSectionsEquivFamily 𝒪 h𝒪 M N X ((MonoidalClosed.curry θ).val.app X p)).1 f x =
      θ.val.app Y (tmulSection 𝒪 h𝒪 M P Y x (P.val.map f p))

theorem

ihomEval_curry

L544 ↗

SheafOfModules.ihomEval_curry

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

theorem ihomEval_curry (θ : M ⊗ P ⟶ N) (X : Cᵒᵖ) (m : M.val.obj X) (p : P.val.obj X) :
    ihomEval 𝒪 h𝒪 M N X m ((MonoidalClosed.curry θ).val.app X p) =
      θ.val.app X (tmulSection 𝒪 h𝒪 M P X m p)

theorem

ihom_ev_val_app_tmulSection

L551 ↗

SheafOfModules.ihom_ev_val_app_tmulSection

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

theorem ihom_ev_val_app_tmulSection (X : Cᵒᵖ) (m : M.val.obj X) (t : ((ihom M).obj N).val.obj X) :
    ((ihom.ev M).app N).val.app X (tmulSection 𝒪 h𝒪 M ((ihom M).obj N) X m t) =
      ihomEval 𝒪 h𝒪 M N X m t

theorem

uncurry_val_app_tmulSection

L560 ↗

SheafOfModules.uncurry_val_app_tmulSection

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

theorem uncurry_val_app_tmulSection (κ : P ⟶ (ihom M).obj N) (X : Cᵒᵖ) (m : M.val.obj X)
    (p : P.val.obj X) :
    (MonoidalClosed.uncurry κ).val.app X (tmulSection 𝒪 h𝒪 M P X m p) =
      ihomEval 𝒪 h𝒪 M N X m (κ.val.app X p)

theorem

ihom_hom_ext

L569 ↗

SheafOfModules.ihom_hom_ext

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

theorem ihom_hom_ext {κ κ' : P ⟶ (ihom M).obj N}
    (h : ∀ (X : Cᵒᵖ) (m : M.val.obj X) (p : P.val.obj X),
      ihomEval 𝒪 h𝒪 M N X m (κ.val.app X p) = ihomEval 𝒪 h𝒪 M N X m (κ'.val.app X p)) :
    κ = κ'

theorem

tensor_hom_ext

L580 ↗

SheafOfModules.tensor_hom_ext

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

theorem tensor_hom_ext {θ θ' : M ⊗ P ⟶ N}
    (h : ∀ (X : Cᵒᵖ) (m : M.val.obj X) (p : P.val.obj X),
      θ.val.app X (tmulSection 𝒪 h𝒪 M P X m p) = θ'.val.app X (tmulSection 𝒪 h𝒪 M P X m p)) :
    θ = θ'

theorem

ihomEval_ihom_map_val_app

L590 ↗

SheafOfModules.ihomEval_ihom_map_val_app

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

theorem ihomEval_ihom_map_val_app {N' : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪)} (g : N ⟶ N')
    (X : Cᵒᵖ) (m : M.val.obj X) (t : ((ihom M).obj N).val.obj X) :
    ihomEval 𝒪 h𝒪 M N' X m (((ihom M).map g).val.app X t) =
      g.val.app X (ihomEval 𝒪 h𝒪 M N X m t)

theorem

ihomEval_pre_val_app

L601 ↗

SheafOfModules.ihomEval_pre_val_app

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

theorem ihomEval_pre_val_app {A B : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪)} (f : B ⟶ A) (X : Cᵒᵖ)
    (b : B.val.obj X) (t : ((ihom A).obj N).val.obj X) :
    ihomEval 𝒪 h𝒪 B N X b (((MonoidalClosed.pre f).app N).val.app X t) =
      ihomEval 𝒪 h𝒪 A N X (f.val.app X b) t

lemma

ε_sheafifyFunctor

L613 ↗

SheafOfModules.ε_sheafifyFunctor

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma ε_sheafifyFunctor :
    Functor.LaxMonoidal.ε (sheafifyFunctor 𝒪 h𝒪) = (sheafifyUnitIso 𝒪 h𝒪).inv

lemma

sheafifyUnitIso_hom_eq_counit

L617 ↗

SheafOfModules.sheafifyUnitIso_hom_eq_counit

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma sheafifyUnitIso_hom_eq_counit :
    (sheafifyUnitIso 𝒪 h𝒪).hom = (sheafifyAdj 𝒪 h𝒪).counit.app (𝟙_ _)

lemma

sheafifyTensorIso_hom_leftUnitor_hom

L622 ↗

SheafOfModules.sheafifyTensorIso_hom_leftUnitor_hom

Source context 17 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
variable (P) in
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

lemma sheafifyTensorIso_hom_leftUnitor_hom :
    (sheafifyTensorIso 𝒪 h𝒪 (𝟙_ _) P).hom ≫ (λ_ P).hom =
      (sheafifyFunctor 𝒪 h𝒪).map (λ_ ((toPMod 𝒪 h𝒪).obj P)).hom ≫
        (sheafifyAdj 𝒪 h𝒪).counit.app P

theorem

leftUnitor_hom_val_app_tmulSection

L636 ↗

SheafOfModules.leftUnitor_hom_val_app_tmulSection

Source context 17 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
variable (P) in
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

theorem leftUnitor_hom_val_app_tmulSection (X : Cᵒᵖ) (r : 𝒪.obj X) (p : P.val.obj X) :
    (λ_ P).hom.val.app X (tmulSection 𝒪 h𝒪 (𝟙_ _) P X r p) = r • p

theorem

leftUnitor_inv_val_app

L653 ↗

SheafOfModules.leftUnitor_inv_val_app

Source context 17 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
variable (P) in
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

theorem leftUnitor_inv_val_app (X : Cᵒᵖ) (p : P.val.obj X) :
    (λ_ P).inv.val.app X p = tmulSection 𝒪 h𝒪 (𝟙_ _) P X (1 : 𝒪.obj X) p

theorem

unitIsoSelf_hom_val_app

L667 ↗

SheafOfModules.unitIsoSelf_hom_val_app

Source context 17 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace SheafOfModules
open PresheafOfModules PresheafOfModules.InternalHom Functor.Monoidal Functor.LaxMonoidal
  Functor.OplaxMonoidal
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable (M N : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
variable {M N}
variable (M N)
variable {M N}
variable (M) (P : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
variable {M P} in
variable {M P}
variable (P) in
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in

Lean source · statement

theorem unitIsoSelf_hom_val_app (X : Cᵒᵖ) (t : ((ihom (𝟙_ _)).obj N).val.obj X) :
    (MonoidalClosed.unitIsoSelf N).hom.val.app X t = ihomEval 𝒪 h𝒪 (𝟙_ _) N X (1 : 𝒪.obj X) t

abbrev

toPMod

L687 ↗

AlgebraicGeometry.Scheme.Modules.toPMod

Documentation

The functor taking a module sheaf on a scheme to its underlying module presheaf.

Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in

Lean source · statement

abbrev toPMod : X.Modules ⥤ X.PresheafOfModules

lemma

toPMod_obj_map_apply

L690 ↗

AlgebraicGeometry.Scheme.Modules.toPMod_obj_map_apply

Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in

Lean source · statement

lemma toPMod_obj_map_apply (S : X.Modules) {V V' : (X.Opens)ᵒᵖ} (f : V ⟶ V') (x : S.val.obj V) :
    ((toPMod X).obj S).map f x = S.val.map f x

lemma

image_preimage_eq_of_le

L699 ↗

AlgebraicGeometry.Scheme.Modules.image_preimage_eq_of_le

Source context 11 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in

Lean source · statement

lemma image_preimage_eq_of_le {V : X.Opens} (h : V ≤ U) : U.ι ''ᵁ (U.ι ⁻¹ᵁ V) = V

abbrev

opHomImage

L705 ↗

AlgebraicGeometry.Scheme.Modules.opHomImage

Documentation

The opposite restriction morphism from an open subset to the image of an open in its associated scheme.

Source context 11 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in

Lean source · statement

abbrev opHomImage (W : (U : Scheme.{u}).Opens) : Opposite.op U ⟶ Opposite.op (U.ι ''ᵁ W)

lemma

restrict_ringHom_apply

L708 ↗

AlgebraicGeometry.Scheme.Modules.restrict_ringHom_apply

Source context 11 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in

Lean source · statement

lemma restrict_ringHom_apply (W : (U : Scheme.{u}).Opens) (a : Γ(X, U.ι ''ᵁ W)) :
    (U.ι.appIso W).inv.hom a = a

lemma

restrict_smul_eq

L715 ↗

AlgebraicGeometry.Scheme.Modules.restrict_smul_eq

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in
variable (M N : X.Modules)
variable {U M} in

Lean source · full declaration

lemma restrict_smul_eq (W : (U : Scheme.{u}).Opens) (a : Γ(↑U, W)) (y : Γ(M.restrict U.ι, W)) :
    (a • y : Γ(M.restrict U.ι, W)) =
      ((show Γ(X, U.ι ''ᵁ W) from a) • (show Γ(M, U.ι ''ᵁ W) from y) : Γ(M, U.ι ''ᵁ W)) :=
  (show (a • y : Γ(M.restrict U.ι, W)) =
      ((U.ι.appIso W).inv.hom a • (show Γ(M, U.ι ''ᵁ W) from y) : Γ(M, U.ι ''ᵁ W)) from rfl).trans
    (congrArg (fun r : Γ(X, U.ι ''ᵁ W) =>
      r • (show Γ(M, U.ι ''ᵁ W) from y))
      (restrict_ringHom_apply U W (show Γ(X, U.ι ''ᵁ W) from a)))

def

restrictHomOfFamily

L727 ↗

AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily

Documentation

The morphism between restricted module sheaves induced by a natural family below an open subset.

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in
variable (M N : X.Modules)
variable {U M} in

Lean source · statement

def restrictHomOfFamily
    (φ : PresheafOfModules.InternalHom.naturalFamilies ((toPMod X).obj M) ((toPMod X).obj N)
      (Opposite.op U)) :
    M.restrict U.ι ⟶ N.restrict U.ι

lemma

restrictHomOfFamily_app_apply

L744 ↗

AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in
variable (M N : X.Modules)
variable {U M} in

Lean source · statement

lemma restrictHomOfFamily_app_apply
    (φ : PresheafOfModules.InternalHom.naturalFamilies ((toPMod X).obj M) ((toPMod X).obj N)
      (Opposite.op U))
    (W : (U : Scheme.{u}).Opens) (x : Γ(M, U.ι ''ᵁ W)) :
    (restrictHomOfFamily U M N φ).app W x = φ.1 (opHomImage U W) x

def

restrictHomAppLE

L753 ↗

AlgebraicGeometry.Scheme.Modules.restrictHomAppLE

Documentation

The linear map on sections over a smaller open induced by a morphism of restricted module sheaves.

Source context 14 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in
variable (M N : X.Modules)
variable {U M} in
variable {U M N} in

Lean source · full declaration

def restrictHomAppLE (ψ : M.restrict U.ι ⟶ N.restrict U.ι) {V : X.Opens} (h : V ≤ U) :
    Γ(M, V) →ₗ[Γ(X, V)] Γ(N, V) where
  toFun x := N.presheaf.map (eqToHom (image_preimage_eq_of_le h).symm).op
    (ψ.app (U.ι ⁻¹ᵁ V) (M.presheaf.map (eqToHom (image_preimage_eq_of_le h)).op x))
  map_add' x y :=
    ((N.presheaf.map (eqToHom (image_preimage_eq_of_le h).symm).op).hom.comp
      ((ψ.app (U.ι ⁻¹ᵁ V)).hom.comp
        (M.presheaf.map (eqToHom (image_preimage_eq_of_le h)).op).hom)).map_add x y
  map_smul' r x := by
    let W : (U : Scheme.{u}).Opens := U.ι ⁻¹ᵁ V
    let a : Γ(X, U.ι ''ᵁ W) := X.presheaf.map (eqToHom (image_preimage_eq_of_le h)).op r
    let z : Γ(M, U.ι ''ᵁ W) := M.presheaf.map (eqToHom (image_preimage_eq_of_le h)).op x
    let aU : Γ(↑U, W) := a
    let zU : Γ(M.restrict U.ι, W) := z
    let n : Γ(N, U.ι ''ᵁ W) → Γ(N, V) :=
      N.presheaf.map (eqToHom (image_preimage_eq_of_le h).symm).op
    have hM : M.presheaf.map (eqToHom (image_preimage_eq_of_le h)).op (r • x) = a • z :=
      Modules.map_smul M (eqToHom (image_preimage_eq_of_le h)) r x
    have hψ : ψ.app W (aU • zU) = aU • ψ.app W zU := Modules.Hom.app_smul ψ aU zU
    have hN : n (a • (show Γ(N, U.ι ''ᵁ W) from ψ.app W zU)) =
        (X.presheaf.map (eqToHom (image_preimage_eq_of_le h).symm).op a) • n (ψ.app W zU) :=
      Modules.map_smul N (eqToHom (image_preimage_eq_of_le h).symm) a (ψ.app W zU)
    have hR : X.presheaf.map (eqToHom (image_preimage_eq_of_le h).symm).op a = r :=
      ((X.presheaf.mapIso (eqToIso (image_preimage_eq_of_le
        h)).op).commRingCatIsoToRingEquiv).symm_apply_apply r
    exact (congrArg (fun t : Γ(M, U.ι ''ᵁ W) => n (ψ.app W t)) hM).trans
      ((congrArg (fun t : Γ(M, U.ι ''ᵁ W) => n (ψ.app W t))
        (restrict_smul_eq (M := M) W aU zU).symm).trans
        ((congrArg n hψ).trans
          ((congrArg n (restrict_smul_eq (M := N) W aU (ψ.app W zU))).trans
            (hN.trans (congrArg (fun c : Γ(X, V) => c • n (ψ.app W zU)) hR)))))

lemma

restrictHomAppLE_apply

L787 ↗

AlgebraicGeometry.Scheme.Modules.restrictHomAppLE_apply

Source context 15 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in
variable (M N : X.Modules)
variable {U M} in
variable {U M N} in
variable {U M N}

Lean source · statement

lemma restrictHomAppLE_apply (ψ : M.restrict U.ι ⟶ N.restrict U.ι) {V : X.Opens} (h : V ≤ U)
    (x : Γ(M, V)) :
    restrictHomAppLE ψ h x = N.presheaf.map (eqToHom (image_preimage_eq_of_le h).symm).op
      (ψ.app (U.ι ⁻¹ᵁ V) (M.presheaf.map (eqToHom (image_preimage_eq_of_le h)).op x))

lemma

map_restrictHomAppLE

L792 ↗

AlgebraicGeometry.Scheme.Modules.map_restrictHomAppLE

Source context 15 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in
variable (M N : X.Modules)
variable {U M} in
variable {U M N} in
variable {U M N}

Lean source · statement

lemma map_restrictHomAppLE (ψ : M.restrict U.ι ⟶ N.restrict U.ι) {V V' : X.Opens} (h : V ≤ U)
    (i : V' ⟶ V) (x : Γ(M, V)) :
    N.presheaf.map i.op (restrictHomAppLE ψ h x) =
      restrictHomAppLE ψ (i.le.trans h) (M.presheaf.map i.op x)

lemma

restrictHomAppLE_image

L822 ↗

AlgebraicGeometry.Scheme.Modules.restrictHomAppLE_image

Source context 15 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in
variable (M N : X.Modules)
variable {U M} in
variable {U M N} in
variable {U M N}

Lean source · statement

lemma restrictHomAppLE_image (ψ : M.restrict U.ι ⟶ N.restrict U.ι) (W : (U : Scheme.{u}).Opens)
    (x : Γ(M, U.ι ''ᵁ W)) :
    restrictHomAppLE ψ (U.ι_image_le W) x = ψ.app W x

def

familyOfRestrictHom

L849 ↗

AlgebraicGeometry.Scheme.Modules.familyOfRestrictHom

Documentation

The natural family of section maps below an open induced by a morphism of restricted module sheaves.

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in
variable (M N : X.Modules)
variable {U M} in
variable {U M N} in
variable {U M N}
variable (U M N)

Lean source · statement

def familyOfRestrictHom (ψ : M.restrict U.ι ⟶ N.restrict U.ι) :
    PresheafOfModules.InternalHom.naturalFamilies ((toPMod X).obj M) ((toPMod X).obj N)
      (Opposite.op U)

lemma

familyOfRestrictHom_app

L855 ↗

AlgebraicGeometry.Scheme.Modules.familyOfRestrictHom_app

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in
variable (M N : X.Modules)
variable {U M} in
variable {U M N} in
variable {U M N}
variable (U M N)

Lean source · statement

lemma familyOfRestrictHom_app (ψ : M.restrict U.ι ⟶ N.restrict U.ι) {V : (X.Opens)ᵒᵖ}
    (f : Opposite.op U ⟶ V) (x : Γ(M, V.unop)) :
    (familyOfRestrictHom U M N ψ).1 f x = restrictHomAppLE ψ (V := V.unop) f.unop.le x

def

restrictHomEquivFamily

L861 ↗

AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily

Documentation

The additive equivalence between morphisms of restricted sheaves and natural linear families below an open.

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in
variable (M N : X.Modules)
variable {U M} in
variable {U M N} in
variable {U M N}
variable (U M N)

Lean source · full declaration

def restrictHomEquivFamily :
    (M.restrict U.ι ⟶ N.restrict U.ι) ≃+
      PresheafOfModules.InternalHom.naturalFamilies ((toPMod X).obj M) ((toPMod X).obj N)
        (Opposite.op U) where
  toFun := familyOfRestrictHom U M N
  invFun := restrictHomOfFamily U M N
  left_inv ψ := by
    ext W x
    exact restrictHomAppLE_image ψ W x
  right_inv φ := by
    apply PresheafOfModules.InternalHom.naturalFamilies_ext
    intro V f x
    have h1 := φ.2 (opHomImage U (U.ι ⁻¹ᵁ V.unop))
      (eqToHom (image_preimage_eq_of_le (f.unop.le : V.unop ≤ U)).symm).op
      (((toPMod X).obj M).map (eqToHom (image_preimage_eq_of_le (f.unop.le : V.unop ≤ U))).op x)
    have h2 : ((toPMod X).obj M).map
        (eqToHom (image_preimage_eq_of_le (f.unop.le : V.unop ≤ U)).symm).op
        (((toPMod X).obj M).map
          (eqToHom (image_preimage_eq_of_le (f.unop.le : V.unop ≤ U))).op x) = x := by
      erw [← PresheafOfModules.map_comp_apply]
      rw [((toPMod X).obj M).congr_map_apply (Subsingleton.elim _ (𝟙 _))]
      exact PresheafOfModules.InternalHom.map_id_apply _ _ _
    exact (h1.trans (congrArg (fun z => φ.1 (opHomImage U (U.ι ⁻¹ᵁ V.unop) ≫
      (eqToHom (image_preimage_eq_of_le (f.unop.le : V.unop ≤ U)).symm).op) z) h2)).trans
      (PresheafOfModules.InternalHom.congr_app φ (Subsingleton.elim _ _) _)
  map_add' ψ ψ' := by
    apply PresheafOfModules.InternalHom.naturalFamilies_ext
    intro V f x
    change restrictHomAppLE (ψ + ψ') (V := V.unop) f.unop.le x =
      restrictHomAppLE ψ (V := V.unop) f.unop.le x + restrictHomAppLE ψ' (V := V.unop) f.unop.le x
    let W : (U : Scheme.{u}).Opens := U.ι ⁻¹ᵁ V.unop
    let z : Γ(M.restrict U.ι, W) :=
      M.presheaf.map (eqToHom (image_preimage_eq_of_le f.unop.le)).op x
    let n : Γ(N.restrict U.ι, W) →+ Γ(N, V.unop) :=
      (N.presheaf.map (eqToHom (image_preimage_eq_of_le f.unop.le).symm).op).hom
    have hψ : (ψ + ψ').app W z = ψ.app W z + ψ'.app W z := rfl
    exact (congrArg n hψ).trans (n.map_add _ _)

lemma

restrictHomEquivFamily_apply

L899 ↗

AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in
variable (M N : X.Modules)
variable {U M} in
variable {U M N} in
variable {U M N}
variable (U M N)

Lean source · statement

lemma restrictHomEquivFamily_apply (ψ : M.restrict U.ι ⟶ N.restrict U.ι) :
    restrictHomEquivFamily U M N ψ = familyOfRestrictHom U M N ψ

lemma

restrictHomEquivFamily_symm_apply

L902 ↗

AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply

Source context 16 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
section restrict
variable (U : X.Opens)
variable {U} in
variable (M N : X.Modules)
variable {U M} in
variable {U M N} in
variable {U M N}
variable (U M N)

Lean source · statement

lemma restrictHomEquivFamily_symm_apply
    (φ : PresheafOfModules.InternalHom.naturalFamilies ((toPMod X).obj M) ((toPMod X).obj N)
      (Opposite.op U)) :
    (restrictHomEquivFamily U M N).symm φ = restrictHomOfFamily U M N φ

def

ihomEval

L912 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval

Documentation

Evaluation of an internal Hom section on a module section over an open subset of a scheme.

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)

Lean source · statement

def ihomEval (U : X.Opens) (m : Γ(M, U)) (t : Γ((ihom M).obj N, U)) : Γ(N, U)

theorem

tmulSection_eq_tensorSections

L917 ↗

AlgebraicGeometry.Scheme.Modules.tmulSection_eq_tensorSections

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

theorem tmulSection_eq_tensorSections {U : X.Opens} (m : Γ(M, U)) (p : Γ(P, U)) :
    SheafOfModules.tmulSection X.sheaf.obj X.ringCatSheaf.property M P (Opposite.op U) m p =
      tensorSections m p

lemma

map_ihomEval

L921 ↗

AlgebraicGeometry.Scheme.Modules.map_ihomEval

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

lemma map_ihomEval {U V : X.Opens} (i : V ⟶ U) (m : Γ(M, U)) (t : Γ((ihom M).obj N, U)) :
    N.presheaf.map i.op (ihomEval M N U m t) =
      ihomEval M N V (M.presheaf.map i.op m) (((ihom M).obj N).presheaf.map i.op t)

lemma

ihom_sections_ext

L926 ↗

AlgebraicGeometry.Scheme.Modules.ihom_sections_ext

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

lemma ihom_sections_ext {U : X.Opens} {t t' : Γ((ihom M).obj N, U)}
    (h : ∀ ⦃V : X.Opens⦄ (i : V ⟶ U) (m : Γ(M, V)),
      ihomEval M N V m (((ihom M).obj N).presheaf.map i.op t) =
        ihomEval M N V m (((ihom M).obj N).presheaf.map i.op t')) : t = t'

lemma

ihomEval_add_left

L932 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_add_left

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

lemma ihomEval_add_left (U : X.Opens) (m m' : Γ(M, U)) (t : Γ((ihom M).obj N, U)) :
    ihomEval M N U (m + m') t = ihomEval M N U m t + ihomEval M N U m' t

lemma

ihomEval_add_right

L936 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_add_right

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

lemma ihomEval_add_right (U : X.Opens) (m : Γ(M, U)) (t t' : Γ((ihom M).obj N, U)) :
    ihomEval M N U m (t + t') = ihomEval M N U m t + ihomEval M N U m t'

lemma

ihomEval_smul_left

L940 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_smul_left

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

lemma ihomEval_smul_left (U : X.Opens) (r : Γ(X, U)) (m : Γ(M, U)) (t : Γ((ihom M).obj N, U)) :
    ihomEval M N U (r • m) t = r • ihomEval M N U m t

lemma

ihomEval_smul_right

L944 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_smul_right

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

lemma ihomEval_smul_right (U : X.Opens) (r : Γ(X, U)) (m : Γ(M, U)) (t : Γ((ihom M).obj N, U)) :
    ihomEval M N U m (r • t) = r • ihomEval M N U m t

lemma

ihomEval_zero_left

L948 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

lemma ihomEval_zero_left (U : X.Opens) (t : Γ((ihom M).obj N, U)) :
    ihomEval M N U 0 t = 0

lemma

ihomEval_zero_right

L951 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

lemma ihomEval_zero_right (U : X.Opens) (m : Γ(M, U)) :
    ihomEval M N U m 0 = 0

theorem

ihomEval_curry_app

L957 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_curry_app

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

theorem ihomEval_curry_app (θ : M ⊗ P ⟶ N) (U : X.Opens) (m : Γ(M, U)) (p : Γ(P, U)) :
    ihomEval M N U m ((MonoidalClosed.curry θ).app U p) = θ.app U (tensorSections m p)

theorem

ihom_ev_app_tensorSections

L962 ↗

AlgebraicGeometry.Scheme.Modules.ihom_ev_app_tensorSections

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

theorem ihom_ev_app_tensorSections (U : X.Opens) (m : Γ(M, U)) (t : Γ((ihom M).obj N, U)) :
    ((ihom.ev M).app N).app U (tensorSections m t) = ihomEval M N U m t

theorem

uncurry_app_tensorSections

L967 ↗

AlgebraicGeometry.Scheme.Modules.uncurry_app_tensorSections

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

theorem uncurry_app_tensorSections (κ : P ⟶ (ihom M).obj N) (U : X.Opens) (m : Γ(M, U))
    (p : Γ(P, U)) :
    (MonoidalClosed.uncurry κ).app U (tensorSections m p) = ihomEval M N U m (κ.app U p)

theorem

ihom_hom_ext

L973 ↗

AlgebraicGeometry.Scheme.Modules.ihom_hom_ext

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

theorem ihom_hom_ext {κ κ' : P ⟶ (ihom M).obj N}
    (h : ∀ (U : X.Opens) (m : Γ(M, U)) (p : Γ(P, U)),
      ihomEval M N U m (κ.app U p) = ihomEval M N U m (κ'.app U p)) : κ = κ'

theorem

tensor_hom_ext

L978 ↗

AlgebraicGeometry.Scheme.Modules.tensor_hom_ext

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

theorem tensor_hom_ext {θ θ' : M ⊗ P ⟶ N}
    (h : ∀ (U : X.Opens) (m : Γ(M, U)) (p : Γ(P, U)),
      θ.app U (tensorSections m p) = θ'.app U (tensorSections m p)) : θ = θ'

theorem

ihomEval_ihom_map_app

L983 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_ihom_map_app

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

theorem ihomEval_ihom_map_app {N' : X.Modules} (g : N ⟶ N') (U : X.Opens) (m : Γ(M, U))
    (t : Γ((ihom M).obj N, U)) :
    ihomEval M N' U m (((ihom M).map g).app U t) = g.app U (ihomEval M N U m t)

theorem

ihomEval_pre_app

L988 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_pre_app

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}

Lean source · statement

theorem ihomEval_pre_app {A B : X.Modules} (f : B ⟶ A) (U : X.Opens) (b : Γ(B, U))
    (t : Γ((ihom A).obj N, U)) :
    ihomEval B N U b (((MonoidalClosed.pre f).app N).app U t) = ihomEval A N U (f.app U b) t

theorem

unitIsoSelf_hom_app

L994 ↗

AlgebraicGeometry.Scheme.Modules.unitIsoSelf_hom_app

Source context 11 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in

Lean source · statement

theorem unitIsoSelf_hom_app (U : X.Opens) (t : Γ((ihom (𝟙_ X.Modules)).obj N, U)) :
    (MonoidalClosed.unitIsoSelf N).hom.app U t = ihomEval (𝟙_ X.Modules) N U (unitSection U) t

def

ihomSectionsEquiv

L1002 ↗

AlgebraicGeometry.Scheme.Modules.ihomSectionsEquiv

Documentation

The additive equivalence between internal Hom sections on an open and morphisms of the restricted sheaves.

Source context 12 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)

Lean source · statement

def ihomSectionsEquiv (U : X.Opens) :
    Γ((ihom M).obj N, U) ≃+ (M.restrict U.ι ⟶ N.restrict U.ι)

lemma

ihomSectionsEquiv_apply

L1009 ↗

AlgebraicGeometry.Scheme.Modules.ihomSectionsEquiv_apply

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}

Lean source · statement

lemma ihomSectionsEquiv_apply (U : X.Opens) (t : Γ((ihom M).obj N, U)) :
    ihomSectionsEquiv M N U t = restrictHomOfFamily U M N
      (SheafOfModules.ihomSectionsEquivFamily X.sheaf.obj X.ringCatSheaf.property M N
        (Opposite.op U) t)

lemma

ihomSectionsEquiv_symm_apply

L1014 ↗

AlgebraicGeometry.Scheme.Modules.ihomSectionsEquiv_symm_apply

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}

Lean source · statement

lemma ihomSectionsEquiv_symm_apply (U : X.Opens) (ψ : M.restrict U.ι ⟶ N.restrict U.ι) :
    (ihomSectionsEquiv M N U).symm ψ =
      (SheafOfModules.ihomSectionsEquivFamily X.sheaf.obj X.ringCatSheaf.property M N
        (Opposite.op U)).symm (familyOfRestrictHom U M N ψ)

theorem

ihomSectionsEquiv_app_apply

L1019 ↗

AlgebraicGeometry.Scheme.Modules.ihomSectionsEquiv_app_apply

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}

Lean source · statement

theorem ihomSectionsEquiv_app_apply (U : X.Opens) (t : Γ((ihom M).obj N, U))
    (W : (U : Scheme.{u}).Opens) (m : Γ(M, U.ι ''ᵁ W)) :
    (ihomSectionsEquiv M N U t).app W m =
      ihomEval M N (U.ι ''ᵁ W) m (((ihom M).obj N).presheaf.map (homOfLE (U.ι_image_le W)).op t)

theorem

ihomEval_map_ihomSectionsEquiv_symm

L1028 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_map_ihomSectionsEquiv_symm

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}

Lean source · statement

theorem ihomEval_map_ihomSectionsEquiv_symm {U V : X.Opens} (h : V ≤ U)
    (ψ : M.restrict U.ι ⟶ N.restrict U.ι) (m : Γ(M, V)) :
    ihomEval M N V m (((ihom M).obj N).presheaf.map (homOfLE h).op ((ihomSectionsEquiv M N
      U).symm ψ)) =
      N.presheaf.map (eqToHom (image_preimage_eq_of_le h).symm).op
        (ψ.app (U.ι ⁻¹ᵁ V) (M.presheaf.map (eqToHom (image_preimage_eq_of_le h)).op m))

theorem

ihomEval_map_ihomSectionsEquiv_symm_image

L1043 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_map_ihomSectionsEquiv_symm_image

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}

Lean source · statement

theorem ihomEval_map_ihomSectionsEquiv_symm_image (U : X.Opens)
    (ψ : M.restrict U.ι ⟶ N.restrict U.ι) (W : (U : Scheme.{u}).Opens) (m : Γ(M, U.ι ''ᵁ W)) :
    ihomEval M N (U.ι ''ᵁ W) m
      (((ihom M).obj N).presheaf.map (homOfLE (U.ι_image_le W)).op
        ((ihomSectionsEquiv M N U).symm ψ)) = ψ.app W m

lemma

ihomEval_eqToHom

L1050 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_eqToHom

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}

Lean source · statement

lemma ihomEval_eqToHom {A B : X.Opens} (e : A = B) (m : Γ(M, A)) (t : Γ((ihom M).obj N, A)) :
    ihomEval M N B (M.presheaf.map (eqToHom e.symm).op m)
      (((ihom M).obj N).presheaf.map (eqToHom e.symm).op t) =
      N.presheaf.map (eqToHom e.symm).op (ihomEval M N A m t)

theorem

ihomSectionsEquiv_map_app_apply

L1058 ↗

AlgebraicGeometry.Scheme.Modules.ihomSectionsEquiv_map_app_apply

Source context 13 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}

Lean source · statement

theorem ihomSectionsEquiv_map_app_apply {U V : X.Opens} (h : V ≤ U) (t : Γ((ihom M).obj N, U))
    (W : (V : Scheme.{u}).Opens) (W' : (U : Scheme.{u}).Opens) (e : U.ι ''ᵁ W' = V.ι ''ᵁ W)
    (m : Γ(M, U.ι ''ᵁ W')) :
    (ihomSectionsEquiv M N V (((ihom M).obj N).presheaf.map (homOfLE h).op t)).app W
        (M.presheaf.map (eqToHom e.symm).op m) =
      N.presheaf.map (eqToHom e.symm).op ((ihomSectionsEquiv M N U t).app W' m)

def

homOfFamily

L1074 ↗

AlgebraicGeometry.Scheme.Modules.homOfFamily

Documentation

The global morphism of module sheaves induced by a natural linear family below the top open.

Source context 14 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)

Lean source · statement

def homOfFamily (φ : PresheafOfModules.InternalHom.naturalFamilies ((toPMod X).obj M) ((toPMod
  X).obj N)
      (Opposite.op ⊤)) :
    M ⟶ N

lemma

homOfFamily_app_apply

L1088 ↗

AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply

Source context 14 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)

Lean source · statement

lemma homOfFamily_app_apply
    (φ : PresheafOfModules.InternalHom.naturalFamilies ((toPMod X).obj M) ((toPMod X).obj N)
      (Opposite.op ⊤))
    (V : X.Opens) (x : Γ(M, V)) : (homOfFamily M N φ).app V x = φ.1 (homOfLE le_top).op x

def

familyOfHom

L1094 ↗

AlgebraicGeometry.Scheme.Modules.familyOfHom

Documentation

The natural family of section maps induced by a morphism of module sheaves.

Source context 14 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)

Lean source · statement

def familyOfHom (ψ : M ⟶ N) :
    PresheafOfModules.InternalHom.naturalFamilies ((toPMod X).obj M) ((toPMod X).obj N)
      (Opposite.op ⊤)

lemma

familyOfHom_app

L1103 ↗

AlgebraicGeometry.Scheme.Modules.familyOfHom_app

Source context 14 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)

Lean source · statement

lemma familyOfHom_app (ψ : M ⟶ N) {V : (X.Opens)ᵒᵖ} (f : Opposite.op ⊤ ⟶ V)
    (x : Γ(M, V.unop)) : (familyOfHom M N ψ).1 f x = ψ.app V.unop x

def

homEquivFamily

L1108 ↗

AlgebraicGeometry.Scheme.Modules.homEquivFamily

Documentation

The additive equivalence between module sheaf morphisms and natural linear families below the top open.

Source context 14 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)

Lean source · full declaration

def homEquivFamily :
    (M ⟶ N) ≃+ PresheafOfModules.InternalHom.naturalFamilies ((toPMod X).obj M)
      ((toPMod X).obj N) (Opposite.op ⊤) where
  toFun := familyOfHom M N
  invFun := homOfFamily M N
  left_inv ψ := by ext V x; rfl
  right_inv φ := by
    apply PresheafOfModules.InternalHom.naturalFamilies_ext
    intro V f x
    exact PresheafOfModules.InternalHom.congr_app φ (Subsingleton.elim _ _) _
  map_add' ψ ψ' := by
    apply PresheafOfModules.InternalHom.naturalFamilies_ext
    intro V f x
    rfl

def

ihomGlobalSectionsEquiv

L1125 ↗

AlgebraicGeometry.Scheme.Modules.ihomGlobalSectionsEquiv

Documentation

The additive equivalence between global internal Hom sections and morphisms of module sheaves.

Source context 14 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)

Lean source · statement

def ihomGlobalSectionsEquiv : Γ((ihom M).obj N, ⊤) ≃+ (M ⟶ N)

theorem

ihomGlobalSectionsEquiv_app_apply

L1131 ↗

AlgebraicGeometry.Scheme.Modules.ihomGlobalSectionsEquiv_app_apply

Source context 15 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)
variable {M N}

Lean source · statement

theorem ihomGlobalSectionsEquiv_app_apply (t : Γ((ihom M).obj N, ⊤)) (V : X.Opens) (m : Γ(M, V)) :
    (ihomGlobalSectionsEquiv M N t).app V m =
      ihomEval M N V m (((ihom M).obj N).presheaf.map (homOfLE le_top).op t)

theorem

ihomEval_map_ihomGlobalSectionsEquiv_symm

L1140 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_map_ihomGlobalSectionsEquiv_symm

Source context 15 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)
variable {M N}

Lean source · statement

theorem ihomEval_map_ihomGlobalSectionsEquiv_symm (ψ : M ⟶ N) (V : X.Opens) (m : Γ(M, V)) :
    ihomEval M N V m
      (((ihom M).obj N).presheaf.map (homOfLE le_top).op ((ihomGlobalSectionsEquiv M N).symm ψ)) =
      ψ.app V m

theorem

ihomEval_ihomGlobalSectionsEquiv_symm

L1146 ↗

AlgebraicGeometry.Scheme.Modules.ihomEval_ihomGlobalSectionsEquiv_symm

Source context 15 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)
variable {M N}

Lean source · statement

theorem ihomEval_ihomGlobalSectionsEquiv_symm (ψ : M ⟶ N) (m : Γ(M, ⊤)) :
    ihomEval M N ⊤ m ((ihomGlobalSectionsEquiv M N).symm ψ) = ψ.app ⊤ m

theorem

ihomSectionsEquiv_map_app_apply_of_top

L1154 ↗

AlgebraicGeometry.Scheme.Modules.ihomSectionsEquiv_map_app_apply_of_top

Source context 15 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)
variable {M N}

Lean source · statement

theorem ihomSectionsEquiv_map_app_apply_of_top (t : Γ((ihom M).obj N, ⊤)) (U : X.Opens)
    (W : (U : Scheme.{u}).Opens) (m : Γ(M, U.ι ''ᵁ W)) :
    (ihomSectionsEquiv M N U (((ihom M).obj N).presheaf.map (homOfLE le_top).op t)).app W m =
      (ihomGlobalSectionsEquiv M N t).app (U.ι ''ᵁ W) m

def

restrictUnitIso'

L1170 ↗

AlgebraicGeometry.Scheme.Modules.restrictUnitIso'

Documentation

The canonical isomorphism between the restricted unit module sheaf along an open immersion and the unit sheaf.

Source context 17 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)
variable {M N}
section restrictUnit
variable {Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f]

Lean source · full declaration

def restrictUnitIso' : (𝟙_ Y.Modules).restrict f ≅ 𝟙_ X.Modules where
  hom := ⟨PresheafOfModules.homMk
    { app := fun U => AddCommGrpCat.ofHom (f.appIso U.unop).hom.hom.toAddMonoidHom
      naturality := fun {U V} i => by
        ext x
        have nat := congr($(f.appIso_inv_naturality (U := U.unop) (V := V.unop) i).hom
          ((f.appIso U.unop).hom.hom x))
        have hx : (f.appIso U.unop).inv.hom ((f.appIso U.unop).hom.hom x) = x :=
          (f.appIso U.unop).commRingCatIsoToRingEquiv.symm_apply_apply x
        exact (congrArg (fun z => (f.appIso V.unop).hom.hom
          ((Y.presheaf.map (f.opensFunctor.op.map i)).hom z)) hx.symm).trans
          ((congrArg (fun z => (f.appIso V.unop).hom.hom z) nat.symm).trans
            ((f.appIso V.unop).commRingCatIsoToRingEquiv.apply_symm_apply _)) }
    (fun U a x => by
      refine (show _ = (f.appIso U.unop).hom.hom
        ((f.appIso U.unop).inv.hom a * (show Γ(Y, f ''ᵁ U.unop) from x)) from rfl).trans ?_
      exact ((f.appIso U.unop).hom.hom.map_mul _ _).trans
        (congrArg (fun b : Γ(X, U.unop) => b *
          (f.appIso U.unop).hom.hom (show Γ(Y, f ''ᵁ U.unop) from x))
          ((f.appIso U.unop).commRingCatIsoToRingEquiv.apply_symm_apply a)))⟩
  inv := ⟨PresheafOfModules.homMk
    { app := fun U => AddCommGrpCat.ofHom (f.appIso U.unop).inv.hom.toAddMonoidHom
      naturality := fun {U V} i => by
        ext y
        have nat := congr($(f.appIso_inv_naturality (U := U.unop) (V := V.unop) i).hom y)
        exact (show _ = (f.appIso V.unop).inv.hom ((X.presheaf.map i).hom y) from rfl).trans nat }
    (fun U a y => by
      refine (show _ = (f.appIso U.unop).inv.hom
        ((show Γ(X, U.unop) from a) * (show Γ(X, U.unop) from y)) from rfl).trans ?_
      exact (f.appIso U.unop).inv.hom.map_mul _ _)⟩
  hom_inv_id := by
    ext U x
    exact (show _ = (f.appIso U).inv.hom ((f.appIso U).hom.hom x) from rfl).trans
      ((f.appIso U).commRingCatIsoToRingEquiv.symm_apply_apply x)
  inv_hom_id := by
    ext U y
    exact (show _ = (f.appIso U).hom.hom ((f.appIso U).inv.hom y) from rfl).trans
      ((f.appIso U).commRingCatIsoToRingEquiv.apply_symm_apply y)

lemma

restrictUnitIso_hom_app_apply

L1209 ↗

AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply

Source context 17 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)
variable {M N}
section restrictUnit
variable {Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f]

Lean source · statement

lemma restrictUnitIso_hom_app_apply (U : X.Opens) (r : Γ((𝟙_ Y.Modules).restrict f, U)) :
    (restrictUnitIso' f).hom.app U r = (f.appIso U).hom.hom r

lemma

restrictUnitIso_inv_app_apply

L1212 ↗

AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply

Source context 17 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)
variable {M N}
section restrictUnit
variable {Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f]

Lean source · statement

lemma restrictUnitIso_inv_app_apply (U : X.Opens) (r : Γ(𝟙_ X.Modules, U)) :
    (restrictUnitIso' f).inv.app U r = (f.appIso U).inv.hom r

lemma

restrictUnitIso_ι_hom_app_apply

L1215 ↗

AlgebraicGeometry.Scheme.Modules.restrictUnitIso_ι_hom_app_apply

Source context 17 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
open scoped TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}}
variable (X) in
variable (M N : X.Modules)
variable {M N} {P : X.Modules}
variable (N) in
variable (M N)
variable {M N}
variable (M N)
variable {M N}
section restrictUnit
variable {Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f]

Lean source · full declaration

lemma restrictUnitIso_ι_hom_app_apply (U : X.Opens) (W : (U : Scheme.{u}).Opens)
    (r : Γ((𝟙_ X.Modules).restrict U.ι, W)) :
    (restrictUnitIso' U.ι).hom.app W r = (show Γ(X, U.ι ''ᵁ W) from r) := by
  rw [restrictUnitIso_hom_app_apply, Scheme.Opens.ι_appIso]; rfl

Module documentation

Internal hom sections and module morphisms

Declarations