Module

Basic.lean

Nyll.SchemeTheory.Normalization.IntegralClosure.RegularPair.Basic

3 declarations indexed from sourceView source ↗

Module documentation

A relatively-prime pair stays regular on a normalization

Let A be an integrally closed domain with fraction field K, let L / K be algebraic, and let B be the integral closure of A in L. If x is prime and x, y are relatively prime nonzero elements of A, then the equality y * b = x * c in B forces x to divide b in B.

The quotient b / x is integral over A[1/x], while the equality identifies it with c / y, which is integral over A[1/y]. The two-localization intersection theorem then puts the quotient back in the normalization. No global UFD instance is used.

Imports3

Nyll.SchemeTheory.Normalization.IntegralClosure.AwayPairIntersection
Nyll.SchemeTheory.Normalization.IntegralClosure.RegularPair.TraceDual
Mathlib.RingTheory.Regular.IsSMulRegular

Imported by2

theorem

exists_integralClosure_factor_of_mul_eq_mul

L38 ↗

EtaleFundamentalGroups.exists_integralClosure_factor_of_mul_eq_mul

Documentation

If x and y are relatively prime and y * b = x * c in the normalization, then b is divisible by x in the normalization.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped Pointwise
open nonZeroDivisors
open RingTheory.Sequence
universe u v w

Lean source · statement

theorem exists_integralClosure_factor_of_mul_eq_mul
    {A : Type u} {K : Type v} {L : Type w}
    [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L]
    [Algebra.IsAlgebraic K L]
    {x y : A} (hxPrime : Prime x) (hx : x ≠ 0) (hy : y ≠ 0)
    (hxy : IsRelPrime x y)
    {b c : integralClosure A L}
    (hbc : algebraMap A (integralClosure A L) y * b =
      algebraMap A (integralClosure A L) x * c) :
    ∃ d : integralClosure A L,
      b = algebraMap A (integralClosure A L) x * d

theorem

isSMulRegular_quotSMulTop_integralClosure_of_isRelPrime

L156 ↗

EtaleFundamentalGroups.isSMulRegular_quotSMulTop_integralClosure_of_isRelPrime

Documentation

For a relatively-prime nonzero pair x, y, multiplication by y is injective on the normalization modulo x. This is the second regularity condition needed for the parameter pair in the dimension-two flatness argument.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped Pointwise
open nonZeroDivisors
open RingTheory.Sequence
universe u v w

Lean source · statement

theorem isSMulRegular_quotSMulTop_integralClosure_of_isRelPrime
    {A : Type u} {K : Type v} {L : Type w}
    [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L]
    [Algebra.IsAlgebraic K L]
    {x y : A} (hxPrime : Prime x) (hx : x ≠ 0) (hy : y ≠ 0)
    (hxy : IsRelPrime x y) :
    IsSMulRegular (QuotSMulTop x (integralClosure A L)) y

theorem

isSMulRegular_quotSMulTop_integralClosure_of_isRegular

L186 ↗

EtaleFundamentalGroups.isSMulRegular_quotSMulTop_integralClosure_of_isRegular

Documentation

A regular pair remains regular in the second coordinate on a finite normalization in a finite separable extension.

Unlike isSMulRegular_quotSMulTop_integralClosure_of_isRelPrime, this finite-separable form needs neither integral closedness of the base nor a primality hypothesis on the first parameter. The trace-dual divisibility theorem supplies precisely the saturation statement needed in the quotient.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped Pointwise
open nonZeroDivisors
open RingTheory.Sequence
universe u v w

Lean source · statement

theorem isSMulRegular_quotSMulTop_integralClosure_of_isRegular
    {A : Type u} {K : Type v} {L : Type w}
    [CommRing A] [IsDomain A] [IsNoetherianRing A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Module.Finite A (integralClosure A L)]
    {x y : A} (hregular : IsRegular A [x, y]) :
    IsSMulRegular (QuotSMulTop x (integralClosure A L)) y

Module documentation

A relatively-prime pair stays regular on a normalization

Declarations

exists_integralClosure_factor_of_mul_eq_mul

isSMulRegular_quotSMulTop_integralClosure_of_isRelPrime

isSMulRegular_quotSMulTop_integralClosure_of_isRegular