EtaleFundamentalGroups.exists_finite_fractionField_normalization_model
Finite generation at one base prime produces a finite subalgebra of the original extension field, with that fraction field and the actual local normalization algebra. No Noetherian or separability hypothesis is used.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct nonZeroDivisors
universe u
attribute [local instance] Algebra.TensorProduct.rightAlgebraLean source · statement
theorem exists_finite_fractionField_normalization_model
(R K L : Type u) [CommRing R] [IsDomain R]
[Field K] [Algebra R K] [IsFractionRing R K]
[Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L]
[FiniteDimensional K L] (p : PrimeSpectrum R)
[Module.Finite (Localization.AtPrime p.asIdeal)
(Localization.AtPrime p.asIdeal ⊗[R] integralClosure R L)] :
∃ C : Subalgebra R L, Module.Finite R C ∧ IsFractionRing C L ∧
Nonempty ((Localization.AtPrime p.asIdeal ⊗[R] C) ≃ₐ[Localization.AtPrime p.asIdeal]
(Localization.AtPrime p.asIdeal ⊗[R] integralClosure R L))