The inductive step of Theorem 97: the defects, and the pieces of the one-step descent

In the proof of [Kol07, Theorem 97], Kollár picks local coordinates x_1, …, x_n on X_i = X'_i with Z_i = Z'_i = (x_1 = ⋯ = x_k = 0) and writes, by induction, ψ'^*_i(x_j) = ψ^*_i(x_j) − b(i, j) with b(i, j) ∈ (Π^U_i)^{-1}_*(MC(I^U), 1). This file defines the defects b(i, j) and proves the ingredients of the one-step descent of agreement through a blow-up, which is assembled in Hironaka/Resolution/Algebraic/MaximalContact/AgreeOnBlowUpKernel.lean. Everything here is stated for arbitrary schemes and arbitrary morphisms; flatness enters only the descent of the centres (eq_of_comap_eq_of_agreeOn_of_le).

• defect ψ ψ' V a: the defect ψ^* a − ψ'^* a of a section a ∈ Γ(X, V) under two maps ψ, ψ' : U ⟶ X, a section over ψ^{-1} V ⊓ ψ'^{-1} V (the open on which both pull-backs are defined; Kollár's b(i, j) for a = x_j); germ_defect_mem: at the points of V(M) the defects lie in the stalks of M when ψ, ψ' agree on V(M), the stalkwise content of "ψ_i and ψ'_i agree on V(M_i)" (AgreeOn).
• eq_of_comap_eq_of_agreeOn_of_le: Z_i = ψ_i(Z^U_i) = ψ'_i(Z^U_i) = Z'_i by descent of closed subschemes along flat maps agreeing on the common preimage, the agreement on the common pulled-back centre coming from M ≤ Z^U by AgreeOn.mono.
• comap_blowUpπ_le_markedTransform_one, support_markedTransform_one_subset: π^* M ≤ π^{-1}_*(M, 1) and V(π^{-1}_*(M, 1)) ⊆ π^{-1} V(M), formal properties of the colon.
• AgreeOn.comp_left, agreeOn_blowUpMap_comp_π: agreement pulls back along any morphism, and the lifts to the blow-ups, composed with the projection of the target blow-up, agree on V(π^{-1}_*(M, 1)): Kollár's "clear if y_j = x_j", for every function of the base.
• exceptionalDivisor_mul_markedTransform_one: 𝒪(F) · π^{-1}_*(M, 1) = π^* M for M ≤ J, the formula (60.1) of [Kol07, Definition 60] at mark 1: the division of the defects by the exceptional equation.
• isUnit_one_sub_of_mem_stalkIdeal, ratio_identity: the unit 1 − d at a point of the support (the step that shows the two lifts land in a common chart) and Kollár's displayed quotient after cancelling the nonzerodivisor e.
• sub_mem_of_forall_mem_closure, agreeOn_iff_forall_gen: the equalizer ideal of two ring homomorphisms is generated by the defects of ring generators; for morphisms from an affine scheme into Spec B, agreement on V(M) is the membership of the generators' defects in M.

The defects

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.defect {U X : Scheme} (ψ ψ' : U ⟶ X) (V : X.Opens) (a : ↑(X.presheaf.obj (Opposite.op V))) : ↑(U.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map ψ.base).obj V ⊓ (TopologicalSpace.Opens.map ψ'.base).obj V)))

Kollár's "ψ'^*_i(x_j) = ψ^*_i(x_j) − b(i, j)" (the proof of [Kol07, Theorem 97]): the defect ψ^* a − ψ'^* a of a section a ∈ Γ(X, V) under the two maps ψ, ψ' : U ⟶ X, a section of 𝒪_U over ψ^{-1} V ⊓ ψ'^{-1} V.

Equations

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

