Theorem 103 in the compatible-family form

The order-reduction functor BO_{n,m} of [Kol07, Theorem 103], assembled in the form suited to non-compact analytic manifolds: the structure BOanFam 𝕜 n m (Functor/Family.lean), whose values are compatible families of finite blow-up sequences over the relatively compact open subsets, from the marked structures BMOanFam 𝕜 (n - 1) s at every mark s, Kollár's hypothesis "assume that (69) holds in dimensions < n". The assembly follows the proof of Theorem 103:

• bdanFam, bdanFamDataOfInput — Lemma 102's functor BD_{n,s,j} ([Kol07, Lemma 102]) as a compatible family (BDanFam, BDFam.lean: on each relatively compact open, from the marked family one dimension down at the mark tuningParam s, the tuning of Step 1 being applied inside Lemma 102 as in Kollár's proof) and as the data BDanFamData ψ₀ s (FamilyData.lean) at every mark, its clauses being proved in BDFamOrder.lean, BDFamComm.lean, BDFamIndiff.lean and BDFamCompat.lean; at an empty member the family is trivial ([Kol07, 32]).
• hfLocalFunctorFam, localFunctorFam — the local family functor on the class LocalMCClass m of triples with a global hypersurface of maximal contact: Steps 1 and 2 of the proof on each relatively compact open (localFunctorFamOn, LocalFunctorFam.lean: the tuning, Step 2.1 member by member along a shrinking chain of opens, Step 2.2 at the hypersurface), with its commutation with local analytic isomorphisms (Theorem 103 (2) for the local functor, through the independence of Step 2.3) and its indifference to empty members. The general form is over the data HFData of Step 2 (HFamData.lean), of which Lemma 102's data is the instance.
• BO.BOanFamOfInputOf, BO.BOanFamOfInput — Step 3 of the proof: the descent of the local family functor to the class BOClass m along covers by pieces with maximal contact (globalizeFam, GlobalizeFam.lean), with the clauses of Theorem 103 descended (GlobalizeFamClauses.lean).

BO.BOanFamOfInput 𝕜 n inp m is the first reduction step of the order-reduction tower (theorem103FamStar, Stage/InstancesFam.lean); its clause (3), the commutation with closed embeddings when the boundary is empty, is proved in ClosedEmbeddingFam.lean. Włodarczyk's modified algorithm (the proof of [Wlo09, Theorem 7.4.1]: the components on which the ideal has become the ideal of a smooth hypersurface are left alone) is the same assembly at other data of Step 2 (Modified/).

Lemma 102's family data from the marked families one dimension down

noncomputable def Hironaka.Manifold.BO.bdanFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m : ℕ) (inp : BMOanFam 𝕜 (n - 1) (IsLocalRing.tuningParam m)) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass m T) (j : T.F.ι) : CompatibleFamily T

Lemma 102's functor at the member j as a compatible family ([Kol07, Lemma 102]): the sequence BDanFam (BDFam.lean) on every relatively compact open, without empty centres (noEmptyCenters_BDanFam), compatible under restriction (BDanFam_compat).

Equations

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

theorem Hironaka.Manifold.BO.bdanFam_seqOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m : ℕ) (inp : BMOanFam 𝕜 (n - 1) (IsLocalRing.tuningParam m)) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass m T) (j : T.F.ι) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (bdanFam m inp T hT j).seqOn U hU = BDanFam m inp T hT j U hU

The value of bdanFam on an open is BDanFam, by definition.

