Module

PullbackResidue.lean

Nyll.SchemeTheory.FiniteEtale.BaseChange.PullbackResidue

5 declarations indexed from sourceView source ↗

Module documentation

Residue fields of Artinian pullback tensors

For a point of a scheme-theoretic pullback, the pullback carrier API gives a canonical map from the tensor product of the two residue fields to the residue field of the point. When that tensor product is Artinian, this map is surjective: the prime selected by the point is maximal, so its canonical residue map is already a quotient map.

Imports2

Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.RingTheory.Artinian.Module

Imported by3

def

tensorIsoTensorProduct

L35 ↗

AlgebraicGeometry.Scheme.Pullback.Triplet.tensorIsoTensorProduct

Documentation

The categorical pushout used in the pullback-carrier description is canonically the ordinary tensor product of the two residue fields.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits
open scoped TensorProduct
namespace AlgebraicGeometry.Scheme.Pullback
universe u
variable {X Y S : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S}
namespace Triplet

Lean source · full declaration

def tensorIsoTensorProduct (T : Triplet f g) :
    letI : Algebra (S.residueField T.s) (X.residueField T.x) :=
      (((S.residueFieldCongr T.hx).inv ≫
        f.residueFieldMap T.x).hom).toAlgebra
    letI : Algebra (S.residueField T.s) (Y.residueField T.y) :=
      (((S.residueFieldCongr T.hy).inv ≫
        g.residueFieldMap T.y).hom).toAlgebra
    T.tensor ≅ CommRingCat.of
      (X.residueField T.x ⊗[S.residueField T.s]
        Y.residueField T.y) := by
  letI : Algebra (S.residueField T.s) (X.residueField T.x) :=
    (((S.residueFieldCongr T.hx).inv ≫
      f.residueFieldMap T.x).hom).toAlgebra
  letI : Algebra (S.residueField T.s) (Y.residueField T.y) :=
    (((S.residueFieldCongr T.hy).inv ≫
      g.residueFieldMap T.y).hom).toAlgebra
  exact (IsPushout.of_hasPushout _ _).isoIsPushout _ _
    (CommRingCat.isPushout_tensorProduct
      (S.residueField T.s) (X.residueField T.x)
      (Y.residueField T.y))

theorem

tensorInl_tensorIsoTensorProduct_hom

L57 ↗

AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInl_tensorIsoTensorProduct_hom

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits
open scoped TensorProduct
namespace AlgebraicGeometry.Scheme.Pullback
universe u
variable {X Y S : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S}
namespace Triplet

Lean source · full declaration

theorem tensorInl_tensorIsoTensorProduct_hom (T : Triplet f g) :
    letI : Algebra (S.residueField T.s) (X.residueField T.x) :=
      (((S.residueFieldCongr T.hx).inv ≫
        f.residueFieldMap T.x).hom).toAlgebra
    letI : Algebra (S.residueField T.s) (Y.residueField T.y) :=
      (((S.residueFieldCongr T.hy).inv ≫
        g.residueFieldMap T.y).hom).toAlgebra
    T.tensorInl ≫ (tensorIsoTensorProduct T).hom =
      CommRingCat.ofHom (Algebra.TensorProduct.includeLeftRingHom
        (R := S.residueField T.s) (A := X.residueField T.x)
        (B := Y.residueField T.y)) := by
  let : Algebra (S.residueField T.s) (X.residueField T.x) :=
    (((S.residueFieldCongr T.hx).inv ≫
      f.residueFieldMap T.x).hom).toAlgebra
  let : Algebra (S.residueField T.s) (Y.residueField T.y) :=
    (((S.residueFieldCongr T.hy).inv ≫
      g.residueFieldMap T.y).hom).toAlgebra
  exact IsPushout.inl_isoIsPushout_hom
    (X.residueField T.x) (Y.residueField T.y)
    (IsPushout.of_hasPushout _ _)
    (CommRingCat.isPushout_tensorProduct
      (S.residueField T.s) (X.residueField T.x)
      (Y.residueField T.y))

theorem

tensorInr_tensorIsoTensorProduct_hom

L82 ↗

AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInr_tensorIsoTensorProduct_hom

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits
open scoped TensorProduct
namespace AlgebraicGeometry.Scheme.Pullback
universe u
variable {X Y S : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S}
namespace Triplet

Lean source · full declaration

theorem tensorInr_tensorIsoTensorProduct_hom (T : Triplet f g) :
    letI : Algebra (S.residueField T.s) (X.residueField T.x) :=
      (((S.residueFieldCongr T.hx).inv ≫
        f.residueFieldMap T.x).hom).toAlgebra
    letI : Algebra (S.residueField T.s) (Y.residueField T.y) :=
      (((S.residueFieldCongr T.hy).inv ≫
        g.residueFieldMap T.y).hom).toAlgebra
    T.tensorInr ≫ (tensorIsoTensorProduct T).hom =
      CommRingCat.ofHom ((Algebra.TensorProduct.includeRight
        (R := S.residueField T.s) (A := X.residueField T.x)
        (B := Y.residueField T.y)).toRingHom) := by
  let : Algebra (S.residueField T.s) (X.residueField T.x) :=
    (((S.residueFieldCongr T.hx).inv ≫
      f.residueFieldMap T.x).hom).toAlgebra
  let : Algebra (S.residueField T.s) (Y.residueField T.y) :=
    (((S.residueFieldCongr T.hy).inv ≫
      g.residueFieldMap T.y).hom).toAlgebra
  exact IsPushout.inr_isoIsPushout_hom
    (X.residueField T.x) (Y.residueField T.y)
    (IsPushout.of_hasPushout _ _)
    (CommRingCat.isPushout_tensorProduct
      (S.residueField T.s) (X.residueField T.x)
      (Y.residueField T.y))

theorem

ofPointTensor_SpecTensorTo_surjective

L108 ↗

AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo_surjective

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open scoped TensorProduct
namespace AlgebraicGeometry.Scheme.Pullback
universe u
variable {X Y S : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S}

Lean source · statement

theorem ofPointTensor_SpecTensorTo_surjective
    (T : Triplet f g) (p : Spec T.tensor)
    [IsArtinianRing T.tensor] :
    Function.Surjective (ofPointTensor (T.SpecTensorTo p))

theorem

ofPointTensor_surjective_of_isArtinian

L148 ↗

AlgebraicGeometry.Scheme.Pullback.ofPointTensor_surjective_of_isArtinian

Documentation

The canonical map from the tensor product of the projected residue fields to the residue field of a pullback point is surjective whenever the tensor product is Artinian.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open scoped TensorProduct
namespace AlgebraicGeometry.Scheme.Pullback
universe u
variable {X Y S : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S}

Lean source · statement

theorem ofPointTensor_surjective_of_isArtinian
    (t : ↑(pullback f g))
    [IsArtinianRing (Triplet.ofPoint t).tensor] :
    Function.Surjective (ofPointTensor t)

Module documentation

Residue fields of Artinian pullback tensors

Declarations

tensorIsoTensorProduct

tensorInl_tensorIsoTensorProduct_hom

tensorInr_tensorIsoTensorProduct_hom

ofPointTensor_SpecTensorTo_surjective

ofPointTensor_surjective_of_isArtinian