theorem AlgebraicGeometry.Scheme.IdealSheafData.defect_eq {U X : Scheme} (ψ ψ' : U ⟶ X) (V : X.Opens) (a : ↑(X.presheaf.obj (Opposite.op V))) : defect ψ ψ' V a = (CategoryTheory.ConcreteCategory.hom (U.presheaf.map (CategoryTheory.homOfLE ⋯).op)) ((CategoryTheory.ConcreteCategory.hom (Hom.app ψ V)) a) - (CategoryTheory.ConcreteCategory.hom (U.presheaf.map (CategoryTheory.homOfLE ⋯).op)) ((CategoryTheory.ConcreteCategory.hom (Hom.app ψ' V)) a)

The defect unfolded.

theorem AlgebraicGeometry.Scheme.IdealSheafData.germ_defect_mem {U X : Scheme} (ψ ψ' : U ⟶ X) (M : U.IdealSheafData) (h : AgreeOn ψ ψ' M) (V : X.Opens) (a : ↑(X.presheaf.obj (Opposite.op V))) {w : ↥U} (hw : w ∈ M.support) (hw' : w ∈ (TopologicalSpace.Opens.map ψ.base).obj V ⊓ (TopologicalSpace.Opens.map ψ'.base).obj V) : (CategoryTheory.ConcreteCategory.hom (U.presheaf.germ ((TopologicalSpace.Opens.map ψ.base).obj V ⊓ (TopologicalSpace.Opens.map ψ'.base).obj V) w hw')) (defect ψ ψ' V a) ∈ M.stalkIdeal w

Kollár's "b(i, j) ∈ (Π^U_i)^{-1}_*(MC(I^U), 1)": at a point w ∈ V(M) in the common domain, the germ of the defect ψ^* a − ψ'^* a lies in the stalk M_w, when ψ, ψ' agree on V(M); the restrictions to the common open do not change the germs, and germ_app_sub_germ_app_mem_stalkIdeal applies.

Equality of the centres by descent

theorem AlgebraicGeometry.Scheme.IdealSheafData.eq_of_comap_eq_of_agreeOn_of_le {U X : Scheme} (ψ ψ' : U ⟶ X) [Flat ψ] [Flat ψ'] (Z Z' : X.IdealSheafData) (M : U.IdealSheafData) (hZ : Z.comap ψ = Z'.comap ψ') (hsup : ↑Z.support ⊆ Set.range ⇑ψ) (hsup' : ↑Z'.support ⊆ Set.range ⇑ψ') (hM : M ≤ Z.comap ψ) (hfg : AgreeOn ψ ψ' M) : Z = Z'

Kollár's "Z_i = ψ_i(Z^U_i) = ψ'_i(Z^U_i) = Z'_i" (the proof of [Kol07, Theorem 97]): for flat ψ, ψ' : U ⟶ X, centres Z, Z' with equal inverse images, supports in the images of ψ, ψ', and an ideal sheaf M ≤ ψ^{-1} Z on which ψ, ψ' agree, Z = Z'; this is the descent eq_of_comap_eq_of_agreeOn of closed subschemes along flat maps, the agreement on the common pulled-back centre V(ψ^{-1} Z) inherited from V(M) by AgreeOn.mono.

The marked transform contains the pull-back

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_blowUpπ_le_markedTransform_one {U : Scheme} (J M : U.IdealSheafData) : M.comap J.blowUpπ ≤ M.markedTransform J 1

π^* M ≤ π^{-1}_*(M, 1): the marked transform is the colon (π^* M : 𝒪(F)) (markedTransform_eq_colon), which contains π^* M.

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_markedTransform_one_subset {U : Scheme} (J M : U.IdealSheafData) : ↑(M.markedTransform J 1).support ⊆ ⇑J.blowUpπ ⁻¹' ↑M.support

V(π^{-1}_*(M, 1)) ⊆ π^{-1}(V(M)), so the base maps agree at π(u) for every u ∈ V(M'): supports are antitone and V(π^* M) = π^{-1} V(M) (Mathlib's support_comap).

The defects of the base functions

theorem AlgebraicGeometry.Scheme.IdealSheafData.AgreeOn.comp_left {U X T : Scheme} (π : T ⟶ U) {f g : U ⟶ X} {M : U.IdealSheafData} (hfg : AgreeOn f g M) : AgreeOn (CategoryTheory.CategoryStruct.comp π f) (CategoryTheory.CategoryStruct.comp π g) (M.comap π)

Kollár's "this is clear if y_j = x_j", for every function of the base: agreement on V(M) pulls back along any π : T ⟶ U to agreement on V(π^* M); the closed immersion of V(π^* M) composed with π factors through the closed immersion of V(M) (Mathlib's subschemeMap).

theorem AlgebraicGeometry.Scheme.IdealSheafData.agreeOn_blowUpMap_comp_π {U X : Scheme} (f g : U ⟶ X) (C : X.IdealSheafData) (M : U.IdealSheafData) (hJ : C.comap f = C.comap g) (hfg : AgreeOn f g M) : AgreeOn (CategoryTheory.CategoryStruct.comp (Hom.blowUpMap f C) C.blowUpπ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (Hom.blowUpMap g C)) C.blowUpπ) (M.markedTransform (C.comap f) 1)

The lifts composed with the blow-up projection π_X : B_C X ⟶ X agree on V(π^{-1}_*(M, 1)): f̃ ≫ π_X = π ≫ f and g̃ ≫ π_X = π ≫ g (blowUpMap_π, with the transport AlgebraicGeometry.eqToHom_comp_blowUpπ), agreement on V(M) pulls back to V(π^* M) (AgreeOn.comp_left), and π^* M ≤ M' (AgreeOn.mono).

Division by the exceptional equation

theorem AlgebraicGeometry.Scheme.IdealSheafData.exceptionalDivisor_mul_markedTransform_one {U : Scheme} {J M : U.IdealSheafData} (hM : M ≤ J) : J.exceptionalDivisor * M.markedTransform J 1 = M.comap J.blowUpπ

Kollár's "the b(i, j) vanish along Z^U_i and so (π^U_i)^* b(i, j) = ψ^*_{i+1}(x_r) b(i+1, j)" (the formula (60.1) of [Kol07, Definition 60] at mark 1): for M ≤ J, 𝒪(F) · π^{-1}_*(M, 1) = π^* M on B_J U, because π^* M ≤ π^* J = 𝒪(F) and 𝒪(F) is invertible, so 𝒪(F) ∣ π^* M and pow_mul_markedTransform applies.

The common chart and the ratio identity

theorem AlgebraicGeometry.Scheme.IdealSheafData.isUnit_one_sub_of_mem_stalkIdeal {U : Scheme} (M : U.IdealSheafData) {w : ↥U} (hw : w ∈ M.support) {d : ↑(U.presheaf.stalk w)} (hd : d ∈ M.stalkIdeal w) : IsUnit (1 - d)

At a point w ∈ V(M), 1 − d is a unit of the stalk for every d ∈ M_w: the stalk of M at a point of its support lies in the maximal ideal (mem_support_iff_stalkIdeal_le_maximalIdeal). This is what puts the two lifts into a common chart of the blow-up.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ratio_identity {R : Type u_1} [CommRing R] {e a a' x d dj : R} (he : e ∈ nonZeroDivisors R) (h1 : e * a = x) (h2 : e * ((1 - d) * a') = x - e * dj) : (1 - d) * (a - a') = dj - d * a

Kollár's displayed identity ψ^*_{i+1}(y_j) − ψ'^*_{i+1}(y_j) = (b(i+1, j) − b(i+1, r) ψ^*_{i+1}(y_j)) / (1 − b(i+1, r)), after cancelling the nonzerodivisor: in a commutative ring, if e is a nonzerodivisor, e · a = x and e · ((1 − d) · a') = x − e · dj, then (1 − d) · (a − a') = dj − d · a.

Generation of the equalizer ideal by the defects of generators

theorem AlgebraicGeometry.Scheme.IdealSheafData.sub_mem_of_forall_mem_closure {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ φ' : R →+* S) (N : Ideal S) {T : Set R} (hT : Subring.closure T = ⊤) (h : ∀ s ∈ T, φ s - φ' s ∈ N) (r : R) : φ r - φ' r ∈ N

For ring homomorphisms φ, φ' : R → S and an ideal N of S, if the defects φ s − φ' s of the elements of a set T generating R as a ring lie in N, so does every defect φ r − φ' r: induction over Subring.closure, the product case being φ(r₁ r₂) − φ'(r₁ r₂) = φ r₁ (φ r₂ − φ' r₂) + φ' r₂ (φ r₁ − φ' r₁).

theorem AlgebraicGeometry.Scheme.IdealSheafData.agreeOn_iff_forall_gen {W : Scheme} [IsAffine W] {B : CommRingCat} (a a' : W ⟶ Spec B) (M : W.IdealSheafData) {T : Set ↑B} (hT : Subring.closure T = ⊤) : AgreeOn a a' M ↔ ∀ s ∈ T, (CategoryTheory.ConcreteCategory.hom (Hom.appTop a)) ((CategoryTheory.ConcreteCategory.hom (ΓSpecIso B).inv) s) - (CategoryTheory.ConcreteCategory.hom (Hom.appTop a')) ((CategoryTheory.ConcreteCategory.hom (ΓSpecIso B).inv) s) ∈ M.ideal ⟨⊤, ⋯⟩

The scheme form on an affine source: two morphisms a, a' from an affine scheme W to Spec B agree on V(M) iff the defects of the elements of a set T generating B as a ring lie in M(W). Indeed M(W) is the kernel of the closed immersion of V(M) on global sections (Mathlib's ker_subschemeι_app), morphisms into the affine Spec B are determined by their maps on global sections (ext_of_isAffine), and the ring-level generation lemma finishes.