NYLL
Module

InternalHomSheaf.lean

Nyll.SchemeTheory.Modules.InternalHomSheaf
10 declarations indexed from sourceView source ↗

Module documentation

The sheaf condition for internal Hom

Natural linear families are identified with a subpresheaf of the ordinary presheaf Hom. When the target module presheaf is a sheaf, this description proves that the internal-Hom module presheaf is also a sheaf.

Imports4
Imported by5

Declarations

def

toPresheafHom

L52 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isSheaf_ihomObj.PresheafOfModules.InternalHom.toPresheafHom
Documentation

A natural linear family viewed as a morphism of underlying presheaves over X.

Source context 16 commands

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

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

appAt

L63 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isSheaf_ihomObj.PresheafOfModules.InternalHom.appAt
Documentation

Evaluation of a presheaf-Hom section at an object of the over category.

Source context 17 commands

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

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

appAt_toPresheafHom

L67 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isSheaf_ihomObj.PresheafOfModules.InternalHom.appAt_toPresheafHom
Source context 17 commands

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

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

linearSub

L72 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isSheaf_ihomObj.PresheafOfModules.InternalHom.linearSub
Documentation

The subfunctor of presheaf-Hom sections whose component maps are linear over the local rings.

Source context 17 commands

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

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

ofPresheafHom

L78 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isSheaf_ihomObj.PresheafOfModules.InternalHom.ofPresheafHom
Documentation

The natural linear family recovered from a section of the linear presheaf-Hom subfunctor.

Source context 17 commands

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

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

ofPresheafHom_app

L89 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isSheaf_ihomObj.PresheafOfModules.InternalHom.ofPresheafHom_app
Source context 17 commands

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

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

equivLinearSub

L95 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isSheaf_ihomObj.PresheafOfModules.InternalHom.equivLinearSub
Documentation

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

Source context 17 commands

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

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

isoLinearSub

L104 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isSheaf_ihomObj.PresheafOfModules.InternalHom.isoLinearSub
Documentation

The natural isomorphism from the underlying internal-Hom presheaf to the linear presheaf-Hom subfunctor.

Source context 17 commands

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

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

linearSub_local

L110 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isSheaf_ihomObj.PresheafOfModules.InternalHom.linearSub_local
Source context 18 commands

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

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

isSheaf_ihomObj

L140 ↗
PresheafOfModules.isSheaf_ihomObj
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.PresheafOfModules_isSheaf_ihomObj
universe u v' u'
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
open _root_.Opposite
Lean source · statement
theorem _root_.PresheafOfModules.isSheaf_ihomObj {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

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