Module

FiberDegreeCriterion.lean

Nyll.EtaleFundamentalGroups.Normalization.FiberDegreeCriterion

1 declaration indexed from sourceView source ↗

Module documentation

Fiberwise degree detects finite étale normalization

At each base prime, the actual integral-closure localization and the actual residue-field tensor identify the original fiber with the closed fiber of the local normalization. The normal-local criterion supplies étaleness, which the non-Noetherian normalization spreading theorem glues globally.

Imports6

Nyll.EtaleFundamentalGroups.Normalization.NormalLocalFiberDegree
Nyll.EtaleFundamentalGroups.Normalization.FiniteNormalizationLocalCriterion
Nyll.SchemeTheory.RingTheory.Localization.Fraction.FieldLocalization
Mathlib.FieldTheory.IsSepClosed
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.RingTheory.Smooth.IntegralClosure

Imported by2

theorem

finite_etale_normalization_of_fiber_degrees

L33 ↗

EtaleFundamentalGroups.finite_etale_normalization_of_fiber_degrees

Documentation

The affine ring form of original Tag 0BTF (8) ⇒ (4), for the actual integral closure in an arbitrary finite extension of the fraction field.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u

Lean source · statement

theorem finite_etale_normalization_of_fiber_degrees
    (R K L : Type u) [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L]
    [FiniteDimensional K L]
    (hfiber : ∀ p : PrimeSpectrum R,
      Algebra.Etale p.asIdeal.ResidueField
          (p.asIdeal.ResidueField ⊗[R] integralClosure R L) ∧
        Module.finrank K L ≤ Module.finrank p.asIdeal.ResidueField
          (p.asIdeal.ResidueField ⊗[R] integralClosure R L)) :
    Module.Finite R (integralClosure R L) ∧ Algebra.Etale R (integralClosure R L)

Module documentation

Fiberwise degree detects finite étale normalization

Declarations

finite_etale_normalization_of_fiber_degrees