Algebra.exists_model_of_etale_faithfullyFlat_cover
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public noncomputable section
open AlgebraicGeometry
open scoped TensorProduct
universe u
namespace AlgebraLean source · full declaration
theorem exists_model_of_etale_faithfullyFlat_cover
{R B : Type u} [CommRing R] [CommRing B]
(f : R →+* B) (S M A : Type u)
[CommRing S] [CommRing M] [CommRing A]
[Algebra R S] [Algebra B M] [Algebra S A]
[Module.Finite B M] [Etale B M]
[IsIntegralHom (Spec.map (CommRingCat.ofHom (algebraMap R S)))]
[UniversallyInjective (Spec.map (CommRingCat.ofHom (algebraMap R S)))]
[Surjective (Spec.map (CommRingCat.ofHom (algebraMap R S)))]
(hf : f.FaithfullyFlat) :
let : Algebra R B := f.toAlgebra;
let : Algebra R M := Algebra.compHom M f;
∀ (_ : IsScalarTower R B M),
let : Algebra (S ⊗[R] B) (S ⊗[R] M) :=
TensorProduct.baseChangeAlgebra R S B M;
let : IsScalarTower S (S ⊗[R] B) (S ⊗[R] M) :=
TensorProduct.baseChangeAlgebra_isScalarTower R S B M;
Etale R B →
((S ⊗[R] M) ≃ₐ[S ⊗[R] B] (S ⊗[R] B) ⊗[S] A) →
∃ (I : Type u) (_ : CommRing I) (_ : Algebra R I),
Module.Finite R I ∧ Etale R I ∧ Nonempty (S ⊗[R] I ≃ₐ[S] A) := by
intro hRB hRM hTower hEU hEUTower hBEtale e
obtain ⟨ρ, hcounit, hcoassoc, hcomparison⟩ :=
Descent.exists_coaction_of_radicial_model R S B M A e
obtain ⟨hε, hδ⟩ :=
Descent.nativeCoactionAxioms_of_pointwise f M ρ hcounit hcoassoc
let I := FaithfullyFlatDescent.invariants f M ρ
obtain ⟨hfinite, hEtale⟩ :=
FaithfullyFlatDescent.invariants_finite_etale f M hf ρ hε hδ
exact ⟨I, inferInstance, inferInstance, hfinite, hEtale,
⟨FaithfullyFlatDescent.invariantsScalarExtensionEquiv
f S M A hf ρ hε hδ e hcomparison⟩⟩