The contracting homotopy of a block, one localization at a time #
Step 3 of #340's proof plan contracts each block C_F of the Čech complex through a cone point
i₀ ∉ F: the homotopy sends a cochain s to y ↦ Π (s (i₀ :: y)), where Π restricts a
fraction from the denominator of i₀ :: y back to the denominator of y. This file supplies
Π — here laurentHomotopy — and the two identities the homotopy computation
d ∘ h + h ∘ d = id consumes, at the level of one localization.
The definition, and why it is a composite #
The denominator of i₀ :: y is X_{i₀} · Xᵞ with γ the denominator exponent of y — but
γ may itself contain i₀ (the tuple y may mention the cone point), and the sign
projection's defining equations require a target free of i₀. So Π projects out all of
X_{i₀} first and then reinserts the surplus:
Π = laurentFace (γ = X_{i₀}^t · γ'') ∘ signProjection (X_{i₀}·Xᵞ = X_{i₀}^{1+t} · γ'')
with t = γ i₀ and γ'' = γ.erase i₀. Both constituents are pinned by their awayMk
equations, so Π is well defined and additive with no new descent argument, and
laurentHomotopy_awayMk is the equation everything else runs on. When t = 0 the reinserted
face is multiplication by X_{i₀}^0 = 1 and Π is the plain sign projection.
The two identities #
laurentHomotopy_laurentFace_comm—Πcommutes with every face, with no restriction: not only the faces in a variablee ≠ i₀(where it reduces to the projection square of #539), but also the faces ini₀itself, where the surplus exponenttshifts by one and the reinserted power rebalances exactly. This unrestricted square is what the composite definition buys; the bare sign projection satisfies no such identity.laurentHomotopy_laurentFace_blockProj—Πretracts the cone face on the block: fori₀ ∉ F, applying the front faceX_{i₀}and thenΠis the identity on block-Felements. This is the only place the block hypothesis enters, and it is genuinely needed: on a block withα i₀ < 0the projection half ofΠkills terms the face half cannot restore.
In the homotopy computation these two are the whole story: the j = 0 face of i₀ :: y
produces the identity through the retraction, and every other face cancels between
d (h s) and h (d s) through the square.
Tags #
contracting homotopy, Čech complex, homogeneous localization, graded module
Numerator-level cancellation #
A monomial divided out of a polynomial that it wholly divides is restored by multiplying it
back. The support hypothesis cannot be dropped: on a term not divisible by Xˢ the division
truncates and the multiplication cannot restore it. In the retraction below the hypothesis is
supplied by the block structure — on block F with i₀ ∉ F every term carries at least
X_{i₀}^{m·t}.
On block F with i₀ ∉ F, every numerator term carries at least the denominator's power
of X_{i₀}: the Laurent exponent at i₀ is nonnegative, so β i₀ ≥ m · γ i₀. This is the
support bound that feeds monomial_mul_divMonomial_cancel in the retraction.
The homotopy map #
The full splitting of the cone denominator: X_{i₀} · Xᵞ = X_{i₀}^{1+γ(i₀)} · Xᵞ'' with
γ'' = γ.erase i₀. This is the splitting the projection half of the homotopy uses; unlike the
naive c = 1 splitting it leaves a target free of i₀, so the projection's equations apply
whatever the tuple y contains.
The reinsertion splitting: Xᵞ = X_{i₀}^{γ(i₀)} · Xᵞ''. The face at this splitting puts
back the surplus power of X_{i₀} that the full projection removed beyond the cone factor.
The homotopy map Π : (A(d)_{X_{i₀}·Xᵞ})₀ → (A(d)_{Xᵞ})₀: project out all of
X_{i₀}, then reinsert the surplus X_{i₀}^{γ(i₀)} by a face. A composite of two maps that
are already well defined and additive, so it is both, with no new descent argument. Callers
use laurentHomotopy_awayMk.
Equations
- MvPolynomial.laurentHomotopy h𝓜 i₀ γ = (MvPolynomial.laurentFace 𝓜 ⋯).comp (MvPolynomial.signProjectionHom h𝓜 ⋯ ⋯)
Instances For
The numerator produced by the homotopy map is a legitimate numerator for Xᵞ.
The defining equation of the homotopy map: on q / (X_{i₀}·Xᵞ)ᵐ it divides the
numerator by X_{i₀}^{m(1+γ(i₀))} and multiplies X_{i₀}^{m·γ(i₀)} back in.
The retraction on a block #
Π retracts the cone face on the block. For i₀ ∉ F, restricting a block-F element
along the cone face X_{i₀} and then applying the homotopy map gives it back.
The front face multiplies the numerator by X_{i₀}^m; the projection half of Π divides by
X_{i₀}^{m(1+t)}, which eats the face's factor and X_{i₀}^{m·t} more; the reinsertion
restores that surplus — and restoring is exact precisely because on block F with i₀ ∉ F
every term had β i₀ ≥ m·t to give (laurentFilter_apply_ge). This is the only identity in
the homotopy that sees the block.
The square with every other face #
Π commutes with every face — no restriction. For a face in a variable e ≠ i₀ this
is the projection square of #539 conjugated by the reinsertion; for e = i₀ the surplus
exponent shifts by one on the left and the reinserted power grows to match on the right, and
the two sides agree exactly. The composite definition of Π is what makes the e = i₀ case
true — the bare sign projection satisfies no unrestricted square.
The two splittings are hypotheses in the lane's usual style; both are associativity-and- commutativity rearrangements the Čech caller has in hand.