Module

GlobalBaseChange.lean

Nyll.SchemeTheory.Affine.WeilRestriction.GlobalBaseChange

3 declarations indexed from sourceView source ↗

Module documentation

Base change of the global affine internal Hom

For finite free A/R and finitely presented B/R, the explicit spectrum representing the relative internal Hom commutes with arbitrary affine base change. The comparison is an isomorphism over Spec S, obtained from the algebraic base-change isomorphism and the spectrum of a tensor product.

Imports5

Nyll.SchemeTheory.Affine.WeilRestriction.Global
Nyll.SchemeTheory.Affine.WeilRestriction.FiniteEtale
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Comma.Over.Pullback
Mathlib.RingTheory.TensorProduct.Finite

Imported by2

def

specOverBaseChangeIso

L38 ↗

SchemeTheory.Affine.specOverBaseChangeIso

Documentation

The pullback of a spectrum to Spec S is the spectrum of its scalar extension.

Source context 7 commands

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

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

Lean source · statement

def specOverBaseChangeIso
    (R S C : Type u) [CommRing R] [CommRing S] [CommRing C]
    [Algebra R S] [Algebra R C] :
    (Over.pullback
      (Spec.map (CommRingCat.ofHom (algebraMap R S)))).obj
        ((specOverFunctor (CommRingCat.of R)).obj
          (Opposite.op (CommAlgCat.of R C))) ≅
      (specOverFunctor (CommRingCat.of S)).obj
        (Opposite.op (CommAlgCat.of S (S ⊗[R] C)))

def

globalInternalHomSpecBaseChangeIso

L73 ↗

SchemeTheory.Affine.globalInternalHomSpecBaseChangeIso

Documentation

The global affine internal Hom representer commutes with affine base change.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
open scoped TensorProduct
universe u
noncomputable section
namespace SchemeTheory.Affine
section BaseChange
variable {R S A B : Type u}
  [CommRing R] [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]

Lean source · statement

def globalInternalHomSpecBaseChangeIso :
    (Over.pullback
      (Spec.map (CommRingCat.ofHom (algebraMap R S)))).obj
        (globalInternalHomSpecRepresenter (R := R) (A := A) (B := B)) ≅
      globalInternalHomSpecRepresenter
        (R := S) (A := S ⊗[R] A) (B := S ⊗[R] B)

def

globalInternalHomSpecBaseChangeRepresentable

L86 ↗

SchemeTheory.Affine.globalInternalHomSpecBaseChangeRepresentable

Documentation

The pulled-back representer represents the internal Hom after scalar extension.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry
open scoped TensorProduct
universe u
noncomputable section
namespace SchemeTheory.Affine
section BaseChange
variable {R S A B : Type u}
  [CommRing R] [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]

Lean source · statement

def globalInternalHomSpecBaseChangeRepresentable :
    (globalInternalHomFunctor
      (R := S) (A := S ⊗[R] A) (B := S ⊗[R] B)).RepresentableBy
        ((Over.pullback
          (Spec.map (CommRingCat.ofHom (algebraMap R S)))).obj
            (globalInternalHomSpecRepresenter (R := R) (A := A) (B := B)))

Module documentation

Base change of the global affine internal Hom

Declarations

specOverBaseChangeIso

globalInternalHomSpecBaseChangeIso

globalInternalHomSpecBaseChangeRepresentable