SchemeTheory.exists_generic_split_of_strictHenselian_fiber_degree
An integral algebra over a strictly Henselian ring with an étale closed fiber supplies an actual generic splitting whenever it injects into a finite-dimensional algebra of degree no greater than that closed fiber.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
open scoped TensorProduct
universe uLean source · statement
theorem exists_generic_split_of_strictHenselian_fiber_degree
(R K B T : Type u) [CommRing R] [HenselianLocalRing R]
[IsSepClosed (IsLocalRing.ResidueField R)] [Field K]
[CommRing B] [Algebra R B] [Algebra.IsIntegral R B]
[CommRing T] [Algebra R T] [Algebra K T] [FiniteDimensional K T]
(f : B →ₐ[R] T) (hf : Function.Injective f)
[Algebra.Etale (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField R ⊗[R] B)]
(hdegree : Module.finrank K T ≤ Module.finrank (IsLocalRing.ResidueField R)
(IsLocalRing.ResidueField R ⊗[R] B)) :
∃ (ι : Type u) (_ : Finite ι), Nonempty (T ≃ₐ[K] (ι → K))