NYLL
Module

PrimeAtPrimeEquiv.lean

Nyll.EtaleFundamentalGroups.Normalization.Localization.IntegralClosure.PrimeAtPrimeEquiv
4 declarations indexed from sourceView source ↗

Module documentation

Prime-local comparison for a localized normalization

For a normalization prime Q over a base prime P, localizing the global normalization at Q agrees canonically with first localizing the base at P, normalizing there, and then localizing at the image of Q. The equivalence is over the literal base localization A_P.

Imports3
Imported by5

Declarations

def

integralClosurePrimeLocalizationAlgEquiv

L36 ↗
EtaleFundamentalGroups.integralClosurePrimeLocalizationAlgEquiv
Documentation

The local ring at a normalization prime is canonically unchanged by first localizing the base at the contracted prime and transporting the normalization prime. No separately chosen prime or comparison equality is used.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
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 integralClosurePrimeLocalizationAlgEquiv
    (P : Ideal A) [P.IsPrime]
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver P] :
    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
    Localization.AtPrime Q ≃ₐ[Localization.AtPrime P]
      Localization.AtPrime q := by
  let V := Localization.AtPrime P
  let C := integralClosure A L
  letI := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
  letI : IsScalarTower A V L :=
    localizationAtPrimeToExtension_isScalarTower (K := K) (L := L) P
  let Cp := integralClosure V L
  letI := integralClosureLocalizationAlgebra (L := L) P
  let M := Algebra.algebraMapSubmonoid C P.primeCompl
  letI : IsLocalization M Cp :=
    isLocalization_integralClosure_localizationAtPrime
      (K := K) (L := L) P
  let q := localizedNormalizationPrime (K := K) (L := L) P Q
  letI : q.IsMaximal :=
    localizedNormalizationPrime_isMaximal (K := K) (L := L) P Q
  let Dglobal := Localization.AtPrime Q
  let Dlocal := Localization.AtPrime q
  letI : Algebra V Dglobal :=
    Localization.AtPrime.algebraOfLiesOver P Q
  have hdisj : Disjoint (M : Set C) (Q : Set C) := by
    exact Set.disjoint_image_left.mpr
      (Set.disjoint_compl_left_iff_subset.mpr
        (show Q.under A ≤ P by rw [Q.over_def P]))
  have hunder : q.under C = Q := by
    change (Q.map (algebraMap C Cp)).under C = Q
    exact IsLocalization.under_map_of_isPrime_disjoint M Cp inferInstance hdisj
  letI : IsLocalization Q.primeCompl Dlocal := by
    have hloc :=
      IsLocalization.isLocalization_isLocalization_atPrime_isLocalization
        M Dlocal q
    have hsub : (q.under C).primeCompl = Q.primeCompl := by
      ext x
      change (x ∉ q.under C) ↔ x ∉ Q
      rw [hunder]
    exact hsub ▸ hloc
  let e : Dglobal ≃ₐ[C] Dlocal :=
    IsLocalization.algEquiv Q.primeCompl Dglobal Dlocal
  refine
    { toRingEquiv := e.toRingEquiv
      commutes' := fun z ↦ ?_ }
  apply DFunLike.congr_fun (f :=
      e.toRingHom.comp (algebraMap V Dglobal))
    (g := algebraMap V Dlocal) ?_ z
  apply IsLocalization.ringHom_ext P.primeCompl
  ext a
  simp only [RingHom.comp_apply]
  rw [← IsScalarTower.algebraMap_apply A V Dglobal,
    ← IsScalarTower.algebraMap_apply A V Dlocal]
  exact e.commutes (algebraMap A C a)
def

integralClosurePrimeLocalizationAtUnderAlgEquiv

L102 ↗
EtaleFundamentalGroups.integralClosurePrimeLocalizationAtUnderAlgEquiv
Documentation

Contraction-specialized form of integralClosurePrimeLocalizationAlgEquiv. This is the form used for an arbitrary terminal normalization prime: the base prime and the transported prime are both constructed canonically from Q.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
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 integralClosurePrimeLocalizationAtUnderAlgEquiv
    (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
    Localization.AtPrime Q ≃ₐ[Localization.AtPrime P]
      Localization.AtPrime q := by
  dsimp only
  exact integralClosurePrimeLocalizationAlgEquiv
    (K := K) (L := L) (Q.under A) Q
def

IsAwayMapEtale

L121 ↗
EtaleFundamentalGroups.IsAwayMapEtale
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
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 · statement
def IsAwayMapEtale
    {R D : Type*} [CommRing R] [CommRing D] [Algebra R D]
    (f : R) : Prop
theorem

localization_awayMap_integralClosurePrime_etale_of_localized

L131 ↗
EtaleFundamentalGroups.localization_awayMap_integralClosurePrime_etale_of_localized
Documentation

Transport a literal local Away map from the normalization after base localization back to the local ring of the original normalization prime. The target is the literal Localization.AtPrime Q required by the global target-prime criterion.

Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
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]
omit [IsDomain A] in
Lean source · full declaration
theorem localization_awayMap_integralClosurePrime_etale_of_localized
    (P : Ideal A) [P.IsPrime]
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver P]
    (f : Localization.AtPrime P)
    (hAway :
      letI := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
      letI := localizationAtPrimeToExtension_isScalarTower
        (K := K) (L := L) P
      let q := localizedNormalizationPrime (K := K) (L := L) P Q
      letI : q.IsMaximal :=
        localizedNormalizationPrime_isMaximal (K := K) (L := L) P Q
      letI : q.IsPrime := (inferInstance : q.IsMaximal).isPrime
      IsAwayMapEtale (R := Localization.AtPrime P)
        (D := Localization.AtPrime q) f) :
    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
    RingHom.Etale
      (R := Localization.Away f)
      (S := Localization.Away
        (algebraMap (Localization.AtPrime P) (Localization.AtPrime Q) f))
      (Localization.awayMap
        (algebraMap (Localization.AtPrime P) (Localization.AtPrime Q)) f) := by
  let V := Localization.AtPrime P
  let := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
  let : IsScalarTower A V L :=
    localizationAtPrimeToExtension_isScalarTower (K := K) (L := L) P
  let : Algebra V (Localization.AtPrime Q) :=
    Localization.AtPrime.algebraOfLiesOver P Q
  let q := localizedNormalizationPrime (K := K) (L := L) P Q
  let : q.IsMaximal :=
    localizedNormalizationPrime_isMaximal (K := K) (L := L) P Q
  let : q.IsPrime := (inferInstance : q.IsMaximal).isPrime
  let E : Localization.AtPrime Q ≃ₐ[V] Localization.AtPrime q :=
    integralClosurePrimeLocalizationAlgEquiv
      (K := K) (L := L) P Q
  exact localization_awayMap_etale_of_algEquiv E.symm f hAway

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