The block homotopy on the variable Čech cover #
The block projections and the contracting homotopy of #340 live at monomial denominators
Xᵞ, while the Čech complex of the variable cover names its denominators as products
∏ₐ X_{x a}. The two are equal ring elements, and this file carries the whole toolkit across
that equality: tupleExponent is the exponent vector of a Čech tuple,
DegreeZeroLocalization.powersCongr transports a degree-zero localization along an equality of
denominators, and the Čech-level cechBlockProj and cechHomotopy are the monomial-level maps
conjugated by that transport.
The payoff is the three identities the vanishing computation runs on, now stated against
polynomialVariableCechFace itself:
cechFace_cechBlockProj— the Čech faces commute with the block projections;cechHomotopy_cechFace_zero— the homotopy retracts the cone face on a block (i₀ ∉ F);cechHomotopy_cechFace_succ— the homotopy commutes with every other face, unrestricted.
together with sum_cechBlockProj (the finitely many blocks of a tuple exhaust its term) and
cechBlockProj_eq_zero_of_not_subset (a block off the tuple's support is zero), which are what
the reassembly of per-block primitives sums over.
Implementation notes #
powersCongr is defined by subst and every one of its equations is proved by subst plus
proof irrelevance — the transported element never moves, only its type's name does. The face
transport powersCongr_faceMap takes equalities for both denominators and the face's
multiplier, because the Čech side multiplies by X i and the monomial side by
monomial (single i 1) 1; the two are definitionally equal, but keeping the equality explicit
lets one lemma serve every instantiation.
The Fin.cons combinatorics is isolated in two lemmas — the 0-face of a cone tuple is the
base tuple, and the j.succ-face of a cone tuple is the cone over the j-face — so the
vanishing computation never touches succAbove directly.
Tags #
Čech complex, contracting homotopy, block decomposition, multivariate polynomial
The exponent vector of a Čech tuple #
The exponent vector of the Čech denominator of a tuple: one for each occurrence of each variable.
Equations
- MvPolynomial.tupleExponent ι x = ∑ a : Fin n, Finsupp.single (x a) 1
Instances For
The Čech denominator is the monomial with exponent tupleExponent. This is the equality
everything in this file transports along.
Prepending a cone point adds one power of its variable.
The cone denominator in monomial form, split at the cone variable.
The 0-face of a cone tuple is the base tuple.
The Čech term in monomial form #
The Čech term of a tuple, presented at the monomial denominator.
Equations
Instances For
The comparison carries a Čech face to the monomial-level face at the same variable.
The block projections on Čech terms #
The block projection of a Čech term: the monomial-level blockProj conjugated by the
denominator comparison.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The finitely many blocks of a tuple exhaust its term.
The block projections are idempotent, transported from blockProj_blockProj_self.
A block off the tuple's support is zero.
The Čech faces commute with the block projections. The transported form of
laurentFace_blockProj: the differential preserves every block.
The homotopy map on Čech terms #
The homotopy map on Čech terms: the monomial-level laurentHomotopy conjugated by the
denominator comparisons of the cone tuple and the base tuple.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Transport along an equality of tuples #
The faces of a cone tuple land at tuples like (i₀ :: x) ∘ (j.succ).succAbove, which equal
i₀ :: (x ∘ j.succAbove) only propositionally. The transport, and the one dependent-rewriting
lemma every use reduces to: a cochain takes transported values at equal tuples.
Transport a Čech term along an equality of tuples.
Equations
Instances For
A cochain takes transported values at equal tuples. This is the whole of the dependent rewriting the vanishing computation needs.
The block projections commute with tuple transport.
The homotopy identities on Čech terms #
laurentHomotopy_laurentFace_comm with the enlarged denominator's exponent named by a
hypothesis rather than fixed as γ₀ + single e 1. The Čech caller's exponent is
tupleExponent x, which equals that sum only propositionally.
The homotopy retracts the cone face on a block. The Čech form of
laurentHomotopy_laurentFace_blockProj: for i₀ ∉ F, restricting a block-F element of the
base tuple along the 0-face of the cone tuple and applying the homotopy gives it back. The
transport on the face's input names the tuple identity (i₀ :: y) ∘ δ₀ = y.
The homotopy commutes with every other face. The Čech form of
laurentHomotopy_laurentFace_comm, with no restriction on the block or the face's variable.
The transport on the face's input names the tuple identity
(i₀ :: x) ∘ δ_{j.succ} = i₀ :: (x ∘ δⱼ).