EtaleFundamentalGroups.StrictHenselian.integralClosure_etale_of_normal_local_fiber_degree
An étale closed fiber whose degree is at least the original generic degree makes the actual normalization étale over a normal local domain. No separability, Galoisness, or Noetherianity is assumed.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe uLean source · statement
theorem integralClosure_etale_of_normal_local_fiber_degree
{R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R] [IsLocalRing R]
[Field Ω] [IsSepClosed Ω] (φ : R →+* Ω) [IsLocalHom φ]
(L : Type u) [CommRing L] [Algebra R L] [Algebra (FractionRing R) L]
[IsScalarTower R (FractionRing R) L] [Module.Finite (FractionRing R) L]
[Algebra.Etale (IsLocalRing.ResidueField R)
(IsLocalRing.ResidueField R ⊗[R] integralClosure R L)]
(hdegree : Module.finrank (FractionRing R) L ≤
Module.finrank (IsLocalRing.ResidueField R)
(IsLocalRing.ResidueField R ⊗[R] integralClosure R L)) :
Algebra.Etale R (integralClosure R L)