The graph of two coordinate systems: the definitions

Kollár realizes the formal automorphism x_1 ↦ x_1' between two local coordinate systems x_1, x_2, …, x_n and x_1', x_2, …, x_n at a point p of the smooth X on an étale neighbourhood: the closed subscheme U_1(p) = (x_{11} − x_{21}' = x_{12} − x_{22} = ⋯ = 0) ⊆ X × X has two étale coordinate projections ψ_p, ψ_p' : U_2(p) ⇉ X after shrinking, (p, p) ∈ U_2(p), and its completion at (p, p) is the graph of the formal automorphism ([Kol07, 95], the proof of Theorem 92). Włodarczyk takes the fibre product U ×_{𝔸ⁿ} U of the two étale coordinate morphisms φ_1, φ_2 : U → 𝔸ⁿ and an irreducible component of it through the point above x ([Wlo05, Lemma 2.9.5], step (0) of the proof). This file defines the objects:

• EtaleCoordinates.graph c c' := pullback φ_u φ_v, with projections graphFst = ψ_u, graphSnd = ψ_v and graphToProd : W ⟶ U ×_k U (pullback.mapDesc along 𝔸ⁿ_k ⟶ Spec k).
• EtaleNbhdPair X p (the pair ψ, ψ' : U ⇉ X of [Kol07, Definition 91], without surjectivity): a scheme W with a point q and two étale maps ψ, ψ' : W ⟶ X sending q to p with trivial residue field extension; EtaleCoordinates.NbhdPair c c' hpU: the same landing in U, carrying the coordinate identity ψ^*(u_i) = ψ'^*(v_i), with NbhdPair.toEtaleNbhdPair.

The properties of the graph are proved in GraphBasic.lean, GraphPoint.lean, GraphFormal.lean, GraphCompletion.lean, GraphComponent.lean and GraphDiagonalPair.lean; the pairs enter the étale equivalence of hypersurfaces of maximal contact (Hironaka/Resolution/Algebraic/MaximalContact/).

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.affineSpaceToSpec (k : Type u) [Field k] (n : ℕ) : Spec ↧(MvPolynomial (Fin n) k) ⟶ Spec ↧k

The structure morphism 𝔸ⁿ_k = Spec k[t_0, …, t_{n-1}] ⟶ Spec k.

Equations

• AlgebraicGeometry.affineSpaceToSpec k n = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k (MvPolynomial (Fin n) k)))

@[reducible, inline]

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

The graph scheme W = U ×_{𝔸ⁿ} U of the two coordinate systems, the fibre product of φ_u and φ_v (Kollár's U_1(p), [Kol07, 95]; Włodarczyk's U ×_{𝔸ⁿ} U, the proof of Wlo05, Lemma 2.9.5).

Equations

• c.graph c' = CategoryTheory.Limits.pullback (AlgebraicGeometry.toAffineSpace f (↑U) c.v) (AlgebraicGeometry.toAffineSpace f (↑U) c'.v)

@[reducible, inline]

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

The first projection ψ_u : W ⟶ U.

Equations

• c.graphFst c' = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.toAffineSpace f (↑U) c.v) (AlgebraicGeometry.toAffineSpace f (↑U) c'.v)

@[reducible, inline]

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

The second projection ψ_v : W ⟶ U.

Equations

