Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo

∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g)
  (p : ↥(AlgebraicGeometry.Spec T.tensor)),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap T.SpecTensorTo p))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.ofPointTensor (T.SpecTensorTo p)))
        (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯).hom)) =
    (AlgebraicGeometry.Spec T.tensor).fromSpecResidueField p

Defined in

Mathlib.AlgebraicGeometry.PullbackCarrier

Cited by

0 results in Mathlib

Foundations

Depth 187 from the axioms · uses propext, Classical.choice, Quot.sound