Algebra.FiniteEtale.exists_finite_subalgebra_model
A finite étale algebra over an integral extension descends to a finite étale algebra over an actual finite subalgebra of that extension.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open scoped TensorProduct
universe u v w
namespace Algebra.FiniteEtaleLean source · statement
theorem exists_finite_subalgebra_model
(R : Type v) (S : Type u) (A : Type w)
[CommRing R] [CommRing S] [CommRing A]
[Algebra R S] [Algebra.IsIntegral R S] [Algebra S A]
[Module.Finite S A] [Algebra.Etale S A] :
∃ (S₀ : Subalgebra R S) (A₀ : Type u) (_ : CommRing A₀) (_ : Algebra S₀ A₀),
Module.Finite R S₀ ∧ Module.Finite S₀ A₀ ∧ Algebra.Etale S₀ A₀ ∧
Nonempty (A ≃ₐ[S] S ⊗[S₀] A₀)