Hauser's coordinates (1)–(4) at a point of the centre #
[Hau14, Proposition 5.4 (1)–(4)]: a smooth X over a perfect field, an snc family E of divisors
one of whose members V = E v contains the centre Z (E v ≤ Z in the ideal-sheaf order,
I_V ⊆ I_Z), Z having simple normal crossings with E, and a point a of Z. Kollár's snc data
at a [Kol07, Definition 24 (1)–(4)] are a regular system of parameters z_1, …, z_n of 𝒪_{X,a},
an injective assignment c of a coordinate to every component through a with
I_{E^i,a} = (z_{c(i)}), and a set s of indices with I_{Z,a} = (z_l : l ∈ s).
(1)–(3). Since I_{V,a} ⊆ I_{Z,a}, the coordinate z_{c(v)} of V lies in (z_l : l ∈ s), so
c(v) ∈ s (mem_span_image_iff of Hironaka.Scheme.Snc.ParameterSubset: a parameter lies in the
ideal generated by a subset of the parameters only if it is one of them). Hauser's positions are
reached by reindexing: hauserReindex s j is the permutation of Fin n sending s onto the last
k = |s| positions n − k, …, n − 1 with j = c(v) ↦ n − k — the composite of sncReindex s
(which puts s first), the reversal Fin.rev, and a transposition inside the last k positions.
The reindexed parameters z' = z ∘ σ⁻¹ are again a regular system of parameters (same range), the
snc assignment becomes σ ∘ c, I_{V,a} = (z'_{n-k}) and I_{Z,a} = (z'_l : l ≥ n − k)
(exists_hauser_coordinates). Condition (1), a = (0, …, 0), is that the z'_i lie in the maximal
ideal, part of being a regular system of parameters.
(4). The ideal of the (not necessarily reduced) divisor D = ∑_{i ≠ v} m_i E^i at a is the
product ∏_{i ≠ v} I_{E^i,a}^{m_i} ([Hau14, Remark 3.16, Remark 3.20]: unions of schemes are
products of ideals). A component through a contributes (z_{c(i)})^{m_i} = (z_{c(i)}^{m_i}), a
component missing a contributes ⊤ = (1); the product of principal ideals is the principal ideal
of the product (Mathlib's Ideal.prod_span_singleton), and regrouping the factors by their
coordinate (Finset.prod_fiberwise_of_maps_to) writes the generator as the monomial ∏_j z_j^{q_j}
with q_j = ∑_{c(i) = j, i ≠ v} m_i. The exponent of V's coordinate is q_{c(v)} = 0: by
injectivity of c the only component with coordinate c(v) is V itself, which is excluded
(exists_prod_stalkIdeal_pow_eq_span_monomial). Hauser states (4) in V: the ideal of D ∩ V in
𝒪_{V,a} = 𝒪_{X,a}/I_{V,a} is the image of I_{D,a}, generated by the image of the monomial
(exists_map_prod_stalkIdeal_pow_eq_span_monomial).
The transversality of Z and D enters through the snc data at a (the hypothesis
E.HasSncWith Z). The forms of these statements on the predicates IsSncAt and HasSncWith are in
Hironaka.Scheme.Snc.MonomialCoordinates.
Sources: [Hau14, Proposition 5.4 (1)–(4); Remark 3.16; Remark 3.20]; [Hau03, Appendix C] (the proof,
"(1) to (3) … and (4) follows immediately from the fact that D and Z are transversal");
[Kol07, Definition 24].
The reindexing of Fin n sending s onto the last s.card positions, the members of the
complement onto the first n - s.card ones: sncReindex s inverted, then Fin.rev.
Equations
Instances For
Hauser's reindexing: s goes onto the last s.card positions and the distinguished member
j ∈ s (the coordinate of the hypersurface V) onto position n - s.card, Hauser's
x_{n-k+1}.
Equations
- AlgebraicGeometry.hauserReindex s hj = (AlgebraicGeometry.lastReindex s).trans (Equiv.swap ((AlgebraicGeometry.lastReindex s) j) ⟨n - s.card, ⋯⟩)
Instances For
[Hau14, Proposition 5.4 (1)–(3)] ([Hau03, Appendix C]): Kollár's snc data at a point a of the
centre Z for a family E whose member v contains Z, reindexed to Hauser's positions — a
regular system of parameters z' at a, snc coordinates for E, with I_{V,a} = (z'_{n-k}) and
I_{Z,a} = (z'_l : l ≥ n − k), k = |s| the codimension of Z at a.
[Hau14, Proposition 5.4 (4)] in 𝒪_{X,a} ([Hau14, Remark 3.16, Remark 3.20]): for snc
coordinates z at a with I_{V,a} = (z_p), the ideal ∏_{i ≠ v} I_{E^i,a}^{m_i} of the divisor
D = ∑_{i ≠ v} m_i E^i is generated by a monomial ∏_j z_j^{q_j} with q_p = 0.
[Hau14, Proposition 5.4 (4)] as printed: D ∩ V is defined in V locally at a — in
𝒪_{V,a} = 𝒪_{X,a} ⧸ I_{V,a} — by the image of the monomial ∏_j z_j^{q_j}, q_p = 0.