Module

ModulesTildePullback.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesTildePullback

5 declarations indexed from sourceView source ↗

Module documentation

Affine pullback and associated module sheaves

Compares pullback of an associated module sheaf with extension of scalars.

Imports3

Mathlib.AlgebraicGeometry.Modules.Tilde
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Mathlib.CategoryTheory.Adjunction.Unique

Imported by14

def

pushforwardSpecCompΓIso

L35 ↗

AlgebraicGeometry.Scheme.Modules.pushforwardSpecCompΓIso

Documentation

Global sections of pushforward along Spec.map agree with restriction of scalars.

Source context 5 commands

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

universe u
open CategoryTheory AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

def Scheme.Modules.pushforwardSpecCompΓIso :
    Scheme.Modules.pushforward (Spec.map φ) ⋙ moduleSpecΓFunctor (R := R) ≅
      moduleSpecΓFunctor (R := S) ⋙ ModuleCat.restrictScalars φ.hom

def

functorCompPullbackSpecIso

L66 ↗

AlgebraicGeometry.tilde.functorCompPullbackSpecIso

Documentation

The natural comparison between pulling back an associated module sheaf and extending scalars.

Source context 5 commands

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

universe u
open CategoryTheory AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

def tilde.functorCompPullbackSpecIso :
    tilde.functor R ⋙ Scheme.Modules.pullback (Spec.map φ) ≅
      ModuleCat.extendScalars φ.hom ⋙ tilde.functor S

def

pullbackSpecIso

L76 ↗

AlgebraicGeometry.tilde.pullbackSpecIso

Documentation

The comparison between the pullback of an associated module sheaf and the sheaf of the scalar extension.

Source context 5 commands

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

universe u
open CategoryTheory AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

def tilde.pullbackSpecIso (M : ModuleCat.{u} R) :
    (Scheme.Modules.pullback (Spec.map φ)).obj (tilde M) ≅
      tilde ((ModuleCat.extendScalars φ.hom).obj M)

theorem

functorCompPullbackSpecIso_app

L81 ↗

AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app

Source context 5 commands

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

universe u
open CategoryTheory AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

theorem tilde.functorCompPullbackSpecIso_app (M : ModuleCat.{u} R) :
    (tilde.functorCompPullbackSpecIso φ).app M = tilde.pullbackSpecIso φ M

theorem

pullbackSpecIso_hom_naturality

L84 ↗

AlgebraicGeometry.tilde.pullbackSpecIso_hom_naturality

Source context 5 commands

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

universe u
open CategoryTheory AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

theorem tilde.pullbackSpecIso_hom_naturality {M M' : ModuleCat.{u} R} (f : M ⟶ M') :
    (Scheme.Modules.pullback (Spec.map φ)).map ((tilde.functor R).map f) ≫
        (tilde.pullbackSpecIso φ M').hom =
      (tilde.pullbackSpecIso φ M).hom ≫ (tilde.functor S).map ((ModuleCat.extendScalars
        φ.hom).map f)

Module documentation

Affine pullback and associated module sheaves

Declarations

pushforwardSpecCompΓIso

functorCompPullbackSpecIso

pullbackSpecIso

functorCompPullbackSpecIso_app

pullbackSpecIso_hom_naturality