Nyll.SchemeTheory.FiniteEtale.Algebra.IntegralRadicialEssentialSurjectivity

Module documentation

Finite étale models over affine universal homeomorphisms

The upper algebra first descends to an actual finite intermediate universal homeomorphism. Finite radicial descent then constructs its model over the original ring. The tensor-product associator supplies the comparison with the original upper algebra.

theorem

exists_finite_model_of_universalHomeomorphism

L33 ↗

Algebra.Etale.exists_finite_model_of_universalHomeomorphism

Documentation

A finite étale algebra over any affine universal homeomorphism is the scalar extension of a finite étale algebra over the original ring.

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 Algebra

Lean source · statement

theorem Etale.exists_finite_model_of_universalHomeomorphism
    (R S A : Type u) [CommRing R] [CommRing S] [CommRing A]
    [Algebra R S] [Algebra.IsIntegral R S] [Algebra S A]
    [Module.Finite S A] [Etale S A]
    [UniversallyInjective (Spec.map (CommRingCat.ofHom (algebraMap R S)))]
    [Surjective (Spec.map (CommRingCat.ofHom (algebraMap R S)))] :
    ∃ (I : Type u) (_ : CommRing I) (_ : Algebra R I),
      Module.Finite R I ∧ Etale R I ∧ Nonempty (S ⊗[R] I ≃ₐ[S] A)

Module documentation

Finite étale models over affine universal homeomorphisms

Declarations

exists_finite_model_of_universalHomeomorphism