Completions of the graph: the formal automorphism, the fixed locus, the point (p, p)

Kollár: "the completion of U_1(p) at (p, p) is the graph of φ_p" ([Kol07, 95], the proof of Theorem 92): the two coordinate projections ψ_p, ψ_p' : U_2(p) ⇉ X induce isomorphisms Ô_{X,p} ≅ Ô_{U_2(p),(p,p)}, and φ := ψ̂' ∘ ψ̂⁻¹ is the formal automorphism x_1 ↦ x_1' of [Kol07, Definition 91]. Włodarczyk adds that φ_u, φ_v coincide on the fixed locus of v − u ([Wlo05, Lemma 2.9.5], step (1) of the proof). The definitions:

• EtaleNbhdPair.stalkHom Q, stalkHom' Q: the local homomorphisms ψ^*, ψ'^* : 𝒪_{X,p} →+* 𝒪_{W,q} of an étale neighbourhood pair (Graph.lean), the stalk maps at q transported along ψ(q) = p.
• EtaleNbhdPair.formalAutomorphism Q ha ha': φ := (ψ̂'^*)⁻¹ ∘ ψ̂^*, an automorphism of Ô_{X,p}, from the bijectivity of the two induced maps on completions (proved in GraphCompletion.lean).
• EtaleCoordinates.fixedLocusIdeal c c', fixedLocus, fixedLocusι: the closed subscheme Z = V(ψ_u^*(v_j − u_j) : j) of the graph W = U ×_{𝔸ⁿ} U; coincidenceLocus c c', coincidenceLocusι: the locus of Z where ψ_u and ψ_v coincide, the preimage of the diagonal of φ_v under (ψ_u, ψ_v) : Z ⟶ U ×_{𝔸ⁿ} U.
• EtaleCoordinates.graphPoint c c' hpU hc hc': the canonical point (p, p) : Spec κ(p) ⟶ W when all coordinates vanish at p (the construction inside exists_graph_point of GraphPoint.lean, named).

noncomputable def AlgebraicGeometry.EtaleNbhdPair.stalkHom {X : Scheme} {p : ↥X} (Q : EtaleNbhdPair X p) : ↑(X.presheaf.stalk p) →+* ↑(Q.W.presheaf.stalk Q.q)

The local homomorphism ψ^* : 𝒪_{X,p} →+* 𝒪_{W,q} of the first map of an étale neighbourhood pair: the stalk map ψ.stalkMap q : 𝒪_{X,ψ(q)} ⟶ 𝒪_{W,q} transported along ψ(q) = p.

Equations

• Q.stalkHom = (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Q.ψ Q.q)).comp ↑(X.presheaf.stalkCongr ⋯).commRingCatIsoToRingEquiv

noncomputable def AlgebraicGeometry.EtaleNbhdPair.stalkHom' {X : Scheme} {p : ↥X} (Q : EtaleNbhdPair X p) : ↑(X.presheaf.stalk p) →+* ↑(Q.W.presheaf.stalk Q.q)

The local homomorphism ψ'^* : 𝒪_{X,p} →+* 𝒪_{W,q} of the second map.

Equations

• Q.stalkHom' = (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Q.ψ' Q.q)).comp ↑(X.presheaf.stalkCongr ⋯).commRingCatIsoToRingEquiv

instance AlgebraicGeometry.EtaleNbhdPair.isLocalHom_stalkHom {X : Scheme} {p : ↥X} (Q : EtaleNbhdPair X p) : IsLocalHom Q.stalkHom

instance AlgebraicGeometry.EtaleNbhdPair.isLocalHom_stalkHom' {X : Scheme} {p : ↥X} (Q : EtaleNbhdPair X p) : IsLocalHom Q.stalkHom'

noncomputable def AlgebraicGeometry.EtaleNbhdPair.formalAutomorphism {X : Scheme} {p : ↥X} (Q : EtaleNbhdPair X p) (ha : Function.Bijective ⇑(IsLocalRing.completionMap Q.stalkHom)) (ha' : Function.Bijective ⇑(IsLocalRing.completionMap Q.stalkHom')) : AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) ↑(X.presheaf.stalk p) ≃+* AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) ↑(X.presheaf.stalk p)

The formal automorphism φ := (ψ̂'^*)⁻¹ ∘ ψ̂^* of Ô_{X,p} (the "automorphism φ : X̂ → X̂" of [Kol07, Definition 91]), from the bijectivity of the two maps induced on the 𝔪-adic completions. For the pair of two coordinate systems it sends the completed germ of u_i to that of v_i (the coordinate identity ψ^*(u_i) = ψ'^*(v_i)); Kollár's φ_p^*(x_1', x_2, …) = (x_1, x_2, …) ([Kol07, 95]) is its inverse on functions.

