Étale pairs in the image form and their disjoint unions

Kollár's étale equivalence of two hypersurfaces of maximal contact takes "étale surjections ψ, ψ' : U ⇉ X" [Kol07, Definition 91]. Here surjectivity is replaced by the image form: the images of ψ and ψ' each contain the relevant closed set (the cosupport of the marked ideal), because surjective pairs need not exist. Kollár's construction ends with "The images of finitely many of the U(p) cover X. We can take U to be their disjoint union" ([Kol07, 95], the proof of Theorem 92).

• EtaleImagePair X S: étale ψ, ψ' : U ⟶ X whose images both contain S, the pair of [Kol07, Definition 91] in the image form. The étale equivalence of Hironaka/Resolution/Algebraic/MaximalContact/EtaleEquiv.lean adds the conditions (91.1′)–(91.4′) to this pair.
• EtaleImagePair.sigma: the disjoint union ∐ W_i of a finite family of pairs with ψ := Sigma.desc ψ_i, ψ' := Sigma.desc ψ'_i, étale because étaleness is local at the source (IsZariskiLocalAtSource.sigmaDesc), covering because each ψ_i factors through ψ.

instance AlgebraicGeometry.instIsZariskiLocalAtSourceEtale : IsZariskiLocalAtSource @Etale

Étaleness is Zariski-local at the source (Mathlib's HasRingHomProperty.instIsZariskiLocalAtSource for RingHom.Etale); instance search does not find this instance by itself, so it is registered here.

theorem AlgebraicGeometry.subset_range_sigmaDesc_of_subset_iUnion {X : Scheme} {ι : Type u} (W : ι → Scheme) (g : (i : ι) → W i ⟶ X) {S : Set ↥X} (h : S ⊆ ⋃ (i : ι), Set.range ⇑(g i)) : S ⊆ Set.range ⇑(CategoryTheory.Limits.Sigma.desc g)

The image of the coproduct map ∐ g_i : ∐ W_i ⟶ X contains every set covered by the images of the g_i.

structure AlgebraicGeometry.EtaleImagePair (X : Scheme) (S : Set ↥X) : Type (u + 1)

A pair of étale morphisms ψ, ψ' : U ⟶ X whose images both contain the set S (in the application, the cosupport of a marked ideal): the "étale surjections ψ, ψ' : U ⇉ X" of [Kol07, Definition 91], in the image form.

• U : Scheme

  The étale neighbourhood.

• ψ : self.U ⟶ X

  The first étale map.

• ψ' : self.U ⟶ X

  The second étale map.

• etale_ψ : Etale self.ψ
• etale_ψ' : Etale self.ψ'
• covers : S ⊆ Set.range ⇑self.ψ

  The image of ψ contains S (the replacement for surjectivity).

• covers' : S ⊆ Set.range ⇑self.ψ'

  The image of ψ' contains S.

noncomputable def AlgebraicGeometry.EtaleImagePair.sigma {X : Scheme} {S : Set ↥X} {ι : Type u} (W : ι → Scheme) (ψ ψ' : (i : ι) → W i ⟶ X) [∀ (i : ι), Etale (ψ i)] [∀ (i : ι), Etale (ψ' i)] (h : S ⊆ ⋃ (i : ι), Set.range ⇑(ψ i)) (h' : S ⊆ ⋃ (i : ι), Set.range ⇑(ψ' i)) : EtaleImagePair X S

The disjoint union of a family of étale pairs ψ_i, ψ'_i : W_i ⟶ X whose images cover S, with ψ := ∐ ψ_i, ψ' := ∐ ψ'_i ("we can take U to be their disjoint union", [Kol07, 95]).

Equations

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

theorem AlgebraicGeometry.EtaleImagePair.sigma_ψ {X : Scheme} {S : Set ↥X} {ι : Type u} (W : ι → Scheme) (ψ ψ' : (i : ι) → W i ⟶ X) [∀ (i : ι), Etale (ψ i)] [∀ (i : ι), Etale (ψ' i)] (h : S ⊆ ⋃ (i : ι), Set.range ⇑(ψ i)) (h' : S ⊆ ⋃ (i : ι), Set.range ⇑(ψ' i)) : (sigma W ψ ψ' h h').ψ = CategoryTheory.Limits.Sigma.desc ψ ∧ (sigma W ψ ψ' h h').ψ' = CategoryTheory.Limits.Sigma.desc ψ'