English
For a triplet T and a point p in Spec T.tensor, the Spec map composed with ofPointTensor and tensorCongr recovers the FromSpecResidueField map of the tensor, matching the pullback’s residue field data.
Русский
Для тройки T и точки p в Spec T.tensor композиции Spec.map с ofPointTensor и tensorCongr восстанавливают FromSpecResidueField для тензора.
LaTeX
$$$\forall T p:\; (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) \; \circ \; Spec.map (ofPointTensor (T.SpecTensorTo.base p)) \; \circ \; Spec.map (tensorCongr (T.ofPoint_SpecTensorTo p).symm).hom) = (Spec T.tensor).fromSpecResidueField p$$$
Lean4
/-- Given a triple `(x, y, s)` with `f x = s = f y` there exists `t : X ×[S] Y` above
`x` and `ỳ`. For the unpacked version without `Triplet`, see
`AlgebraicGeometry.Scheme.Pullback.exists_preimage`. -/
theorem exists_preimage (T : Triplet f g) :
∃ t : ↑(pullback f g), (pullback.fst f g).base t = T.x ∧ (pullback.snd f g).base t = T.y :=
⟨carrierEquiv.symm ⟨T, Nonempty.some inferInstance⟩, by simp⟩
