The disjoint union of the étale neighbourhoods

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." Given, for every closed point p of the cosupport cosupp(I, m) = {x | m ≤ ord_x I}, an étale neighbourhood pair ψₚ, ψₚ' : Wₚ ⇉ X over k and an open Vₚ ∋ qₚ on which (1′)–(4′) hold (Hironaka/Resolution/Algebraic/MaximalContact/EtaleNbhdConditions.lean), the disjoint union U := ∐ Vₚ with ψ := ∐ ψₚ|_{Vₚ} and ψ' := ∐ ψₚ'|_{Vₚ} is an étale equivalence of H and H' with respect to (X, I, E) (EtaleEquiv):

• the images cover the cosupport (subset_iUnion_range_ι_comp_ψ): étale maps are open and every point of the closed cosupport specializes to a closed point;
• the coproduct maps are étale and the pair is EtaleImagePair.sigma;
• (1′)–(3′) descend from the summands because an ideal sheaf on a coproduct is determined by its restrictions to the summands (ext_of_openCover with sigmaOpenCover), and MC commutes with the étale ψ and with the open immersions Sigma.ι ([Kol07, Lemma 74 (4)], MC_comap_of_etale);
• (4′) descends because the closed subscheme V(MC(ψ^*I)) of the coproduct is covered by its traces on the summands (AlgebraicGeometry.isPullback_subschemeι_comap, Scheme.Cover.hom_ext).

