Module

AffineBaseChangeProperties.lean

Nyll.SchemeTheory.Etale.AffineBaseChangeProperties

5 declarations indexed from sourceView source ↗

Module documentation

Ring properties of actual affine base changes

The canonical tensor-product spectrum isomorphism identifies the structure map, so properties of the scheme pullback give properties of the tensor algebra with its canonical scalar action. Prime localization then gives etaleness at every point over the chosen base prime.

Imports4

Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Pullbacks
Nyll.SchemeTheory.RingTheory.Descent.EtalePrimeLocalization

Imported by3

def

tensorSpecBaseChangeIso

L32 ↗

SchemeTheory.tensorSpecBaseChangeIso

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TensorProduct
namespace SchemeTheory
universe u
variable (R A B : Type u) [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]

Lean source · statement

def tensorSpecBaseChangeIso :
    Spec (.of (A ⊗[R] B)) ≅
      pullback (Spec.map (CommRingCat.ofHom (algebraMap R B)))
        (Spec.map (CommRingCat.ofHom (algebraMap R A)))

theorem

tensorSpecBaseChangeIso_hom_snd

L40 ↗

SchemeTheory.tensorSpecBaseChangeIso_hom_snd

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TensorProduct
namespace SchemeTheory
universe u
variable (R A B : Type u) [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]

Lean source · statement

theorem tensorSpecBaseChangeIso_hom_snd :
    (tensorSpecBaseChangeIso R A B).hom ≫ pullback.snd _ _ =
      Spec.map (CommRingCat.ofHom (algebraMap A (A ⊗[R] B)))

theorem

tensorProduct_etale_of_spec_baseChange

L48 ↗

SchemeTheory.tensorProduct_etale_of_spec_baseChange

Documentation

Etaleness of the actual affine pullback gives etaleness of the tensor algebra over the new base.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TensorProduct
namespace SchemeTheory
universe u
variable (R A B : Type u) [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]

Lean source · statement

theorem tensorProduct_etale_of_spec_baseChange
    (h : Etale (pullback.snd
      (Spec.map (CommRingCat.ofHom (algebraMap R B)))
      (Spec.map (CommRingCat.ofHom (algebraMap R A))))) :
    Algebra.Etale A (A ⊗[R] B)

theorem

tensorProduct_finite_of_spec_baseChange

L62 ↗

SchemeTheory.tensorProduct_finite_of_spec_baseChange

Documentation

Finiteness of the actual affine pullback gives module finiteness of its canonical tensor algebra.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TensorProduct
namespace SchemeTheory
universe u
variable (R A B : Type u) [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]

Lean source · statement

theorem tensorProduct_finite_of_spec_baseChange
    (h : IsFinite (pullback.snd
      (Spec.map (CommRingCat.ofHom (algebraMap R B)))
      (Spec.map (CommRingCat.ofHom (algebraMap R A))))) :
    Module.Finite A (A ⊗[R] B)

theorem

isEtaleAt_of_spec_baseChange_atPrime

L75 ↗

SchemeTheory.isEtaleAt_of_spec_baseChange_atPrime

Documentation

Etaleness after the actual base change to a prime localization implies etaleness at every target prime over that base prime.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TensorProduct
namespace SchemeTheory
universe u
variable (R A B : Type u) [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]

Lean source · statement

theorem isEtaleAt_of_spec_baseChange_atPrime
    (p : PrimeSpectrum R)
    (h : Etale (pullback.snd
      (Spec.map (CommRingCat.ofHom (algebraMap R B)))
      (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.AtPrime p.asIdeal))))))
    (P : PrimeSpectrum B)
    (hP : PrimeSpectrum.comap (algebraMap R B) P = p) :
    Algebra.IsEtaleAt R P.asIdeal

Module documentation

Ring properties of actual affine base changes

Declarations

tensorSpecBaseChangeIso

tensorSpecBaseChangeIso_hom_snd

tensorProduct_etale_of_spec_baseChange

tensorProduct_finite_of_spec_baseChange

isEtaleAt_of_spec_baseChange_atPrime