NYLL
Module

UnitGlobalization.lean

Nyll.EtaleFundamentalGroups.LocalGeometry.HeightTwo.UnitGlobalization
1 declaration indexed from sourceView source ↗

Module documentation

Globalizing an integer unit from height-two localizations

For a prime divisor in a Noetherian local domain, failure of an integer to be a unit on the divisor is detected at a height-two localization. Thus a unit result at every such localization globalizes to the generic point of the divisor.

Imports1
Imported by2

Declarations

theorem

isUnit_natCast_mod_prime_of_heightTwo_localizations

L25 ↗
EtaleFundamentalGroups.isUnit_natCast_mod_prime_of_heightTwo_localizations
Documentation

If a positive integer is a unit at every height-two localization lying strictly above a prime parameter, then it is already a unit modulo that parameter.

Source context 2 commands

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

namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem isUnit_natCast_mod_prime_of_heightTwo_localizations
    {A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A]
    [IsLocalRing A]
    (t : A) (ht : Prime t) (e : ℕ) (he : 0 < e)
    [CharZero (A ⧸ Ideal.span {t})]
    (hlocal : ∀ (P : Ideal A) [P.IsPrime],
      Ideal.span {t} < P → P.height = 2 →
        IsUnit (algebraMap A (Localization.AtPrime P) (e : A))) :
    IsUnit (e : A ⧸ Ideal.span {t})

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