Quasi-coherent modules on an affine scheme

The category of quasi-coherent modules on an affine scheme X is abelian and has enough injectives. Pullback along X.isoSpec and Mathlib's tilde equivalence identify it with ModuleCat Γ(X, ⊤). These are the category theoretic inputs for deriving exact global sections.

noncomputable def TauCeti.AlgebraicGeometry.QuasicoherentSheaf.affineEquiv (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : QuasicoherentSheaf X ≌ ModuleCat ↑(X.presheaf.obj (Opposite.op ⊤))

Quasi-coherent modules on an affine scheme are equivalent to modules over its global sections.

Equations

• TauCeti.AlgebraicGeometry.QuasicoherentSheaf.affineEquiv X = (TauCeti.AlgebraicGeometry.QuasicoherentSheaf.equivOfIso X.isoSpec).symm.trans AlgebraicGeometry.tildeEquiv.symm

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.affineEquiv_functor (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : (affineEquiv X).functor = (pullback X.isoSpec.inv).comp AlgebraicGeometry.tildeEquiv.inverse

The forward functor of the affine equivalence is pullback to the spectrum followed by global sections.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.affineEquiv_inverse (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : (affineEquiv X).inverse = AlgebraicGeometry.tildeEquiv.functor.comp (pullback X.isoSpec.hom)

The inverse functor of the affine equivalence is tilde followed by pullback to the affine scheme.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.QuasicoherentSheaf.instAbelianOfIsAffine (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : CategoryTheory.Abelian (QuasicoherentSheaf X)

Quasi-coherent modules on an affine scheme form an abelian category.

Equations

• TauCeti.AlgebraicGeometry.QuasicoherentSheaf.instAbelianOfIsAffine X = CategoryTheory.abelianOfEquivalence (TauCeti.AlgebraicGeometry.QuasicoherentSheaf.affineEquiv X).functor

instance TauCeti.AlgebraicGeometry.QuasicoherentSheaf.instEnoughInjectivesOfIsAffine (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : CategoryTheory.EnoughInjectives (QuasicoherentSheaf X)

Quasi-coherent modules on an affine scheme admit injective resolutions.