NYLL
Module

LocalCover.lean

Nyll.SchemeTheory.Affine.WeilRestriction.LocalCover
5 declarations indexed from sourceView source ↗

Module documentation

A principal open cover carrying finite étale internal Homs

For finite étale R-algebras A and B, we construct an open cover of Spec R by spectra of principal localizations. On each member of the cover, the restriction of the fixed global internal Hom presheaf is represented by an explicitly chosen finite étale scheme. These are local witnesses for the subsequent gluing construction.

Imports6
Imported by2

Declarations

def

finiteEtaleInternalHomLocalElement

L44 ↗
SchemeTheory.Affine.finiteEtaleInternalHomLocalElement
Documentation

An element outside p whose principal neighborhood admits a finite étale representer of the restricted 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.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 finiteEtaleInternalHomLocalElement (p : PrimeSpectrum R) : R
lemma

finiteEtaleInternalHomLocalElement_not_mem

L48 ↗
SchemeTheory.Affine.finiteEtaleInternalHomLocalElement_not_mem
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.Finite R A] [Algebra.Etale R A]
  [Module.Finite R B] [Algebra.Etale R B]
Lean source · statement
lemma finiteEtaleInternalHomLocalElement_not_mem (p : PrimeSpectrum R) :
    finiteEtaleInternalHomLocalElement (R := R) (A := A) (B := B) p ∉ p.asIdeal
def

finiteEtaleInternalHomOpenCover

L55 ↗
SchemeTheory.Affine.finiteEtaleInternalHomOpenCover
Documentation

A cover of Spec R by principal neighborhoods carrying finite étale representers of the relative 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.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 finiteEtaleInternalHomOpenCover : (Spec (CommRingCat.of R)).OpenCover where
  I₀ := PrimeSpectrum R
  X p := Spec (CommRingCat.of (Localization.Away
    (finiteEtaleInternalHomLocalElement (R := R) (A := A) (B := B) p)))
  f p := Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away
    (finiteEtaleInternalHomLocalElement (R := R) (A := A) (B := B) p))))
  mem₀ := by
    rw [Scheme.presieve₀_mem_precoverage_iff]
    refine ⟨?_, ?_⟩
    · intro p
      refine ⟨p, ?_⟩
      change p ∈ Set.range (PrimeSpectrum.comap (algebraMap R (Localization.Away
        (finiteEtaleInternalHomLocalElement (R := R) (A := A) (B := B) p))))
      rw [PrimeSpectrum.localization_away_comap_range
        (Localization.Away
          (finiteEtaleInternalHomLocalElement (R := R) (A := A) (B := B) p))
        (finiteEtaleInternalHomLocalElement (R := R) (A := A) (B := B) p)]
      exact finiteEtaleInternalHomLocalElement_not_mem (R := R) (A := A) (B := B) p
    · intro p
      exact Scheme.isOpenImmersion_SpecMap_localizationAway
        (R := CommRingCat.of R)
        (finiteEtaleInternalHomLocalElement (R := R) (A := A) (B := B) p)
def

finiteEtaleInternalHomOpenCoverRepresenter

L79 ↗
SchemeTheory.Affine.finiteEtaleInternalHomOpenCoverRepresenter
Documentation

A finite étale representer on a member of the principal open cover.

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.Finite R A] [Algebra.Etale R A]
  [Module.Finite R B] [Algebra.Etale R B]
Lean source · statement
def finiteEtaleInternalHomOpenCoverRepresenter (p : PrimeSpectrum R) :
    FiniteEtale ((finiteEtaleInternalHomOpenCover (R := R) (A := A) (B := B)).X p)
def

finiteEtaleInternalHomOpenCoverRepresentable

L86 ↗
SchemeTheory.Affine.finiteEtaleInternalHomOpenCoverRepresentable
Documentation

On each member of the cover, the chosen finite étale scheme represents the restriction of the same global internal Hom presheaf.

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.Finite R A] [Algebra.Etale R A]
  [Module.Finite R B] [Algebra.Etale R B]
Lean source · statement
def finiteEtaleInternalHomOpenCoverRepresentable (p : PrimeSpectrum R) :
    ((Over.map ((finiteEtaleInternalHomOpenCover
      (R := R) (A := A) (B := B)).f p)).op ⋙
        globalInternalHomFunctor (R := R) (A := A) (B := B)).RepresentableBy
          ((FiniteEtale.forget ((finiteEtaleInternalHomOpenCover
            (R := R) (A := A) (B := B)).X p)).obj
              (finiteEtaleInternalHomOpenCoverRepresenter (R := R) (A := A) (B := B) p))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.