Free coherent sheaves on an affine noetherian scheme

𝒪^k on Spec R, as the coherent sheaf tilde (Fin k → R), with the three facts the affine Ext comparison consumes:

• it is projective among coherent sheaves, because Fin k → R is projective among finitely generated modules and affineTilde is a left adjoint whose right adjoint is an equivalence (Adjunction.map_projective);
• its underlying module sheaf is a biproduct of k copies of 𝒪, because tilde is additive and tilde R = 𝒪;
• every coherent sheaf is a quotient of some 𝒪^k, because every finitely generated module is a quotient of a free module of finite rank and Coh (Spec R) ≌ FGModuleCat R.

Coh.affineFree is an abbreviation so that instance search sees through it to affineTilde.obj _.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Coh.affineFree {R : CommRingCat} [IsNoetherianRing ↑R] (k : ℕ) : Coh (Spec R)

𝒪^k as a coherent sheaf on Spec R: tilde of the free module of rank k.

Equations

• AlgebraicGeometry.Coh.affineFree k = AlgebraicGeometry.FGModuleCat.affineTilde.obj (FGModuleCat.of (↑R) (Fin k → ↑R))

theorem AlgebraicGeometry.Coh.projective_affineFree {R : CommRingCat} [IsNoetherianRing ↑R] (k : ℕ) : CategoryTheory.Projective (affineFree k)

𝒪^k is projective among coherent sheaves on an affine noetherian scheme.

noncomputable def AlgebraicGeometry.Coh.ιAffineFreeIso {R : CommRingCat} [IsNoetherianRing ↑R] (k : ℕ) : (ι (Spec R)).obj (affineFree k) ≅ ⨁ fun (x : Fin k) => (tilde.functor R).obj (ModuleCat.of ↑R ↑R)

The underlying module sheaf of 𝒪^k is a biproduct of k copies of 𝒪.

Equations

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

theorem AlgebraicGeometry.Coh.exists_affineFree_epi {R : CommRingCat} [IsNoetherianRing ↑R] (X : Coh (Spec R)) : ∃ (P : Coh (Spec R)) (p : P ⟶ X), (∃ (k : ℕ), P = affineFree k) ∧ CategoryTheory.Epi p

Every coherent sheaf on Spec R is a quotient of some 𝒪^k.