Module

MinimalLocalizationDomain.lean

Nyll.EtaleFundamentalGroups.Normalization.Primes.MinimalLocalizationDomain

3 declarations indexed from sourceView source ↗

Module documentation

Killing a minimal prime in a domain localization

This file isolates the order-sensitive final step used for a retained generic component. A prime over the generic point of an integral base is a minimal prime. Its extension to a larger-prime localization is zero once that localization has independently been shown to be a domain.

The domain hypothesis is deliberately imposed only on the localization; it is not used to produce minimality of the original prime.

Imports2

Mathlib.RingTheory.Ideal.GoingUp
Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Imported by3

theorem

prime_liesOver_bot_mem_minimalPrimes

L30 ↗

EtaleFundamentalGroups.prime_liesOver_bot_mem_minimalPrimes

Documentation

A prime of an integral algebra lying over the zero ideal of the base is a minimal prime of the algebra.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uA

Lean source · statement

theorem prime_liesOver_bot_mem_minimalPrimes
    {R : Type uR} {A : Type uA}
    [CommRing R] [CommRing A] [Algebra R A] [Algebra.IsIntegral R A]
    (N : Ideal A) [N.IsPrime] [N.LiesOver (⊥ : Ideal R)] :
    N ∈ minimalPrimes A

theorem

minimalPrime_map_eq_bot_localizationAtPrime_of_isDomain

L44 ↗

EtaleFundamentalGroups.minimalPrime_map_eq_bot_localizationAtPrime_of_isDomain

Documentation

A minimal prime contained in Q maps to zero in the localization at Q, provided that localization has already been proved to be a domain.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uA

Lean source · statement

theorem minimalPrime_map_eq_bot_localizationAtPrime_of_isDomain
    {A : Type uA} [CommRing A]
    (N Q : Ideal A) [N.IsPrime] [Q.IsPrime]
    [IsDomain (Localization.AtPrime Q)]
    (hNMinimal : N ∈ minimalPrimes A) (hNQ : N ≤ Q) :
    N.map (algebraMap A (Localization.AtPrime Q)) = ⊥

theorem

prime_liesOver_bot_map_eq_bot_localizationAtPrime_of_isDomain

L72 ↗

EtaleFundamentalGroups.prime_liesOver_bot_map_eq_bot_localizationAtPrime_of_isDomain

Documentation

Combined integral-generic-prime form: after domainhood of the localization at a containing prime has been established, a prime lying over the base generic point vanishes there.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uA

Lean source · statement

theorem prime_liesOver_bot_map_eq_bot_localizationAtPrime_of_isDomain
    {R : Type uR} {A : Type uA}
    [CommRing R] [CommRing A] [Algebra R A] [Algebra.IsIntegral R A]
    (N Q : Ideal A) [N.IsPrime] [N.LiesOver (⊥ : Ideal R)] [Q.IsPrime]
    [IsDomain (Localization.AtPrime Q)] (hNQ : N ≤ Q) :
    N.map (algebraMap A (Localization.AtPrime Q)) = ⊥

Module documentation

Killing a minimal prime in a domain localization

Declarations

prime_liesOver_bot_mem_minimalPrimes

minimalPrime_map_eq_bot_localizationAtPrime_of_isDomain

prime_liesOver_bot_map_eq_bot_localizationAtPrime_of_isDomain