The per-index Čech comparison is k-linear

intCechTermSectionAddEquiv_smul says the comparison between a Čech term and its sections respects the base-field action. intCechIndexEquiv is that comparison composed with one transport, because a Čech index names sections over a categorical product of charts while the term comparison is stated over a basic open, and piObj_polynomialVariableChart only says those two opens are equal. This file carries the linearity across that transport.

The transport is the whole content

eqToIso_transport_varietyScalarAction is subst h; rfl — moving sections along an equality of opens cannot fail to commute with anything. All the difficulty is in getting the statement to elaborate, and that difficulty has a single diagnosed cause.

The scalar-type rule, and why it is not a diamond to be fixed

Γ(Proj 𝒜, U) and (ProjectiveSpectrum.Proj.structureSheaf 𝒜).1.obj (op U) are definitionally equal at default transparency and not at reducible transparency. Instance search runs at reducible. The Module instance on associated-sheaf sections is stated over the second, so a • whose left factor is written as the first leaves HSMul unsolved — even though the two are the same type.

That is the same shape as #662, where Coh X carries two Preadditive instances defeq at default but not at reducible. So the obvious repair — adding a second Module instance over (Proj 𝒜).presheaf.obj — would reproduce that bug rather than fix this one: lemmas stated against one instance would stop applying to goals carrying the other.

The rule instead is a convention, and it costs nothing:

• state scalar actions on sections with varietyScalarAction's app, never with •. That form always elaborates, and it is the definitionally canonical one anyway;
• convert to • with varietyScalarAction_app_eq only inside a proof, where the expected type is already fixed and search has what it needs;
• when a scalar genuinely has to be named, give it a definition with an explicit result type — constSectionOn is that, and it is the only such definition needed so far.

Occurrences before the rule was written down: cechBlockSpan (#670), constSection and constSectionOn (#674), and the transport here.

Next

Degreewise linearity of intCechCochainsDegreewiseAddEquiv is a product of this over the tuple index; the homology statement r • [s] = [r • s] is then homologyπ naturality. Neither is here.

theorem AlgebraicGeometry.Proj.eqToIso_transport_varietyScalarAction (ι k : Type u) [Field k] (d : ℤ) {W W' : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top (MvPolynomial.polynomialGrading ι k))} (h : W = W') (r : k) (s : ↑((intTwistPresheaf ι k d).obj (Opposite.op W))) : (CategoryTheory.eqToIso ⋯).addCommGroupIsoToAddEquiv ((ModuleCat.Hom.hom (((Cohomology.varietyScalarAction (Proj (MvPolynomial.polynomialGrading ι k)) (associatedSheaf (MvPolynomial.polynomialGrading ι k) (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d))) r).val.app (Opposite.op W))) s) = (ModuleCat.Hom.hom (((Cohomology.varietyScalarAction (Proj (MvPolynomial.polynomialGrading ι k)) (associatedSheaf (MvPolynomial.polynomialGrading ι k) (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d))) r).val.app (Opposite.op W'))) ((CategoryTheory.eqToIso ⋯).addCommGroupIsoToAddEquiv s)

Transport along an equality of opens commutes with the endomorphism a scalar induces.

theorem AlgebraicGeometry.Proj.intCechTermSectionAddEquiv_symm_varietyScalarAction (ι k : Type u) [Field k] (d : ℤ) {n : ℕ} (x : Fin (n + 1) → ι) (r : k) (w : (associatedSheafInType (MvPolynomial.polynomialGrading ι k) (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d)).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen (MvPolynomial.polynomialGrading ι k) (MvPolynomial.polynomialVariableCechDenominator ι k x)))) : (intCechTermSectionAddEquiv ι k d x).symm ((ModuleCat.Hom.hom (((Cohomology.varietyScalarAction (Proj (MvPolynomial.polynomialGrading ι k)) (associatedSheaf (MvPolynomial.polynomialGrading ι k) (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d))) r).val.app (Opposite.op (ProjectiveSpectrum.basicOpen (MvPolynomial.polynomialGrading ι k) (MvPolynomial.polynomialVariableCechDenominator ι k x))))) w) = r • (intCechTermSectionAddEquiv ι k d x).symm w

The symm form of the term-level comparison lemma, against the sheaf endomorphism.

theorem AlgebraicGeometry.Proj.intCechIndexEquiv_smul (ι k : Type u) [Field k] (d : ℤ) {n : ℕ} (x : Fin (n + 1) → ι) (r : k) (s : ↑((intTwistPresheaf ι k d).obj (Opposite.op (∏ᶜ polynomialVariableChart ι k ∘ x)))) : (intCechIndexEquiv ι k d x) ((ModuleCat.Hom.hom (((Cohomology.varietyScalarAction (Proj (MvPolynomial.polynomialGrading ι k)) (associatedSheaf (MvPolynomial.polynomialGrading ι k) (GradedModule.intShift (MvPolynomial.polynomialGrading ι k) d))) r).val.app (Opposite.op (∏ᶜ polynomialVariableChart ι k ∘ x)))) s) = r • (intCechIndexEquiv ι k d x) s

The per-index comparison is k-linear.