Module

GluedRepresentable.lean

Nyll.SchemeTheory.Affine.WeilRestriction.GluedRepresentable

2 declarations indexed from sourceView source ↗

Module documentation

Finite étale internal Hom without a global basis

For finite étale R-algebras A and B, the locally constructed internal Hom schemes glue to a finite étale scheme representing the internal Hom on all schemes over Spec R. The sheaf condition supplies the global representing property. Pulling this object back represents the internal Hom after an arbitrary scheme base change.

No global freeness assumption on A is used.

Imports6

Imported by2

def

finiteEtaleInternalHomGluedRepresentable

L46 ↗

SchemeTheory.Affine.finiteEtaleInternalHomGluedRepresentable

Documentation

The glued finite étale scheme represents the internal Hom on all test schemes.

Source context 7 commands

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

@[expose] public section
open CategoryTheory AlgebraicGeometry
open SchemeTheory.WeilRestriction
noncomputable section
universe u
namespace SchemeTheory.Affine
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
  [Module.Finite R A] [Algebra.Etale R A]
  [Module.Finite R B] [Algebra.Etale R B]

Lean source · statement

def finiteEtaleInternalHomGluedRepresentable :
    (globalInternalHomFunctor (R := R) (A := A) (B := B)).RepresentableBy
      ((FiniteEtale.forget (Spec (CommRingCat.of R))).obj
        (finiteEtaleInternalHomGlued (R := R) (A := A) (B := B)))

def

finiteEtaleInternalHomGluedBaseChangeRepresentable

L61 ↗

SchemeTheory.Affine.finiteEtaleInternalHomGluedBaseChangeRepresentable