The primitive of a polynomial variable Čech cocycle in nonnegative degree

The vanishing computation of #340, in cochain form. Given a degree-(n+1) cochain s of the variable Čech cover whose differential vanishes, cechPrimitive is the cochain t with d t = s: per block F, a cone point i₀ ∉ F is chosen and the block component of s is contracted through the homotopy y ↦ Π (s_F (i₀ :: y)); the finitely many blocks of each tuple then reassemble by sum_cechBlockProj.

• cechBlockPrimitive — the per-block candidate primitive. For a block with no cone point — only possible when the block is all of a finite variable set — it is 0, and cechBlockProj_eq_zero_of_forall_mem says the block component of everything vanishes there: such a block would need every variable's exponent negative, while the twist d ≥ 0 fixes the total at d. This is where nonnegativity of the twist is spent, and the only place.
• cechPrimitive_isPrimitive — the homotopy computation d (h s) + h (d s) = s, elementwise. The j = 0 face of the cone tuple returns the block component through the retraction (cechHomotopy_cechFace_zero); every other face cancels between the two sides through the square (cechHomotopy_cechFace_succ); and the per-block identities sum over (tupleExponent x).support.powerset to s x.

The statement is against the face maps directly, not against the complex; the complex-level exactness and the Hⁿ(Pⁿ, O(d)) = 0 statement are derived downstream, where polynomialVariableCechComplex_d_apply converts between the two forms.

Tags

contracting homotopy, Čech complex, multivariate polynomial, vanishing

The top block is empty for a nonnegative twist

theorem MvPolynomial.laurentFilter_eq_zero_of_forall_mem {ι R : Type u} [CommRing R] (j₀ : ι) {F : Finset ι} (hF : ∀ (j : ι), j ∈ F) {γ : ι →₀ ℕ} {d m : ℕ} {p : MvPolynomial ι R} (hp : p ∈ GradedModule.natShift (polynomialGrading ι R) d (m • Finsupp.degree γ)) : laurentFilter γ m F p = 0

If every variable lies in F, the block-F component of a legitimate numerator vanishes: its Laurent exponents would be everywhere negative while their total is the twist d ≥ 0. The witness j₀ rules out the empty variable set, where the empty block carries the constants. This is the only place the nonnegativity of the twist enters the vanishing argument.

theorem MvPolynomial.blockProj_eq_zero_of_forall_mem {ι R : Type u} [CommRing R] [IsDomain R] (j₀ : ι) {F : Finset ι} (hF : ∀ (j : ι), j ∈ F) (γ : ι →₀ ℕ) (d : ℕ) (z : ↥(GradedModule.DegreeZeroLocalization (polynomialGrading ι R) (GradedModule.natShift (polynomialGrading ι R) d) (Submonoid.powers ((monomial γ) 1)))) : blockProj ⋯ γ F z = 0

The block of everything, over a nonempty variable set, projects everything to zero when the twist is nonnegative.

theorem MvPolynomial.cechBlockProj_eq_zero_of_forall_mem (ι k : Type u) [Field k] (d : ℕ) {n : ℕ} (x : Fin (n + 1) → ι) {F : Finset ι} (hF : ∀ (j : ι), j ∈ F) (z : ↥(polynomialVariableCechTerm ι k d n x)) : (cechBlockProj ι k ⋯ x F) z = 0

The Čech form: any tuple supplies the witness.

Support bookkeeping for the reassembly

theorem MvPolynomial.tupleExponent_support_succAbove (ι : Type u) {n : ℕ} (x : Fin (n + 2) → ι) (j : Fin (n + 2)) : (tupleExponent ι (x ∘ j.succAbove)).support ⊆ (tupleExponent ι x).support

Dropping an index shrinks the support of the tuple exponent.

theorem MvPolynomial.tupleExponent_support_card_le (ι : Type u) {n : ℕ} (x : Fin n → ι) : (tupleExponent ι x).support.card ≤ n

A tuple's exponent is supported on at most its own length: each index contributes one variable, and repetitions only shrink the support.

