[Merged by Bors] - feat(AlgebraicGeometry/Pullback): description of the underlying topological space of a fiber product of schemes

[chrisflav]

Let f : X ⟶ S and g : Y ⟶ S be morphisms of schemes. In this PR we describe the underlying
topological space of pullback f g, i.e. the fiber product X ×[S] Y. In particular, we show that the points of X ×[S] Y correspond bijectively to pairs (z, p) of triples z = (x, y, s) with f x = s = g y and prime ideals q of κ(x) ⊗[κ(s)] κ(y).

From the valuative criterion project.

Co-authored-by: Qi Ge
Co-authored-by: Andrew Yang

---

• depends on: [Merged by Bors] - feat(AlgebraicGeometry): Classification of Spec R ⟶ X with R local. #15240
• depends on: [Merged by Bors] - feat(AlgebraicGeometry/ResidueField): classification of Spec K ⟶ X with K a field #17768
• depends on: [Merged by Bors] - feat(AlgebraicGeometry): pre-requisites of description of topological space of pullback #18255

[github-actions]

PR summary 2205925ca6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicGeometry.PullbackCarrier	1858

---

Declarations diff

+ SpecOfPoint
+ SpecTensorTo
+ SpecTensorTo_SpecOfPoint
+ Spec_map_tensorInl_fromSpecResidueField
+ Spec_map_tensor_isPullback
+ Triplet
+ Triplet.Spec_ofPointTensor_SpecTensorTo
+ Triplet.exists_preimage
+ carrierEquiv
+ carrierEquiv_eq_iff
+ carrierEquiv_symm_fst
+ carrierEquiv_symm_snd
+ exists_preimage_pullback
+ ext
+ instance (T : Triplet f g) : Nontrivial T.tensor
+ mk'
+ ofPoint
+ ofPointTensor
+ ofPointTensor_SpecTensorTo
+ ofPoint_SpecTensorTo
+ range_fst
+ range_fst_comp
+ range_map
+ range_snd
+ range_snd_comp
+ residueFieldCongr_inv_residueFieldMap_ofPoint
+ specTensorTo_base_fst
+ specTensorTo_base_snd
+ specTensorTo_fst
+ specTensorTo_snd
+ tensor
+ tensorCongr
+ tensorCongr_SpecTensorTo
+ tensorCongr_inv
+ tensorCongr_refl
+ tensorCongr_symm
+ tensorCongr_trans
+ tensorCongr_trans_hom
+ tensorInl
+ tensorInr

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[erdOne]

LGTM but I also contributed a significant portion of this.

[erdOne]

LGTM

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(AlgebraicGeometry): Classification of Spec R ⟶ X with R local. #15240
• [Merged by Bors] - feat(AlgebraicGeometry/ResidueField): classification of Spec K ⟶ X with K a field #17768
• [Merged by Bors] - feat(AlgebraicGeometry): pre-requisites of description of topological space of pullback #18255
  By Dependent Issues (🤖). Happy coding!

[kim-em]

bors d+

[mathlib-bors]

✌️ chrisflav can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[chrisflav]

Thanks for the reviews!

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build