Nyll.EtaleFundamentalGroups.Normalization.Primes.GoingUp

Module documentation

Following a chosen normalization prime to a larger base prime

If a chosen prime of a normalization lies over p and p \le P, going-up produces a prime over P which still contains the chosen prime. This keeps the same height-one branch factor when it is followed to a codimension-two point; no new normalization component is selected.

theorem

exists_normalizationPrime_over_largerPrime

L27 ↗

EtaleFundamentalGroups.exists_normalizationPrime_over_largerPrime

Documentation

A chosen normalization prime can be followed, by going-up, to every larger prime of the base. The resulting prime contains the original chosen prime and lies over the prescribed larger base prime.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uL

Lean source · statement

theorem exists_normalizationPrime_over_largerPrime
    {A : Type uA} {L : Type uL}
    [CommRing A] [Field L] [Algebra A L]
    (p P : Ideal A) [p.IsPrime] [P.IsPrime] (hpP : p ≤ P)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver p] :
    ∃ N : Ideal (integralClosure A L),
      Q ≤ N ∧ N.IsPrime ∧ N.LiesOver P

Module documentation

Following a chosen normalization prime to a larger base prime

Declarations

exists_normalizationPrime_over_largerPrime