The core on an open as a core over a transported sequence

The core on a relatively compact open U (BDan.coreFamOn, BDFam.lean) reads the input family at the trace of π_{-1}^{-1}(U) on S_0, pushes the value forward to the open π_{-1}^{-1}(U) and pulls it back along the corestricted lift liftIncl of the inclusion U ⊆ M. This module identifies it with a core over a sequence (coreOfListOf, BD.lean) on the restricted data, the manifold U, its centre Z_{-1} ∩ U, the transform of E^j ∩ U and the input's value transported to it (coreFamOn_eq_coreOfListOf): the push-forward to the open is the push-forward along the bundle diffeomorphism of the restricted hypersurface (BlowUpSequence.pushforwardRestrictOf_eq), and the push-forward commutes with pull-back along a local analytic isomorphism (BlowUpSequence.pushforward_pullback; the proof of [Kol07, Lemma 102]: pulling back and restricting commute). Kollár's S_0 and centre are here those of the restricted data, propositionally rather than definitionally, so the two clauses of the core over a sequence (BDCore.lean, BDCosupp.lean) are first restated over an arbitrary closed hypersurface Z and a closed hypersurface S' of its blowing-up equal to Z_{-1} and S_0 (coreOfListOf_isOfOrderGe, coreOfListOf_cosupp_disjoint).

