Module

ComponentDimensionTwo.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.ComponentDimensionTwo

2 declarations indexed from sourceView source ↗

Module documentation

Generic finite-etale components over a two-dimensional regular local base

The normalization of a selected generic component of a finite-etale algebra is finite etale over a normal base. In dimension two, regular-local geometry produces that normality internally, so it need not be supplied as an input.

Imports2

Imported by2

theorem

integralClosure_etale_genericFiberComponent_of_regularLocal_dimension_two

L28 ↗

EtaleFundamentalGroups.integralClosure_etale_genericFiberComponent_of_regularLocal_dimension_two

Documentation

Over a two-dimensional regular local domain, the normalization of every specified generic component of a finite-etale algebra is finite etale.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uT uK uA

Lean source · statement

theorem integralClosure_etale_genericFiberComponent_of_regularLocal_dimension_two
    {R : Type uR} {T : Type uT} {K : Type uK}
    [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    [CommRing T] [Algebra R T] [Module.Finite R T] [Algebra.Etale R T]
    [Field K] [Algebra R K] [IsFractionRing R K]
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (m : Ideal (T ⊗[R] K)) [m.IsMaximal] :
    Algebra.Etale R
      (integralClosure R (FiniteEtaleGenericFiberComponent m))

theorem

integralClosure_etale_genericFiberComponent_localizationAtPrime_of_height_eq_two

L45 ↗

EtaleFundamentalGroups.integralClosure_etale_genericFiberComponent_localizationAtPrime_of_height_eq_two