noncomputable def Hironaka.Manifold.BO.bdanFamDataOfInput {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (inp : (s : ℕ) → BMOanFam 𝕜 (n - 1) s) (s : ℕ) : BDanFamData ψ₀ s

Lemma 102's family data at every mark ([Kol07, Lemma 102]) from the marked families one dimension down: at the mark s, bdanFam on the input at the mark tuningParam s, the mark of the tuned ideal sheaf (Step 1 of the proof of Theorem 103, applied inside Lemma 102), with the order clause and Lemma 102 (1) (BDFamOrder.lean), the commutation with local analytic isomorphisms (BDFamComm.lean) and the indifference to empty members (BDFamIndiff.lean).

Equations

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

theorem Hironaka.Manifold.BO.bdanFamDataOfInput_fam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (inp : (s : ℕ) → BMOanFam 𝕜 (n - 1) s) (s : ℕ) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (j : T.F.ι) : (bdanFamDataOfInput inp s).fam T hT j = bdanFam s (inp (IsLocalRing.tuningParam s)) T hT j

The family of bdanFamDataOfInput at the mark s is bdanFam on the input at the mark tuningParam s, by definition.

theorem Hironaka.Manifold.BO.bdanFamDataOfInput_fam_eq_nil_of_hyp_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (inp : (s : ℕ) → BMOanFam 𝕜 (n - 1) s) (s : ℕ) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (j : T.F.ι) (hj : T.F.hyp j = ∅) : (bdanFamDataOfInput inp s).fam T hT j = CompatibleFamily.nil T

At an empty member Lemma 102's family is the trivial one ([Kol07, 32]): the hypothesis under which the local family functor commutes with local analytic isomorphisms (localFunctorFam_commutesWithLocalIsos).

The local family functor

noncomputable def Hironaka.Manifold.BO.hfLocalFunctorFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m : ℕ) (d : HFData ψ₀ (IsLocalRing.tuningParam m)) : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.LocalMCClass m

The local family functor of the data d of Step 2 (HFData, HFamData.lean) on the class LocalMCClass m: Steps 1 and 2 of the proof of [Kol07, Theorem 103] on every relatively compact open (hfLocalFunctorFamOn, LocalFunctorFam.lean), without empty centres and compatible under restriction.

Equations

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

theorem Hironaka.Manifold.BO.hfLocalFunctorFam_fam_seqOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m : ℕ) (d : HFData ψ₀ (IsLocalRing.tuningParam m)) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hL : Manifold.AnalyticTriple.LocalMCClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((hfLocalFunctorFam m d).fam T hL).seqOn U hU = hfLocalFunctorFamOn m d T hL U hU

The value of hfLocalFunctorFam on an open is hfLocalFunctorFamOn, by definition.

theorem Hironaka.Manifold.BO.hfLocalFunctorFam_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m : ℕ) (d : HFData ψ₀ (IsLocalRing.tuningParam m)) (hnil : ∀ {M' : AnalyticManifold 𝕜 E} (T' : Manifold.AnalyticTriple ψ₀ M') (hT' : Manifold.AnalyticTriple.BOClass (IsLocalRing.tuningParam m) T') (j : T'.F.ι), T'.F.hyp j = ∅ → d.bd₁.fam T' hT' j = CompatibleFamily.nil T') : (hfLocalFunctorFam m d).CommutesWithLocalIsos

The local family functor of data d of Step 2 commutes with local analytic isomorphisms (Theorem 103 (2) for the local functor, [Kol07, 104, Step 2.3]) when the family of Step 2.1's data is trivial at an empty member (hnil): a pull-back need not be surjective and may empty a member that Step 2.1 iterates over.

theorem Hironaka.Manifold.BO.hfLocalFunctorFam_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m : ℕ) (d : HFData ψ₀ (IsLocalRing.tuningParam m)) : (hfLocalFunctorFam m d).IndifferentToEmptyMembers

The local family functor of data d of Step 2 is indifferent to empty boundary members.

noncomputable def Hironaka.Manifold.BO.localFunctorFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (bd : (s : ℕ) → BDanFamData ψ₀ s) (m : ℕ) : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.LocalMCClass m

The local family functor on LocalMCClass m for Lemma 102's data bd at every mark: Steps 1 and 2 of the proof of [Kol07, Theorem 103] on every relatively compact open (localFunctorFamOn).

Equations

• Hironaka.Manifold.BO.localFunctorFam bd m = Hironaka.Manifold.BO.hfLocalFunctorFam m (Hironaka.Manifold.HFData.ofBDanFamData bd (IsLocalRing.tuningParam m))

