NYLL
Module

Affine.lean

Nyll.SchemeTheory.WeilRestriction.Affine
4 declarations indexed from sourceView source ↗

Module documentation

Finite étale internal Hom over an affine scheme

The global sections of a finite étale scheme over an affine base form a finite étale algebra. The naturality square of isoSpec identifies the original relative scheme with the pullback of the spectrum of this algebra. Pulling back the algebraic internal Hom representer and transporting its two arguments therefore gives an internal Hom over any affine base scheme.

Imports6
Imported by3

Declarations

def

affineFiniteEtaleAlgebra

L39 ↗
SchemeTheory.WeilRestriction.affineFiniteEtaleAlgebra
Documentation

Global sections with the algebra structure induced by the structure morphism.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable (S : Scheme.{u}) [IsAffine S]
Lean source · statement
def affineFiniteEtaleAlgebra (U : FiniteEtale S) :
    CommAlgCat.FiniteEtale.{u} Γ(S, ⊤)
def

affineFiniteEtaleSpecPullbackIso

L58 ↗
SchemeTheory.WeilRestriction.affineFiniteEtaleSpecPullbackIso
Documentation

The naturality square of isoSpec presents a finite étale object as a pullback.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable (S : Scheme.{u}) [IsAffine S]
Lean source · statement
def affineFiniteEtaleSpecPullbackIso (U : FiniteEtale S) :
    (FiniteEtale.forget S).obj U ≅
      (Over.pullback S.isoSpec.hom).obj
        (SchemeTheory.Affine.specAOver
          (R := Γ(S, ⊤)) (A := affineFiniteEtaleAlgebra S U))
def

affineFiniteEtaleInternalHomRepresenter

L76 ↗
SchemeTheory.WeilRestriction.affineFiniteEtaleInternalHomRepresenter
Documentation

A finite étale representer of relative internal Hom over an affine base.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable (S : Scheme.{u}) [IsAffine S]
Lean source · statement
def affineFiniteEtaleInternalHomRepresenter (U V : FiniteEtale S) : FiniteEtale S
def

affineFiniteEtaleInternalHomRepresentable

L83 ↗
SchemeTheory.WeilRestriction.affineFiniteEtaleInternalHomRepresentable
Documentation

The constructed finite étale object represents relative internal Hom.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable (S : Scheme.{u}) [IsAffine S]
Lean source · statement
def affineFiniteEtaleInternalHomRepresentable (U V : FiniteEtale S) :
    (relativeInternalHomFunctor
      ((FiniteEtale.forget S).obj U) ((FiniteEtale.forget S).obj V)).RepresentableBy
        ((FiniteEtale.forget S).obj (affineFiniteEtaleInternalHomRepresenter S U V))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.