The bounded-coherent identification on affine noetherian schemes

CoherentExtComparison (Spec R) for a noetherian ring R, hence HasBoundedCoherentDqcIdentification (Spec R) through Dqc/Identification.lean.

The Ext comparison is Functor.bijective_mapExtAddHom_of_generators applied to Coh.ι (Spec R) with the free sheaves 𝒪^k as generators:

• every coherent sheaf is a quotient of some 𝒪^k (Coh.exists_affineFree_epi);
• Ext^(n+1) (𝒪^k, G) vanishes in Coh (Spec R) because 𝒪^k is projective there (Coh.projective_affineFree);
• Ext^(n+1) (𝒪^k, G) vanishes in all module sheaves because it is H^(n+1)(G)^k (Scheme.Modules.extUnitAddEquivDerivedH, Ext.subsingleton_biproduct_left) and quasi-coherent sheaves on an affine scheme have no higher cohomology (modules_H_subsingleton_of_isQuasicoherent);
• Coh.ι is fully faithful, so bijective on Ext⁰.

This is the first scheme marked as satisfying CoherentExtComparison. The general case remains open; see docs/architecture/cutover-ledger.md.

theorem AlgebraicGeometry.DerivedCategory.Dqc.subsingleton_ext_ι_affineFree {R : CommRingCat} [IsNoetherianRing ↑R] (k : ℕ) (Y : Coh (Spec R)) (n : ℕ) : Subsingleton (CategoryTheory.Abelian.Ext ((Coh.ι (Spec R)).obj (Coh.affineFree k)) ((Coh.ι (Spec R)).obj Y) (n + 1))

Ext^(n+1) (𝒪^k, G) in all module sheaves vanishes for coherent G on Spec R: it is H^(n+1)(G)^k, and quasi-coherent sheaves on an affine scheme have no higher cohomology.

theorem AlgebraicGeometry.DerivedCategory.Dqc.coherentExtComparison_spec {R : CommRingCat} [IsNoetherianRing ↑R] : CoherentExtComparison (Spec R)

The coherent Ext comparison holds on affine noetherian schemes.

theorem AlgebraicGeometry.DerivedCategory.Dqc.hasBoundedCoherentDqcIdentification_spec {R : CommRingCat} [IsNoetherianRing ↑R] : HasBoundedCoherentDqcIdentification (Spec R)

The bounded-coherent identification holds on affine noetherian schemes.