Module

Global.lean

Nyll.SchemeTheory.Affine.WeilRestriction.Global

11 declarations indexed from sourceView source ↗

Module documentation

Affine Weil restriction on arbitrary test schemes

For finite free A/R and finitely presented B/R, the algebraic Weil restriction represents the relative internal Hom on every scheme over Spec R. The proof extends the affine comparison along the cover-dense affine subsite. The final representing object is the spectrum of the explicit representing algebra.

This is the finite-free affine-base step towards Stacks Project, Tag 0BL7.

Imports4

Nyll.SchemeTheory.Affine.WeilRestriction.InternalHom
Nyll.SchemeTheory.WeilRestriction.Sheaf
Mathlib.AlgebraicGeometry.Sites.BigZariski
Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Imported by7

instance

affineForgetCoverDense

L38 ↗

SchemeTheory.Affine.affineForgetCoverDense

Documentation

Affine schemes over an affine base cover every object of its big Zariski site.

Source context 6 commands

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

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

Lean source · full declaration

instance affineForgetCoverDense (R : CommRingCat.{u}) :
    (affineForget R).IsCoverDense (Scheme.zariskiTopology.over (Spec R)) where
  is_cover T := by
    rw [GrothendieckTopology.mem_over_iff]
    refine Scheme.zariskiTopology.superset_covering ?_
      T.left.affineCover.mem_grothendieckTopology
    rw [Sieve.generate_le_iff]
    intro X f hf
    obtain ⟨i⟩ := hf
    rw [Sieve.overEquiv_iff]
    have h : IsAffineHom (T.left.affineCover.f i ≫ T.hom) :=
      isAffineHom_of_isAffine (T.left.affineCover.f i ≫ T.hom)
    let Y : affineHomProperty.Over ⊤ (Spec R) :=
      MorphismProperty.Over.mk ⊤ (T.left.affineCover.f i ≫ T.hom) h
    let g : (affineForget R).obj Y ⟶ T := Over.homMk (T.left.affineCover.f i)
    change Nonempty (Presieve.CoverByImageStructure (affineForget R) _)
    refine ⟨⟨Y, 𝟙 _, g, ?_⟩⟩
    ext
    rfl

def

affineForgetYonedaIso

L59 ↗

SchemeTheory.Affine.affineForgetYonedaIso

Documentation

Restricting the Yoneda presheaf of an affine object gives its affine Yoneda presheaf.

Source context 6 commands

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

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

Lean source · statement

def affineForgetYonedaIso (R : CommRingCat.{u})
    (X : affineHomProperty.Over ⊤ (Spec R)) :
    (affineForget R).op ⋙ yoneda.obj ((affineForget R).obj X) ≅ yoneda.obj X

abbrev

globalInternalHomFunctor

L79 ↗

SchemeTheory.Affine.globalInternalHomFunctor

Documentation

The relative internal Hom on all schemes over Spec R.

Source context 8 commands

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

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

Lean source · statement

abbrev globalInternalHomFunctor :
    (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type u

abbrev

globalInternalHomRepresenter

L85 ↗

SchemeTheory.Affine.globalInternalHomRepresenter

Documentation

The affine representer viewed in the category of all schemes over Spec R.

Source context 8 commands

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

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

Lean source · statement

abbrev globalInternalHomRepresenter : Over (Spec (CommRingCat.of R))

def

affineActualProductOpIso

L91 ↗

SchemeTheory.Affine.affineActualProductOpIso

Documentation

The opposite affine fibre-product functor is the composite of the opposite forgetful and fibre-product functors.

Source context 8 commands

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

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

Lean source · statement

def affineActualProductOpIso :
    (affineActualProductFunctor (R := R) (A := A)).op ≅
      (affineForget (CommRingCat.of R)).op ⋙
        (MonoidalCategory.tensorRight (specAOver (R := R) (A := A))).op

def

affineInternalHomRestrictionIso

L99 ↗

SchemeTheory.Affine.affineInternalHomRestrictionIso

Documentation

The affine internal-Hom functor is the restriction of the global internal-Hom functor to affine test schemes.

Source context 8 commands

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

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

Lean source · statement

def affineInternalHomRestrictionIso :
    affineInternalHomFunctor (R := R) (A := A) (B := B) ≅
      (affineForget (CommRingCat.of R)).op ⋙
        globalInternalHomFunctor (R := R) (A := A) (B := B)

def

restrictedGlobalInternalHomIso

L109 ↗

SchemeTheory.Affine.restrictedGlobalInternalHomIso

Documentation

The global internal-Hom representation restricts to its natural representation on affine test schemes.

Source context 8 commands

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

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

Lean source · statement

def restrictedGlobalInternalHomIso :
    (affineForget (CommRingCat.of R)).op ⋙
        yoneda.obj (globalInternalHomRepresenter (R := R) (A := A) (B := B)) ≅
      (affineForget (CommRingCat.of R)).op ⋙
        globalInternalHomFunctor (R := R) (A := A) (B := B)

def

globalInternalHomRepresentable

L120 ↗

SchemeTheory.Affine.globalInternalHomRepresentable

Documentation

The affine representer represents the internal Hom on arbitrary test schemes.

Source context 8 commands

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

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

Lean source · statement

def globalInternalHomRepresentable :
    (globalInternalHomFunctor (R := R) (A := A) (B := B)).RepresentableBy
      (globalInternalHomRepresenter (R := R) (A := A) (B := B))

abbrev

globalInternalHomSpecRepresenter

L142 ↗

SchemeTheory.Affine.globalInternalHomSpecRepresenter

Documentation

The spectrum of the algebraic Weil restriction, with its structure map to Spec R.

Source context 8 commands

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

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

Lean source · statement

abbrev globalInternalHomSpecRepresenter : Over (Spec (CommRingCat.of R))

def

globalInternalHomRepresenterIsoSpec

L147 ↗

SchemeTheory.Affine.globalInternalHomRepresenterIsoSpec

Documentation

Identify the affine-category construction with the explicit spectrum.

Source context 8 commands

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

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

Lean source · statement

def globalInternalHomRepresenterIsoSpec :
    globalInternalHomRepresenter (R := R) (A := A) (B := B) ≅
      globalInternalHomSpecRepresenter (R := R) (A := A) (B := B)

def

globalInternalHomSpecRepresentable

L157 ↗

SchemeTheory.Affine.globalInternalHomSpecRepresentable

Documentation

The explicit spectrum represents the relative internal Hom on all test schemes.

Source context 8 commands

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

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

Lean source · statement

def globalInternalHomSpecRepresentable :
    (globalInternalHomFunctor (R := R) (A := A) (B := B)).RepresentableBy
      (globalInternalHomSpecRepresenter (R := R) (A := A) (B := B))

Module documentation

Affine Weil restriction on arbitrary test schemes

Declarations