Nyll.EtaleFundamentalGroups.Normalization.Localization.IntegralClosure.IsoOver

def

arrowStalkMapIsoOfIsoOver

EtaleFundamentalGroups.arrowStalkMapIsoOfIsoOver

Documentation

If Z and S are isomorphic over X, the stalk map from Z at the point corresponding to s : S is isomorphic, as an arrow of commutative rings, to the stalk map from S at s.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open CategoryTheory
open AlgebraicGeometry
universe u uK

Lean source · statement

def arrowStalkMapIsoOfIsoOver
    {Z S X : Scheme.{u}} (e : Z ≅ S)
    (f : Z ⟶ X) (g : S ⟶ X) (h : e.hom ≫ g = f) (s : S) :
    Arrow.mk (f.stalkMap (e.inv s)) ≅ Arrow.mk (g.stalkMap s)

def

integralClosureStalkArrowIsoOfIsoOver

L61 ↗

EtaleFundamentalGroups.integralClosureStalkArrowIsoOfIsoOver

Documentation

A global morphism which is identified over Spec A with the spectrum of integralClosure A L has, at the point corresponding to Q, the canonical local map obtained by normalizing after localization at Q.under A.

Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open CategoryTheory
open AlgebraicGeometry
universe u uK
variable {A : Type u} {K : Type uK} {L : Type u}
variable [CommRing A] [IsDomain A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]

Lean source · full declaration

def integralClosureStalkArrowIsoOfIsoOver
    {Z : Scheme.{u}} (z : Z ⟶ Spec (.of A))
    (e : Z ≅ Spec (.of (integralClosure A L)))
    (h : e.hom ≫
      Spec.map (CommRingCat.ofHom
        (algebraMap A (integralClosure A L))) = z)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] :
    let P := Q.under A
    letI : P.IsPrime := inferInstance
    letI : Q.LiesOver P := inferInstance
    letI := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
    letI := localizationAtPrimeToExtension_isScalarTower
      (K := K) (L := L) P
    letI : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) :=
      Localization.AtPrime.algebraOfLiesOver P Q
    let q := localizedNormalizationPrime (K := K) (L := L) P Q
    letI : q.IsMaximal :=
      localizedNormalizationPrime_isMaximal (K := K) (L := L) P Q
    Arrow.mk
        (z.stalkMap
          (e.inv (⟨Q, inferInstance⟩ :
            PrimeSpectrum (integralClosure A L)))) ≅
      Arrow.mk (CommRingCat.ofHom
        (R := Localization.AtPrime P) (S := Localization.AtPrime q)
        (algebraMap (Localization.AtPrime P) (Localization.AtPrime q))) := by
  dsimp only
  exact arrowStalkMapIsoOfIsoOver e z
      (Spec.map (CommRingCat.ofHom
        (algebraMap A (integralClosure A L)))) h
      (⟨Q, inferInstance⟩ : PrimeSpectrum (integralClosure A L)) ≪≫
    integralClosureSpecStalkArrowIso (K := K) (L := L) Q

IsoOver.lean

Module documentation

Stalk comparison through an isomorphism over the base

arrowStalkMapIsoOfIsoOver

integralClosureStalkArrowIsoOfIsoOver

Module documentation

Stalk comparison through an isomorphism over the base

Declarations

arrowStalkMapIsoOfIsoOver

integralClosureStalkArrowIsoOfIsoOver