theorem Hironaka.Manifold.BO.localFunctorFam_fam_seqOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (bd : (s : ℕ) → BDanFamData ψ₀ s) (m : ℕ) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hL : Manifold.AnalyticTriple.LocalMCClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((localFunctorFam bd m).fam T hL).seqOn U hU = localFunctorFamOn bd m T hL U hU

The value of localFunctorFam on an open is localFunctorFamOn, by definition.

theorem Hironaka.Manifold.BO.localFunctorFam_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (bd : (s : ℕ) → BDanFamData ψ₀ s) (hnil : ∀ (s' : ℕ) {M' : AnalyticManifold 𝕜 E} (T' : Manifold.AnalyticTriple ψ₀ M') (hT' : Manifold.AnalyticTriple.BOClass s' T') (j : T'.F.ι), T'.F.hyp j = ∅ → (bd s').fam T' hT' j = CompatibleFamily.nil T') (m : ℕ) : (localFunctorFam bd m).CommutesWithLocalIsos

Theorem 103 (2) for the local family functor ([Kol07, 104, Step 2.3]): it commutes with local analytic isomorphisms when the data's family at an empty member is trivial at every mark.

theorem Hironaka.Manifold.BO.localFunctorFam_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (bd : (s : ℕ) → BDanFamData ψ₀ s) (m : ℕ) : (localFunctorFam bd m).IndifferentToEmptyMembers

The local family functor is indifferent to empty boundary members.

The structure BOanFam at the standard model

noncomputable def Hironaka.Manifold.BO.BOanFamOfInputOf (𝕜 : Type) [RCLike 𝕜] (n : ℕ) (inp : (s : ℕ) → BMOanFam 𝕜 (n - 1) s) (m : ℕ) (hcomm : (localFunctorFam (bdanFamDataOfInput inp) m).CommutesWithLocalIsos) : BOanFam 𝕜 n m

The structure BOanFam 𝕜 n m from the marked structures one dimension down, given that the local family functor commutes with local analytic isomorphisms (hcomm, the hypothesis of Step 3 of the proof of [Kol07, Theorem 103]): the descent globalizeFam (GlobalizeFam.lean) of the local family functor to the class BOClass m, with the four clauses of BOanFam. The order clause and the output clause descend from the local functor along the covers (isOfOrderGe_of_agreeFam, ord_lt_of_agreeFam, GlobalizeFamClauses.lean; the output clause for the controlled transform follows from the one for the weak transform because along a sequence of order ≥ m starting from an ideal sheaf of order ≤ m the two transforms agree); the descent commutes with local analytic isomorphisms (globalizeFam_commutesWithLocalIsos) and is indifferent to empty members (indifferentToEmptyMembers_of_agreeFam).

Equations

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

noncomputable def Hironaka.Manifold.BO.BOanFamOfInput (𝕜 : Type) [RCLike 𝕜] (n : ℕ) (inp : (s : ℕ) → BMOanFam 𝕜 (n - 1) s) (m : ℕ) : BOanFam 𝕜 n m

Order reduction for ideals in the compatible-family form ([Kol07, Theorem 103]): the structure BOanFam 𝕜 n m from the marked structures BMOanFam 𝕜 (n - 1) s at every mark, without further hypothesis, the local family functor commuting with local analytic isomorphisms because Lemma 102's family is trivial at an empty member (bdanFamDataOfInput_fam_eq_nil_of_hyp_eq_empty). This is the first reduction step of the order-reduction tower (theorem103FamStar, Stage/InstancesFam.lean).

Equations

• Hironaka.Manifold.BO.BOanFamOfInput 𝕜 n inp m = Hironaka.Manifold.BO.BOanFamOfInputOf 𝕜 n inp m ⋯

theorem Hironaka.Manifold.BO.BOanFamOfInput_functor (𝕜 : Type) [RCLike 𝕜] (n : ℕ) (inp : (s : ℕ) → BMOanFam 𝕜 (n - 1) s) (m : ℕ) : (BOanFamOfInput 𝕜 n inp m).functor = (localFunctorFam (bdanFamDataOfInput inp) m).globalizeFam ⋯

The family functor of BO.BOanFamOfInput is the descent of the local family functor, by definition.