NYLL
Module

FiniteEtale.lean

Nyll.SchemeTheory.WeilRestriction.FiniteEtale
5 declarations indexed from sourceView source ↗

Module documentation

Finite étale internal Hom over arbitrary schemes

Restrict two finite étale schemes to the directed cover by all affine opens of the base. The affine internal Hom representers represent the restrictions of a single sheaf, by the base change comparison. Their canonical transitions therefore glue to a finite étale representer over the whole base.

Imports8
Imported by5

Declarations

def

finiteEtaleInternalHomCoverRepresenter

L41 ↗
SchemeTheory.WeilRestriction.finiteEtaleInternalHomCoverRepresenter
Documentation

The finite etale scheme representing the relative internal Hom of U and V on a chart of the directed affine cover of S.

Source context 6 commands

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

@[expose] public section
open CategoryTheory AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable (S : Scheme.{u}) (U V : FiniteEtale S)
Lean source · statement
def finiteEtaleInternalHomCoverRepresenter (i : S.directedAffineCover.I₀) :
    FiniteEtale (S.directedAffineCover.X i)
def

finiteEtaleInternalHomCoverRepresentable

L51 ↗
SchemeTheory.WeilRestriction.finiteEtaleInternalHomCoverRepresentable
Documentation

The representation of the relative internal Hom restricted to an affine-cover chart by its finite etale local representer.

Source context 6 commands

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

@[expose] public section
open CategoryTheory AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable (S : Scheme.{u}) (U V : FiniteEtale S)
Lean source · statement
def finiteEtaleInternalHomCoverRepresentable (i : S.directedAffineCover.I₀) :
    ((Over.map (S.directedAffineCover.f i)).op ⋙
      relativeInternalHomFunctor ((FiniteEtale.forget S).obj U)
        ((FiniteEtale.forget S).obj V)).RepresentableBy
          ((FiniteEtale.forget (S.directedAffineCover.X i)).obj
            (finiteEtaleInternalHomCoverRepresenter S U V i))
def

finiteEtaleInternalHomRepresenter

L66 ↗
SchemeTheory.WeilRestriction.finiteEtaleInternalHomRepresenter
Documentation

The finite étale scheme representing the relative internal Hom of U and V.

Source context 6 commands

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

@[expose] public section
open CategoryTheory AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable (S : Scheme.{u}) (U V : FiniteEtale S)
Lean source · full declaration
def finiteEtaleInternalHomRepresenter : FiniteEtale S where
  toComma := gluedLocalRepresenter
    (relativeInternalHomFunctor ((FiniteEtale.forget S).obj U) ((FiniteEtale.forget S).obj V))
    S.directedAffineCover
    (fun i ↦ (FiniteEtale.forget (S.directedAffineCover.X i)).obj
      (finiteEtaleInternalHomCoverRepresenter S U V i))
    (fun i ↦ finiteEtaleInternalHomCoverRepresentable S U V i)
  prop := gluedLocalRepresenter_isFiniteEtale
    (relativeInternalHomFunctor ((FiniteEtale.forget S).obj U) ((FiniteEtale.forget S).obj V))
    S.directedAffineCover
    (fun i ↦ (FiniteEtale.forget (S.directedAffineCover.X i)).obj
      (finiteEtaleInternalHomCoverRepresenter S U V i))
    (fun i ↦ finiteEtaleInternalHomCoverRepresentable S U V i)
    (fun i ↦ (finiteEtaleInternalHomCoverRepresenter S U V i).prop)
def

finiteEtaleInternalHomRepresentable

L82 ↗
SchemeTheory.WeilRestriction.finiteEtaleInternalHomRepresentable
Documentation

The constructed finite étale scheme represents internal Hom on all schemes over the base.

Source context 6 commands

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

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

finiteEtaleInternalHomBaseChangeRepresentable

L96 ↗
SchemeTheory.WeilRestriction.finiteEtaleInternalHomBaseChangeRepresentable
Documentation

Pulling back the representing finite étale scheme represents the pulled-back internal Hom.

Source context 6 commands

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

@[expose] public section
open CategoryTheory AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction
variable (S : Scheme.{u}) (U V : FiniteEtale S)
Lean source · statement
def finiteEtaleInternalHomBaseChangeRepresentable {S T : Scheme.{u}}
    (f : T ⟶ S) (U V : FiniteEtale S) :
    (relativeInternalHomFunctor
      ((FiniteEtale.forget T).obj ((FiniteEtale.pullback f).obj U))
      ((FiniteEtale.forget T).obj ((FiniteEtale.pullback f).obj V))).RepresentableBy
        ((FiniteEtale.forget T).obj ((FiniteEtale.pullback f).obj
          (finiteEtaleInternalHomRepresenter 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.