Étale equivalence of blow-up sequences

[Kol07, Definition 96] calls two blow-up sequences B and B' of order m = max-ord I starting with (X, I), X a smooth variety over a field of characteristic zero, étale equivalent when there are étale surjections ψ, ψ' : U ⇉ X with (1) ψ^*(I) = ψ'^*(I), (2) ψ^*(h) − ψ'^*(h) ∈ MC ψ^*(I) for every function h on X, and (3) ψ^* B = ψ'^* B'.

Conventions. As for [Kol07, Definition 91] (Hironaka/Resolution/Algebraic/MaximalContact/EtaleEquiv.lean), the definition is stated for étale maps whose images each contain the cosupport cosupp(I, m) = {x | ord_x I ≥ m} (EtaleImagePair). Every centre of an order-m sequence lies over the cosupport, so the surjective form is recovered by adjoining X ∖ cosupp(I, m) with both maps the inclusion; the image form is what Theorem 92 and the functoriality argument of [Kol07, Theorem 103, Step 2.3] produce. Condition (2) is stated as the agreement of morphisms on the closed subscheme V(MC(ψ^*I)) (AgreeOn); condition (3) is an equality of terms of BlowUpSequence U, B.pullback ψ = B'.pullback ψ', for the pull-back of a blow-up sequence of [Kol07, 30.1]. Kollár's ψ, ψ' are morphisms of k-varieties: the field comp_eq (ψ ≫ f = ψ' ≫ f) records it, and it is what makes MC(ψ^*I) in (2) independent of which of the two maps induces the k-structure of U.

• EtaleEquivSeq f I m B B': the étale equivalence datum for two blow-up sequences, an EtaleImagePair X (cosupp I m) with (1)–(3) and ψ ≫ f = ψ' ≫ f. Kollár's standing hypothesis "B, B' are blow-up sequences of order m = max-ord I" is a hypothesis of the theorems that use the relation (Theorem 97), not a field.
• EtaleEquivSeq.refl: B is étale equivalent to itself through U = X, ψ = ψ' = 𝟙 X.

structure AlgebraicGeometry.Scheme.IdealSheafData.EtaleEquivSeq {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (I : X.IdealSheafData) (m : ℕ) (B B' : X.BlowUpSequence) extends AlgebraicGeometry.EtaleImagePair X {x : ↥X | ↑m ≤ I.ord x} : Type (u + 1)

[Kol07, Definition 96], with images containing the cosupport in place of surjections: the blow-up sequences B and B' on X are étale equivalent for (X, I) and the mark m through the étale pair ψ, ψ' : U ⟶ X whose images each contain cosupp(I, m) = {x | ord_x I ≥ m} (EtaleImagePair), when (1) ψ^*I = ψ'^*I, (2) ψ and ψ' agree on V(MC(ψ^*I)) (Kollár's "ψ^*(h) − ψ'^*(h) ∈ MC ψ^*(I) for every h", AgreeOn), and (3) ψ^*B = ψ'^*B' as terms of BlowUpSequence U (the pullback of [Kol07, 30.1]); ψ and ψ' are morphisms of k-schemes (ψ ≫ f = ψ' ≫ f, Kollár's varieties over k).

• U : Scheme
• ψ : self.U ⟶ X
• ψ' : self.U ⟶ X
• etale_ψ : Etale self.ψ
• etale_ψ' : Etale self.ψ'
• covers : {x : ↥X | ↑m ≤ I.ord x} ⊆ Set.range ⇑self.ψ
• covers' : {x : ↥X | ↑m ≤ I.ord x} ⊆ Set.range ⇑self.ψ'
• comp_eq : CategoryTheory.CategoryStruct.comp self.ψ f = CategoryTheory.CategoryStruct.comp self.ψ' f

  Kollár's ψ, ψ' : U ⇉ X are morphisms of varieties over k.

• h1 : I.comap self.ψ = I.comap self.ψ'

  (1) ψ^*(I) = ψ'^*(I).

• h2 : AgreeOn self.ψ self.ψ' (MC (CategoryTheory.CategoryStruct.comp self.ψ f) (I.comap self.ψ) m)

  (2) ψ^*(h) − ψ'^*(h) ∈ MC ψ^*(I) for every h ∈ 𝒪_X: ψ, ψ' agree on V(MC(ψ^*I)).

• h3 : B.pullback self.ψ = B'.pullback self.ψ'

  (3) ψ^* B = ψ'^* B'.

theorem AlgebraicGeometry.Scheme.IdealSheafData.EtaleEquivSeq.conditions {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {I : X.IdealSheafData} {m : ℕ} {B B' : X.BlowUpSequence} (Q : EtaleEquivSeq f I m B B') : I.comap Q.ψ = I.comap Q.ψ' ∧ AgreeOn Q.ψ Q.ψ' (MC (CategoryTheory.CategoryStruct.comp Q.ψ f) (I.comap Q.ψ) m) ∧ B.pullback Q.ψ = B'.pullback Q.ψ'

The three conditions (1)–(3) of [Kol07, Definition 96], bundled.

theorem AlgebraicGeometry.Scheme.IdealSheafData.EtaleEquivSeq.covers_covers' {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {I : X.IdealSheafData} {m : ℕ} {B B' : X.BlowUpSequence} (Q : EtaleEquivSeq f I m B B') : {x : ↥X | ↑m ≤ I.ord x} ⊆ Set.range ⇑Q.ψ ∧ {x : ↥X | ↑m ≤ I.ord x} ⊆ Set.range ⇑Q.ψ'

In place of Kollár's "étale surjections": the images of ψ and ψ' each contain the cosupport cosupp(I, m).

theorem AlgebraicGeometry.Scheme.IdealSheafData.EtaleEquivSeq.ψ_comp_eq {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {I : X.IdealSheafData} {m : ℕ} {B B' : X.BlowUpSequence} (Q : EtaleEquivSeq f I m B B') : CategoryTheory.CategoryStruct.comp Q.ψ f = CategoryTheory.CategoryStruct.comp Q.ψ' f

Kollár's ψ, ψ' : U ⇉ X are morphisms of varieties over k: the field comp_eq restated.

def AlgebraicGeometry.Scheme.IdealSheafData.EtaleEquivSeq.refl {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (I : X.IdealSheafData) (m : ℕ) (B : X.BlowUpSequence) : EtaleEquivSeq f I m B B

The trivial instance: B is étale equivalent to itself through U = X, ψ = ψ' = 𝟙 X (pullback_id).

Equations

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

theorem AlgebraicGeometry.Scheme.IdealSheafData.EtaleEquiv.isOver_ψ' {k : Type u} [Field k] {X : Scheme} [X.Over (Spec ↧k)] {I : X.IdealSheafData} {m : ℕ} {E : X.DivisorFamily} {H H' : X.IdealSheafData} (Q : EtaleEquiv (X ↘ Spec ↧k) I m E H H') [Q.U.Over (Spec ↧k)] [Hom.IsOver Q.ψ (Spec ↧k)] : Hom.IsOver Q.ψ' (Spec ↧k)

Kollár's ψ, ψ' : U ⇉ X are morphisms of k-varieties: when U is over Spec k and ψ is over Spec k, so is ψ', by comp_eq; the second map of an étale equivalence commutes with the structure morphisms.