The triple of Step 2.2 over a first sequence, and its pull-back

The functoriality of Step 2.2 of the proof of [Kol07, Theorem 103] is that of Lemma 102 ([Kol07, 104, Step 2.3]). The triple of Step 2.2 is built on the last stage of the first sequence (the sequence of Step 2.1), so it is defined over an arbitrary first sequence (step22TripleOf), the dependent types being handled as in BDOf.lean. For the pulled-back data over the pulled-back first sequence it is the pull-back of the triple of Step 2.2 along the lift to the last stage: the controlled transform, the exceptional divisors and the transform of H all pull back along the lift (ConcatPullback.lean).

• HypersurfaceFamily.append_comap, HypersurfaceFamily.empty_comap, BlowUpSequence.strictTransformSeq_last_pullbackLiftLast — the pieces of the boundary pull back.
• BO.transformHOf, BO.exceptionalOf, BO.step22TripleOf, BO.stepHClass_step22TripleOf_congr — the data of Step 2.2 over an arbitrary first sequence.
• BO.step22TripleOf_isPullbackOf — the triple of Step 2.2 of the pull-back.

Step 2.2 in the compatible-family form (Step22Fam.lean) is built on these data.

theorem Manifold.HypersurfaceFamily.append_comap {M N : Type u} (F : HypersurfaceFamily M) (H : Set M) (g : N → M) : comap g (F.append H) = (comap g F).append (g ⁻¹' H)

Appending a hypersurface commutes with the inverse image of a family.

theorem Manifold.HypersurfaceFamily.empty_comap {M N : Type u} (g : N → M) : comap g (empty M) = empty N

The inverse image of the empty family is the empty family.

theorem AnalyticManifold.BlowUpSequence.strictTransformSeq_last_pullbackLiftLast {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (H : Set M.carrier) : (L.pullback h hh).toSuccession.strictTransformSeq (⇑h ⁻¹' H) (Fin.last (L.pullback h hh).toSuccession.length) = ⇑(L.pullbackLiftLast h hh) ⁻¹' L.toSuccession.strictTransformSeq H (Fin.last L.toSuccession.length)

The strict transform of h⁻¹(H) at the last stage of h^* L is the preimage under the lift h_r of the strict transform of H at the last stage of L.

The data of Step 2.2 parametrized by the first sequence

def Hironaka.Manifold.BO.transformHOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : AnalyticManifold.BlowUpSequence ψ₀ M) (H : Set M.carrier) : Set (L.stage (Fin.last L.length)).carrier

The birational transform H_r of H at the last stage of an arbitrary first sequence L.

Equations

• Hironaka.Manifold.BO.transformHOf L H = L.toSuccession.strictTransformSeq H (Fin.last L.toSuccession.length)

noncomputable def Hironaka.Manifold.BO.exceptionalOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : AnalyticManifold.BlowUpSequence ψ₀ M) : Manifold.HypersurfaceFamily (L.stage (Fin.last L.length)).carrier

The family of exceptional divisors at the last stage of an arbitrary first sequence L (from the empty start).

Equations

• Hironaka.Manifold.BO.exceptionalOf L = L.toSuccession.totalTransformSeq (Fin.last L.toSuccession.length)

noncomputable def Hironaka.Manifold.BO.step22TripleOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (T : Manifold.AnalyticTriple ψ₀ M) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) {H : Set M.carrier} (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) : Manifold.AnalyticTriple ψ₀ (L.stage (Fin.last L.length))

The triple (X_r, I_r, E_r^{exc} + H_r) of Step 2.2 over an arbitrary first sequence L (the normal-crossings proof as a hypothesis).

Equations

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

theorem Hironaka.Manifold.BO.stepHClass_step22TripleOf_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (T : Manifold.AnalyticTriple ψ₀ M) {H : Set M.carrier} {L₁ L₂ : AnalyticManifold.BlowUpSequence ψ₀ M} (e : L₁ = L₂) (hL₁ : L₁.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hL₂ : L₂.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hsnc₁ : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L₁).append (transformHOf L₁ H))) (hsnc₂ : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L₂).append (transformHOf L₂ H))) (hcls : stepHClass s (step22TripleOf T L₁ hL₁ hsnc₁)) : stepHClass s (step22TripleOf T L₂ hL₂ hsnc₂)

The class of Step 2.2 for the parametrized triple depends only on the first sequence.

theorem Hironaka.Manifold.BO.step22TripleOf_isPullbackOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (T : Manifold.AnalyticTriple ψ₀ M) {H : Set M.carrier} {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hL' : (L.pullback h hh).toSuccession.IsOfOrderGe (T.pullback h hh).I s (T.pullback h hh).F.idealSheaf) (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf (L.pullback h hh)).append (transformHOf (L.pullback h hh) (⇑h ⁻¹' H)))) : (step22TripleOf (T.pullback h hh) (L.pullback h hh) hL' hsnc').IsPullbackOf (step22TripleOf T L hL hsnc) (L.pullbackLiftLast h hh)

The triple of Step 2.2 for the pulled-back data over the pulled-back first sequence is the pull-back of the triple of Step 2.2 along the lift h_r to the last stage ([Kol07, 104, Step 2.3]): the controlled transform, the exceptional divisors and the transform of H pull back along the lift.