NYLL
Module

EtaleOpenImage.lean

Nyll.SchemeTheory.RingTheory.Descent.EtaleOpenImage
1 declaration indexed from sourceView source ↗

Module documentation

A genuine étale principal neighborhood in the image of an étale source

For R → S → T with S → T and R → T étale, every prime of S in the actual image of Spec T has a principal neighborhood étale over R. The open image supplies its defining ideal. Localizing at an element of that ideal makes the source cover faithfully flat, and genuine source étale descent supplies finite presentation as well as formal étaleness.

Imports10
Imported by2

Declarations

theorem

exists_etale_away_of_mem_image_etale_source

L37 ↗
SchemeTheory.exists_etale_away_of_mem_image_etale_source
Documentation

Étaleness of a source cover and its composite supplies a genuine étale principal neighborhood around each point in the actual source image.

Source context 3 commands

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

open scoped TensorProduct
namespace SchemeTheory
universe u v w
Lean source · statement
theorem exists_etale_away_of_mem_image_etale_source
    (R : Type u) (S : Type v) (T : Type w)
    [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
    [Algebra.Etale S T] [Algebra.Etale R T]
    (p : PrimeSpectrum S)
    (hp : p ∈ Set.range (PrimeSpectrum.comap (algebraMap S T))) :
    ∃ f : S, f ∉ p.asIdeal ∧ Algebra.Etale R (Localization.Away f)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.