NYLL
Module

AffineEquivalence.lean

Nyll.SchemeTheory.FiniteEtale.AffineEquivalence
7 declarations indexed from sourceView source ↗

Module documentation

Finite étale covers of an affine scheme

This file identifies finite étale covers of an affine scheme with finite étale algebras. Under this identification, the contravariance of Spec accounts for the opposite category on the scheme side.

Imports3
Imported by10

Declarations

def

equivUnder

L34 ↗
CommAlgCat.FiniteEtale.equivUnder
Documentation

Finite étale algebras over R are the same as finite étale ring homomorphisms under R.

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
open scoped TensorProduct
namespace CommAlgCat.FiniteEtale
Lean source · full declaration
def equivUnder (R : CommRingCat.{u}) :
    CommAlgCat.FiniteEtale.{u} R ≌
      CategoryTheory.MorphismProperty.Under
        (RingHom.toMorphismProperty RingHom.FiniteEtale) ⊤ R where
  functor.obj A :=
    ⟨(commAlgCatEquivUnder R).functor.obj A.obj, by
      change RingHom.FiniteEtale (algebraMap R A.obj)
      rw [RingHom.finiteEtale_algebraMap_iff]
      let : Module.Finite R A.obj := A.property.left
      let : Algebra.Etale R A.obj := A.property.right
      constructor⟩
  functor.map {A B} f :=
    ⟨(commAlgCatEquivUnder R).functor.map f.hom, trivial, trivial⟩
  inverse.obj A :=
    ⟨CommAlgCat.of R A.right, by
      let := A.hom.hom.toAlgebra
      let h : Algebra.FiniteEtale R A.right := A.2
      change Module.Finite R A.right ∧ Algebra.Etale R A.right
      exact ⟨h.toFinite, h.toEtale⟩⟩
  inverse.map {A B} f :=
    ObjectProperty.homMk (CommAlgCat.ofHom (CommRingCat.toAlgHom f.hom))
  unitIso := NatIso.ofComponents fun A ↦
    ObjectProperty.isoMk _
      (CommAlgCat.isoMk { toRingEquiv := .refl A.obj, commutes' _ := rfl })
  counitIso := .refl _
def

equivUnderInverseCompBaseChangeIso

L64 ↗
CommAlgCat.FiniteEtale.equivUnderInverseCompBaseChangeIso
Documentation

Under equivUnder, tensor-product base change is pushout of finite étale ring homomorphisms.

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
open scoped TensorProduct
namespace CommAlgCat.FiniteEtale
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
Lean source · statement
def equivUnderInverseCompBaseChangeIso :
    (equivUnder (.of R)).inverse ⋙ CommAlgCat.FiniteEtale.baseChange R S ≅
      CategoryTheory.MorphismProperty.Under.pushout
          (RingHom.toMorphismProperty RingHom.FiniteEtale) ⊤
          (CommRingCat.ofHom (algebraMap R S)) ⋙
        (equivUnder (.of S)).inverse
instance

finiteEtaleOverCategoryAffine

L110 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategoryAffine
Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
open scoped TensorProduct
namespace AlgebraicGeometry.FiniteEtale
Lean source · statement
instance finiteEtaleOverCategoryAffine (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X)
def

affineEquivalence

L117 ↗
AlgebraicGeometry.FiniteEtale.affineEquivalence
Documentation

Finite étale covers of Spec R, with arrows reversed, are equivalent to finite étale R-algebras.

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
open scoped TensorProduct
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryAffine (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  FiniteEtale.instCategory X
Lean source · statement
def affineEquivalence (R : CommRingCat.{u}) :
    (AlgebraicGeometry.FiniteEtale (AlgebraicGeometry.Spec R))ᵒᵖ ≌
      CommAlgCat.FiniteEtale.{u} R
def

affineEquivalenceCompBaseChangeIso

L129 ↗
AlgebraicGeometry.FiniteEtale.affineEquivalenceCompBaseChangeIso
Documentation

Pulling back finite étale covers along Spec S ⟶ Spec R corresponds to tensor-product base change of finite étale algebras.

Source context 8 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
open scoped TensorProduct
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryAffine (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  FiniteEtale.instCategory X
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
Lean source · statement
def affineEquivalenceCompBaseChangeIso :
    (affineEquivalence (.of R)).functor ⋙
        CommAlgCat.FiniteEtale.baseChange R S ≅
      (AlgebraicGeometry.FiniteEtale.pullback
          (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))).op ⋙
        (affineEquivalence (.of S)).functor
instance

finiteEtaleInfStableUnderBaseChange

L162 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleInfStableUnderBaseChange
Source context 8 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
open scoped TensorProduct
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryAffine (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  FiniteEtale.instCategory X
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
Lean source · statement
instance finiteEtaleInfStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓
        (@Etale : MorphismProperty Scheme.{u}))
theorem

pullback_specMap_isEquivalence_iff

L172 ↗
AlgebraicGeometry.FiniteEtale.pullback_specMap_isEquivalence_iff
Documentation

The canonical pullback on finite étale covers of affine schemes is an equivalence exactly when tensor-product base change of finite étale algebras is an equivalence. This also identifies the legacy finite-étale property with the intersection of the finite and étale morphism properties.

Source context 9 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
open scoped TensorProduct
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryAffine (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  FiniteEtale.instCategory X
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
local instance finiteEtaleInfStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓
        (@Etale : MorphismProperty Scheme.{u})) :=
  MorphismProperty.IsStableUnderBaseChange.inf
Lean source · statement
theorem pullback_specMap_isEquivalence_iff :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓
        (@Etale : MorphismProperty Scheme.{u})) ⊤
      (Spec.map (CommRingCat.ofHom (algebraMap R S)))).IsEquivalence ↔
    (CommAlgCat.FiniteEtale.baseChange R S : CommAlgCat.FiniteEtale.{u} R ⥤
      CommAlgCat.FiniteEtale.{u} S).IsEquivalence

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