NYLL
Module

Kmf2FiberSpecTensorStalkLeg1AffineDatum.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Kmf2FiberSpecTensorStalkLeg1AffineDatum
5 declarations indexed from sourceView source ↗

Module documentation

Kmf2 Fiber Spec Tensor Stalk Leg1 Affine Datum

Imports8
  • Mathlib.AlgebraicGeometry.Fiber
  • Mathlib.AlgebraicGeometry.Pullbacks
  • Mathlib.AlgebraicGeometry.ResidueField
  • Mathlib.AlgebraicGeometry.StructureSheaf
  • Mathlib.AlgebraicGeometry.Stalk
  • Mathlib.RingTheory.LocalRing.ResidueField.Fiber
  • Mathlib.RingTheory.TensorProduct.Basic
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Imported by2

Declarations

def

kmf2_fiberSpecTensorIso

L34 ↗
Documentation

Identify the scheme-theoretic fiber of an affine scheme map with the spectrum of the residue-field tensor product.

Source context 3 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
Lean source · statement
def kmf2_fiberSpecTensorIso
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) :
    (Spec.map (CommRingCat.ofHom (algebraMap R S))).fiber p ≅
      Spec (CommRingCat.of (p.asIdeal.Fiber S))
theorem

kmf2_fiberSpecTensorIso_hom_includeRight

L48 ↗
Documentation

The tensor-product inclusion of the target ring corresponds to the original fiber inclusion.

Source context 3 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
Lean source · statement
theorem kmf2_fiberSpecTensorIso_hom_includeRight
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) :
    (kmf2_fiberSpecTensorIso R S p).hom ≫
        Spec.map (CommRingCat.ofHom (RingHomClass.toRingHom
          (Algebra.TensorProduct.includeRight
            (R := R) (A := p.asIdeal.ResidueField) (B := S)))) =
      (Spec.map (CommRingCat.ofHom (algebraMap R S))).fiberι p
theorem

kmf2_fiberSpecTensorIso_point_comap

L85 ↗
Documentation

Comapping the prime of a fiber point along the target-ring inclusion recovers its image prime.

Source context 3 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
Lean source · statement
theorem kmf2_fiberSpecTensorIso_point_comap
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R)
    (w : (Spec.map (CommRingCat.ofHom (algebraMap R S))).fiber p) :
    (((kmf2_fiberSpecTensorIso R S p).hom w).asIdeal).comap
        (Algebra.TensorProduct.includeRight
          (R := R) (A := p.asIdeal.ResidueField) (B := S)).toRingHom =
      ((Spec.map (CommRingCat.ofHom (algebraMap R S))).fiberι p w).asIdeal
theorem

kmf2_fiberStalk_localizationAtPrime

L103 ↗
Documentation

The stalk at a fiber point is the localization of the residue-field tensor product at its corresponding prime.

Source context 3 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
Lean source · full declaration
theorem kmf2_fiberStalk_localizationAtPrime
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R)
    (w : (Spec.map (CommRingCat.ofHom (algebraMap R S))).fiber p) :
    let q : PrimeSpectrum (p.asIdeal.Fiber S) := (kmf2_fiberSpecTensorIso R S p).hom w
    Nonempty
      (((Spec.map (CommRingCat.ofHom (algebraMap R S))).fiber p).presheaf.stalk w ≃+*
        Localization.AtPrime q.asIdeal) := by
  let q : PrimeSpectrum (p.asIdeal.Fiber S) := (kmf2_fiberSpecTensorIso R S p).hom w
  exact ⟨(asIso ((kmf2_fiberSpecTensorIso R S p).hom.stalkMap
    w)).commRingCatIsoToRingEquiv.symm.trans
    ((StructureSheaf.stalkIso (p.asIdeal.Fiber S) q).symm.toRingEquiv)⟩
theorem

kmf2_fiberStalkLeg1_affineDatum

L117 ↗
Documentation

For an affine point, construct the prime over its original prime and identify its fiber stalk with the prime localization.

Source context 3 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
Lean source · full declaration
theorem kmf2_fiberStalkLeg1_affineDatum
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
    (x : Spec (CommRingCat.of S)) :
    let p : PrimeSpectrum R := Spec.map (CommRingCat.ofHom (algebraMap R S)) x
    ∃ (Q : Ideal (p.asIdeal.Fiber S)) (_ : Q.IsPrime),
      Q.comap (Algebra.TensorProduct.includeRight
        (R := R)
        (A := p.asIdeal.ResidueField)
        (B := S)).toRingHom = x.asIdeal ∧
      Nonempty
        (((Spec.map (CommRingCat.ofHom (algebraMap R S))).fiber
            (Spec.map (CommRingCat.ofHom (algebraMap R S)) x)).presheaf.stalk
          ((Spec.map (CommRingCat.ofHom (algebraMap R S))).asFiber x) ≃+*
          Localization.AtPrime Q) := by
  refine ⟨((kmf2_fiberSpecTensorIso R S
      (Spec.map (CommRingCat.ofHom (algebraMap R S)) x)).hom
        ((Spec.map (CommRingCat.ofHom (algebraMap R S))).asFiber x)).asIdeal,
    ((kmf2_fiberSpecTensorIso R S
      (Spec.map (CommRingCat.ofHom (algebraMap R S)) x)).hom
        ((Spec.map (CommRingCat.ofHom (algebraMap R S))).asFiber x)).2, ?_, ?_⟩
  · exact (kmf2_fiberSpecTensorIso_point_comap R S
      (show PrimeSpectrum R from Spec.map (CommRingCat.ofHom (algebraMap R S)) x)
      ((Spec.map (CommRingCat.ofHom (algebraMap R S))).asFiber x)).trans
      (congrArg (fun z : Spec (CommRingCat.of S) => z.asIdeal)
        (Scheme.Hom.fiberι_asFiber (Spec.map (CommRingCat.ofHom (algebraMap R S))) x))
  · exact kmf2_fiberStalk_localizationAtPrime R S
      (Spec.map (CommRingCat.ofHom (algebraMap R S)) x)
      ((Spec.map (CommRingCat.ofHom (algebraMap R S))).asFiber x)

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