Module

PullbackResidueTensorProduct.lean

Nyll.SchemeTheory.FiniteEtale.BaseChange.PullbackResidueTensorProduct

4 declarations indexed from sourceView source ↗

Module documentation

The explicit residue-field tensor map of a pullback point

This file replaces the categorical pushout in the pullback-carrier API by the ordinary tensor product and records the two factor maps. The resulting map is surjective as soon as the categorical residue tensor is Artinian.

Imports1

Nyll.SchemeTheory.FiniteEtale.BaseChange.PullbackResidue

Imported by3

def

tensorProductToResidueField

L30 ↗

AlgebraicGeometry.Scheme.Pullback.tensorProductToResidueField

Documentation

The canonical map from the ordinary tensor product of the projected residue fields to the residue field of a pullback point.

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 · full declaration

def tensorProductToResidueField (t : ↑(pullback f g)) :
    let T := Triplet.ofPoint t
    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
    CommRingCat.of (X.residueField T.x ⊗[S.residueField T.s]
      Y.residueField T.y) ⟶ (pullback f g).residueField t := by
  let T := Triplet.ofPoint t
  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 (T.tensorIsoTensorProduct).inv ≫ ofPointTensor t

theorem

includeLeft_tensorIsoTensorProduct_inv

L51 ↗

AlgebraicGeometry.Scheme.Pullback.includeLeft_tensorIsoTensorProduct_inv

Documentation

The inverse tensor-product comparison sends the explicit left inclusion to the categorical pushout inclusion.

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 · full declaration

theorem includeLeft_tensorIsoTensorProduct_inv
    (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
    CommRingCat.ofHom (Algebra.TensorProduct.includeLeftRingHom
        (R := S.residueField T.s) (A := X.residueField T.x)
        (B := Y.residueField T.y)) ≫
      (T.tensorIsoTensorProduct).inv = T.tensorInl := 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
  rw [← cancel_mono (T.tensorIsoTensorProduct).hom]
  simp

theorem

includeRight_tensorIsoTensorProduct_inv

L74 ↗

AlgebraicGeometry.Scheme.Pullback.includeRight_tensorIsoTensorProduct_inv

Documentation

The inverse tensor-product comparison sends the explicit right inclusion to the categorical pushout inclusion.

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 · full declaration

theorem includeRight_tensorIsoTensorProduct_inv
    (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
    CommRingCat.ofHom ((Algebra.TensorProduct.includeRight
        (R := S.residueField T.s) (A := X.residueField T.x)
        (B := Y.residueField T.y)).toRingHom) ≫
      (T.tensorIsoTensorProduct).inv = T.tensorInr := 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
  rw [← cancel_mono (T.tensorIsoTensorProduct).hom]
  simp

theorem

tensorProductToResidueField_surjective_of_isArtinian

L97 ↗

AlgebraicGeometry.Scheme.Pullback.tensorProductToResidueField_surjective_of_isArtinian

Documentation

The explicit residue-field tensor map is surjective whenever the categorical residue tensor selected by the pullback carrier 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 · full declaration

theorem tensorProductToResidueField_surjective_of_isArtinian
    (t : ↑(pullback f g))
    [IsArtinianRing (Triplet.ofPoint t).tensor] :
    let T := Triplet.ofPoint t
    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
    Function.Surjective (tensorProductToResidueField t) := by
  dsimp only
  let T := Triplet.ofPoint t
  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 (ofPointTensor_surjective_of_isArtinian t).comp
    (T.tensorIsoTensorProduct).commRingCatIsoToRingEquiv.symm.surjective

Module documentation

The explicit residue-field tensor map of a pullback point

Declarations

tensorProductToResidueField

includeLeft_tensorIsoTensorProduct_inv

includeRight_tensorIsoTensorProduct_inv

tensorProductToResidueField_surjective_of_isArtinian