NYLL
Module

EtaleStalkPrimeLocalization.lean

Nyll.SchemeTheory.LocalGeometry.EtaleStalkPrimeLocalization
7 declarations indexed from sourceView source ↗

Module documentation

Prime localizations of etale scheme stalks

An etale morphism induces a formally etale, essentially finite type map on stalks. These properties persist after localizing the target stalk at an arbitrary prime. The resulting map need not be etale: prime localization is not finite presentation in general. A separate theorem records the exact finite-presentation hypothesis which upgrades the map to an etale algebra.

Imports2
  • Mathlib.AlgebraicGeometry.Morphisms.Etale
  • Mathlib.RingTheory.RingHom.EssFiniteType
Imported by3

Declarations

def

stalkPrimeLocalizationAlgebra

L33 ↗
AlgebraicGeometry.Scheme.Hom.stalkPrimeLocalizationAlgebra
Documentation

The canonical algebra structure on a prime localization of a source stalk, over the corresponding target stalk of a scheme morphism.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}}
Lean source · statement
def stalkPrimeLocalizationAlgebra
    (f : Y ⟶ X) (y : Y) (P : Ideal (Y.presheaf.stalk y)) [P.IsPrime] :
    Algebra (X.presheaf.stalk (f y)) (Localization.AtPrime P)
theorem

stalkMap_ringHom_formallyEtale_of_etale

L40 ↗
AlgebraicGeometry.Scheme.Hom.stalkMap_ringHom_formallyEtale_of_etale
Documentation

The map on stalks of an etale morphism is formally etale.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}}
Lean source · statement
theorem stalkMap_ringHom_formallyEtale_of_etale
    (f : Y ⟶ X) [Etale f] (y : Y) :
    (f.stalkMap y).hom.FormallyEtale
theorem

stalkMap_formallyEtale_of_etale

L57 ↗
AlgebraicGeometry.Scheme.Hom.stalkMap_formallyEtale_of_etale
Documentation

The map on stalks of an etale morphism is formally etale.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}}
Lean source · full declaration
theorem stalkMap_formallyEtale_of_etale
    (f : Y ⟶ X) [Etale f] (y : Y) :
    letI : Algebra (X.presheaf.stalk (f y)) (Y.presheaf.stalk y) :=
      (f.stalkMap y).hom.toAlgebra
    Algebra.FormallyEtale (X.presheaf.stalk (f y))
      (Y.presheaf.stalk y) := by
  exact f.stalkMap_ringHom_formallyEtale_of_etale y
theorem

stalkPrimeLocalization_ringHom_formallyEtale_of_etale

L67 ↗
AlgebraicGeometry.Scheme.Hom.stalkPrimeLocalization_ringHom_formallyEtale_of_etale
Documentation

Localizing the source stalk of an etale morphism at any prime remains formally etale over the target stalk, for the literal composite algebra map.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}}
Lean source · statement
theorem stalkPrimeLocalization_ringHom_formallyEtale_of_etale
    (f : Y ⟶ X) [Etale f] (y : Y)
    (P : Ideal (Y.presheaf.stalk y)) [P.IsPrime] :
    ((algebraMap (Y.presheaf.stalk y) (Localization.AtPrime P)).comp
      (f.stalkMap y).hom).FormallyEtale
theorem

stalkPrimeLocalization_formallyEtale_of_etale

L86 ↗
AlgebraicGeometry.Scheme.Hom.stalkPrimeLocalization_formallyEtale_of_etale
Documentation

Localizing the source stalk of an etale morphism at any prime remains formally etale over the target stalk, for the literal composite algebra map.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}}
Lean source · full declaration
theorem stalkPrimeLocalization_formallyEtale_of_etale
    (f : Y ⟶ X) [Etale f] (y : Y)
    (P : Ideal (Y.presheaf.stalk y)) [P.IsPrime] :
    letI : Algebra (X.presheaf.stalk (f y)) (Localization.AtPrime P) :=
      f.stalkPrimeLocalizationAlgebra y P
    Algebra.FormallyEtale (X.presheaf.stalk (f y))
      (Localization.AtPrime P) := by
  exact f.stalkPrimeLocalization_ringHom_formallyEtale_of_etale y P
theorem

stalkPrimeLocalization_essFiniteType_of_etale

L97 ↗
AlgebraicGeometry.Scheme.Hom.stalkPrimeLocalization_essFiniteType_of_etale
Documentation

Localizing the source stalk of an etale morphism at any prime is essentially of finite type over the target stalk.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}}
Lean source · full declaration
theorem stalkPrimeLocalization_essFiniteType_of_etale
    (f : Y ⟶ X) [Etale f] (y : Y)
    (P : Ideal (Y.presheaf.stalk y)) [P.IsPrime] :
    letI : Algebra (X.presheaf.stalk (f y)) (Localization.AtPrime P) :=
      f.stalkPrimeLocalizationAlgebra y P
    Algebra.EssFiniteType (X.presheaf.stalk (f y))
      (Localization.AtPrime P) := by
  let A := X.presheaf.stalk (f y)
  let B := Y.presheaf.stalk y
  let C := Localization.AtPrime P
  have hAB : (f.stalkMap y).hom.EssFiniteType :=
    AlgebraicGeometry.LocallyOfFiniteType.stalkMap f y
  have hBC : (algebraMap B C).EssFiniteType := by
    rw [RingHom.essFiniteType_algebraMap]
    exact Algebra.EssFiniteType.of_isLocalization C P.primeCompl
  change ((algebraMap B C).comp (f.stalkMap y).hom).EssFiniteType
  exact hAB.comp hBC
theorem

stalkPrimeLocalization_etale_of_finitePresentation

L117 ↗
AlgebraicGeometry.Scheme.Hom.stalkPrimeLocalization_etale_of_finitePresentation
Documentation

The prime-localized stalk map is etale exactly when finite presentation is supplied in addition to the canonical formal-etaleness result.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}}
Lean source · full declaration
theorem stalkPrimeLocalization_etale_of_finitePresentation
    (f : Y ⟶ X) [Etale f] (y : Y)
    (P : Ideal (Y.presheaf.stalk y)) [P.IsPrime]
    (hfp :
      letI : Algebra (X.presheaf.stalk (f y)) (Localization.AtPrime P) :=
        f.stalkPrimeLocalizationAlgebra y P
      Algebra.FinitePresentation (X.presheaf.stalk (f y))
        (Localization.AtPrime P)) :
    letI : Algebra (X.presheaf.stalk (f y)) (Localization.AtPrime P) :=
      f.stalkPrimeLocalizationAlgebra y P
    Algebra.Etale (X.presheaf.stalk (f y))
      (Localization.AtPrime P) := by
  let A := X.presheaf.stalk (f y)
  let B := Y.presheaf.stalk y
  let C := Localization.AtPrime P
  let phi := (algebraMap B C).comp (f.stalkMap y).hom
  change phi.Etale
  exact @Algebra.Etale.mk A C _ _ phi.toAlgebra
    (f.stalkPrimeLocalization_ringHom_formallyEtale_of_etale y P) hfp

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