The corestricted lift is surjective onto π_{-1}^{-1}(U) (surjective_liftIncl): the blowing-up of Z_{-1} restricted over U is a blowing-up of U along Z_{-1} ∩ U ([BM88, Definition 4.1]: a blowing-up is determined by its restrictions to charts; IsBlowUp.restrictOpens'), and a map over the identity between two blowings-up of the same centre is surjective (surjective_of_comm).

• piRestrict, isBlowUp_piRestrict, surjective_liftIncl;
• coreOfListOf_isOfOrderGe, coreOfListOf_cosupp_disjoint;
• bundleInvOf, isClosedSubmanifold_transformSUOf, liftInclSOf, transportedValueOf — the transport of the input's value from the trace of π^{-1}(U) on S' to the transform of E^j in the restricted blowing-up, along the inverse of the bundle diffeomorphism and the restriction of the corestricted lift, over an arbitrary centre Z and transform S'; bundleInv, isClosedSubmanifold_transformSU, liftInclS, transportedValue at Z_{-1} and S_0;
• coreFamOn_eq_coreOfListOf — the identification.

With it, the order clause and clause (1) of Lemma 102 for BDanFam reduce to the transport of the input family's clauses along two local analytic isomorphisms (BDFamOrder.lean), and the compatibility and commutation clauses to the behaviour of the core over a sequence under pull-back (BDFamPullback.lean, BDFamCompat.lean, BDFamComm.lean).

The corestricted lift is surjective

noncomputable def Hironaka.Manifold.BDan.piRestrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (U : TopologicalSpace.Opens M.carrier) : ((Manifold.blowUp ψ₀ ⋯).restrict (piOpen T s j U)).carrier → (M.restrict U).carrier

The blowing-up π_{-1} restricted over U, as a map π_{-1}^{-1}(U) → U.

Equations

• Hironaka.Manifold.BDan.piRestrict T s j U q = ⟨(Hironaka.Manifold.BDan.piMinusOne T s j) ↑q, ⋯⟩

theorem Hironaka.Manifold.BDan.isBlowUp_piRestrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (U : TopologicalSpace.Opens M.carrier) : Manifold.IsBlowUp ψ₀ (⇑(M.inclusion U) ⁻¹' BD.Zminus1 T.I s (T.F.hyp j)) 1 (piRestrict T s j U)

The blowing-up of Z_{-1} restricted over U is a blowing-up of U along Z_{-1} ∩ U ([BM88, Definition 4.1]: a blowing-up is characterised by its restrictions to charts).

theorem Hironaka.Manifold.BDan.surjective_liftIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (U : TopologicalSpace.Opens M.carrier) : Function.Surjective ⇑(liftIncl T s j U)

The corestricted lift liftIncl of the inclusion U ⊆ M is surjective onto π_{-1}^{-1}(U): it is a map over the identity of U between two blowings-up of U along Z_{-1} ∩ U, and such a map is surjective (surjective_of_comm; the pull-back of a blow-up sequence along an open embedding in [Kol07, Definition 30 (1)]).

The core over a sequence, with an arbitrary centre and transform

theorem Hironaka.Manifold.BDan.coreOfListOf_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) (hT : BDClass s T) (hZeq : Z = BD.Zminus1 T.I s (T.F.hyp j)) (hSeq : S' = transformSOf T j hZ) (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) hS'.toAnalyticManifold) (hLne : L.NoEmptyCenters) (hL : L.toSuccession.IsOfOrderGe (restrictedTripleOf T s j hZ hS' hT hZeq hSeq).I s (restrictedTripleOf T s j hZ hS' hT hZeq hSeq).F.idealSheaf) : (coreOfListOf hZ hS' L).toSuccession.IsOfOrderGe T.I s T.F.idealSheaf

The order clause coreOfListOf_isOfOrderGe_of_bridge over an arbitrary centre and transform equal to Z_{-1} and S_0.

theorem Hironaka.Manifold.BDan.coreOfListOf_cosupp_disjoint {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) (hT : BDClass s T) (hZeq : Z = BD.Zminus1 T.I s (T.F.hyp j)) (hSeq : S' = transformSOf T j hZ) (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) hS'.toAnalyticManifold) (hLne : L.NoEmptyCenters) (hL : L.toSuccession.IsOfOrderGe (restrictedTripleOf T s j hZ hS' hT hZeq hSeq).I s (restrictedTripleOf T s j hZ hS' hT hZeq hSeq).F.idealSheaf) (hlt : ∀ (y : ↑↧(L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier), Manifold.IdealSheaf.ord (L.toSuccession.markedTransformSeq (restrictedTripleOf T s j hZ hS' hT hZeq hSeq).I s (Fin.last L.toSuccession.length)) y < ↑s) : Disjoint {x : ↑↧((coreOfListOf hZ hS' L).toSuccession.stage (Fin.last (coreOfListOf hZ hS' L).toSuccession.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord ((coreOfListOf hZ hS' L).toSuccession.weakTransformSeq T.I (Fin.last (coreOfListOf hZ hS' L).toSuccession.length)) x} ((coreOfListOf hZ hS' L).toSuccession.strictTransformSeq (T.F.hyp j) (Fin.last (coreOfListOf hZ hS' L).toSuccession.length))

Clause (1) coreOfListOf_cosupp_disjoint_of_bridge over an arbitrary centre and transform equal to Z_{-1} and S_0.

The transport over an arbitrary centre and transform

noncomputable def Hironaka.Manifold.BDan.bundleInvOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) (U : TopologicalSpace.Opens M.carrier) : AnalyticMap ⋯.toAnalyticManifold (hS'.toAnalyticManifold.restrict (hS'.preimageOpens (piOpenOf hZ U)))

The inverse of the bundle diffeomorphism (bundleInv) over an arbitrary closed hypersurface Z and a closed hypersurface S' of its blowing-up.

Equations

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

theorem Hironaka.Manifold.BDan.isClosedSubmanifold_transformSUOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) (U : TopologicalSpace.Opens M.carrier) : Manifold.IsClosedSubmanifold ψ₀ (⇑(liftInclOf hZ U) ⁻¹' ⇑((Manifold.blowUp ψ₀ hZ).inclusion (piOpenOf hZ U)) ⁻¹' S') 1

The transform S' pulled back along the corestricted lift of the inclusion of U, over an arbitrary centre, is a closed hypersurface (isClosedSubmanifold_transformSU in general).

noncomputable def Hironaka.Manifold.BDan.liftInclSOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) (U : TopologicalSpace.Opens M.carrier) : AnalyticMap ⋯.toAnalyticManifold ⋯.toAnalyticManifold

The corestricted lift of the inclusion of U restricted to the transforms (liftInclS), over an arbitrary centre and transform.

Equations

• Hironaka.Manifold.BDan.liftInclSOf hZ hS' U = ⋯.restrictMap ⋯ ⇑(Hironaka.Manifold.BDan.liftInclOf hZ U) ⋯ ⋯

theorem Hironaka.Manifold.BDan.transformSUOf_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (j : T.F.ι) {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (U : TopologicalSpace.Opens M.carrier) (hSeq : S' = transformSOf T j hZ) : ⇑(liftInclOf hZ U) ⁻¹' ⇑((Manifold.blowUp ψ₀ hZ).inclusion (piOpenOf hZ U)) ⁻¹' S' = transformSOf (T.pullback (M.inclusion U) ⋯) j ⋯

The transform over the restriction to U is the transform of the restricted data (transformSU_eq over an arbitrary centre).

noncomputable def Hironaka.Manifold.BDan.transportedValueOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) (U : TopologicalSpace.Opens M.carrier) (inp : BMOanFam 𝕜 (n - 1) s) (hT : BDClass s T) (hZeq : Z = BD.Zminus1 T.I s (T.F.hyp j)) (hSeq : S' = transformSOf T j hZ) (hU : IsCompact (closure ↑U)) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) ⋯.toAnalyticManifold

The transported value of the input (transportedValue) over an arbitrary centre and transform.

Equations

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

The core on an open as a core over the transported sequence

noncomputable def Hironaka.Manifold.BDan.bundleInv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (U : TopologicalSpace.Opens M.carrier) : AnalyticMap ⋯.toAnalyticManifold (⋯.toAnalyticManifold.restrict (⋯.preimageOpens (piOpen T s j U)))

The inverse of the bundle diffeomorphism between the restriction of S_0 over π_{-1}^{-1}(U) and the open U_S of the hypersurface S_0 regarded as a manifold, as an analytic map from the former to the latter.

Equations

• Hironaka.Manifold.BDan.bundleInv T s j U = Hironaka.Manifold.BDan.bundleInvOf ⋯ ⋯ U

theorem Hironaka.Manifold.BDan.isLocalDiffeomorph_bundleInv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (U : TopologicalSpace.Opens M.carrier) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) ⊤ ⇑(bundleInv T s j U)

theorem Hironaka.Manifold.BDan.surjective_bundleInv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (U : TopologicalSpace.Opens M.carrier) : Function.Surjective ⇑(bundleInv T s j U)

theorem Hironaka.Manifold.BDan.isClosedSubmanifold_transformSU {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (U : TopologicalSpace.Opens M.carrier) : Manifold.IsClosedSubmanifold ψ₀ (⇑(liftIncl T s j U) ⁻¹' ⇑((Manifold.blowUp ψ₀ ⋯).inclusion (piOpen T s j U)) ⁻¹' transformS T s j) 1

The transform of E^j inside the restricted blowing-up: the preimage under the corestricted lift of S_0 ∩ π_{-1}^{-1}(U), a closed hypersurface.

noncomputable def Hironaka.Manifold.BDan.liftInclS {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (U : TopologicalSpace.Opens M.carrier) : AnalyticMap ⋯.toAnalyticManifold ⋯.toAnalyticManifold

The corestricted lift of the inclusion restricted to the transforms of E^j.

Equations

• Hironaka.Manifold.BDan.liftInclS T s j U = Hironaka.Manifold.BDan.liftInclSOf ⋯ ⋯ U

noncomputable def Hironaka.Manifold.BDan.transportedValue {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (inp : BMOanFam 𝕜 (n - 1) s) (hT : BDClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) ⋯.toAnalyticManifold

The input family's value at the trace of π_{-1}^{-1}(U) on S_0, transported to the transform of E^j in the restricted blowing-up along the inverse of the bundle diffeomorphism and the restricted lift.

Equations

• Hironaka.Manifold.BDan.transportedValue T s j inp hT U hU = Hironaka.Manifold.BDan.transportedValueOf T s j ⋯ ⋯ U inp hT ⋯ ⋯ hU

theorem Hironaka.Manifold.BDan.coreFamOn_eq_coreOfListOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (inp : BMOanFam 𝕜 (n - 1) s) (hT : BDClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : coreFamOn T s j inp hT U hU = coreOfListOf ⋯ ⋯ (transportedValue T s j inp hT U hU)

The core on U is the core over the transported value, on the restricted data: the push-forward to the open π_{-1}^{-1}(U) is the push-forward along the bundle diffeomorphism (BlowUpSequence.pushforwardRestrictOf_eq), and the push-forward commutes with the pull-back along the corestricted lift (BlowUpSequence.pushforward_pullback; "we get the same result" whether one first pulls back or first restricts, the proof of [Kol07, Lemma 102]).