Module

BoundaryPrimeDichotomy.lean

Nyll.SchemeTheory.LocalGeometry.HeightOne.BoundaryPrimeDichotomy

3 declarations indexed from sourceView source ↗

Module documentation

Height-one primes relative to one- and two-branch boundary equations

If a boundary equation is associated to a prime parameter, every height-one prime either is that parameter divisor or lies on its complement. If the boundary is associated to a prime parameter times a power of a second prime parameter, the only additional possibility is the second parameter divisor.

These statements use only the principal-prime geometry of a domain. In particular, they do not require a Noetherian hypothesis or any root-cover presentation.

Imports2

Mathlib.Algebra.BigOperators.Associated
Mathlib.RingTheory.Ideal.Height

Imported by3

theorem

heightOnePrime_eq_span_of_prime_mem

L29 ↗

EtaleFundamentalGroups.heightOnePrime_eq_span_of_prime_mem

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem heightOnePrime_eq_span_of_prime_mem
    {B : Type u} [CommRing B] [IsDomain B]
    {y : B} (hy : Prime y)
    (q : Ideal B) [q.IsPrime] (hqheight : q.height = 1)
    (hyq : y ∈ q) :
    q = Ideal.span {y}

theorem

heightOnePrime_eq_span_or_disjoint_powers_of_associated

L53 ↗

EtaleFundamentalGroups.heightOnePrime_eq_span_or_disjoint_powers_of_associated

Documentation

If a boundary equation is associated to a prime parameter, a height-one prime is either the corresponding parameter divisor or is disjoint from all powers of the boundary equation.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem heightOnePrime_eq_span_or_disjoint_powers_of_associated
    {B : Type u} [CommRing B] [IsDomain B]
    {f y : B} (hy : Prime y) (hfy : Associated f y)
    (q : Ideal B) [q.IsPrime] (hqheight : q.height = 1) :
    q = Ideal.span {y} ∨
      Disjoint ((Submonoid.powers f : Submonoid B) : Set B) (q : Set B)

theorem

heightOnePrime_eq_span_or_eq_span_or_disjoint_powers_of_associated_mul_pow

L71 ↗

EtaleFundamentalGroups.heightOnePrime_eq_span_or_eq_span_or_disjoint_powers_of_associated_mul_pow

Documentation

If a boundary equation is associated to a prime parameter times a power of a second prime parameter, a height-one prime is one of the two parameter divisors or is disjoint from all powers of the boundary equation.

No positivity assumption on n is needed: for n = 0 the statement reduces to the one-branch case.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem heightOnePrime_eq_span_or_eq_span_or_disjoint_powers_of_associated_mul_pow
    {B : Type u} [CommRing B] [IsDomain B]
    {f y z : B} {n : ℕ}
    (hy : Prime y) (hz : Prime z) (hfy : Associated f (y * z ^ n))
    (q : Ideal B) [q.IsPrime] (hqheight : q.height = 1) :
    q = Ideal.span {y} ∨ q = Ideal.span {z} ∨
      Disjoint ((Submonoid.powers f : Submonoid B) : Set B) (q : Set B)

Module documentation

Height-one primes relative to one- and two-branch boundary equations

Declarations

heightOnePrime_eq_span_of_prime_mem

heightOnePrime_eq_span_or_disjoint_powers_of_associated

heightOnePrime_eq_span_or_eq_span_or_disjoint_powers_of_associated_mul_pow