The monomial ideal of the input family is the monomial part of the restricted triple

The monomial part M(𝓘|_U) of the restricted triple is indexed by the connected components of the restricted members (BMO/MonomialPart.lean), while the input piece family of the monomial procedure (BMO/Step3Monomial/Input.lean) has as pieces the traces on U of the ambient components meeting closure U. The two products agree (monomialIdeal_inputFamily): stalk by stalk, both are the product, over the members through the point, of the vanishing stalk of the member raised to the exponent of the ambient component through the point. On one side the pieces through x are the traces of the ambient components through x, one per member through x; on the other the active components of E|_U at x are one per member through x, each with the stalk of its member and with the exponent of the ambient component (the exponent transports along the open inclusion). The two products are matched member by member.

theorem Hironaka.Manifold.BMO.monomialIdeal_inputFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (inputFamily T U hU).monomialIdeal ⋯ ⋯ = monomialPart (T.pullback (M.inclusion U) ⋯).F ⋯ (T.pullback (M.inclusion U) ⋯).I

The monomial ideal of the input family is the monomial part of the restricted triple: every component of a trace carries the exponent of its ambient component, and the locally finite product over the components of the restricted members regroups into the finite product over the traces.