NYLL
Module

DVRFiniteEtaleAlgebra.lean

Nyll.SchemeTheory.RingTheory.Ramification.Unramified.DVRFiniteEtaleAlgebra
2 declarations indexed from sourceView source ↗

Module documentation

Unramified normalization of a finite étale generic fibre

A finite étale algebra over a fraction field is a product of its actual maximal-ideal quotient fields. The normalization in that algebra therefore splits as the product of the normalizations in those fields. Over a DVR, the ramification-index-one and separable-residue-extension conditions on every field factor make the whole normalization finite étale.

Its generic fibre recovers the original algebra. This supplies the algebraic extension at a codimension-one point used in Stacks Project, Tag 0H2W.

Imports8
Imported by2

Declarations

theorem

finite_etale_integralClosure_of_finiteEtale_unramifiedOverDVR

L44 ↗
SchemeTheory.finite_etale_integralClosure_of_finiteEtale_unramifiedOverDVR
Documentation

A finite étale algebra over a DVR's fraction field has finite étale normalization when each of its actual field factors is unramified over the DVR. The hypothesis consists of residue separability and ramification index one at the maximal primes of each field factor's integral closure.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace SchemeTheory
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem finite_etale_integralClosure_of_finiteEtale_unramifiedOverDVR
    (R : Type u) (K : Type v) (A : Type w)
    [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [CommRing A] [Algebra R A] [Algebra K A] [IsScalarTower R K A]
    [Module.Finite K A] [Algebra.Etale K A]
    (h : ∀ m : MaximalSpectrum A, IsUnramifiedOverDVR R (A ⧸ m.asIdeal)) :
    Module.Finite R (integralClosure R A) ∧
      Algebra.Etale R (integralClosure R A)
def

integralClosureFiniteEtaleGenericFiberEquiv

L72 ↗
SchemeTheory.integralClosureFiniteEtaleGenericFiberEquiv
Documentation

The generic fibre of the literal normalization in a finite étale algebra is the given algebra, including when that algebra has several field factors or is the zero ring. No ramification hypothesis is needed for this comparison.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace SchemeTheory
attribute [local instance] Ideal.Quotient.field
Lean source · statement
def integralClosureFiniteEtaleGenericFiberEquiv
    (R : Type u) (K : Type v) (A : Type w)
    [CommRing R] [IsDomain R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [CommRing A] [Algebra R A] [Algebra K A] [IsScalarTower R K A]
    [Module.Finite K A] [Algebra.Etale K A] :
    K ⊗[R] integralClosure R A ≃ₐ[K] A

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