The numerator side of the sign projection #
The projective Čech contracting homotopy consumes a sign projection: given a monomial denominator
Xᵞ = X_{i₀}^c · Xᵞ' with γ' i₀ = 0, a map
π : (A(d)_{Xᵞ})₀ → (A(d)_{Xᵞ'})₀
that keeps exactly the Laurent monomials whose i₀-exponent has not gone negative — the ones
still admissible once X_{i₀} is no longer inverted.
On a representative p / (Xᵞ)ᵐ that operation is division by a monomial: keep the terms of p
divisible by X_{i₀}^{m·c} and shift them down. The geometry-free division identities live in
DerivedAlgGeo.Algebra.MvPolynomial.DivMonomial; this file applies them to degree-zero
localizations of polynomially graded modules, without assuming a geometric realization.
Main statements #
divMonomial_mem_natShift— the degree bookkeeping: dividing offX_{i₀}^{m·c}moves a numerator forXᵞat twistdto a numerator forXᵞ'at the same twist. The twist is untouched, which is what keepsπa map ofO(d)-sections.signProjection— the projection itself, withsignProjection_awayMkthe equation that pins it down andsignProjection_laurentFacethe retractionπ ∘ ι = id.MvPolynomial.divMonomial_pow_mul— the well-definedness identity. Raising a representative to a higher power ofXᵞand then projecting is the same as projecting and then raising to a higher power ofXᵞ':
Paired with((Xᵞ)ᵗ · p) /ᵐᵒⁿᵒᵐⁱᵃˡ X_{i₀}^{(m+t)c} = (Xᵞ')ᵗ · (p /ᵐᵒⁿᵒᵐⁱᵃˡ X_{i₀}^{m·c})DegreeZeroLocalization.awayMk_shift, this is exactly what makes the projection independent of the chosen representative: any two representatives of one element become equal numerators after raising both to a common denominator, and this identity says the projection survives that move.
Implementation notes #
MvPolynomial.divMonomial_monomial_mul_comm is the key generic polynomial fact. A monomial
factor may be pulled out through a division only when the two monomials have disjoint support
— the hypothesis ∀ j, a j = 0 ∨ s j = 0. Without it the statement is false: dividing X_{i₀}
out of X_{i₀} · p is not X_{i₀} · anything. The disjointness is available here for a
structural reason, not a lucky one: the factor being pulled out is a power of Xᵞ', which by
hypothesis does not involve i₀, while the divisor is a pure power of X_{i₀}.
The γ = X_{i₀}^c · γ' splitting is taken as a hypothesis rather than built with Finsupp.erase.
The caller that matters is a Čech face, which produces the two pieces separately (c = 1 and
γ' the denominator of the smaller intersection) and never has to take them apart again.
Tags #
monomial division, homogeneous localization, graded module
The projection on numerators #
The degree bookkeeping. Dividing off X_{i₀}^{m·c} carries a numerator for Xᵞ at twist
d to a numerator for Xᵞ' at the same twist d.
Only the denominator's contribution m • γ.degree moves; the twist is untouched. That is what
makes the projection a map of O(d)-sections rather than a comparison between different
twists.
The degree bookkeeping, for a twist of either sign.
divMonomial_mem_natShift with natShift replaced by any IsPolynomialTwist. The twist is again
untouched: only the denominator's contribution m • γ.degree moves.
The nonnegative proof reads the membership as homogeneity and cancels m * c off the degree
directly. That cancellation is not available here, because a negative twist can put the numerator's
degree below m * c — and then there is nothing to divide, so the quotient is zero and the p = 0
disjunct of IsPolynomialTwist carries it. The by_cases on the quotient is therefore not
defensive bookkeeping; it is the only place the two signs behave differently in this whole
argument.
Multiplying a numerator by a homogeneous factor raises its graded piece by that factor's degree and leaves the twist alone.
Three places need this — raising a representative to a higher power of the denominator, and the
two columns of the projection square — and each of them read natShift's membership as
homogeneity directly. Through IsPolynomialTwist the reading is a case split, because the
numerator may be zero in a degree the twist names no graded piece for.
The projection itself #
The numerator operation descends to a map on the localization. A representative is packaged as
AwayRep; AwayRep.frac_project_congr says two representatives of one element project to the
same fraction, and signProjection is the resulting map, chosen through Exists.choose and
pinned by signProjection_awayMk.
A representative p / (Xᵞ)ᵐ of a degree-zero fraction of the twist 𝓜.
The twist is carried by the graded family rather than by a natural number, so that the whole
projection layer is available at either sign; IsPolynomialTwist 𝓜 d is the hypothesis the
degree bookkeeping consumes, and it is required only where a degree actually moves.
- pow : ℕ
The exponent of the denominator.
- num : MvPolynomial ι R
The numerator.
The numerator sits in the graded piece the denominator forces.
Instances For
The fraction a representative names.
Equations
- r.frac = GradedModule.DegreeZeroLocalization.awayMk ⋯ r.pow r.num ⋯
Instances For
Every fraction has a representative — this is exists_awayMk, repackaged.
The projected representative: divide the numerator by X_{i₀}^{m·c}, keep the exponent.
Equations
- MvPolynomial.AwayRep.project h𝓜 hγ r = { pow := r.pow, num := r.num.divMonomial (Finsupp.single i₀ (r.pow * c)), num_mem := ⋯ }
Instances For
Raising a representative by (Xᵞ)ᵗ keeps it a legitimate numerator.
The nonnegative proof read num_mem as homogeneity directly. Here the reading goes through
IsPolynomialTwist, which also supplies the zero case — a numerator may be zero in a degree
where the twist names no graded piece at all.
Projecting a representative is the same as raising it first and then projecting.
This is divMonomial_pow_mul on the numerator and awayMk_shift on the fraction, and it is the
only place either is used. Well-definedness follows immediately: it lets both representatives of
one element be moved to the same exponent before they are compared.
Well-definedness. Two representatives of one fraction project to the same fraction.
awayMk_eq_awayMk_iff turns the hypothesis into a cross-multiplication of numerators, and
frac_project_raise moves both projections to the common exponent r₁.pow + r₂.pow where that
cross-multiplication is literally the equality of numerators.
The sign projection, as a map on the localization.
Defined by choosing a representative; signProjection_awayMk is the equation that pins it down
and is what every caller should use. The hypothesis γ' i₀ = 0 is not needed to make the
definition — only to make it independent of the choice — so it is required by the equations rather
than by the definition.
Equations
- MvPolynomial.signProjection h𝓜 hγ z = (MvPolynomial.AwayRep.project h𝓜 hγ ⋯.choose).frac
Instances For
The defining equation of the sign projection: on a representative it divides the numerator
by X_{i₀}^{m·c} and keeps the exponent.
The projection retracts the face inclusion #
The face inclusion (A(d)_{Xᵞ'})₀ → (A(d)_{Xᵞ})₀, in the shape the sign projection
retracts. This is DegreeZeroLocalization.faceMap at g₁ * h = g₂ with h = X_{i₀}^c, which is
exactly the Čech face of #340's complex.
Equations
Instances For
The face inclusion in awayMk normal form: it multiplies the numerator by
X_{i₀}^{m·c}.
The sign projection retracts the face inclusion: π ∘ ι = id.
This is the first of the two properties #340's homotopy consumes. On a representative the face
multiplies the numerator by X_{i₀}^{m·c} and the projection divides it straight back out
(divMonomial_monomial_mul), so nothing survives to check — the content is all in the degree
bookkeeping, and in awayMk_deg_congr reconciling the two names γ.degree and c + γ'.degree
for the same natural number.
Additivity of the projection #
The contracting homotopy applies the projection to an alternating sum of faces, so it consumes
the projection as an additive map. Additivity is not free from the definition — signProjection
is choice-based — but it reduces to the defining equation once the two summands are put over a
common denominator, which is exactly what DegreeZeroLocalization.exists_awayMk_pair supplies.
This is the first use of that lemma outside frac_project_raise's single-element version.
The sign projection is additive. Align the two fractions at a common denominator
(exists_awayMk_pair), where the projection is division of the numerator by a fixed monomial
(signProjection_awayMk), and division by a monomial is additive (add_divMonomial).
The sign projection as an additive map. The hypothesis γ' i₀ = 0 is what additivity
costs — see signProjection — so the bundled form carries it. map_zero comes with the
bundling; callers should reach equations through signProjectionHom_apply and then
signProjection_awayMk.
Equations
- MvPolynomial.signProjectionHom h𝓜 hγ hγ' = AddMonoidHom.mk' (MvPolynomial.signProjection h𝓜 hγ) ⋯
Instances For
The projection commutes with the remaining faces #
signProjection_laurentFace handles the face that reinserts X_{i₀} itself — the j = 0 face
of the homotopy, which the projection retracts. Every other face of the Čech complex multiplies
the denominator by a variable X_e that is not X_{i₀}, and for those the projection and
the face commute. That square is the second and last property #340's contracting homotopy
consumes.
The restriction of §1 of the proof plan — the square only holds on the summands with
i₀ ∉ N α — enters here as the hypothesis δ' i₀ = 0: the target denominator of the
projection on the face side must not invert X_{i₀}, which encodes both e ≠ i₀ (or the face
is the retracted one) and the well-definedness hypothesis of each projection. The unrestricted
square with e = i₀ is false, and no statement of it appears.
Multiplying a numerator by (X_e^{c'})ᵐ raises its graded piece by m·c' and keeps the
twist. This is the membership fact the face side of the projection square feeds
laurentFace_awayMk, stated once because both columns of the square need it.
The projection square. Away from the retracted face, the sign projection commutes with
the Čech face: restricting along X_e and then projecting out X_{i₀} is projecting first and
restricting after.
The four denominators are supplied as separate splittings because the caller — a Čech
differential — produces each of them separately and never has to take one apart. hδ'₀
(δ' i₀ = 0) is the restriction of §1 of #340's proof plan in hypothesis form: with hγ' it
forces X_e ≠ X_{i₀} unless c' = 0, which is exactly the disjointness
divMonomial_monomial_mul_comm needs to pull the face's monomial through the projection's
division. The unrestricted square at e = i₀ is false — that face is the retraction
signProjection_laurentFace, not this square.