The block decomposition of an away localization #
Step 2 of #340's proof plan decomposes the Čech complex of O(d) by the negative support
N α = {j | α j < 0} of the Laurent exponent: the differential preserves N α, each block with
a cone point contracts, and for d ≥ 0 every block has a cone point. This file supplies the
decomposition at the level of one away localization (A(d)_{Xᵞ})₀, in the form the vanishing
argument consumes.
The decomposition is deliberately not packaged as a direct-sum isomorphism or a
∏_F-indexed complex. The consumer — "every positive-degree cocycle is a coboundary" — needs
exactly a family of additive projections blockProj γ F d with
sum_blockProj— they sum to the identity over the finite indexγ.support.powerset, which is the step that keeps an infinite variable set harmless: each single localization only ever meets finitely many blocks, and no infinite product is exchanged with an infinite sum;blockProj_blockProj_self/blockProj_blockProj_of_ne— they are orthogonal idempotents;laurentFace_blockProj— the faces of the Čech complex commute with them, because a face moves the numerator and the denominator together and the Laurent exponent never changes.
Main definitions #
intNegSupport— the negative support of an integer exponent vector;laurentFilter— keep the monomials of a numerator whose Laurent exponent has a given negative support;AwayRep.blockFilter— the same operation on a representative;blockProj— the block projection on the localization, pinned byblockProj_awayMk.
Implementation notes #
laurentFilter is characterised coefficientwise by coeff_laurentFilter_of_eq and
coeff_laurentFilter_of_ne, and every identity about it is proved by ext plus a case split on
the block of the exponent. This keeps the Finset.filter in its definition — and the classical
decidability instance it needs — out of every statement.
laurentFilter_monomial_mul is the single shift identity behind both well-definedness and the
face square. Multiplying the numerator by Xᵟ and moving the denominator data from (γ, m) to
(γ', m') fixes every Laurent exponent as soon as σ + m • γ = m' • γ'; raising a
representative (σ = t • γ) and applying a Čech face (σ = m • single e c) are the two
instances, so one lemma serves where #526 needed divMonomial_pow_mul and #539 needed
divMonomial_monomial_mul_comm separately.
blockProj descends to the localization through Exists.choose exactly as signProjection
does, and everything must go through blockProj_awayMk; the definition itself has no useful
rfl behaviour.
Tags #
Laurent monomial, negative support, block decomposition, graded module
The negative support of a Laurent exponent #
The negative support of an integer exponent vector: the variables that occur with a negative
exponent. This is the N α of #340's proof plan; the block of a Laurent monomial is its
negative support, and the Čech differential preserves it.
Equations
- MvPolynomial.intNegSupport α = {j ∈ α.support | α j < 0}
Instances For
The negative support of a Laurent exponent lies inside the support of the denominator: a
variable the localization does not invert cannot go negative. This is
laurentExponent_nonneg_of_apply_eq_zero read as a Finset inclusion, and it is what makes
γ.support.powerset a complete block index for (A(d)_{Xᵞ})₀.
The full block is indexed by finitely many Laurent exponents.
An exponent in the block of every variable is negative in every coordinate, and its coordinates
sum to the twist. Each coordinate is therefore trapped between -1 above and
d + (card ι) - 1 below — the latter because the other card ι - 1 coordinates contribute at most
-1 each — so the exponents form a subset of a finite box.
This is the finiteness the top cohomology of Pⁿ rests on. Below the top degree the full block is
empty for a counting reason (cechBlockProj_eq_zero_of_card_lt); in the top degree it is not, and
this says it is at least small. Note the set is empty unless d ≤ -(card ι), which is Serre's
Hⁿ(Pⁿ, O(d)) = 0 for d > -(n+1) in exponent form — but that is a consequence, not what is
proved here.
The shift identity for Laurent exponents. Multiplying a numerator exponent by Xᵟ while
the denominator data moves from (γ, m) to (γ', m') fixes the Laurent exponent as soon as
σ + m • γ = m' • γ'. Raising a representative and applying a Čech face are both instances.
Filtering a numerator by block #
Keep the monomials of a numerator whose Laurent exponent over (Xᵞ)ᵐ has negative support
exactly F. Characterised coefficientwise by coeff_laurentFilter_of_eq and
coeff_laurentFilter_of_ne; the classical decidability this definition needs never reaches a
statement.
Equations
- MvPolynomial.laurentFilter γ m F p = ∑ β ∈ p.support with MvPolynomial.intNegSupport (γ.laurentExponent m β) = F, (MvPolynomial.monomial β) (MvPolynomial.coeff β p)
Instances For
Filtering is additive in the numerator, which is what the block projection's additivity descends from.
Filtering preserves the graded piece: it only discards monomials.
The blocks exhaust the numerator. Summing the filters over all subsets of the
denominator's support recovers the numerator: every monomial lands in the single block named by
its negative support, and that block is admissible by intNegSupport_laurentExponent_subset.
The index γ.support.powerset is finite for every γ, whatever the variable set.
Filtering twice by the same block changes nothing.
Distinct blocks are disjoint: filtering by one then the other kills everything.
A block outside the denominator's support is empty.
The shift identity for filters. Multiplying the numerator by Xᵟ while the denominator
data moves from (γ, m) to (γ', m') commutes with filtering, as soon as
σ + m • γ = m' • γ' — the hypothesis under which laurentExponent_sub_of_add_eq says no
Laurent exponent moves. Raising a representative (σ = t • γ) and applying a Čech face
(σ = m • single e c) are the two instances; this one identity is the whole content of both
the well-definedness of blockProj and its commutation with the faces.
The block projection on the localization #
The filter descends to the away localization exactly as the sign projection did in #526: a
representative is filtered, well-definedness is the shift identity plus cross-multiplication,
and the resulting map is pinned by its awayMk equation.
The block-filtered representative: keep the numerator's monomials in block F.
Equations
- MvPolynomial.AwayRep.blockFilter h𝓜 F r = { pow := r.pow, num := MvPolynomial.laurentFilter γ r.pow F r.num, num_mem := ⋯ }
Instances For
Filtering a representative is the same as raising it first and then filtering. This is
laurentFilter_monomial_mul at σ = t • γ on the numerator and awayMk_shift on the
fraction; well-definedness follows exactly as it did for the sign projection.
Well-definedness. Two representatives of one fraction filter to the same fraction.
The block projection, as a map on the localization. Defined by choosing a
representative; blockProj_awayMk is the equation that pins it down and is what every caller
should use.
Equations
- MvPolynomial.blockProj h𝓜 γ F z = (MvPolynomial.AwayRep.blockFilter h𝓜 F ⋯.choose).frac
Instances For
The defining equation of the block projection: on a representative it filters the numerator and keeps the exponent.
The block projection is additive: align the fractions at a common denominator, where it is
laurentFilter_add.
The block projection bundled as an additive map.
Equations
- MvPolynomial.blockProjHom h𝓜 γ F = AddMonoidHom.mk' (MvPolynomial.blockProj h𝓜 γ F) ⋯
Instances For
The blocks exhaust the localization. The projections over the finite index
γ.support.powerset sum to the identity. This is the whole decomposition step in the form the
vanishing argument consumes: no direct sum, no reindexed complex — each element is the finite
sum of its blocks, one localization at a time.
The block projections are idempotent.
Distinct block projections are orthogonal.
A block outside the denominator's support projects to zero.
The faces commute with the block projections #
A Čech face multiplies numerator and denominator together, so the Laurent exponent of every
monomial — and with it the block — never moves. This is the statement "the differential
preserves N α" of #340's proof plan, one face and one localization at a time.
The faces commute with the block projections. Restricting along X_e and then taking
the block-F component is taking the block-F component and restricting after. This is
laurentFilter_monomial_mul at σ = m • single e c; no restriction on F is needed, in
contrast to the sign projection's square.