Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst

∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g),
  CategoryTheory.CategoryStruct.comp T.SpecTensorTo (CategoryTheory.Limits.pullback.fst f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInl) (X.fromSpecResidueField T.x)

Defined in: Mathlib.AlgebraicGeometry.PullbackCarrier
Cited by: 3 results in Mathlib
Foundations: Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites18

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
AlgebraicGeometry.Schemestatement and proof · cited by 2,540
CategoryTheory.Limits.pullbackstatement · cited by 864
CategoryTheory.Limits.pullback.fststatement · cited by 639
AlgebraicGeometry.Specstatement · cited by 626
AlgebraicGeometry.Spec.mapstatement and proof · cited by 332
AlgebraicGeometry.Scheme.residueFieldstatement · cited by 95
AlgebraicGeometry.Scheme.fromSpecResidueFieldstatement and proof · cited by 47
CategoryTheory.Limits.pullback.lift_fstproof · cited by 40
AlgebraicGeometry.Scheme.Pullback.Tripletstatement and proof · cited by 33
AlgebraicGeometry.Scheme.Pullback.Triplet.tensorstatement · cited by 25

Cited by3

Results whose statement or proof uses this declaration.

AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorToproof · cited by 2
AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst_assocproof · cited by 0
AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorToproof · cited by 0