The graph of two coordinate systems: projections and the coordinate identity

For two coordinate systems u, v on the affine open U (CoordinateSystem.lean), W = U ×_{𝔸ⁿ} U with projections ψ_u, ψ_v (Hironaka/Scheme/Smooth/Graph.lean). Kollár's U_1(p) and its coordinate projections ([Kol07, 95], the proof of Theorem 92); Włodarczyk's U ×_{𝔸ⁿ} U and the functions w_i on it ([Wlo05, Lemma 2.9.5], step (0) of the proof).

• φ_u ∘ ψ_u = φ_v ∘ ψ_v (pullback.condition); W ⟶ U ×_k U is a closed immersion, 𝔸ⁿ_k ⟶ Spec k being separated (Mathlib's IsClosedImmersion (pullback.mapDesc f g i)); and W is the locus where the pulled back coordinates agree: a pair of k-morphisms a, b : T ⟶ U with a^*(u_i) = b^*(v_i) has a ≫ φ_u = b ≫ φ_v, because a morphism into the affine 𝔸ⁿ_k = Spec k[t] is determined by its map on global sections (Mathlib's ext_of_isAffine), that map on k[t] by the images of the t_i and of the constants (MvPolynomial.ringHom_ext), the t_i go to the coordinates (toAffineSpace_appTop_X) and the constants to the pullbacks along U ⟶ Spec k (toAffineSpace_appTop_C, from toAffineSpace_comp_structure); so the pair factors uniquely through W (existsUnique_lift_graph).
• The projections are étale, as base changes of étale maps (Mathlib's instances).
• The coordinate identity ψ_u^*(u_i) = ψ_v^*(v_i) in Γ(W, 𝒪_W): pullback.condition applied to the coordinate functions (graphFst_appTop_eq).

theorem AlgebraicGeometry.toAffineSpace_appTop_C {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} {U : ↑X.affineOpens} (v : Fin n → ↑(X.presheaf.obj (Opposite.op ↑U))) (r : k) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (toAffineSpace f (↑U) v))) ((CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso ↧(MvPolynomial (Fin n) k)).inv) (MvPolynomial.C r)) = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (CategoryTheory.CategoryStruct.comp (↑U).ι f))) ((CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso ↧k).inv) r)

The coordinate morphism pulls the constant C r of k[t] back to the pullback of r along U ⟶ Spec k (toAffineSpace_comp_structure).

theorem AlgebraicGeometry.toAffineSpace_ext {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} {U : ↑X.affineOpens} {T : Scheme} (v v' : Fin n → ↑(X.presheaf.obj (Opposite.op ↑U))) (a b : T ⟶ ↑↑U) (hk : CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp (↑U).ι f) = CategoryTheory.CategoryStruct.comp b (CategoryTheory.CategoryStruct.comp (↑U).ι f)) (hcoord : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop a)) ((CategoryTheory.ConcreteCategory.hom (↑U).topIso.inv) (v i)) = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop b)) ((CategoryTheory.ConcreteCategory.hom (↑U).topIso.inv) (v' i))) : CategoryTheory.CategoryStruct.comp a (toAffineSpace f (↑U) v) = CategoryTheory.CategoryStruct.comp b (toAffineSpace f (↑U) v')

Two k-morphisms a, b : T ⟶ U with a^*(u_i) = b^*(v_i) for all i have a ≫ φ_u = b ≫ φ_v: a morphism to 𝔸ⁿ_k is determined by the coordinates and the k-structure.

theorem AlgebraicGeometry.EtaleCoordinates.graphFst_comp_toAffineSpace {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n : ℕ} {U : ↑X.affineOpens} (c c' : EtaleCoordinates f n U) : CategoryTheory.CategoryStruct.comp (c.graphFst c') (toAffineSpace f (↑U) c.v) = CategoryTheory.CategoryStruct.comp (c.graphSnd c') (toAffineSpace f (↑U) c'.v)

φ_u ∘ ψ_u = φ_v ∘ ψ_v.

theorem AlgebraicGeometry.EtaleCoordinates.graphFst_appTop_eq {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n : ℕ} {U : ↑X.affineOpens} (c c' : EtaleCoordinates f n U) (i : Fin n) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (c.graphFst c'))) ((CategoryTheory.ConcreteCategory.hom (↑U).topIso.inv) (c.v i)) = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (c.graphSnd c'))) ((CategoryTheory.ConcreteCategory.hom (↑U).topIso.inv) (c'.v i))

The coordinate identity ψ_u^*(u_i) = ψ_v^*(v_i) in Γ(W, 𝒪_W) (Włodarczyk's w_i = φ_u^*(u_i) = φ_v^*(v_i), the proof of [Wlo05, Lemma 2.9.5]).

theorem AlgebraicGeometry.EtaleCoordinates.existsUnique_lift_graph {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n : ℕ} {U : ↑X.affineOpens} (c c' : EtaleCoordinates f n U) {T : Scheme} (a b : T ⟶ ↑↑U) (hk : CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp (↑U).ι f) = CategoryTheory.CategoryStruct.comp b (CategoryTheory.CategoryStruct.comp (↑U).ι f)) (hcoord : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop a)) ((CategoryTheory.ConcreteCategory.hom (↑U).topIso.inv) (c.v i)) = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop b)) ((CategoryTheory.ConcreteCategory.hom (↑U).topIso.inv) (c'.v i))) : ∃! h : T ⟶ c.graph c', CategoryTheory.CategoryStruct.comp h (c.graphFst c') = a ∧ CategoryTheory.CategoryStruct.comp h (c.graphSnd c') = b

W is the locus of U ×_k U where the pulled-back coordinate vectors agree: a pair of k-morphisms a, b : T ⟶ U with a^*(u_i) = b^*(v_i) factors uniquely through W.