Module

GlobalFiniteEtale.lean

Nyll.SchemeTheory.Affine.WeilRestriction.GlobalFiniteEtale

4 declarations indexed from sourceView source ↗

Module documentation

Finite étale internal Homs over an affine base

For finite étale R-algebras A and B, with A free as an R-module, the relative internal Hom from Spec A to Spec B is represented by a finite étale scheme over Spec R. The representing equivalence applies to every scheme over Spec R.

The finite étale structure is obtained from the algebraic Weil restriction theorem and the affine criteria for finite and étale scheme morphisms.

Imports8

Nyll.SchemeTheory.Affine.WeilRestriction.Global
Nyll.SchemeTheory.WeilRestriction.BaseChange
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Mathlib.RingTheory.RingHom.Finite
Mathlib.RingTheory.RingHom.Etale

Imported by2

instance

globalInternalHomSpecRepresenter_isFiniteEtale

L48 ↗

SchemeTheory.Affine.globalInternalHomSpecRepresenter_isFiniteEtale

Documentation

The structure morphism of the internal Hom's explicit affine representer is finite étale.

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.Affine
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.Etale R A]
  [Module.Finite R B] [Algebra.Etale R B]

Lean source · statement

instance globalInternalHomSpecRepresenter_isFiniteEtale :
    IsFiniteEtale (globalInternalHomSpecRepresenter
      (R := R) (A := A) (B := B)).hom

def

finiteEtaleInternalHomRepresenter

L65 ↗

SchemeTheory.Affine.finiteEtaleInternalHomRepresenter

Documentation

The finite étale scheme representing the relative internal Hom from Spec A to Spec B over Spec R.

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.Affine
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.Etale R A]
  [Module.Finite R B] [Algebra.Etale R B]

Lean source · full declaration

def finiteEtaleInternalHomRepresenter : FiniteEtale (Spec (CommRingCat.of R)) where
  toComma := globalInternalHomSpecRepresenter (R := R) (A := A) (B := B)
  prop := globalInternalHomSpecRepresenter_isFiniteEtale (R := R) (A := A) (B := B)

def

finiteEtaleInternalHomRepresentable

L71 ↗

SchemeTheory.Affine.finiteEtaleInternalHomRepresentable

Documentation

The finite étale internal Hom represents morphisms from T ×_{Spec R} Spec A to Spec B for every scheme T over Spec R.

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.Affine
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.Etale R A]
  [Module.Finite R B] [Algebra.Etale R B]

Lean source · statement

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

def

finiteEtaleInternalHomBaseChangeRepresentable

L79 ↗

SchemeTheory.Affine.finiteEtaleInternalHomBaseChangeRepresentable

Documentation

After any scheme base change, the finite etale pullback of the affine internal Hom still represents morphisms between the two pulled-back schemes.

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.Affine
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.Etale R A]
  [Module.Finite R B] [Algebra.Etale R B]

Lean source · statement

def finiteEtaleInternalHomBaseChangeRepresentable
    {S : Scheme.{u}} (f : S ⟶ Spec (CommRingCat.of R)) :
    (SchemeTheory.WeilRestriction.relativeInternalHomFunctor
      ((Over.pullback f).obj (specAOver (R := R) (A := A)))
      ((Over.pullback f).obj (specBOver (R := R) (B := B)))).RepresentableBy
        ((FiniteEtale.forget S).obj
          ((FiniteEtale.pullback f).obj
            (finiteEtaleInternalHomRepresenter (R := R) (A := A) (B := B))))

Module documentation

Finite étale internal Homs over an affine base

Declarations

globalInternalHomSpecRepresenter_isFiniteEtale

finiteEtaleInternalHomRepresenter

finiteEtaleInternalHomRepresentable

finiteEtaleInternalHomBaseChangeRepresentable