Equations

• Q.formalAutomorphism ha ha' = (RingEquiv.ofBijective (IsLocalRing.completionMap Q.stalkHom) ha).trans (RingEquiv.ofBijective (IsLocalRing.completionMap Q.stalkHom') ha').symm

theorem AlgebraicGeometry.EtaleNbhdPair.completionMap_stalkHom'_formalAutomorphism {X : Scheme} {p : ↥X} (Q : EtaleNbhdPair X p) (ha : Function.Bijective ⇑(IsLocalRing.completionMap Q.stalkHom)) (ha' : Function.Bijective ⇑(IsLocalRing.completionMap Q.stalkHom')) (x : AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) ↑(X.presheaf.stalk p)) : (IsLocalRing.completionMap Q.stalkHom') ((Q.formalAutomorphism ha ha') x) = (IsLocalRing.completionMap Q.stalkHom) x

theorem AlgebraicGeometry.EtaleCoordinates.graphFst_comp_structure {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') (CategoryTheory.CategoryStruct.comp (↑U).ι f) = CategoryTheory.CategoryStruct.comp (c.graphSnd c') (CategoryTheory.CategoryStruct.comp (↑U).ι f)

The two projections of the graph are morphisms over k: ψ_u ≫ (U ⟶ X ⟶ Spec k) = ψ_v ≫ (U ⟶ X ⟶ Spec k) (φ_u ψ_u = φ_v ψ_v composed with the structure map of 𝔸ⁿ_k, toAffineSpace_comp_structure).

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

The ideal sheaf of the fixed locus Z = V(ψ_u^*(v_j − u_j) : j) ⊆ W of the graph (Włodarczyk's φ_u^{-1}(V(h)), h := v − u, the proof of [Wlo05, Lemma 2.9.5]; Kollár's x_1 − x_1' ∈ MC(I), [Kol07, 95]): for v = (x_1', x_2, …, x_n) and u = (x_1, x_2, …, x_n) only j = 1 contributes.

Equations

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

@[reducible, inline]

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

The fixed locus Z ⊆ W as a closed subscheme.

Equations

• c.fixedLocus c' = (c.fixedLocusIdeal c').subscheme

@[reducible, inline]

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

The closed immersion Z ⟶ W of the fixed locus.

Equations

• c.fixedLocusι c' = (c.fixedLocusIdeal c').subschemeι

theorem AlgebraicGeometry.EtaleCoordinates.fixedLocusι_comp_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.fixedLocusι c') (CategoryTheory.CategoryStruct.comp (c.graphFst c') (toAffineSpace f (↑U) c'.v)) = CategoryTheory.CategoryStruct.comp (c.fixedLocusι c') (CategoryTheory.CategoryStruct.comp (c.graphSnd c') (toAffineSpace f (↑U) c'.v))

On the fixed locus Z the two projections agree after composing with φ_v, i.e. ψ_u|_Z^*(v_j) = ψ_v|_Z^*(v_j) for every j: on Z, ψ_u^*(v_j) = ψ_u^*(u_j), and ψ_u^*(u_j) = ψ_v^*(v_j) on all of W (the coordinate identity).

