Module

Glued.lean

Nyll.SchemeTheory.Affine.WeilRestriction.Glued

5 declarations indexed from sourceView source ↗

Module documentation

Gluing finite étale internal Hom candidates

For finite étale R-algebras A and B, refine the principal open cover carrying local internal Hom representers to a locally directed open cover. Pulling back the local representers gives representations of the restrictions of one fixed presheaf. These representations determine the transition maps and pullback squares, so the local finite étale schemes glue over Spec R.

No global freeness assumption on A is used. The representing property of the glued scheme is a separate sheaf-descent step.

Imports6

Imported by2

abbrev

finiteEtaleInternalHomDirectedCover

L47 ↗

SchemeTheory.Affine.finiteEtaleInternalHomDirectedCover

Documentation

A locally directed refinement of the principal cover carrying local internal Homs.

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

abbrev finiteEtaleInternalHomDirectedCover : (Spec (CommRingCat.of R)).OpenCover

def

finiteEtaleInternalHomDirectedRepresenter

L51 ↗

SchemeTheory.Affine.finiteEtaleInternalHomDirectedRepresenter

Documentation

Pull back a principal-cover representer to a member of the directed refinement.

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 finiteEtaleInternalHomDirectedRepresenter
    (i : (finiteEtaleInternalHomDirectedCover (R := R) (A := A) (B := B)).I₀) :
    FiniteEtale ((finiteEtaleInternalHomDirectedCover (R := R) (A := A) (B := B)).X i)

def

finiteEtaleInternalHomDirectedRepresentable

L61 ↗

SchemeTheory.Affine.finiteEtaleInternalHomDirectedRepresentable

Documentation

Each refined local scheme represents the restriction of the fixed internal Hom presheaf.

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 finiteEtaleInternalHomDirectedRepresentable
    (i : (finiteEtaleInternalHomDirectedCover (R := R) (A := A) (B := B)).I₀) :
    ((Over.map ((finiteEtaleInternalHomDirectedCover
      (R := R) (A := A) (B := B)).f i)).op ⋙
        globalInternalHomFunctor (R := R) (A := A) (B := B)).RepresentableBy
          ((FiniteEtale.forget ((finiteEtaleInternalHomDirectedCover
            (R := R) (A := A) (B := B)).X i)).obj
              (finiteEtaleInternalHomDirectedRepresenter (R := R) (A := A) (B := B) i))

def

finiteEtaleInternalHomGluingData

L91 ↗

SchemeTheory.Affine.finiteEtaleInternalHomGluingData

Documentation

The local universal elements determine relative gluing data over the directed cover.

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 finiteEtaleInternalHomGluingData :
    (finiteEtaleInternalHomDirectedCover (R := R) (A := A) (B := B)).RelativeGluingData

def

finiteEtaleInternalHomGlued

L102 ↗

SchemeTheory.Affine.finiteEtaleInternalHomGlued

Documentation

The finite étale scheme obtained by gluing the local internal Hom representers.

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 · full declaration

def finiteEtaleInternalHomGlued : FiniteEtale (Spec (CommRingCat.of R)) where
  toComma := Over.mk (finiteEtaleInternalHomGluingData (R := R) (A := A) (B := B)).toBase
  prop := gluedLocalRepresenter_isFiniteEtale
    (globalInternalHomFunctor (R := R) (A := A) (B := B))
    (finiteEtaleInternalHomDirectedCover (R := R) (A := A) (B := B))
    (fun i ↦ (FiniteEtale.forget ((finiteEtaleInternalHomDirectedCover
      (R := R) (A := A) (B := B)).X i)).obj
        (finiteEtaleInternalHomDirectedRepresenter (R := R) (A := A) (B := B) i))
    (fun i ↦ finiteEtaleInternalHomDirectedRepresentable (R := R) (A := A) (B := B) i)
    (fun i ↦ (finiteEtaleInternalHomDirectedRepresenter (R := R) (A := A) (B := B) i).prop)

Module documentation

Gluing finite étale internal Hom candidates

Declarations

finiteEtaleInternalHomDirectedCover

finiteEtaleInternalHomDirectedRepresenter

finiteEtaleInternalHomDirectedRepresentable

finiteEtaleInternalHomGluingData

finiteEtaleInternalHomGlued