The étale neighbourhood pair of the graph at the diagonal point (p, p) #
Kollár shrinks the graph U₁(p) to an open U₂(p) ∋ (p, p) on which "both coordinate
projections ψₚ, ψₚ' : U₂(p) ⇉ X are étale" ([Kol07, 95], the proof of Theorem 92). The graph
U₁(p) = U ×_{𝔸ⁿ} U of two étale coordinate systems c, c' on an affine U ∋ p (graph), its
two projections (graphFst, graphSnd, étale as base changes of the étale coordinate maps, so no
shrinking is needed), and the canonical point (p, p) : Spec κ(p) ⟶ U₁(p) (graphPoint) are
defined in Graph.lean, GraphBasic.lean and GraphFormal.lean. This module packages the pair AT
THE DIAGONAL POINT as a NbhdPair and proves the three properties the comparison of two
hypersurfaces of maximal contact needs of it
(Hironaka/Resolution/Algebraic/MaximalContact/Theorem92.lean):
- (i) both projections are morphisms of
k-schemes (graphFst_comp_structure:U₁(p) ⊆ X ×_k X); - (ii)
ψ^*(s) − ψ'^*(s) ∈ 𝔪_qfor everys ∈ 𝒪_{X,p}: the two projections induce the SAME identification ofκ(p)withκ(q), because(p, p)lies on the diagonal: the compositesSpec κ(p) → U₁(p) ⇉ Xare both the canonicalSpec κ(p) → X, so the defectsψ^*(s) − ψ'^*(s)die under the local homomorphism𝒪_{W,q} → 𝒪_{Spec κ(p)}and hence lie in𝔪_q(this clause is what pins the pair's formal automorphism whenκ(p) ≠ k; it is not in the sources); - (iii) the graph equations
ψ^*(cᵢ) = ψ'^*(cᵢ')on stalks (the coordinate identitycoord).
The existence statement exists_etaleNbhdPair_of_etaleCoordinates packages the three properties
on an EtaleNbhdPair.
Two equal morphisms have equal stalk maps, up to the transport of the source stalk along the two (propositionally equal) image points.
The point (p, p) of the graph U₁(p) = U ×_{𝔸ⁿ} U (the image of the morphism
graphPoint : Spec κ(p) ⟶ W).
Equations
- c.graphDiagonalPoint c' hpU hc hc' = (c.graphPoint c' hpU hc hc') default
Instances For
The étale neighbourhood pair of p for the coordinate data c, c' given by the whole graph
U₁(p) = U ×_{𝔸ⁿ} U at the diagonal point (p, p) with its two étale projections (Kollár's
U₂(p), [Kol07, 95], without shrinking; the proof of [Wlo05, Lemma 2.9.5]).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The étale neighbourhood pair of p ∈ X of the graph at its diagonal point: graphNbhdPair
composed with U ⟶ X (NbhdPair.toEtaleNbhdPair).
Equations
- c.graphEtaleNbhdPair c' hpU hc hc' = AlgebraicGeometry.EtaleCoordinates.NbhdPair.toEtaleNbhdPair c c' (c.graphNbhdPair c' hpU hc hc')
Instances For
(i) Both projections of the graph are morphisms of k-schemes: U₁(p) ⊆ X ×_k X ([Kol07, 95];
φ_u ψ_u = φ_v ψ_v composed with the structure map of 𝔸ⁿ_k).
The two composites Spec κ(p) → U₁(p) ⇉ X through the diagonal point are the canonical
Spec κ(p) → X, hence equal (Kollár's point (p, p), [Kol07, 95]).
The stalk map of the diagonal point (p, p) : Spec κ(p) → W, typed at the pair's stalk
𝒪_{W,q}.
Equations
- c.diagonalStalkMap c' hpU hc hc' = AlgebraicGeometry.Scheme.Hom.stalkMap (c.graphPoint c' hpU hc hc') default
Instances For
ψ^* on the stalk, composed with the stalk map of the diagonal point (p, p) : Spec κ(p) → W,
is the stalk map of the composite Spec κ(p) → W → X (transported from p).
ψ'^* on the stalk, composed with the stalk map of the diagonal point.
(ii) At the diagonal point the two projections agree on functions to first order:
ψ^*(s) − ψ'^*(s) ∈ 𝔪_q for every s ∈ 𝒪_{X,p} — both induce the same identification
κ(p) = κ(q). Proof: the defect is killed by the local homomorphism 𝒪_{W,q} → 𝒪_{Spec κ(p)}
induced by (p, p) : Spec κ(p) → W, because the two composites Spec κ(p) → W ⇉ X coincide
(graphPoint_comp_eq), and a local homomorphism detects the maximal ideal.
(iii) The graph equations on stalks: ψ^*(cᵢ) = ψ'^*(cᵢ') (the coordinate identity coord,
read at the germs of the coordinates).
For two étale coordinate systems c, c' on an affine U ∋ p whose coordinates all vanish at
p, the graph U₁(p) at its diagonal point is an étale neighbourhood pair Q of p with (i)
ψ ≫ f = ψ' ≫ f, (ii) ψ^*(s) − ψ'^*(s) ∈ 𝔪_q for every s ∈ 𝒪_{X,p}, and (iii)
ψ^*(cᵢ) = ψ'^*(cᵢ') for every i (Kollár's "(p, p) ∈ U₂(p) ⊂ U₁(p) such that both coordinate
projections ψₚ, ψₚ' : U₂(p) ⇉ X are étale", [Kol07, 95]; the proof of [Wlo05, Lemma 2.9.5];
clause (ii) is not in the sources).