Module

LocalRestriction.lean

Nyll.SchemeTheory.Affine.WeilRestriction.LocalRestriction

2 declarations indexed from sourceView source ↗

Module documentation

Local representers of the restricted global internal Hom

The local tensor-product construction represents the restriction of one fixed presheaf on schemes over Spec R. The comparison combines geometric base change with the spectrum of a tensor product. This provides the local witnesses needed for gluing without assuming compatibility of separately constructed functors.

Imports5

Imported by2

def

globalInternalHomRestrictionBaseChangeIso

L38 ↗

SchemeTheory.Affine.globalInternalHomRestrictionBaseChangeIso

Documentation

Restricting the affine internal Hom to Spec S agrees with scalar extension of its two input algebras. No freeness or finiteness is needed for this comparison.

Source context 6 commands

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

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

Lean source · statement

def globalInternalHomRestrictionBaseChangeIso
    {R S A B : Type u} [CommRing R] [CommRing S] [CommRing A] [CommRing B]
    [Algebra R S] [Algebra R A] [Algebra R B] :
    (Over.map (Spec.map (CommRingCat.ofHom (algebraMap R S)))).op ⋙
        globalInternalHomFunctor (R := R) (A := A) (B := B) ≅
      globalInternalHomFunctor (R := S) (A := S ⊗[R] A) (B := S ⊗[R] B)

theorem

exists_finiteEtaleInternalHomRepresentable_restrict_away

L52 ↗

SchemeTheory.Affine.exists_finiteEtaleInternalHomRepresentable_restrict_away