Module

BaseChange.lean

Nyll.SchemeTheory.WeilRestriction.BaseChange

9 declarations indexed from sourceView source ↗

Module documentation

Base change for relative internal Hom

Restriction from schemes over S to schemes over S' identifies the relative internal Hom with the internal Hom of the two pullbacks. The comparison is obtained from pullback pasting and the adjunction between composition and base change. Consequently, a representing scheme pulls back to a representing scheme.

Imports4

Nyll.SchemeTheory.WeilRestriction.Sheaf
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Comma.Over.Pullback
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Imported by5

def

tensorBaseChangeLeftIso

L40 ↗

SchemeTheory.WeilRestriction.tensorBaseChangeLeftIso

Documentation

The canonical isomorphism between taking a fibre product after base change and composing the test scheme with the base-change morphism.

Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
open scoped MonoidalCategory
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable {S S' : Scheme.{u}}

Lean source · statement

def tensorBaseChangeLeftIso (f : S' ⟶ S) (U : Over S) (T : Over S') :
    pullback T.hom (pullback.snd U.hom f) ≅ pullback (T.hom ≫ f) U.hom

lemma

tensorBaseChangeLeftIso_hom_fst

L46 ↗

SchemeTheory.WeilRestriction.tensorBaseChangeLeftIso_hom_fst

Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
open scoped MonoidalCategory
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable {S S' : Scheme.{u}}

Lean source · statement

lemma tensorBaseChangeLeftIso_hom_fst
    (f : S' ⟶ S) (U : Over S) (T : Over S') :
    (tensorBaseChangeLeftIso f U T).hom ≫ pullback.fst (T.hom ≫ f) U.hom =
      pullback.fst T.hom (pullback.snd U.hom f)

lemma

tensorBaseChangeLeftIso_hom_snd

L54 ↗

SchemeTheory.WeilRestriction.tensorBaseChangeLeftIso_hom_snd

Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
open scoped MonoidalCategory
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable {S S' : Scheme.{u}}

Lean source · statement

lemma tensorBaseChangeLeftIso_hom_snd
    (f : S' ⟶ S) (U : Over S) (T : Over S') :
    (tensorBaseChangeLeftIso f U T).hom ≫ pullback.snd (T.hom ≫ f) U.hom =
      pullback.snd T.hom (pullback.snd U.hom f) ≫ pullback.fst U.hom f

def

mapTensorPullbackIso

L64 ↗

SchemeTheory.WeilRestriction.mapTensorPullbackIso

Documentation

Pushing a fibre product with a pulled-back scheme to the original base agrees with forming the fibre product there.

Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
open scoped MonoidalCategory
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable {S S' : Scheme.{u}}

Lean source · statement

def mapTensorPullbackIso (f : S' ⟶ S) (U : Over S) (T : Over S') :
    (Over.map f).obj (T ⊗ (Over.pullback f).obj U) ≅ (Over.map f).obj T ⊗ U

lemma

mapTensorPullbackIso_hom_left_fst

L73 ↗

SchemeTheory.WeilRestriction.mapTensorPullbackIso_hom_left_fst

Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
open scoped MonoidalCategory
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable {S S' : Scheme.{u}}

Lean source · statement

lemma mapTensorPullbackIso_hom_left_fst
    (f : S' ⟶ S) (U : Over S) (T : Over S') :
    (mapTensorPullbackIso f U T).hom.left ≫ pullback.fst (T.hom ≫ f) U.hom =
      pullback.fst T.hom (pullback.snd U.hom f)

lemma

mapTensorPullbackIso_hom_left_snd

L80 ↗

SchemeTheory.WeilRestriction.mapTensorPullbackIso_hom_left_snd

Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
open scoped MonoidalCategory
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable {S S' : Scheme.{u}}

Lean source · statement

lemma mapTensorPullbackIso_hom_left_snd
    (f : S' ⟶ S) (U : Over S) (T : Over S') :
    (mapTensorPullbackIso f U T).hom.left ≫ pullback.snd (T.hom ≫ f) U.hom =
      pullback.snd T.hom (pullback.snd U.hom f) ≫ pullback.fst U.hom f

def

tensorRightBaseChangeIso

L87 ↗

SchemeTheory.WeilRestriction.tensorRightBaseChangeIso

Documentation

Composition to S commutes with product by the pullback of a fixed S-scheme.

Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
open scoped MonoidalCategory
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable {S S' : Scheme.{u}}

Lean source · statement

def tensorRightBaseChangeIso (f : S' ⟶ S) (U : Over S) :
    MonoidalCategory.tensorRight ((Over.pullback f).obj U) ⋙ Over.map f ≅
      Over.map f ⋙ MonoidalCategory.tensorRight U

def

relativeInternalHomBaseChangeIso

L131 ↗

SchemeTheory.WeilRestriction.relativeInternalHomBaseChangeIso

Documentation

Restriction to schemes over S' is the internal Hom of the pulled-back schemes.

Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
open scoped MonoidalCategory
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable {S S' : Scheme.{u}}

Lean source · statement

def relativeInternalHomBaseChangeIso (f : S' ⟶ S) (U V : Over S) :
    (Over.map f).op ⋙ relativeInternalHomFunctor U V ≅
      relativeInternalHomFunctor ((Over.pullback f).obj U) ((Over.pullback f).obj V)

def

relativeInternalHomRepresentableBaseChange

L144 ↗

SchemeTheory.WeilRestriction.relativeInternalHomRepresentableBaseChange

Documentation

A relative internal Hom representer remains a representer after arbitrary base change.

Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
open scoped MonoidalCategory
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable {S S' : Scheme.{u}}

Lean source · statement

def relativeInternalHomRepresentableBaseChange (f : S' ⟶ S) {U V W : Over S}
    (h : (relativeInternalHomFunctor U V).RepresentableBy W) :
    (relativeInternalHomFunctor ((Over.pullback f).obj U)
      ((Over.pullback f).obj V)).RepresentableBy ((Over.pullback f).obj W)

Module documentation

Base change for relative internal Hom

Declarations