NYLL
Module

AtLargerPrime.lean

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

Module documentation

A normalization prime after localization at a larger base prime

Let q be a prime of the normalization of A in L, and let P be a prime of A containing the contraction of q. Then q is disjoint from the elements inverted in A_P. Consequently its image in the normalization over A_P is prime, lies over the localized contraction of q, and has the same ramification index.

Unlike NormalizationPrime, the contraction of q need not equal P here. This is the form needed when a height-one ramification prime is viewed inside a height-two localization.

Imports1
Imported by11

Declarations

theorem

ramificationIdx_map_eq_of_isLocalization

L40 ↗
EtaleFundamentalGroups.ramificationIdx_map_eq_of_isLocalization
Documentation

Simultaneously localizing the source and target preserves the ramification index of every target prime disjoint from the target-side multiplicative set. The source localization need not be at the contraction of that prime.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uR' uS'
section LocalizationRamification
variable {R : Type uR} {S : Type uS} {R' : Type uR'} {S' : Type uS'}
variable [CommRing R] [CommRing S] [CommRing R'] [CommRing S']
variable [Algebra R S] [Algebra R R'] [Algebra S S'] [Algebra R' S']
variable [Algebra R S'] [IsScalarTower R S S'] [IsScalarTower R R' S']
Lean source · statement
theorem ramificationIdx_map_eq_of_isLocalization
    (M : Submonoid R) (T : Submonoid S)
    [IsLocalization M R'] [IsLocalization T S']
    (q : Ideal S) [q.IsPrime]
    (hdisj : Disjoint (T : Set S) (q : Set S)) :
    (q.map (algebraMap S S')).ramificationIdx R' =
      q.ramificationIdx R
theorem

normalizationPrime_disjoint_algebraMapSubmonoid

L112 ↗
EtaleFundamentalGroups.normalizationPrime_disjoint_algebraMapSubmonoid
Documentation

A normalization prime whose contraction is contained in P is disjoint from the normalization-side multiplicative set used to localize at P.

Source context 12 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uR' uS'
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 LargerPrime
variable (P : Ideal A) [P.IsPrime]
omit [IsDomain A] in
Lean source · statement
theorem normalizationPrime_disjoint_algebraMapSubmonoid
    (q : Ideal (integralClosure A L)) [q.IsPrime]
    (hqP : q.under A ≤ P) :
    Disjoint
      ((Algebra.algebraMapSubmonoid (integralClosure A L) P.primeCompl :
        Submonoid (integralClosure A L)) : Set (integralClosure A L))
      (q : Set (integralClosure A L))
theorem

localizedNormalizationPrime_isPrime_of_under_le

L125 ↗
EtaleFundamentalGroups.localizedNormalizationPrime_isPrime_of_under_le
Documentation

The image of q in the normalization over A_P is prime whenever the contraction of q is contained in P.

Source context 12 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uR' uS'
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 LargerPrime
variable (P : Ideal A) [P.IsPrime]
omit [IsDomain A] in
Lean source · statement
theorem localizedNormalizationPrime_isPrime_of_under_le
    (q : Ideal (integralClosure A L)) [q.IsPrime]
    (hqP : q.under A ≤ P) :
    (localizedNormalizationPrime (K := K) (L := L) P q).IsPrime
theorem

localizedNormalizationPrime_liesOver_map_under

L149 ↗
EtaleFundamentalGroups.localizedNormalizationPrime_liesOver_map_under
Documentation

The image of q lies over the image in A_P of its original contraction to A.

Source context 12 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uR' uS'
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 LargerPrime
variable (P : Ideal A) [P.IsPrime]
omit [IsDomain A] in
Lean source · statement
theorem localizedNormalizationPrime_liesOver_map_under
    (q : Ideal (integralClosure A L)) [q.IsPrime]
    (hqP : q.under A ≤ P) :
    (localizedNormalizationPrime (K := K) (L := L) P q).LiesOver
      ((q.under A).map (algebraMap A (Localization.AtPrime P)))
theorem

localizedNormalizationPrime_ramificationIdx_of_under_le

L184 ↗
EtaleFundamentalGroups.localizedNormalizationPrime_ramificationIdx_of_under_le
Documentation

Localizing the base at a prime containing the contraction of q preserves the ramification index at q.

Source context 12 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uR' uS'
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 LargerPrime
variable (P : Ideal A) [P.IsPrime]
omit [IsDomain A] in
Lean source · statement
theorem localizedNormalizationPrime_ramificationIdx_of_under_le
    (q : Ideal (integralClosure A L)) [q.IsPrime]
    (hqP : q.under A ≤ 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.