Nyll.SchemeTheory.FiniteEtale.AffineUniversalHomeomorphismModel

Module documentation

Finite models retaining the universal-homeomorphism property

An actual finite subalgebra model for a finite étale algebra over an integral extension also retains surjectivity and universal injectivity of the base map. The larger integral algebra surjects onto this intermediate spectrum by lying over, so both properties descend through that surjection.

theorem

exists_finite_subalgebra_model_of_universalHomeomorphism

L34 ↗

AlgebraicGeometry.FiniteEtale.exists_finite_subalgebra_model_of_universalHomeomorphism

Documentation

A finite étale algebra over an affine universal homeomorphism has a model over an actual finite intermediate universal homeomorphism.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory
open scoped TensorProduct
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem exists_finite_subalgebra_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] [Algebra.Etale S A]
    [UniversallyInjective (Spec.map (CommRingCat.ofHom (algebraMap R S)))]
    [Surjective (Spec.map (CommRingCat.ofHom (algebraMap R S)))] :
    ∃ (S₀ : Subalgebra R S) (A₀ : Type u) (_ : CommRing A₀) (_ : Algebra S₀ A₀),
      Module.Finite R S₀ ∧
      UniversallyInjective (Spec.map (CommRingCat.ofHom (algebraMap R S₀))) ∧
      Surjective (Spec.map (CommRingCat.ofHom (algebraMap R S₀))) ∧
      Module.Finite S₀ A₀ ∧ Algebra.Etale S₀ A₀ ∧
      Nonempty (A ≃ₐ[S] S ⊗[S₀] A₀)

Module documentation

Finite models retaining the universal-homeomorphism property

Declarations

exists_finite_subalgebra_model_of_universalHomeomorphism