Theorem 92 with an affine étale neighbourhood

Kollár ends the proof of Theorem 92 ([Kol07, 95]) by covering X with the images of finitely many of the neighbourhoods U(p): "We can take U to be their disjoint union." The proof in Hironaka/Resolution/Algebraic/MaximalContact/Theorem92.lean (etaleEquiv_of_isMCInvariant) takes U to be the coproduct over all closed points of the cosupport, a cover that may be infinite. The functoriality argument of [Kol07, Theorem 103, Step 2.3] applies a blow-up sequence functor to the pulled-back triples on U, and etaleEquivSeq_of_functor asks for U to carry the hypotheses it places on the base of a functor (the Lean form of the functoriality [Kol07, 34.1]): quasi-compact and separated over k, of finite type, equidimensional smooth. This file supplies them at once by making U affine:

• at each closed point p of the cosupport, the open V ∋ (p, p) on which (1′)–(4′) hold is shrunk to an affine open (exists_isAffineOpen_mem_and_subset), the four conditions restricting along the inclusion (conditions_restrict_of_le: comap_ι_eq_of_le and AgreeOn.restrict_of_le, with MC commuting with étale maps, [Kol07, Lemma 74 (4)]);
• finitely many of these affine opens have images covering the closed, hence compact, cosupport (exists_finset_subset_biUnion_range; X is quasi-compact over k);
• their disjoint union is the étale equivalence (etaleEquivOfFamily) and is affine (Mathlib: a finite coproduct of affine schemes is affine).

The result, exists_etaleEquiv_isAffine, is Theorem 92 with an affine U; the instances on U ↘ Spec k are derived from it in Hironaka/Resolution/Algebraic/MaximalContact/FunctorIndependence.lean.

theorem AlgebraicGeometry.Scheme.IdealSheafData.conditions_restrict_of_le {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [Smooth f] (I : X.IdealSheafData) (m : ℕ) (E : X.DivisorFamily) (H H' : X.IdealSheafData) {p : ↥X} (Q : EtaleNbhdPair X p) {V V₁ : Q.W.Opens} (hle : V ≤ V₁) (h1 : H.comap (CategoryTheory.CategoryStruct.comp V₁.ι Q.ψ) = H'.comap (CategoryTheory.CategoryStruct.comp V₁.ι Q.ψ')) (h2 : I.comap (CategoryTheory.CategoryStruct.comp V₁.ι Q.ψ) = I.comap (CategoryTheory.CategoryStruct.comp V₁.ι Q.ψ')) (h3 : ∀ (i : E.ι), (E.component i).comap (CategoryTheory.CategoryStruct.comp V₁.ι Q.ψ) = (E.component i).comap (CategoryTheory.CategoryStruct.comp V₁.ι Q.ψ')) (h4 : AgreeOn (CategoryTheory.CategoryStruct.comp V₁.ι Q.ψ) (CategoryTheory.CategoryStruct.comp V₁.ι Q.ψ') (MC (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp V₁.ι Q.ψ) f) (I.comap (CategoryTheory.CategoryStruct.comp V₁.ι Q.ψ)) m)) : H.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) = H'.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ') ∧ I.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) = I.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ') ∧ (∀ (i : E.ι), (E.component i).comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) = (E.component i).comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ')) ∧ AgreeOn (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) (CategoryTheory.CategoryStruct.comp V.ι Q.ψ') (MC (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) f) (I.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ)) m)

The four conditions (1′)–(4′) of [Kol07, Definition 91] on an open V₁ of an étale neighbourhood pair restrict to every open V ⊆ V₁: (1′)–(3′) because comap composes, (4′) because V(MC(ψ^*I)) restricts to its trace (AgreeOn.restrict_of_le) and MC commutes with the étale maps V.ι ≫ ψ ([Kol07, Lemma 74 (4)], MC_comap_of_etale).

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_etaleEquiv_isAffine {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] [QuasiCompact f] (I : X.IdealSheafData) {m : ℕ} (hm : 1 ≤ m) (hI : IsMCInvariant f I m) (E : X.DivisorFamily) (H H' : X.IdealSheafData) (hH : IsMaximalContact f I m H) (hH' : IsMaximalContact f I m H') (hHE : (E.append H).IsSnc) (hH'E : (E.append H').IsSnc) : ∃ (Q : EtaleEquiv f I m E H H'), IsAffine Q.U

Theorem 92 with an affine étale neighbourhood (Kollár's "we can take U to be their disjoint union", [Kol07, 95]): under the hypotheses of etaleEquiv_of_isMCInvariant with X quasi-compact over k, there is an étale equivalence of H and H' with respect to (X, I, E) whose scheme is affine, the disjoint union of finitely many affine opens of the graph neighbourhoods U(p).