@[reducible, inline]

abbrev Proposition18.Scheme.Qcoh (X : AlgebraicGeometry.Scheme) : Type (u + 1)

The category of quasi-coherent sheaves of modules on a scheme X, realized as the full subcategory of X.Modules cut out by the quasi-coherence property.

def Proposition18.Scheme.Qcoh.incl (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor (Qcoh X) X.Modules

Inclusion of quasi-coherent sheaves on X into all sheaves of modules on X.

noncomputable def Proposition18.tildeFunctorToQcoh (R : CommRingCat) : CategoryTheory.Functor (ModuleCat ↑R) (Scheme.Qcoh (AlgebraicGeometry.Spec R))

The tilde functor M ↦ M̃ viewed with codomain the quasi-coherent subcategory of (Spec R).Modules; sends an R-module to the associated quasi-coherent sheaf on Spec R.

noncomputable def Proposition18.tilde_fullyFaithful (R : CommRingCat) : (AlgebraicGeometry.tilde.functor R).FullyFaithful

The tilde functor Mod R → (Spec R).Modules is fully faithful, the fundamental input to Thm 11.1 / Thm 12.1.

noncomputable def Proposition18.tildeGammaAdj (R : CommRingCat) : AlgebraicGeometry.tilde.functor R ⊣ AlgebraicGeometry.moduleSpecΓFunctor

The adjunction tilde ⊣ Γ between the tilde functor and the global-sections functor, one half of the equivalence Mod R ≃ QCoh(Spec R).

theorem Proposition18.tilde_isQuasicoherent {R : CommRingCat} (M : ModuleCat ↑R) : SheafOfModules.IsQuasicoherent (AlgebraicGeometry.tilde M)

For any R-module M, the sheaf M̃ on Spec R is quasi-coherent (Cor 16).

instance Proposition18.tildeFunctorToQcoh_full (R : CommRingCat) : (tildeFunctorToQcoh R).Full

tildeFunctorToQcoh R is full: every map between tilde sheaves comes from a module map, lifted from fullness of the underlying tilde functor.

instance Proposition18.tildeFunctorToQcoh_faithful (R : CommRingCat) : (tildeFunctorToQcoh R).Faithful

tildeFunctorToQcoh R is faithful: two R-module maps with equal tilde images coincide.

theorem Proposition18.isQuasicoherent_of_mem_essImage_tilde {R : CommRingCat} {ℱ : (AlgebraicGeometry.Spec R).Modules} (h : (AlgebraicGeometry.tilde.functor R).essImage ℱ) : SheafOfModules.IsQuasicoherent ℱ

If a sheaf of modules ℱ on Spec R is in the essential image of the tilde functor, then it is quasi-coherent.

theorem Proposition18.mem_essImage_tilde_of_isQuasicoherent {R : CommRingCat} (ℱ : (AlgebraicGeometry.Spec R).Modules) [hℱ : SheafOfModules.IsQuasicoherent ℱ] : (AlgebraicGeometry.tilde.functor R).essImage ℱ

Converse direction (Thm 12.1): every quasi-coherent sheaf on Spec R arises (up to isomorphism) as M̃ for some R-module M.

theorem Proposition18.mem_essImage_tilde_iff_isQuasicoherent {R : CommRingCat} (ℱ : (AlgebraicGeometry.Spec R).Modules) : (AlgebraicGeometry.tilde.functor R).essImage ℱ ↔ SheafOfModules.IsQuasicoherent ℱ

Characterization (Thm 11.1 / Thm 12.1): a sheaf of modules on Spec R is quasi-coherent iff it lies in the essential image of the tilde functor.

instance Proposition18.tildeFunctorToQcoh_essSurj (R : CommRingCat) : (tildeFunctorToQcoh R).EssSurj

tildeFunctorToQcoh R is essentially surjective: every quasi-coherent sheaf on Spec R is isomorphic to M̃ for some module M.

instance Proposition18.tildeFunctorToQcoh_isEquivalence (R : CommRingCat) : (tildeFunctorToQcoh R).IsEquivalence

The tilde functor Mod R → QCoh(Spec R) is an equivalence of categories, combining fullness, faithfulness, and essential surjectivity.

noncomputable def Proposition18.qcoh_spec_equiv_moduleCat (R : CommRingCat) : ModuleCat ↑R ≌ Scheme.Qcoh (AlgebraicGeometry.Spec R)

The fundamental equivalence (Thm 11.1 / Thm 12.1): Mod(R) ≃ QCoh(Spec R) via M ↦ M̃, with inverse the global-sections functor Γ.

theorem Proposition18.pushforward_isQuasicoherent_of_isAffineHom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] (ℱ : X.Modules) [hℱ : SheafOfModules.IsQuasicoherent ℱ] : SheafOfModules.IsQuasicoherent ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj ℱ)

Lem 24 (Lec 12): the pushforward f_* along an affine morphism preserves quasi-coherent sheaves.