Étale equivalent hypersurfaces give étale equivalent blow-up sequences

In [Kol07, Theorem 103, Step 2.3], for two hypersurfaces of maximal contact H, H' such that H + E and H' + E are simple normal crossing divisors, Theorem 92 makes (X, I, H + E) and (X, I, H' + E) étale equivalent, and Kollár concludes that the two blow-up sequences BD_{n,m,0}(X, I, H + E) and BD_{n,m,0}(X, I, H' + E) "are also étale equivalent". The introduction of [Kol07, §10] makes the same argument for an automorphism φ in place of the étale pair. This file proves that conclusion for an arbitrary functor, without deleting empty blow-ups:

Let B be a smooth blow-up sequence functor of order m (OrderSeqFunctor) that commutes with smooth morphisms in the sense of [Kol07, 34.1] (CommutesWithSmooth), and let Q = (U, ψ, ψ') be an étale equivalence of H and H' with respect to (X, I, E) (EtaleEquiv). Write T = (X, I, H + E), T' = (X, I, H' + E).

• By the second clause of [Kol07, 34.1], B(ψ^*T) = del(ψ^* B(T)) and B(ψ'^*T') = del(ψ'^* B(T')), where del deletes the empty blow-ups (eraseEmpty). No deletion occurs: B(T) has no empty centre (the output convention of the named functors, [Kol07, 32], OrderSeqAssignment.noEmptyCenters) and every centre of the order-m sequence B(T) lies over cosupp(I, m) ⊆ im ψ, so no centre of ψ^* B(T) is empty (noEmptyCenters_pullback_of_centersInRange) and eraseEmpty is the identity on it (eraseEmpty_eq_self_iff).
• The two pulled-back triples on U are equal: ψ^*I = ψ'^*I is (2′), and ψ^{-1}(H + E) = ψ'^{-1}(H' + E) componentwise is (1′) with (3′) (DivisorFamily.comap_append_eq); the k-structure of U is the one of the ambient Over instance on both sides (Triple.pullback_eq_pullback). Hence B(ψ^*T) = B(ψ'^*T') (OrderSeqAssignment.seq_congr).
• Therefore ψ^* B(T) = ψ'^* B(T'), which is condition (3) of [Kol07, Definition 96] for the two outputs; conditions (1) and (2) are (2′) and (4′) of Q, and the covering conditions and ψ ≫ f = ψ' ≫ f are Q's: B(T) and B(T') are étale equivalent through the same (U, ψ, ψ') (etaleEquivSeq_of_functor).

theorem Hironaka.OrderSeqAssignment.seq_congr {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) {T₁ T₂ : AlgebraicGeometry.Triple k} (h : T₁ = T₂) (h₁ : Dom T₁) (h₂ : Dom T₂) : B.seq T₁ h₁ ≍ B.seq T₂ h₂

The value of a blow-up sequence functor depends only on the triple, not on the proof of class membership; stated as a HEq because the ambient schemes of the two triples are equal only propositionally.

theorem AlgebraicGeometry.Triple.pullback_eq_pullback {k : Type u} [Field k] [PerfectField k] (T T' : Triple k) {Y : Scheme} [Y.Over (Spec ↧k)] [QuasiCompact (Y ↘ Spec ↧k)] [IsSeparated (Y ↘ Spec ↧k)] (hY : ∃ (n : ℕ), SmoothOfRelativeDimension n (Y ↘ Spec ↧k)) (ψ : Y ⟶ T.X.left) (ψ' : Y ⟶ T'.X.left) [Smooth ψ] [Smooth ψ'] (hI : T.I.comap ψ = T'.I.comap ψ') (hE : T.E.comap ψ = T'.E.comap ψ') : T.pullback hY ψ = T'.pullback hY ψ'

Two pull-backs of triples along maps from the same Y (with Y's given k-structure) are equal when the pulled-back ideals and divisor families agree.

theorem AlgebraicGeometry.Scheme.DivisorFamily.comap_append_eq {X U : Scheme} (E : X.DivisorFamily) (H H' : X.IdealSheafData) (ψ ψ' : U ⟶ X) (h1 : H.comap ψ = H'.comap ψ') (h3 : ∀ (i : E.ι), (E.component i).comap ψ = (E.component i).comap ψ') : (E.append H).comap ψ = (E.append H').comap ψ'

The conditions (1′) and (3′) of [Kol07, Definition 91] read on the family H + E: ψ^{-1}(H + E) = ψ'^{-1}(H' + E) when ψ^{-1}H = ψ'^{-1}H' and ψ^{-1}E^i = ψ'^{-1}E^i for every component; H + E is E.append H, with H the last member.

theorem AlgebraicGeometry.Scheme.IdealSheafData.etaleEquivSeq_of_functor {k : Type u} [Field k] [CharZero k] {m : ℕ} {Dom : Triple k → Prop} (B : Hironaka.OrderSeqAssignment k m Dom) (hB : B.CommutesWithSmooth) (T : Triple k) (hT : Dom T) (E : T.X.left.DivisorFamily) (H H' : T.X.left.IdealSheafData) (hE : T.E = E.append H) (hsnc' : (E.append H').IsSnc) (hT' : Dom { X := T.X, smoothOfRelativeDimension := ⋯, I := T.I, isNonzeroEverywhere := ⋯, E := E.append H', isSnc := hsnc' }) (Q : EtaleEquiv (T.X.left ↘ Spec ↧k) T.I m E H H') [Q.U.Over (Spec ↧k)] [Hom.IsOver Q.ψ (Spec ↧k)] [QuasiCompact (Q.U ↘ Spec ↧k)] [IsSeparated (Q.U ↘ Spec ↧k)] (hU : ∃ (n : ℕ), SmoothOfRelativeDimension n (Q.U ↘ Spec ↧k)) (hDU : Dom (T.pullback hU Q.ψ)) (hDU' : Dom ({ X := T.X, smoothOfRelativeDimension := ⋯, I := T.I, isNonzeroEverywhere := ⋯, E := E.append H', isSnc := hsnc' }.pullback hU Q.ψ')) : Nonempty (EtaleEquivSeq (T.X.left ↘ Spec ↧k) T.I m (B.seq T hT) (B.seq { X := T.X, smoothOfRelativeDimension := ⋯, I := T.I, isNonzeroEverywhere := ⋯, E := E.append H', isSnc := hsnc' } hT'))

Kollár's conclusion in [Kol07, Theorem 103, Step 2.3] that the two blow-up sequences BD_{n,m,0}(X, I, H + E) and BD_{n,m,0}(X, I, H' + E) are étale equivalent, for an arbitrary functor: for a smooth blow-up sequence functor B of order m commuting with smooth morphisms (CommutesWithSmooth), a triple T = (X, I, H + E) of its class, the triple T' = (X, I, H' + E) (H' + E simple normal crossing, also in the class), and an étale equivalence Q = (U, ψ, ψ') of H and H' with respect to (X, I, E) whose U carries the hypotheses of [Kol07, 34.1] and whose pulled-back triples ψ^*T, ψ'^*T' lie in the class, B(T) and B(T') are étale equivalent blow-up sequences through (U, ψ, ψ'): ψ^* B(T) = B(ψ^*T) = B(ψ'^*T') = ψ'^* B(T'), by [Kol07, 34.1] without deletion (OrderSeqAssignment.noEmptyCenters and the centres lying over the cosupport) and the equality of the pulled-back triples from (1′)–(3′).