The descended centre in chart coordinates #
The pushforward criterion of Hironaka.Scheme.BlowUp.Composite (mem_ideal_map_iff_of_le_iSup) in
the coordinates of the charts of the blow-up: for an affine open U of X, generators s of
I(U) and an ideal sheaf L on the blow-up, a function x ∈ Γ(X, U) lies in the pushforward
(L.map b)(U) iff its image in every chart ring Γ(X, U)[I(U)/c], c ∈ s, lies in the chart
ideal L_c (mem_ideal_map_iff_chart). For L = J' · E^m this is the chart description of
Hironaka's J(m): x ∈ I^m lies in K_m iff x/c^m ∈ J'_c on every chart. The transport is
the identification of the pullback of x along chart c ≫ b = Spec (algebraMap) ≫ fromSpec_U
with algebraMap x on global sections (appLE_chart_mem_ideal_iff), through
Scheme.Hom.appIso, appLE_comp_appLE, IsAffineOpen.SpecMap_appLE_fromSpec and the
injectivity of Spec.map. Used by Hironaka.Scheme.BlowUp.Composite.Bound and for the kernels of
chart maps in Hironaka.Resolution.Algebraic.MaximalContact.AgreeOnBlowUpKernel.
The pullback of x ∈ Γ(X, V) along Spec ψ ≫ fromSpec_V, on global sections, is
ΓSpecIso⁻¹ (ψ x): Spec of that pullback map composed with fromSpec_V is the morphism itself
(IsAffineOpen.SpecMap_appLE_fromSpec), and Spec.map is injective.
appLE of a morphism known to factor as Spec ψ ≫ fromSpec_V.
The image of the chart of c lies over U.
The affine open chart c ''ᵁ ⊤ of the blow-up.
Equations
Instances For
The pullback of x ∈ Γ(X, U) to the chart of c, as a section over chart c ''ᵁ ⊤, is the
transport of algebraMap x ∈ Γ(X, U)[I(U)/c] along the chart's identification of sections.
Membership in the chart ideal, read on the affine open chart c ''ᵁ ⊤ of the blow-up.
The pullback of x to the chart of c lies in L iff algebraMap x lies in the chart
ideal L_c.
The pushforward criterion in chart coordinates: for generators s of I(U), x ∈ (L.map b)(U)
iff algebraMap x ∈ L_c for every chart c ∈ s.