The base field acting on a homogeneous localization, and the finiteness of a full block

LaurentBlock.lean decomposes an away localization by the negative support of the Laurent exponent and proves the combinatorial fact the top cohomology of Pⁿ rests on: finite_setOf_degree_eq_of_neg, that only finitely many exponents are negative in every variable at a fixed total degree. This file turns that count into a statement about the localization itself.

Why the base field has to appear

Everything in the Čech lane is valued in abelian groups, and "finitely many exponents" is not by itself a finiteness statement about a group: the block is a k-vector space, and it is spanned — not generated as an abelian group — by the corresponding monomial fractions. So the k-action has to be named before the count can be used.

It is not extra data. A constant is a degree-zero homogeneous element, so k maps into every homogeneous localization through HomogeneousLocalization.fromZeroRingHom, and degreeZeroLocalizationModule is the restriction of scalars along that map. awayMk_smul is the computation that makes it usable: scaling a fraction scales its numerator.

The spanning argument

blockProj_univ_mem_span decomposes an arbitrary element into monomial fractions, filters to the full block, strips each coefficient with awayMk_smul, and replaces each monomial fraction by blockRep of its Laurent exponent. The replacement is what makes the spanning family fixed rather than dependent on the element, and it is sound because the Laurent exponent is a complete invariant (awayMk_monomial_eq_iff_laurentExponent).

Scope

One localization. Assembling the blocks of a Čech cochain, and matching this action against the cechScalarAction that module_finite_linearCoherentH_of_cech consumes, are separate and are not done here.

noncomputable def MvPolynomial.polynomialToHomogeneousLocalization (ι k : Type u) [Field k] (S : Submonoid (MvPolynomial ι k)) : k →+* HomogeneousLocalization (polynomialGrading ι k) S

The base field acts on every homogeneous localization of the polynomial ring, through the constants — which are exactly the degree-zero part of the grading.

Equations

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

@[implicit_reducible]

noncomputable instance MvPolynomial.degreeZeroLocalizationModule (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓜 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] (S : Submonoid (MvPolynomial ι k)) : Module k ↥(GradedModule.DegreeZeroLocalization (polynomialGrading ι k) 𝓜 S)

The base field acting on a degree-zero homogeneous localization, by restriction of scalars along polynomialToHomogeneousLocalization.

Equations

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

theorem MvPolynomial.awayMk_smul (ι 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) {f : MvPolynomial ι k} {e : ℕ} (hf : f ∈ polynomialGrading ι k e) (n : ℕ) (c : k) (p : MvPolynomial ι k) (hp : p ∈ 𝓜 (n • e)) : c • GradedModule.DegreeZeroLocalization.awayMk hf n p hp = GradedModule.DegreeZeroLocalization.awayMk hf n (c • p) ⋯

The base field acts on the numerator. Scalar multiplication on a fraction p / fⁿ is scalar multiplication on p, because a constant is a degree-zero homogeneous element with denominator 1. This is what lets a spanning argument strip coefficients off monomials.

The full block is finitely spanned

