Module

Sheaf.lean

Nyll.SchemeTheory.WeilRestriction.Sheaf

4 declarations indexed from sourceView source ↗

Module documentation

Relative internal Hom as a sheaf

For schemes U and V over S, the relative internal Hom presheaf sends T to morphisms over S from T ×ₛ U to V. It is a sheaf for the topology induced on Over S by any subcanonical topology on schemes.

The key observation is that product with U is pullback to U followed by composition with its structure morphism. Both functors are continuous for the induced topologies, without any affineness or finiteness assumptions.

Imports5

Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Mathlib.CategoryTheory.Sites.Continuous
Mathlib.CategoryTheory.Sites.Over
Mathlib.CategoryTheory.Sites.SubcanonicalOver

Imported by9

abbrev

relativeInternalHomFunctor

L40 ↗

SchemeTheory.WeilRestriction.relativeInternalHomFunctor

Documentation

The presheaf of morphisms over S from T ×ₛ U to V.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction

Lean source · statement

abbrev relativeInternalHomFunctor {S : Scheme.{u}} (U V : Over S) :
    (Over S)ᵒᵖ ⥤ Type u

def

tensorRightIsoPullbackMap

L45 ↗

SchemeTheory.WeilRestriction.tensorRightIsoPullbackMap

Documentation

Product with U is base change to U followed by composition to the base.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction

Lean source · statement

def tensorRightIsoPullbackMap {S : Scheme.{u}} (U : Over S) :
    MonoidalCategory.tensorRight U ≅ Over.pullback U.hom ⋙ Over.map U.hom

lemma

continuous_tensorRight

L55 ↗

SchemeTheory.WeilRestriction.continuous_tensorRight

Documentation

Product with a fixed scheme over S is continuous for the induced topology.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction

Lean source · statement

lemma continuous_tensorRight (J : GrothendieckTopology Scheme.{u})
    {S : Scheme.{u}} (U : Over S) :
    (MonoidalCategory.tensorRight U).IsContinuous (J.over S) (J.over S)

lemma

relativeInternalHom_isSheaf

L66 ↗

SchemeTheory.WeilRestriction.relativeInternalHom_isSheaf

Documentation

Relative internal Hom is a sheaf for every subcanonical topology on schemes.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction

Lean source · statement

lemma relativeInternalHom_isSheaf (J : GrothendieckTopology Scheme.{u}) [J.Subcanonical]
    {S : Scheme.{u}} (U V : Over S) :
    Presheaf.IsSheaf (J.over S) (relativeInternalHomFunctor U V)

Module documentation

Relative internal Hom as a sheaf

Declarations

relativeInternalHomFunctor

tensorRightIsoPullbackMap

continuous_tensorRight

relativeInternalHom_isSheaf