Flag charts with prescribed centre coordinates #
exists_adaptedChart_flag (Hironaka/Manifold/BlowUp/Transform/StrictFlag.lean) produces, for
nested closed submanifolds Y ⊆ S, a chart adapted to Y in which S is cut out by s of the
c centre coordinates. Its construction exchanges s of the centre coordinates
z_k = ψ_{σ₀ k} ∘ φ₀ of a chart φ₀ adapted to Y for the s equations h_j = ψ_{σ₁ j} ∘ φ₁ of
S taken from a chart φ₁ adapted to S. In the presence of a divisor the exchange has to spare
the centre coordinates that are equations of components of the divisor: this module reproves the
construction with the two charts as inputs and a prescribed set P of centre indices that must be
kept, under the hypothesis that the differentials of the h_j and of the kept z_p are
independent (exists_adaptedChart_flag_protected), recording that the S-block of the new chart
is exactly the h_j and that the kept coordinates are unchanged
(exists_finset_linearIndependent_sum_of_subset is the exchange lemma with the prescribed subset).
A second step (exists_adaptedChart_extend) adjoins further functions with independent
differentials as coordinates outside the centre block, keeping the centre block; the conormal
lemma fderiv_comp_symm_mem_span_of_forall_eq_zero (the differential of a function vanishing on a
submanifold lies in the span of the centre coordinate functionals) supplies the independence
hypotheses. The module closes with the simultaneous chart for (F, H, Z)
(HypersurfaceFamily.exists_isSncChartAt_flag_proper): at a point of Z ⊆ H, from one chart
adapted to Z which is an snc chart of the family F and one chart adapted to H which is an snc
chart of F with no component coordinate in the H-block, a chart adapted to Z, cutting out H
by centre coordinates, which is an snc chart of F with every component coordinate off the
H-block.
These are the coordinates in which Kollár restricts a blow-up sequence to the strict transforms of
a closed subvariety [Kol07, 30.2] and requires the centres to have simple normal crossings with
the boundary [Kol07, Definition 66]; the local coordinates x_1, …, x_n with S = (x_1 = 0) and
centre (x_1 = ⋯ = x_r = 0) of the proof of [Kol07, Theorem 88] are the case c = r, s = 1. Not
in the sources as separate statements; used by Hironaka/Manifold/Snc/Proper.lean and
Hironaka/Manifold/Snc/Trace.lean.
Linear algebra: the exchange lemma with a prescribed kept subset #
The exchange lemma with a prescribed kept subset: if the independent family d of s vectors
inside the span of the independent family e of c vectors stays independent together with the
e p, p ∈ P, it can be completed to a basis of that span by c − s of the e k, k ∈ K, with
P ⊆ K.
Flag charts with prescribed kept centre coordinates #
The flag chart with a prescribed set P of kept centre coordinates: let φ₀ be a chart adapted
to Y and φ₁ a chart adapted to S ⊇ Y, both containing a ∈ Y, and P a set of centre indices
such that the differentials at a of the S-equations h_j = ψ_{σ₁ j} ∘ φ₁ together with the
kept centre coordinates z_p = ψ_{σ₀ p} ∘ φ₀, p ∈ P, are independent. Then there is a chart e
at a, with source inside both sources, adapted to Y (σ), in which S is cut out by the s
centre coordinates σ (τ j) — and these are exactly the h_j — while the kept centre coordinates
σ p, p ∈ P (all outside range τ), are exactly the z_p. Proof: the h_j vanish on Y, so
near a they are combinations h_j = ∑_k g_{jk} z_k of the centre coordinates (the germs of the
h_j lie in the ideal of Y, generated by the z_k); the exchange lemma replaces s non-kept
z_k by the h_j in the cotangent basis, the chart-extension theorem makes the exchanged family
the coordinates of a chart, and on the open set where the s × s minor of (g_{jk}) on the
exchanged indices is invertible the flag equations hold.
The conormal lemma, chart independence of independent differentials, and extension #
The conormal lemma: the differential at a ∈ Y of an analytic function vanishing on Y near
a, read in a chart φ adapted to Y, lies in the span of the centre coordinate functionals
ψ_{σ k} — the conormal space of Y at a (from
IsClosedSubmanifold.stalkIdeal_idealSheaf_eq_span).
The independence of the differentials of a finite family of functions at a, read in a chart,
does not depend on the chart (hasIndependentDifferentialsAt_iff_chart).
A chart e adapted to Y at a ∈ Y and a finite family v of analytic functions vanishing at
a whose differentials are independent together with those of the centre coordinates of e (read
in any chart χ) can be completed to a chart e' adapted to Y, with source inside that of e,
whose centre block is that of e and which has the v l as coordinates outside the centre block
(from the chart-extension theorem exists_chart_extending).
Simultaneous adapted coordinates for (F, H, Z) #
Simultaneous adapted coordinates for (F, H, Z) (the coordinates of the proof of
[Kol07, Theorem 88], with a boundary; [Kol07, Definition 24 (4)]). Let Z ⊆ H be closed
submanifolds and F an snc family; suppose φ₀ is a chart adapted to Z which is an snc chart of
F at a ∈ Z and φ₁ a chart adapted to H which is an snc chart of F at a whose component
coordinates lie outside the H-block (properly: no component contains H near a). Then there
is a chart adapted to Z in which H is cut out by s of the centre coordinates (σ ∘ τ) and
which is an snc chart of F at a with every component coordinate outside the H-block σ ∘ τ.
Proof: the exchange of exists_adaptedChart_flag_protected keeps the centre coordinates of φ₀
that are component equations (their differentials are independent of the H-equations, being
nonzero multiples of the φ₁-coordinates cidx₁ j ∉ range σ₁ by the conormal lemma), and
exists_adaptedChart_extend adjoins the component equations of φ₀ off the centre block
(independent of the centre block, again by the conormal lemma).