• c.graphSnd c' = CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.toAffineSpace f (↑U) c.v) (AlgebraicGeometry.toAffineSpace f (↑U) c'.v)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.EtaleCoordinates.graphToProd {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n : ℕ} {U : ↑X.affineOpens} (c c' : EtaleCoordinates f n U) : c.graph c' ⟶ CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (toAffineSpace f (↑U) c.v) (affineSpaceToSpec k n)) (CategoryTheory.CategoryStruct.comp (toAffineSpace f (↑U) c'.v) (affineSpaceToSpec k n))

The map W ⟶ U ×_k U (Kollár's U_1(p) ⊆ X × X), (ψ_u, ψ_v).

Equations

• c.graphToProd c' = CategoryTheory.Limits.pullback.mapDesc (AlgebraicGeometry.toAffineSpace f (↑U) c.v) (AlgebraicGeometry.toAffineSpace f (↑U) c'.v) (AlgebraicGeometry.affineSpaceToSpec k n)

structure AlgebraicGeometry.EtaleNbhdPair (X : Scheme) (p : ↥X) : Type (u + 1)

An étale neighbourhood pair of p ∈ X: a scheme W with a point q and two étale morphisms ψ, ψ' : W ⟶ X sending q to p, with trivial residue field extension κ(q) = κ(p) along both (the "étale surjections ψ, ψ' : U ⇉ X" of [Kol07, Definition 91] without the surjectivity, which EtaleCover.lean handles; the "étale neighbourhoods φ_u, φ_v : X̄ → X of x = φ_u(x̄) = φ_v(x̄)" of [Wlo05, Lemma 2.9.5]).

• W : Scheme

  The étale neighbourhood.

• q : ↥self.W

  The point over p.

• ψ : self.W ⟶ X

  The first étale map ψ.

• ψ' : self.W ⟶ X

  The second étale map ψ'.

• etale_ψ : Etale self.ψ
• etale_ψ' : Etale self.ψ'
• ψ_q : self.ψ self.q = p
• ψ'_q : self.ψ' self.q = p
• isIso_residueFieldMap_ψ : CategoryTheory.IsIso (Scheme.Hom.residueFieldMap self.ψ self.q)

  κ(q) = κ(p) along ψ.

• isIso_residueFieldMap_ψ' : CategoryTheory.IsIso (Scheme.Hom.residueFieldMap self.ψ' self.q)

  κ(q) = κ(p) along ψ'.

structure AlgebraicGeometry.EtaleCoordinates.NbhdPair {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) : Type (u + 1)

For the coordinate data u, v on U ∋ p: an étale neighbourhood pair landing in U, ψ, ψ' : W ⟶ U étale with ψ(q) = ψ'(q) = p, κ(q) = κ(p), and the coordinate identity ψ^*(u_i) = ψ'^*(v_i) for every i (Włodarczyk's w_1 = φ_u^*(u) = φ_v^*(v), w_i = φ_u^*(u_i) = φ_v^*(u_i), the proof of [Wlo05, Lemma 2.9.5]).

• W : Scheme

  The étale neighbourhood.

• q : ↥self.W

  The point over p.

• ψ : self.W ⟶ ↑↑U

  The first étale map ψ : W ⟶ U.

• ψ' : self.W ⟶ ↑↑U

  The second étale map ψ' : W ⟶ U.

• etale_ψ : Etale self.ψ
• etale_ψ' : Etale self.ψ'
• ψ_q : self.ψ self.q = ⟨p, hpU⟩
• ψ'_q : self.ψ' self.q = ⟨p, hpU⟩
• isIso_residueFieldMap_ψ : CategoryTheory.IsIso (Scheme.Hom.residueFieldMap self.ψ self.q)
• isIso_residueFieldMap_ψ' : CategoryTheory.IsIso (Scheme.Hom.residueFieldMap self.ψ' self.q)
• coord (i : Fin n) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop self.ψ)) ((CategoryTheory.ConcreteCategory.hom (↑U).topIso.inv) (c.v i)) = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop self.ψ')) ((CategoryTheory.ConcreteCategory.hom (↑U).topIso.inv) (c'.v i))

  The coordinate identity ψ^*(u_i) = ψ'^*(v_i).

noncomputable def 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) : EtaleNbhdPair X p

The étale neighbourhood pair of p ∈ X underlying a pair for coordinate data on U ∋ p: compose with the open immersion U ⟶ X.

Equations

• One or more equations did not get rendered due to their size.