Module

HenselianIntegralFiber.lean

Nyll.EtaleFundamentalGroups.Inertia.HenselianIntegralFiber

4 declarations indexed from sourceView source ↗

Module documentation

Idempotents separating finite integral fibers over Henselian local rings

The closed fiber of an integral algebra has dimension zero. If its set of primes is finite, its spectrum is discrete. Its singleton idempotents lift uniquely along the Henselian pair, giving actual idempotents in the integral algebra without a finite-type or finite-presentation hypothesis.

Imports7

Nyll.SchemeTheory.RingTheory.HenselianIdempotents
Mathlib.RingTheory.Ideal.GoingUp
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.LocalRing.Basic
Mathlib.RingTheory.Spectrum.Prime.Topology

Imported by4

theorem

closedFiberPrime_liesOver

L31 ↗

EtaleFundamentalGroups.Inertia.closedFiberPrime_liesOver

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v
variable (A : Type u) (R : Type v) [CommRing A] [HenselianLocalRing A]
  [CommRing R] [Algebra A R]

Lean source · statement

theorem closedFiberPrime_liesOver
    (P : PrimeSpectrum (R ⧸ (IsLocalRing.maximalIdeal A).map (algebraMap A R))) :
    (P.asIdeal.comap
      (Ideal.Quotient.mk ((IsLocalRing.maximalIdeal A).map (algebraMap A R)))).LiesOver
        (IsLocalRing.maximalIdeal A)

def

closedFiberPrimeEquiv

L48 ↗

EtaleFundamentalGroups.Inertia.closedFiberPrimeEquiv

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v
variable (A : Type u) (R : Type v) [CommRing A] [HenselianLocalRing A]
  [CommRing R] [Algebra A R]

Lean source · statement

def closedFiberPrimeEquiv :
    PrimeSpectrum (R ⧸ (IsLocalRing.maximalIdeal A).map (algebraMap A R)) ≃
      (IsLocalRing.maximalIdeal A).primesOver R

theorem

existsUnique_idempotent_of_finite_integral_fiber

L71 ↗

EtaleFundamentalGroups.Inertia.existsUnique_idempotent_of_finite_integral_fiber

Documentation

A point of a finite closed fiber of an integral algebra over a Henselian local ring is cut out by a unique idempotent of the original algebra.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v
variable (A : Type u) (R : Type v) [CommRing A] [HenselianLocalRing A]
  [CommRing R] [Algebra A R]

Lean source · statement

theorem existsUnique_idempotent_of_finite_integral_fiber
    [Algebra.IsIntegral A R]
    (hfinite : ((IsLocalRing.maximalIdeal A).primesOver R).Finite)
    (q : Ideal R) [q.IsPrime] [q.LiesOver (IsLocalRing.maximalIdeal A)] :
    ∃! e : R, IsIdempotentElem e ∧
      ∀ Q : Ideal R, Q.IsPrime → Q.LiesOver (IsLocalRing.maximalIdeal A) →
        (e ∉ Q ↔ Q = q)

theorem

exists_local_factor_of_finite_integral_fiber

L139 ↗

EtaleFundamentalGroups.Inertia.exists_local_factor_of_finite_integral_fiber

Documentation

Each point of a finite integral closed fiber has an actual idempotent local factor. Its unique maximal ideal contracts to the prescribed point.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v
variable (A : Type u) (R : Type v) [CommRing A] [HenselianLocalRing A]
  [CommRing R] [Algebra A R]

Lean source · statement

theorem exists_local_factor_of_finite_integral_fiber
    [Algebra.IsIntegral A R]
    (hfinite : ((IsLocalRing.maximalIdeal A).primesOver R).Finite)
    (q : Ideal R) [q.IsPrime] [q.LiesOver (IsLocalRing.maximalIdeal A)] :
    ∃ e : R, IsIdempotentElem e ∧ e ∉ q ∧ IsLocalRing (Localization.Away e) ∧
      ∀ Q : Ideal (Localization.Away e), Q.IsMaximal →
        Q.comap (algebraMap R (Localization.Away e)) = q

Module documentation

Idempotents separating finite integral fibers over Henselian local rings

Declarations

closedFiberPrime_liesOver

closedFiberPrimeEquiv

existsUnique_idempotent_of_finite_integral_fiber

exists_local_factor_of_finite_integral_fiber