theorem MvPolynomial.cechBlockProj_eq_zero_of_card_lt (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {d : ℤ} [Fintype ι] (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} (hcard : n + 2 < Fintype.card ι) (y : Fin (n + 2) → ι) {G : Finset ι} (hG : ∀ (j : ι), j ∈ G) (z : ↥(cechTerm ι k 𝓜 y)) : (cechBlockProj ι k h𝓜 y G) z = 0

A tuple too short to meet every variable kills the full block.

This is what carries the vanishing computation at a negative twist, where the degree argument behind cechBlockProj_eq_zero_of_forall_mem is unavailable: a block containing every variable has Fintype.card ι elements, while a tuple of length n + 2 supports at most n + 2, so over a larger variable set the block cannot sit inside the tuple's support and cechBlockProj_eq_zero_of_not_subset applies. The twist plays no part.

This is the first statement in the lane that needs the variable set finite.

theorem MvPolynomial.subset_of_subset_cons (ι : Type u) {n : ℕ} {F : Finset ι} {i₀ : ι} (hi₀ : i₀ ∉ F) (y : Fin (n + 1) → ι) (h : F ⊆ (tupleExponent ι (Fin.cons i₀ y)).support) : F ⊆ (tupleExponent ι y).support

A block of the cone tuple avoiding the cone point is a block of the base tuple.

theorem MvPolynomial.cechTermCongr_symm_cechBlockProj (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} {x₁ x₂ : Fin (n + 1) → ι} (h : x₁ = x₂) (F : Finset ι) (z : ↥(cechTerm ι k 𝓜 x₂)) : (cechTermCongr ι k 𝓜 h).symm ((cechBlockProj ι k h𝓜 x₂ F) z) = (cechBlockProj ι k h𝓜 x₁ F) ((cechTermCongr ι k 𝓜 h).symm z)

The block projections commute with the inverse tuple transport.

The candidate primitive

noncomputable def MvPolynomial.cechBlockPrimitive (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} (F : Finset ι) (s : (x : Fin (n + 2) → ι) → ↥(cechTerm ι k 𝓜 x)) (y : Fin (n + 1) → ι) : ↥(cechTerm ι k 𝓜 y)

The per-block candidate primitive: contract the block-F component of s through the cone point, when one exists. A block with no cone point contributes nothing — and by cechBlockProj_eq_zero_of_forall_mem it has nothing to contribute.

Equations

• One or more equations did not get rendered due to their size.

theorem MvPolynomial.cechBlockPrimitive_of_exists (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} {F : Finset ι} (h : ∃ (i₀ : ι), i₀ ∉ F) (s : (x : Fin (n + 2) → ι) → ↥(cechTerm ι k 𝓜 x)) (y : Fin (n + 1) → ι) : cechBlockPrimitive ι k h𝓜 F s y = (cechHomotopy ι k h𝓜 h.choose y) ((cechBlockProj ι k h𝓜 (Fin.cons h.choose y) F) (s (Fin.cons h.choose y)))

theorem MvPolynomial.cechBlockPrimitive_of_forall (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} {F : Finset ι} (h : ¬∃ (i₀ : ι), i₀ ∉ F) (s : (x : Fin (n + 2) → ι) → ↥(cechTerm ι k 𝓜 x)) (y : Fin (n + 1) → ι) : cechBlockPrimitive ι k h𝓜 F s y = 0

theorem MvPolynomial.cechBlockPrimitive_eq_zero_of_not_subset (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} {F : Finset ι} (s : (x : Fin (n + 2) → ι) → ↥(cechTerm ι k 𝓜 x)) {y : Fin (n + 1) → ι} (h : ¬F ⊆ (tupleExponent ι y).support) : cechBlockPrimitive ι k h𝓜 F s y = 0

The per-block primitive of a block off the tuple's support vanishes: the cone point is outside the block, so the cone tuple's support helps only through the base tuple's.

noncomputable def MvPolynomial.cechPrimitive (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} (s : (x : Fin (n + 2) → ι) → ↥(cechTerm ι k 𝓜 x)) (y : Fin (n + 1) → ι) : ↥(cechTerm ι k 𝓜 y)

The candidate primitive: the finitely many blocks of the tuple, contracted and summed.

Equations

• MvPolynomial.cechPrimitive ι k h𝓜 s y = ∑ F ∈ (MvPolynomial.tupleExponent ι y).support.powerset, MvPolynomial.cechBlockPrimitive ι k h𝓜 F s y

The homotopy computation

theorem MvPolynomial.cechBlockPrimitive_faces_of_exists (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} (s : (x : Fin (n + 2) → ι) → ↥(cechTerm ι k 𝓜 x)) (hs : ∀ (x : Fin (n + 3) → ι), ∑ j : Fin (n + 3), (-1) ^ ↑j • (cechFace ι k 𝓜 x j) (s (x ∘ j.succAbove)) = 0) (x : Fin (n + 2) → ι) {F : Finset ι} (hF : ∃ (i₀ : ι), i₀ ∉ F) : ∑ j : Fin (n + 2), (-1) ^ ↑j • (cechFace ι k 𝓜 x j) (cechBlockPrimitive ι k h𝓜 F s (x ∘ j.succAbove)) = (cechBlockProj ι k h𝓜 x F) (s x)

The per-block homotopy identity, on a block with a cone point. The alternating sum of the faces of the per-block primitive is the block-F component of s x.

Apply the block projection and the homotopy map to the cocycle identity at i₀ :: x: the j = 0 face returns (s x)_F through the retraction, and the j.succ faces are exactly the faces of the per-block primitive, with one sign lost, through the square.

No hypothesis on the twist appears here, and none is needed. Every block except the one containing every variable has a cone point, so this alone says the cohomology of the Čech complex is carried entirely by the full block — which is what makes both the vanishing below the top degree and the finiteness of the top group statements about a single block.

theorem MvPolynomial.cechBlockPrimitive_faces (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} (s : (x : Fin (n + 2) → ι) → ↥(cechTerm ι k 𝓜 x)) (hs : ∀ (x : Fin (n + 3) → ι), ∑ j : Fin (n + 3), (-1) ^ ↑j • (cechFace ι k 𝓜 x j) (s (x ∘ j.succAbove)) = 0) (hfull : ∀ {G : Finset ι}, (∀ (j : ι), j ∈ G) → ∀ (y : Fin (n + 2) → ι), (cechBlockProj ι k h𝓜 y G) (s y) = 0) (x : Fin (n + 2) → ι) (F : Finset ι) : ∑ j : Fin (n + 2), (-1) ^ ↑j • (cechFace ι k 𝓜 x j) (cechBlockPrimitive ι k h𝓜 F s (x ∘ j.succAbove)) = (cechBlockProj ι k h𝓜 x F) (s x)

The per-block homotopy identity, for every block.

With a cone point this is cechBlockPrimitive_faces_of_exists; without one both sides vanish, the left because the per-block primitive is 0 by construction and the right by hfull.

hfull is the only place this argument ever cared about the sign of the twist, and taking it as a hypothesis is what makes the computation available at either sign. It constrains s alone rather than every term, which is what lets the top degree use it: there the full block is not empty and only the given cochain can be assumed to miss it. Three things discharge it, for different reasons:

• a nonnegative twist — cechBlockProj_eq_zero_of_forall_mem. Every Laurent exponent in such a block is negative in every variable while their total is d ≥ 0, so the block is empty;
• a tuple too short to meet every variable — cechBlockProj_eq_zero_of_card_lt. A tuple of length n + 2 has support of at most that size, so over a variable set with more elements the full block is not contained in it, whatever the twist;
• a cochain already carrying no full block, whatever the twist and however long the tuple. This is the top-degree use, where neither of the first two is available.

The second is what carries the negative case below the top, and it is why finiteness of the variable set enters the lane here and nowhere earlier.

theorem MvPolynomial.cechPrimitive_isPrimitive (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} (s : (x : Fin (n + 2) → ι) → ↥(cechTerm ι k 𝓜 x)) (hs : ∀ (x : Fin (n + 3) → ι), ∑ j : Fin (n + 3), (-1) ^ ↑j • (cechFace ι k 𝓜 x j) (s (x ∘ j.succAbove)) = 0) (hfull : ∀ {G : Finset ι}, (∀ (j : ι), j ∈ G) → ∀ (y : Fin (n + 2) → ι), (cechBlockProj ι k h𝓜 y G) (s y) = 0) (x : Fin (n + 2) → ι) : ∑ j : Fin (n + 2), (-1) ^ ↑j • (cechFace ι k 𝓜 x j) (cechPrimitive ι k h𝓜 s (x ∘ j.succAbove)) = s x

The vanishing computation. The alternating face sum of cechPrimitive s is s: per block the previous identity applies — after extending each tuple's block sum to the blocks of x, which costs nothing since a block off a tuple's support contributes zero — and the block components of s x reassemble by sum_cechBlockProj.