The nonmonomial triple

Step 1 of the proof of [Kol07, Theorem 107] (item 111) applies order reduction to the nonmonomial part N(𝓘) of the ideal of a triple (M, 𝓘, E). This file forms the triple that step runs on: the nonmonomial triple (M, N(𝓘), E), with the same ambient manifold and boundary and the ideal replaced by its nonmonomial part (BMO/NonmonomialPart.lean). It is a genuine analytic triple because N(𝓘) is nonzero at every point whenever 𝓘 is (nonmonomialPart_isNonzeroEverywhere, BMO/Round.lean).

The ideal type of a bundled triple, AnalyticManifold.IdealSheaf M, is by definition the type IdealSheaf (structureSheaf 𝕜 E M) on which the monomial and nonmonomial parts are defined, and the manifold structure of M supplies the instances those definitions need, so nonmonomialPart T.F T.isSnc T.I is directly an ideal of T. The mark m of Kollár's marked triple (X, I, m, E) is not a field of an analytic triple; it is a parameter of the class BMOClass m. The analytic counterpart of Hironaka.BMO.nonmonomialTriple.

noncomputable def Hironaka.Manifold.BMO.nonmonomialTriple {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) : Manifold.AnalyticTriple ψ₀ M

The nonmonomial triple (M, N(𝓘), E) of an analytic triple (M, 𝓘, E): the same ambient manifold and boundary, the ideal replaced by its nonmonomial part N(𝓘) = 𝓘 : M(𝓘), which is nonzero at every point. This is the triple to which Step 1 of the proof of [Kol07, Theorem 107] applies the order reduction functor.

Equations

• Hironaka.Manifold.BMO.nonmonomialTriple T = { I := Hironaka.Manifold.BMO.nonmonomialPart T.F ⋯ T.I, isNonzeroEverywhere := ⋯, F := T.F, isSnc := ⋯ }

@[simp]

theorem Hironaka.Manifold.BMO.nonmonomialTriple_I {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) : (nonmonomialTriple T).I = nonmonomialPart T.F ⋯ T.I

The ideal of the nonmonomial triple is the nonmonomial part of the ideal.

@[simp]

theorem Hironaka.Manifold.BMO.nonmonomialTriple_F {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) : (nonmonomialTriple T).F = T.F

The boundary of the nonmonomial triple is the boundary of the triple.