Nyll.SchemeTheory.Normalization.IntegralClosure.PrimeAwayIntersection

Module documentation

Intersecting two principal localizations

Let A be a domain with fraction field K. If x is prime and does not divide the nonzero element y, then the images of A[1/x] and A[1/y] inside K intersect in the image of A.

This is the small codimension-two intersection statement needed for the normalization argument. In particular, it avoids installing a global UFD instance on A.

theorem

mem_bot_of_mem_localizationAway_pair_of_prime

L33 ↗

EtaleFundamentalGroups.mem_bot_of_mem_localizationAway_pair_of_prime

Documentation

If x is prime and x ∤ y, then a fraction lying in both A[1/x] and A[1/y] already lies in A.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open nonZeroDivisors
universe u v

Lean source · statement

theorem mem_bot_of_mem_localizationAway_pair_of_prime
    {A : Type u} {K : Type v}
    [CommRing A] [IsDomain A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    {x y : A} (hx : Prime x) (hy : y ≠ 0) (hxy : ¬ x ∣ y)
    (z : K)
    (hzx : z ∈ Localization.subalgebra.ofField K (Submonoid.powers x)
      (Submonoid.powers_le.mpr
        (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero)))
    (hzy : z ∈ Localization.subalgebra.ofField K (Submonoid.powers y)
      (Submonoid.powers_le.mpr
        (mem_nonZeroDivisors_iff_ne_zero.mpr hy))) :
    z ∈ (⊥ : Subalgebra A K)

Module documentation

Intersecting two principal localizations

Declarations

mem_bot_of_mem_localizationAway_pair_of_prime