noncomputable def AlgebraicGeometry.EtaleCoordinates.fixedLocusToDiagonalObj {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n : ℕ} {U : ↑X.affineOpens} (c c' : EtaleCoordinates f n U) : c.fixedLocus c' ⟶ CategoryTheory.Limits.pullback.diagonalObj (toAffineSpace f (↑U) c'.v)

The pair (ψ_u|_Z, ψ_v|_Z) : Z ⟶ U ×_{𝔸ⁿ} U, into the diagonal object of the étale coordinate morphism φ_v.

Equations

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

@[simp]

theorem AlgebraicGeometry.EtaleCoordinates.fixedLocusToDiagonalObj_fst {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.fixedLocusToDiagonalObj c') (CategoryTheory.Limits.pullback.fst (toAffineSpace f (↑U) c'.v) (toAffineSpace f (↑U) c'.v)) = CategoryTheory.CategoryStruct.comp (c.fixedLocusι c') (c.graphFst c')

@[simp]

theorem AlgebraicGeometry.EtaleCoordinates.fixedLocusToDiagonalObj_fst_assoc {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n : ℕ} {U : ↑X.affineOpens} (c c' : EtaleCoordinates f n U) {Z : Scheme} (h : ↑↑U ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.fixedLocusToDiagonalObj c') (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (toAffineSpace f (↑U) c'.v) (toAffineSpace f (↑U) c'.v)) h) = CategoryTheory.CategoryStruct.comp (c.fixedLocusι c') (CategoryTheory.CategoryStruct.comp (c.graphFst c') h)

@[simp]

theorem AlgebraicGeometry.EtaleCoordinates.fixedLocusToDiagonalObj_snd {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.fixedLocusToDiagonalObj c') (CategoryTheory.Limits.pullback.snd (toAffineSpace f (↑U) c'.v) (toAffineSpace f (↑U) c'.v)) = CategoryTheory.CategoryStruct.comp (c.fixedLocusι c') (c.graphSnd c')

@[simp]

theorem AlgebraicGeometry.EtaleCoordinates.fixedLocusToDiagonalObj_snd_assoc {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n : ℕ} {U : ↑X.affineOpens} (c c' : EtaleCoordinates f n U) {Z : Scheme} (h : ↑↑U ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.fixedLocusToDiagonalObj c') (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (toAffineSpace f (↑U) c'.v) (toAffineSpace f (↑U) c'.v)) h) = CategoryTheory.CategoryStruct.comp (c.fixedLocusι c') (CategoryTheory.CategoryStruct.comp (c.graphSnd c') h)

@[reducible, inline]

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

The coincidence locus of ψ_u|_Z and ψ_v|_Z: the preimage of the diagonal Δ : U ⟶ U ×_{𝔸ⁿ} U of the étale φ_v under (ψ_u|_Z, ψ_v|_Z), the equalizer of the two restricted projections (Włodarczyk's locus where "φ_u and φ_v coincide", the proof of [Wlo05, Lemma 2.9.5]).

Equations

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

@[reducible, inline]

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

The immersion of the coincidence locus into the fixed locus Z.

Equations

• c.coincidenceLocusι c' = CategoryTheory.Limits.pullback.fst (c.fixedLocusToDiagonalObj c') (CategoryTheory.Limits.pullback.diagonal (AlgebraicGeometry.toAffineSpace f (↑U) c'.v))

noncomputable def AlgebraicGeometry.EtaleCoordinates.graphPoint {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) (hc : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (c.v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) (hc' : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (c'.v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) : Spec (X.residueField p) ⟶ c.graph c'

The canonical point (p, p) : Spec κ(p) ⟶ W of the graph when all coordinates of both systems vanish at p (Kollár's "(p, p) ∈ U_2(p)", [Kol07, 95]): the lift of Spec κ(p) ⟶ U along both projections (the construction inside exists_graph_point, GraphPoint.lean).

Equations

• c.graphPoint c' hpU hc hc' = CategoryTheory.Limits.pullback.lift (AlgebraicGeometry.specResidueFieldToOpens hpU) (AlgebraicGeometry.specResidueFieldToOpens hpU) ⋯

@[simp]

theorem AlgebraicGeometry.EtaleCoordinates.graphPoint_graphFst {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) (hc : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (c.v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) (hc' : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (c'.v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) : CategoryTheory.CategoryStruct.comp (c.graphPoint c' hpU hc hc') (c.graphFst c') = specResidueFieldToOpens hpU

@[simp]

theorem AlgebraicGeometry.EtaleCoordinates.graphPoint_graphFst_assoc {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) (hc : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (c.v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) (hc' : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (c'.v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) {Z : Scheme} (h : ↑↑U ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.graphPoint c' hpU hc hc') (CategoryTheory.CategoryStruct.comp (c.graphFst c') h) = CategoryTheory.CategoryStruct.comp (specResidueFieldToOpens hpU) h

@[simp]

theorem AlgebraicGeometry.EtaleCoordinates.graphPoint_graphSnd {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) (hc : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (c.v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) (hc' : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (c'.v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) : CategoryTheory.CategoryStruct.comp (c.graphPoint c' hpU hc hc') (c.graphSnd c') = specResidueFieldToOpens hpU

@[simp]

theorem AlgebraicGeometry.EtaleCoordinates.graphPoint_graphSnd_assoc {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) (hc : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (c.v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) (hc' : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (c'.v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) {Z : Scheme} (h : ↑↑U ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.graphPoint c' hpU hc hc') (CategoryTheory.CategoryStruct.comp (c.graphSnd c') h) = CategoryTheory.CategoryStruct.comp (specResidueFieldToOpens hpU) h