Weighted degree cancellation over finite-support fibers #
This file upgrades the unweighted finite-family constant-extension identity to finitely supported multiplicities. The ambient types need not be finite: a nonzero downstairs coefficient forces every point in its fiber into the finite upstairs support, so the relevant fiber can be counted there.
theorem
Finsupp.sum_mul_degree_eq_of_div_gcd_fibers
{Base : Type u_1}
{Up : Type u_2}
(down : Up → Base)
(baseDegree : Base → ℕ)
(upDegree : Up → ℕ)
(baseMultiplicity : Base →₀ ℕ)
(upMultiplicity : Up →₀ ℕ)
(extensionDegree : ℕ)
(hmultiplicity : ∀ (Q : Up), upMultiplicity Q = baseMultiplicity (down Q))
(hdegree : ∀ (Q : Up), upDegree Q = baseDegree (down Q) / extensionDegree.gcd (baseDegree (down Q)))
(hfiber : ∀ (P : Base), Nat.card { Q : Up // down Q = P } = extensionDegree.gcd (baseDegree P))
:
Weighted form of the constant-extension degree cancellation. Suppose
upstairs multiplicities are pulled back from downstairs, upstairs degrees are
obtained by division by gcd(r, degree), and the full fiber has that gcd as
its cardinality. Then the two finitely supported weighted degree sums agree.
No finiteness assumption is imposed on Base or Up; only the supports of
the two Finsupps are used as finite indexing sets.