NYLL
Module

Basic.lean

Nyll.EtaleFundamentalGroups.Normalization.Primes.Basic
5 declarations indexed from sourceView source ↗

Module documentation

Primes in a localized normalization

This file transports a prime of a normalization lying over P to the normalization after localizing the base at P. The construction uses the canonical normalization inclusion from NormalizationLocalization and the general prime-localization API; it does not require the original normalization to be a Dedekind domain.

Imports2
Imported by8

Declarations

def

localizedNormalizationPrime

L38 ↗
EtaleFundamentalGroups.localizedNormalizationPrime
Documentation

The extension of a normalization prime to the normalization after localizing the base at P.

Source context 10 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]
section Prime
variable (P : Ideal A) [P.IsPrime]
Lean source · full declaration
def localizedNormalizationPrime
    (Q : Ideal (integralClosure A L)) :
    letI := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
    letI := localizationAtPrimeToExtension_isScalarTower (K := K) (L := L) P
    Ideal (integralClosure (Localization.AtPrime P) L) :=
  by
    letI := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
    letI : IsScalarTower A (Localization.AtPrime P) L :=
      localizationAtPrimeToExtension_isScalarTower (K := K) (L := L) P
    exact Q.map (integralClosureLocalizationRingHom (L := L) P)
theorem

localizedNormalizationPrime_isPrime

L51 ↗
EtaleFundamentalGroups.localizedNormalizationPrime_isPrime
Documentation

A prime above P remains prime in the localized normalization.

Source context 11 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]
section Prime
variable (P : Ideal A) [P.IsPrime]
omit [IsDomain A] in
Lean source · statement
theorem localizedNormalizationPrime_isPrime
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver P] :
    (localizedNormalizationPrime (K := K) (L := L) P Q).IsPrime
theorem

localizedNormalizationPrime_liesOver

L72 ↗
EtaleFundamentalGroups.localizedNormalizationPrime_liesOver
Documentation

The localized normalization prime lies over the maximal ideal of the prime localization of the base.

Source context 11 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]
section Prime
variable (P : Ideal A) [P.IsPrime]
omit [IsDomain A] in
Lean source · statement
theorem localizedNormalizationPrime_liesOver
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver P] :
    (localizedNormalizationPrime (K := K) (L := L) P Q).LiesOver
      (IsLocalRing.maximalIdeal (Localization.AtPrime P))
theorem

localizedNormalizationPrime_isMaximal

L102 ↗
EtaleFundamentalGroups.localizedNormalizationPrime_isMaximal
Documentation

The localized normalization prime is maximal.

Source context 11 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]
section Prime
variable (P : Ideal A) [P.IsPrime]
omit [IsDomain A] in
Lean source · statement
theorem localizedNormalizationPrime_isMaximal
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver P] :
    (localizedNormalizationPrime (K := K) (L := L) P Q).IsMaximal
theorem

localizedNormalizationPrime_ramificationIdx

L118 ↗
EtaleFundamentalGroups.localizedNormalizationPrime_ramificationIdx
Documentation

Localization at P preserves the ramification index of a normalization prime above P.

Source context 11 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]
section Prime
variable (P : Ideal A) [P.IsPrime]
omit [IsDomain A] in
Lean source · statement
theorem localizedNormalizationPrime_ramificationIdx
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver P] :
    (localizedNormalizationPrime (K := K) (L := L) P Q).ramificationIdx
        (Localization.AtPrime P) =
      Q.ramificationIdx A

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