Algebra.Etale.exists_finite_etale_faithfullyFlat_tensorProduct_algEquiv_pi
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_Etale_exists_finite_etale_faithfullyFlat_tensorProduct_algEquiv_pi
open scoped TensorProduct
universe uLean source · statement
theorem _root_.Algebra.Etale.exists_finite_etale_faithfullyFlat_tensorProduct_algEquiv_pi
(R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
(B : Type u) [CommRing B] [Algebra R B] [Module.Finite R B] [Algebra.Etale R B] :
∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R') (_ : Module.Finite R R')
(_ : Algebra.Etale R R') (_ : Module.FaithfullyFlat R R') (_ : IsNoetherianRing R'),
Nonempty ((R' ⊗[R] B) ≃ₐ[R'] (Fin (Module.finrank R B) → R'))