The nonmonomial part is indifferent to empty boundary members #
The counterpart, for boundary members, of the empty blow-up convention [Kol07, 32], for the
decomposition I = M(I) · N(I) of
[Kol07, Definition–Lemma 110] in its fine form: deleting empty members of the boundary changes
neither the fine monomial part M(I) nor the nonmonomial part N(I) = I : M(I). Two boundary
families G, G' with simple normal crossings which differ by an empty extension along an order
embedding e : G.ι ↪o G'.ι (HypersurfaceFamily.IsEmptyExtension: the members correspond along
e, the members outside its range are empty) have the same connected components: an empty member
has none, and the components of corresponding members are the same subsets of M (emptyExtIdx, a
bijection of the component indices which preserves the component sets and their chosen
representatives). So the stalks of M(I), finite products of the component factors
(stalkIdeal_monomialPart), agree (Finset.prod_bij), hence M(I) and N(I) agree
(IdealSheaf.ofStalks_congr). The nonmonomial triple of a triple with an empty extension of the
boundary is therefore the nonmonomial triple of the original with the boundary replaced
(nonmonomialTriple_eq_of_isEmptyExtension): the input of the indifference property of the rounds
on the nonmonomial part (the value of bo d read at the nonmonomial triple), and of the transport
of the invariant of the descent through the deletion of empty blow-ups.
Connected components along an equality of subsets #
Transport of connected components along an equality of subsets (a cast).
Equations
- Hironaka.Manifold.BMOmod.ccCast h C = cast ⋯ C
Instances For
The chosen representative of a transported component is the representative of the component
(the transport is a cast, so the two Quotient.out are the same term after subst).
The underlying subset of a transported component is the underlying subset of the component.
The components of an empty extension #
The component of G' corresponding to a component ⟨j, C⟩ of G under an empty extension
along e: the member e j (whose set is G.hyp j) with the component C transported.
Equations
Instances For
Every component of G' comes from a component of G: a member outside the range of e is
empty (he.2), so it has no connected component.
The nonempty members of G are finite when those of G' are (they inject along e).
The nonempty members of G' are finite when those of G are (every nonempty member of G'
is the image of a member of G).
The fine monomial part and the nonmonomial part #
Corresponding components have the same reduced ideal sheaf (the ideal sheaf of a closed
submanifold depends only on the subset, IsClosedSubmanifold.idealSheaf_congr).
Corresponding components have the same exponent ord_D I (the same ideal sheaf, read at the
same representative).
Corresponding components have the same fine monomial factor 𝓘_D ^ (ord_D I).
The stalk products which define M(I) agree: the components through x correspond along
emptyExtIdx (same component sets), with the same factors.
Two ideal sheaves prescribed by the same stalk ideals are equal (the generator proofs are irrelevant).
The fine monomial part is indifferent to empty members: M(I) for G' is M(I) for G
under an empty extension G ↪ G' (the counterpart, for boundary members, of [Kol07, 32], for the
decomposition of [Kol07, Definition–Lemma 110]).
The nonmonomial part is indifferent to empty members: N(I) = I : M(I) for G' is N(I)
for G under an empty extension G ↪ G' (the counterpart, for boundary members, of [Kol07, 32],
for the decomposition of [Kol07, Definition–Lemma 110]).
The nonmonomial triple #
The nonmonomial triple of a triple with an empty extension of the boundary is the
nonmonomial triple of the original with the boundary replaced: the ideal N(𝓘) is the same
(nonmonomialPart_eq_of_isEmptyExtension), the boundary is the replaced one. This is the input of
the indifference property of the rounds on the nonmonomial part, the value of bo d being read at
the nonmonomial triple (the counterpart, for boundary members, of [Kol07, 32]).