The full blocks of a Čech degree, assembled

LaurentFinite.lean shows the full block of one localization is a finite-dimensional k-space, stated at the monomial denominator Xᵞ. A Čech term is the same object at the denominator ∏ Xₓₐ, which is that monomial — tupleDenominator_eq — but not syntactically, so the subspace has to be carried across. powersCongrLinear is the transport, and it is k-linear for the same reason its additive form exists at all: it moves nothing but the name of the type.

Two finiteness facts, both needed

fg_cechBlockSpan is one tuple: finitely many Laurent exponents can be negative in every variable at a fixed total degree. module_finite_pi_cechBlockSpan is all tuples at once, and it is a different fact: a Čech index has fixed length and ι is finite, so there are finitely many of them. Neither implies the other, and the top-degree argument needs both — which is why Fintype ι appears twice over in this lane rather than once.

Scope

The cochain side only. Nothing here mentions the differential, cocycles, or cohomology, and the k-action used is degreeZeroLocalizationModule — matching it against the cechScalarAction that module_finite_linearCoherentH_of_cech consumes is a separate step and is not done here.

noncomputable def MvPolynomial.powersCongrLinear (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓜 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {f g : MvPolynomial ι k} (h : f = g) : ↥(GradedModule.DegreeZeroLocalization (polynomialGrading ι k) 𝓜 (Submonoid.powers f)) ≃ₗ[k] ↥(GradedModule.DegreeZeroLocalization (polynomialGrading ι k) 𝓜 (Submonoid.powers g))

powersCongr as a k-linear equivalence. It moves nothing but the name of the type, so linearity is the same subst its additive form is.

Equations

• MvPolynomial.powersCongrLinear ι k 𝓜 h = h ▸ LinearEquiv.refl k ↥(GradedModule.DegreeZeroLocalization (MvPolynomial.polynomialGrading ι k) 𝓜 (Submonoid.powers f))

theorem MvPolynomial.powersCongrLinear_apply (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓜 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {f g : MvPolynomial ι k} (h : f = g) (z : ↥(GradedModule.DegreeZeroLocalization (polynomialGrading ι k) 𝓜 (Submonoid.powers f))) : (powersCongrLinear ι k 𝓜 h) z = (GradedModule.DegreeZeroLocalization.powersCongr h) z

theorem MvPolynomial.powersCongrLinear_symm_apply (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓜 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] {f g : MvPolynomial ι k} (h : f = g) (z : ↥(GradedModule.DegreeZeroLocalization (polynomialGrading ι k) 𝓜 (Submonoid.powers g))) : (powersCongrLinear ι k 𝓜 h).symm z = (GradedModule.DegreeZeroLocalization.powersCongr h).symm z

noncomputable def MvPolynomial.cechBlockSpan (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓜 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] (d : ℤ) {n : ℕ} (x : Fin (n + 1) → ι) : Submodule k ↥(GradedModule.DegreeZeroLocalization (polynomialGrading ι k) 𝓜 (Submonoid.powers (polynomialVariableCechDenominator ι k x)))

The full block of a Čech term, as a k-subspace: the block of the monomial presentation, carried back along the denominator comparison.

Definable without finiteness of ι — only its finite generation needs that.

Equations

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

theorem MvPolynomial.cechBlockProj_mem_cechBlockSpan (ι 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) {n : ℕ} (x : Fin (n + 1) → ι) (z : ↥(cechTerm ι k 𝓜 x)) : (cechBlockProj ι k h𝓜 x Finset.univ) z ∈ cechBlockSpan ι k 𝓜 d x

The full-block projection of any term lands in that subspace.

theorem MvPolynomial.fg_cechBlockSpan (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓜 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] [Fintype ι] (d : ℤ) {n : ℕ} (x : Fin (n + 1) → ι) : (cechBlockSpan ι k 𝓜 d x).FG

The full block of a Čech term is finitely generated.

instance MvPolynomial.module_finite_pi_cechBlockSpan (ι k : Type u) [Field k] {σM : Type u} [SetLike σM (MvPolynomial ι k)] [AddSubgroupClass σM (MvPolynomial ι k)] (𝓜 : ℕ → σM) [SetLike.GradedSMul (polynomialGrading ι k) 𝓜] [Fintype ι] (d : ℤ) {n : ℕ} : Module.Finite k ((x : Fin (n + 1) → ι) → ↥(cechBlockSpan ι k 𝓜 d x))

The full blocks of all tuples together are finite-dimensional.

Two finiteness facts meet here and neither is enough alone: each block is finitely generated because only finitely many Laurent exponents are negative in every variable, and there are only finitely many tuples because ι is finite and a Čech index has fixed length.