feat(AlgebraicGeometry): direct summand theorem and derived variant

[alreadydone]

No description provided.

[kim-em]

🤖 Claude says:

Three changes, one of them a soundness bug.

direct_summand is false as stated. It assumes Module.Finite A B but not that A → B is injective, so B need not be an extension of A. Counterexample at A = ℤ, B = ZMod 2 (both IsRegularRing ℤ and Module.Finite ℤ (ZMod 2) are found by infer_instance):

example : ¬ (∃ π : (ZMod 2) →ₗ[ℤ] ℤ, π ∘ₗ Algebra.linearMap ℤ (ZMod 2) = .id) := by
  rintro ⟨π, hπ⟩
  have h1 : π (Algebra.linearMap ℤ (ZMod 2) 1) = 1 := by
    rw [← LinearMap.comp_apply, hπ]; rfl
  have h2 : (2 : ℤ) • (Algebra.linearMap ℤ (ZMod 2) 1) = 0 := by decide
  have h3 := π.map_smul (2 : ℤ) (Algebra.linearMap ℤ (ZMod 2) 1)
  rw [h2, map_zero, h1] at h3
  simp at h3

Adding (hinj : Function.Injective (algebraMap A B)) fixes it.

The file does not compile. open CategoryTheory AlgebraicGeometry sits inside namespace LeanEval.AlgebraicGeometry.DirectSummand, so AlgebraicGeometry resolves to the enclosing LeanEval.AlgebraicGeometry and the scoped Γ(_, _) notation never comes into scope:

DirectSummand.lean:66:19: error: unexpected token '('; expected ':=' or '|'

open CategoryTheory _root_.AlgebraicGeometry fixes it, and with that one change the whole file elaborates clean. (#516 avoids this by putting the open before the namespace.)

manifests/problems/direct_summand.lean needs to be .toml. This is also why CI is green despite the compile error: loadManifest only reads *.toml, and both validate-manifest and check-problem-build take their work list from it, so the module is never built and the problem is not in the benchmark at all.

On derived_direct_summand itself, I traced the composite and it says the right thing. singleFunctor.map (ofHom (Algebra.linearMap A Γ(X, ⊤))) is A[0] ⟶ Γ(X, 𝒪_X)[0], and rightDerivedFunctorPlusUnit' at SheafOfModules.unit is (F ⋙ single).obj 𝒪_X ⟶ (single ⋙ RF).obj 𝒪_X, i.e. Γ(X, 𝒪_X)[0] ⟶ RΓ(X, 𝒪_X), so IsSplitMono of the composite is exactly de Jong's splitting. No hypotheses are missing: Noetherianity comes with IsRegularRing (it extends IsNoetherianRing), and quasi-compactness comes from UniversallyClosed. Two remarks:

• Once direct_summand gains the injectivity hypothesis it becomes a corollary of derived_direct_summand: take X = Spec B, where module-finite plus injective makes Spec B ⟶ Spec A finite hence proper, and surjective by lying over, with RΓ(Spec B, 𝒪) = B. Worth deciding whether you want both as separate holes.
• EnoughInjectives (SheafOfModules X.ringCatSheaf) is true but handed to the solver, so the statement's meaning depends on a supplied instance rather than a canonical one. Harmless, since all choices give canonically isomorphic derived functors, but worth a conscious decision.

[alreadydone]

Thanks to Claude for catching the error in the statement of direct_summand: I've added the necessary FaithfulSMul condition, equivalent to injectivity of the algebraMap. I moved the statement to the end, since it follows from the derived version, as you pointed out.

I moved open CategoryTheory AlgebraicGeometry before entering the LeanEval.AlgebraicGeometry namespace so it's working properly.

CategoryTheory.EnoughInjectives is Prop, so the statement doesn't depend on specific proofs of the Prop.