The graph of two coordinate systems: Noetherianity and étale restrictions

• The graph W = U ×_{𝔸ⁿ} U is a Noetherian scheme (isNoetherian_graph): affine (a fibre product of affines) and locally Noetherian (of finite type over 𝔸ⁿ_k, Mathlib's LocallyOfFiniteType.isLocallyNoetherian).
• The restriction of an étale morphism to an open subscheme is étale (etale_ι_comp).
• The underlying étale neighbourhood pair of a NbhdPair has the maps ψ ≫ U.ι, ψ' ≫ U.ι (NbhdPair.toEtaleNbhdPair_ψ).

The neighbourhood pair on which two hypersurfaces of maximal contact are compared is the one at the diagonal point (GraphDiagonalPair.lean).

instance AlgebraicGeometry.etale_ι_comp {W Y : Scheme} (V : W.Opens) (ψ : W ⟶ Y) [Etale ψ] : Etale (CategoryTheory.CategoryStruct.comp V.ι ψ)

The restriction of an étale morphism to an open subscheme is étale.

theorem AlgebraicGeometry.EtaleCoordinates.isNoetherian_graph {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n : ℕ} {U : ↑X.affineOpens} (c c' : EtaleCoordinates f n U) : IsNoetherian (c.graph c')

The graph W = U ×_{𝔸ⁿ} U is a Noetherian scheme: affine, and of finite type over 𝔸ⁿ_k through ψ_u ≫ φ_u.

theorem AlgebraicGeometry.EtaleCoordinates.NbhdPair.toEtaleNbhdPair_ψ {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n : ℕ} {U : ↑X.affineOpens} (c c' : EtaleCoordinates f n U) {p : ↥X} {hpU : p ∈ ↑U} (P : c.NbhdPair c' hpU) : (toEtaleNbhdPair c c' P).ψ = CategoryTheory.CategoryStruct.comp P.ψ (↑U).ι ∧ (toEtaleNbhdPair c c' P).ψ' = CategoryTheory.CategoryStruct.comp P.ψ' (↑U).ι

The underlying étale neighbourhood pair of p ∈ X has the maps ψ ≫ U.ι, ψ' ≫ U.ι.