The base cases of order reduction: dimensions zero and one #
Kollรกr settles the two lowest dimensions of the induction directly [Kol07, 70]. In dimension 0,
"I = ๐ช_X", I being nonzero on every irreducible component of X, and "everything is
resolved without blow-ups": on a manifold modelled on ๐โฐ the stalks of the structure sheaf are
fields (regular local domains of Krull dimension 0), so a nonzero stalk ideal is the unit ideal
and the order of the ideal sheaf is 0 < m everywhere (AnalyticTriple.eq_top_of_dim_zero,
AnalyticTriple.ord_lt_of_dim_zero). In dimension 1 the cosupport is a Cartier divisor, "our
algorithm tells us to blow up Z := cosupp(I, m)", and in the marked case the maximal order of
I โ ๐ช_X(Z) drops: the ideal sheaf of a closed hypersurface is invertible in every
dimension, generated near each of its points by the adapted coordinate
(IsClosedSubmanifold.isInvertible_idealSheaf_codimOne); and when cosupp(๐, m) is a closed
hypersurface (on a curve it is a discrete closed set, the zeros of a nonzero analytic function of
one variable being isolated), blowing it up is a smooth blow-up sequence of order โฅ m after
which the controlled transform has order < m everywhere
(AnalyticTriple.orderReduction_dim_one). For the last point the centre has simple normal
crossings with E because on a curve every closed hypersurface has
(HypersurfaceFamily.IsSnc.hasSncWith_of_dim_one), the order of ๐ along the centre is at least
m, over the centre the colon stalk is the unit ideal (ColonOrder.lean; the blowing-up of a
hypersurface is an isomorphism, [Kol07, Warning 20]), and off the centre the controlled transform is
the total transform, of the order of ๐ at the image, which is < m there.
The dimension-zero results give the base stage of the order-reduction tower
(Stage/Family.lean). The dimension-one results stand apart from the tower, whose recursion handles
dimension 1 through Theorem 103; they record Kollรกr's remark on that case.
Dimension zero #
The case dim X = 0 of [Kol07, 70], "here I = ๐ช_X since I is assumed nonzero on every
irreducible component of X": on a manifold modelled on ๐โฐ, the ideal sheaf of a triple is the
unit ideal sheaf. The stalks are fields (regular local domains of Krull dimension 0), so a
nonzero stalk ideal is the unit ideal.
The case dim X = 0 of [Kol07, 70], "everything is resolved without blow-ups": on a manifold
modelled on ๐โฐ, the order of the ideal sheaf of a triple is 0 < m at every point, so the empty
sequence is order reduction.
Codimension one: the ideal sheaf of a hypersurface is invertible #
"The cosupport of an ideal sheaf is a Cartier divisor" in the case dim X = 1 of [Kol07, 70],
in the form true in every dimension: the ideal sheaf of a closed submanifold of codimension one is
invertible, generated near each of its points by the adapted coordinate, a nonzero element of the
domain stalk, and off the submanifold by 1.
Dimension one #
On a curve, two points of a chart's source at which one and the same coordinate vanishes
coincide: the chart is injective on its source and ๐ยน has a single coordinate.
On a curve every closed hypersurface Z has simple normal crossings with every boundary E
with simple normal crossings (the centre Z := cosupp(I, m) of the case dim X = 1 of [Kol07, 70]
must be admissible): at a point of Z on a member of E, the snc chart of E restricted to the
source of an adapted chart of Z is adapted to Z, both meeting that source in the single point;
at a point of Z on no member, an adapted chart of Z is vacuously an snc chart.
The case dim X = 1 of [Kol07, 70], "our algorithm tells us to blow up Z := cosupp(I, m)",
after which the maximal order of I โ ๐ช_X(Z) has dropped: on a manifold modelled on ๐ยน, for a
triple
with 1 โค m and ord ๐ โค m everywhere, blowing up cosupp(๐, m) is a smooth blow-up sequence of
order โฅ m starting with (M, ๐, m, E), after which the controlled transform has order < m at
every point. The centre has normal crossings with E (hasSncWith_of_dim_one) and the order of ๐
along it is at least m; over the centre the colon stalk is the unit ideal
(ord_colon_totalTransform_eq_zero; the blowing-up of a hypersurface is an isomorphism,
[Kol07, Warning 20]), off the centre the controlled transform is the total transform, of the order
of ๐ at the image, < m there. Under the bound ord ๐ โค m one step suffices.