Finiteness of the cover (Kollár's varieties are quasi-compact) plays no part here: the coproduct is taken over all closed points of the cosupport, an index type in Type u. The finite, affine form is Hironaka/Resolution/Algebraic/MaximalContact/EtaleEquivAffine.lean.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.etaleEquivOfFamily {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [Smooth f] (I : X.IdealSheafData) (m : ℕ) (E : X.DivisorFamily) (H H' : X.IdealSheafData) {ι : Type u} (W : ι → Scheme) (ψ ψ' : (i : ι) → W i ⟶ X) [∀ (i : ι), Etale (ψ i)] [∀ (i : ι), Etale (ψ' i)] (hcov : {x : ↥X | ↑m ≤ I.ord x} ⊆ ⋃ (i : ι), Set.range ⇑(ψ i)) (hcov' : {x : ↥X | ↑m ≤ I.ord x} ⊆ ⋃ (i : ι), Set.range ⇑(ψ' i)) (hf : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (ψ i) f = CategoryTheory.CategoryStruct.comp (ψ' i) f) (h1 : ∀ (i : ι), H.comap (ψ i) = H'.comap (ψ' i)) (h2 : ∀ (i : ι), I.comap (ψ i) = I.comap (ψ' i)) (h3 : ∀ (i : ι) (j : E.ι), (E.component j).comap (ψ i) = (E.component j).comap (ψ' i)) (h4 : ∀ (i : ι), AgreeOn (ψ i) (ψ' i) (MC (CategoryTheory.CategoryStruct.comp (ψ i) f) (I.comap (ψ i)) m)) : EtaleEquiv f I m E H H'

Kollár's "we can take U to be their disjoint union" ([Kol07, 95]), as a construction: a family of étale pairs ψᵢ, ψᵢ' : Wᵢ ⇉ X over k whose images each cover the cosupport cosupp(I, m) and which satisfy (1′)–(4′) summand by summand assembles to the étale equivalence ∐ ψᵢ, ∐ ψᵢ' : ∐ Wᵢ ⇉ X of H and H' with respect to (X, I, E) on the coproduct ∐ Wᵢ (etaleEquivOfFamily_U). The construction is needed, rather than the mere existence nonempty_etaleEquiv_of_family, where the scheme of the equivalence matters (its affineness in Hironaka/Resolution/Algebraic/MaximalContact/EtaleEquivAffine.lean).

Equations

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

theorem AlgebraicGeometry.Scheme.IdealSheafData.etaleEquivOfFamily_U {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [Smooth f] (I : X.IdealSheafData) (m : ℕ) (E : X.DivisorFamily) (H H' : X.IdealSheafData) {ι : Type u} (W : ι → Scheme) (ψ ψ' : (i : ι) → W i ⟶ X) [∀ (i : ι), Etale (ψ i)] [∀ (i : ι), Etale (ψ' i)] (hcov : {x : ↥X | ↑m ≤ I.ord x} ⊆ ⋃ (i : ι), Set.range ⇑(ψ i)) (hcov' : {x : ↥X | ↑m ≤ I.ord x} ⊆ ⋃ (i : ι), Set.range ⇑(ψ' i)) (hf : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (ψ i) f = CategoryTheory.CategoryStruct.comp (ψ' i) f) (h1 : ∀ (i : ι), H.comap (ψ i) = H'.comap (ψ' i)) (h2 : ∀ (i : ι), I.comap (ψ i) = I.comap (ψ' i)) (h3 : ∀ (i : ι) (j : E.ι), (E.component j).comap (ψ i) = (E.component j).comap (ψ' i)) (h4 : ∀ (i : ι), AgreeOn (ψ i) (ψ' i) (MC (CategoryTheory.CategoryStruct.comp (ψ i) f) (I.comap (ψ i)) m)) : (etaleEquivOfFamily f I m E H H' W ψ ψ' hcov hcov' hf h1 h2 h3 h4).U = ∐ W

The scheme of etaleEquivOfFamily is the coproduct ∐ Wᵢ (definitional).

theorem AlgebraicGeometry.Scheme.IdealSheafData.nonempty_etaleEquiv_of_family {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [Smooth f] (I : X.IdealSheafData) (m : ℕ) (E : X.DivisorFamily) (H H' : X.IdealSheafData) {ι : Type u} (W : ι → Scheme) (ψ ψ' : (i : ι) → W i ⟶ X) [∀ (i : ι), Etale (ψ i)] [∀ (i : ι), Etale (ψ' i)] (hcov : {x : ↥X | ↑m ≤ I.ord x} ⊆ ⋃ (i : ι), Set.range ⇑(ψ i)) (hcov' : {x : ↥X | ↑m ≤ I.ord x} ⊆ ⋃ (i : ι), Set.range ⇑(ψ' i)) (hf : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (ψ i) f = CategoryTheory.CategoryStruct.comp (ψ' i) f) (h1 : ∀ (i : ι), H.comap (ψ i) = H'.comap (ψ' i)) (h2 : ∀ (i : ι), I.comap (ψ i) = I.comap (ψ' i)) (h3 : ∀ (i : ι) (j : E.ι), (E.component j).comap (ψ i) = (E.component j).comap (ψ' i)) (h4 : ∀ (i : ι), AgreeOn (ψ i) (ψ' i) (MC (CategoryTheory.CategoryStruct.comp (ψ i) f) (I.comap (ψ i)) m)) : Nonempty (EtaleEquiv f I m E H H')

A family of étale pairs ψᵢ, ψᵢ' : Wᵢ ⇉ X over k whose images each cover the cosupport cosupp(I, m) and which satisfy (1′)–(4′) summand by summand assembles to an étale equivalence ∐ ψᵢ, ∐ ψᵢ' : ∐ Wᵢ ⇉ X of H and H' with respect to (X, I, E) (etaleEquivOfFamily).

theorem AlgebraicGeometry.Scheme.IdealSheafData.nonempty_etaleEquiv_of_forall_isClosed {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (m : ℕ) (E : X.DivisorFamily) (H H' : X.IdealSheafData) (Q : (p : { p : ↥X // IsClosed {p} ∧ p ∈ {x : ↥X | ↑m ≤ I.ord x} }) → EtaleNbhdPair X ↑p) (V : (p : { p : ↥X // IsClosed {p} ∧ p ∈ {x : ↥X | ↑m ≤ I.ord x} }) → (Q p).W.Opens) (hV : ∀ (p : { p : ↥X // IsClosed {p} ∧ p ∈ {x : ↥X | ↑m ≤ I.ord x} }), (Q p).q ∈ V p) (hf : ∀ (p : { p : ↥X // IsClosed {p} ∧ p ∈ {x : ↥X | ↑m ≤ I.ord x} }), CategoryTheory.CategoryStruct.comp (Q p).ψ f = CategoryTheory.CategoryStruct.comp (Q p).ψ' f) (h1 : ∀ (p : { p : ↥X // IsClosed {p} ∧ p ∈ {x : ↥X | ↑m ≤ I.ord x} }), H.comap (CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ) = H'.comap (CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ')) (h2 : ∀ (p : { p : ↥X // IsClosed {p} ∧ p ∈ {x : ↥X | ↑m ≤ I.ord x} }), I.comap (CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ) = I.comap (CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ')) (h3 : ∀ (p : { p : ↥X // IsClosed {p} ∧ p ∈ {x : ↥X | ↑m ≤ I.ord x} }) (i : E.ι), (E.component i).comap (CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ) = (E.component i).comap (CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ')) (h4 : ∀ (p : { p : ↥X // IsClosed {p} ∧ p ∈ {x : ↥X | ↑m ≤ I.ord x} }), AgreeOn (CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ) (CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ') (MC (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ) f) (I.comap (CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ)) m)) : Nonempty (EtaleEquiv f I m E H H')

Kollár's "We can take U to be their disjoint union" ([Kol07, 95]), over all closed points: given, for every closed point p of cosupp(I, m) = {x | m ≤ ord_x I}, an étale neighbourhood pair Qₚ of p over k and an open Vₚ ∋ qₚ on which (1′)–(4′) hold for the restricted maps, the disjoint union U := ∐ Vₚ with ψ := ∐ ψₚ|_{Vₚ} and ψ' := ∐ ψₚ'|_{Vₚ} is an étale equivalence of H and H' with respect to (X, I, E): both images contain the cosupport (which is closed), the coproduct maps are étale, and (1′)–(4′) descend from the summands (nonempty_etaleEquiv_of_family). The cover may be infinite.