English
For t in the pullback, the Spec map composed with the SpecTensorTo map equals the canonical Spec map from the pullback to the residue field at t. This expresses that the Spec-level realization of the fiber product matches the point-wise tensor construction.
Русский
Для t в pullback:f, композиция Spec.map с Triplet.ofPoint t .SpecTensorTo равна каноническому отображению Spec из pullback в резидульное поле точки t. Это утверждает, что на уровне Spec реализация расщепления волокна совпадает с тензорной конструкцией.
LaTeX
$$$\operatorname{Spec}.map (\operatorname{ofPointTensor} t) \; ≫ \; (\operatorname{Triplet}.ofPoint t)\!\; \operatorname{SpecTensorTo} = (\text{pullback } f g).\mathrm{fromSpecResidueField} t$$$
Lean4
@[reassoc]
theorem ofPointTensor_SpecTensorTo (t : ↑(pullback f g)) :
Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo = (pullback f g).fromSpecResidueField t :=
by
apply pullback.hom_ext
· rw [← Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField]
simp only [Category.assoc, Triplet.specTensorTo_fst, Triplet.ofPoint_x]
rw [← pushout.inl_desc _ _ (residueFieldCongr_inv_residueFieldMap_ofPoint t), Spec.map_comp]
rfl
· rw [← Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField]
simp only [Category.assoc, Triplet.specTensorTo_snd, Triplet.ofPoint_y]
rw [← pushout.inr_desc _ _ (residueFieldCongr_inv_residueFieldMap_ofPoint t), Spec.map_comp]
rfl
