Mathlib Map

Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInr

{X Y S : AlgebraicGeometry.Scheme} →
  {f : X ⟶ S} → {g : Y ⟶ S} → (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) → Y.residueField T.y ⟶ T.tensor

Given x : X and y : Y such that f x = s = g y, this is the canonical map κ(y) ⟶ κ(x) ⊗[κ(s)] κ(y).

Defined in
Mathlib.AlgebraicGeometry.PullbackCarrier
Cited by
9 results in Mathlib
Foundations
Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AlgebraicGeometry.Scheme.Pullback.Triplet.SpecTensorTo · cited by 13Triplet.SpecTensorToAlgebraicGeometry.Scheme.Pullback.Triplet.SpecMap_tensorInl_fromSpecResidueField · cited by 4Triplet.SpecMap_tensorInl…AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst · cited by 3Triplet.specTensorTo_fstAlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd · cited by 3Triplet.specTensorTo_sndAlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo · cited by 2Pullback.ofPointTensor_Sp…AlgebraicGeometry.Scheme.Pullback.Triplet.snd_SpecTensorTo_apply · cited by 2Triplet.snd_SpecTensorTo_…AlgebraicGeometry.Scheme.Pullback.Triplet.fst_SpecTensorTo_apply · cited by 2Triplet.fst_SpecTensorTo_…AlgebraicGeometry.Scheme.Pullback.Triplet.isPullback_SpecMap_tensor · cited by 1Triplet.isPullback_SpecMa…AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd_assoc · cited by 0Triplet.specTensorTo_snd_…AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo · cited by 0Triplet.Spec_ofPointTenso…Quiver.Hom · cited by 32603Quiver.HomCategoryTheory.CategoryStruct.comp · cited by 17999CategoryStruct.compCategoryTheory.Iso.inv · cited by 6514Iso.invAlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeCommRingCat · cited by 2333CommRingCatCategoryTheory.Limits.pushout.inr · cited by 193pushout.inrAlgebraicGeometry.Scheme.residueField · cited by 95Scheme.residueFieldAlgebraicGeometry.Scheme.Pullback.Triplet · cited by 33Pullback.TripletAlgebraicGeometry.Scheme.Hom.residueFieldMap · cited by 28Hom.residueFieldMapAlgebraicGeometry.Scheme.Pullback.Triplet.tensor · cited by 25Triplet.tensorAlgebraicGeometry.Scheme.Pullback.Triplet.x · cited by 21Triplet.xAlgebraicGeometry.Scheme.Pullback.Triplet.y · cited by 21Triplet.yAlgebraicGeometry.Scheme.residueFieldCongr · cited by 20Scheme.residueFieldCongrAlgebraicGeometry.Scheme.Pullback.Triplet.hx · cited by 4Triplet.hxAlgebraicGeometry.Scheme.Pullback.Triplet.hy · cited by 4Triplet.hyTriplet.tensorInrCITED BYCITES

Cites15

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

Cited by10

Results whose statement or proof uses this declaration.