theorem MvPolynomial.awayMk_congr (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓜 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {f : MvPolynomial ι k} {e : ℕ} (hf : f ∈ polynomialGrading ι k e) (n : ℕ) {p q : MvPolynomial ι k} (hp : p ∈ 𝓜 (n • e)) (hq : q ∈ 𝓜 (n • e)) (h : p = q) : GradedModule.DegreeZeroLocalization.awayMk hf n p hp = GradedModule.DegreeZeroLocalization.awayMk hf n q hq

Numerator congruence for awayMk, so a rewrite under the membership certificate does not have to fight a non-type-correct motive.

theorem MvPolynomial.monomial_one_mem_of_mem_support (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] (𝓜 : ℕ → σM) {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} {q : MvPolynomial ι k} (hq : q ∈ 𝓜 n) {β : ι →₀ ℕ} (hβ : β ∈ q.support) : (monomial β) 1 ∈ 𝓜 n

Every monomial of a numerator is itself a numerator with coefficient one: the coefficient plays no part in the degree bookkeeping.

theorem MvPolynomial.intNegSupport_of_mem_support_laurentFilter (ι k : Type u) [Field k] (γ : ι →₀ ℕ) (m : ℕ) (F : Finset ι) (p : MvPolynomial ι k) {β : ι →₀ ℕ} (hβ : β ∈ (laurentFilter γ m F p).support) : intNegSupport (γ.laurentExponent m β) = F

A monomial surviving the filter has the filtered block as its negative support.

noncomputable def MvPolynomial.blockRep (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓜 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] (γ : ι →₀ ℕ) (α : ι →₀ ℤ) : ↥(GradedModule.DegreeZeroLocalization (polynomialGrading ι k) 𝓜 (Submonoid.powers ((monomial γ) 1)))

A monomial fraction with a prescribed Laurent exponent, chosen once and for all.

Every monomial fraction with that exponent equals it, so a spanning argument can name a fixed finite family instead of one depending on the element being decomposed.

Equations

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

theorem MvPolynomial.awayMk_eq_blockRep (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓜 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] (γ : ι →₀ ℕ) {m : ℕ} {β : ι →₀ ℕ} (h : (monomial β) 1 ∈ 𝓜 (m • Finsupp.degree γ)) : GradedModule.DegreeZeroLocalization.awayMk ⋯ m ((monomial β) 1) h = blockRep ι k 𝓜 γ (γ.laurentExponent m β)

The Laurent exponent selects the representative. A monomial fraction is the chosen representative of its own exponent — awayMk_monomial_eq_iff_laurentExponent is what makes the choice harmless.

theorem MvPolynomial.blockProj_univ_mem_span (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓜 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] [Fintype ι] {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) (γ : ι →₀ ℕ) (z : ↥(GradedModule.DegreeZeroLocalization (polynomialGrading ι k) 𝓜 (Submonoid.powers ((monomial γ) 1)))) : blockProj h𝓜 γ Finset.univ z ∈ Submodule.span k (blockRep ι k 𝓜 γ '' {α : ι →₀ ℤ | Finsupp.degree α = d ∧ ∀ (j : ι), α j < 0})

The full block lies in the span of a fixed family indexed by a finite exponent set.

Decompose into monomial fractions, filter to the full block, strip each coefficient with awayMk_smul, and replace each monomial fraction by the representative of its exponent. What survives is indexed by exponents that are negative in every variable and of total degree d — the set finite_setOf_degree_eq_of_neg shows is finite.

theorem MvPolynomial.fg_blockSpan (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓜 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] [Fintype ι] {d : ℤ} (γ : ι →₀ ℕ) : (Submodule.span k (blockRep ι k 𝓜 γ '' {α : ι →₀ ℤ | Finsupp.degree α = d ∧ ∀ (j : ι), α j < 0})).FG

The full block of one localization is a finite-dimensional k-space.

finite_setOf_degree_eq_of_neg bounds the exponents that can appear — every coordinate negative with a fixed total — and blockProj_univ_mem_span says nothing outside that family is needed.

theorem MvPolynomial.smul_mk (ι 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) (S : Submonoid (MvPolynomial ι k)) (c : GradedModule.NumDenSameDeg (polynomialGrading ι k) 𝓜 S) (r : k) : r • GradedModule.DegreeZeroLocalization.mk c = GradedModule.DegreeZeroLocalization.mk { deg := c.deg, num := ⟨r • ↑c.num, ⋯⟩, den := c.den, den_mem := ⋯ }

Scaling a fraction scales its numerator, at a general homogeneous denominator. The awayMk form is the special case the spanning argument uses; this is the one the section comparison needs, where the denominator is not a power.

theorem MvPolynomial.mapOfLE_smul (ι 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) {S T : Submonoid (MvPolynomial ι k)} (h : S ≤ T) (r : k) (z : ↥(GradedModule.DegreeZeroLocalization (polynomialGrading ι k) 𝓜 S)) : (GradedModule.DegreeZeroLocalization.mapOfLE h) (r • z) = r • (GradedModule.DegreeZeroLocalization.mapOfLE h) z

Enlarging the denominator submonoid is k-linear. Both sides are the same fraction with the same numerator scaled; mapOfLE_mk makes that visible.