NYLL
Module

AffineUniversalHomeomorphismEquivalence.lean

Nyll.SchemeTheory.FiniteEtale.AffineUniversalHomeomorphismEquivalence
5 declarations indexed from sourceView source ↗

Module documentation

Equivalence on finite étale covers of affine universal homeomorphisms

The constructed finite étale algebra model gives essential surjectivity of the actual tensor-product functor. The affine comparison carries this result to scheme pullback. Together with universal-homeomorphism full faithfulness, this gives the finite étale equivalence for maps of spectra.

Imports8
Imported by2

Declarations

theorem

baseChange_essSurj_of_universalHomeomorphism

L36 ↗
CommAlgCat.FiniteEtale.baseChange_essSurj_of_universalHomeomorphism
Documentation

The actual models give essential surjectivity of tensor-product base change.

Source context 4 commands

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

@[expose] public noncomputable section
open CategoryTheory AlgebraicGeometry Opposite
universe u
namespace CommAlgCat.FiniteEtale
Lean source · statement
theorem baseChange_essSurj_of_universalHomeomorphism
    (R S : Type u) [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsIntegral R S]
    [UniversallyInjective (Spec.map (CommRingCat.ofHom (algebraMap R S)))]
    [Surjective (Spec.map (CommRingCat.ofHom (algebraMap R S)))] :
    (baseChange R S : CommAlgCat.FiniteEtale.{u} R ⥤
      CommAlgCat.FiniteEtale.{u} S).EssSurj
instance

finiteEtaleInfStableUnderBaseChangeAffineUniversalHomeomorphism

L53 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleInfStableUnderBaseChangeAffineUniversalHomeomorphism
Source context 4 commands

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

@[expose] public noncomputable section
open CategoryTheory AlgebraicGeometry Opposite
universe u
namespace AlgebraicGeometry.FiniteEtale
Lean source · statement
instance finiteEtaleInfStableUnderBaseChangeAffineUniversalHomeomorphism :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale)
theorem

pullback_specMap_essSurj_of_universalHomeomorphism

L60 ↗
AlgebraicGeometry.FiniteEtale.pullback_specMap_essSurj_of_universalHomeomorphism
Documentation

Finite étale scheme pullback on spectra is essentially surjective along an integral, universally injective, surjective map.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory AlgebraicGeometry Opposite
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeAffineUniversalHomeomorphism :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
Lean source · statement
theorem pullback_specMap_essSurj_of_universalHomeomorphism
    (R S : Type u) [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsIntegral R S]
    [UniversallyInjective (Spec.map (CommRingCat.ofHom (algebraMap R S)))]
    [Surjective (Spec.map (CommRingCat.ofHom (algebraMap R S)))] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤
      (Spec.map (CommRingCat.ofHom (algebraMap R S)))).EssSurj
theorem

pullback_specMap_isEquivalence_of_universalHomeomorphism

L91 ↗
AlgebraicGeometry.FiniteEtale.pullback_specMap_isEquivalence_of_universalHomeomorphism
Documentation

Finite étale covers are invariant under affine universal homeomorphisms.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory AlgebraicGeometry Opposite
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeAffineUniversalHomeomorphism :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
Lean source · statement
theorem pullback_specMap_isEquivalence_of_universalHomeomorphism
    (R S : Type u) [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsIntegral R S]
    [UniversallyInjective (Spec.map (CommRingCat.ofHom (algebraMap R S)))]
    [Surjective (Spec.map (CommRingCat.ofHom (algebraMap R S)))] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤
      (Spec.map (CommRingCat.ofHom (algebraMap R S)))).IsEquivalence
theorem

pullback_isEquivalence_of_isAffine_of_universalHomeomorphism

L111 ↗
AlgebraicGeometry.FiniteEtale.pullback_isEquivalence_of_isAffine_of_universalHomeomorphism
Documentation

The affine result is invariant under the canonical spectrum identifications; only the target needs to be assumed affine, since the map is integral.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory AlgebraicGeometry Opposite
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeAffineUniversalHomeomorphism :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
Lean source · statement
theorem pullback_isEquivalence_of_isAffine_of_universalHomeomorphism
    {X Y : Scheme.{u}} [IsAffine Y] (f : X ⟶ Y)
    [IsIntegralHom f] [UniversallyInjective f] [Surjective f] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ f).IsEquivalence

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