EtaleFundamentalGroups.integralClosure_etale_of_local_fiber_degree
The normalization closed-fiber criterion for an arbitrary chosen fraction field, preserving the original algebra and its field degree.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uLean source · statement
theorem integralClosure_etale_of_local_fiber_degree
{R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R] [IsLocalRing R]
[Field Ω] [IsSepClosed Ω] (φ : R →+* Ω) [IsLocalHom φ]
(K L : Type u) [Field K] [Algebra R K] [IsFractionRing R K]
[CommRing L] [Algebra R L] [Algebra K L] [IsScalarTower R K L]
[Module.Finite K L]
[Algebra.Etale (IsLocalRing.ResidueField R)
(IsLocalRing.ResidueField R ⊗[R] integralClosure R L)]
(hdegree : Module.finrank K L ≤ Module.finrank (IsLocalRing.ResidueField R)
(IsLocalRing.ResidueField R ⊗[R] integralClosure R L)) :
Algebra.Etale R (integralClosure R L)