Module

FiniteUnramifiedNeighborhood.lean

Nyll.SchemeTheory.RingTheory.Descent.FiniteUnramifiedNeighborhood

1 declaration indexed from sourceView source ↗

Module documentation

Spreading unramifiedness around an integral fiber

The unramified locus of a finite type algebra is open without a finite presentation assumption. Its closed complement has closed image under an integral map, so unramifiedness of one entire fiber spreads to a principal neighborhood of the base point.

Imports3

Mathlib.RingTheory.Unramified.Locus
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.Spectrum.Prime.Topology

Imported by2

theorem

exists_unramified_away_of_isUnramifiedAt_fiber

L26 ↗

SchemeTheory.exists_unramified_away_of_isUnramifiedAt_fiber

Documentation

An integral finite type algebra unramified at every prime above p is formally unramified on a principal neighborhood of that entire fiber.

Source context 2 commands

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

namespace SchemeTheory
universe u v

Lean source · statement

theorem exists_unramified_away_of_isUnramifiedAt_fiber
    {R : Type u} {B : Type v} [CommRing R] [CommRing B]
    [Algebra R B] [Algebra.IsIntegral R B] [Algebra.FiniteType R B]
    (p : PrimeSpectrum R)
    (hunramified : ∀ P : PrimeSpectrum B,
      PrimeSpectrum.comap (algebraMap R B) P = p → Algebra.IsUnramifiedAt R P.asIdeal) :
    ∃ r : R, r ∉ p.asIdeal ∧
      Algebra.FormallyUnramified R (Localization.Away (algebraMap R B r))

Module documentation

Spreading unramifiedness around an integral fiber

Declarations

exists_unramified_away_of_isUnramifiedAt_fiber