def QCohSheaves.localizedModuleCat {R : CommRingCat} (M : ModuleCat ↑R) (f : ↑R) : ModuleCat ↑R

Localization of an R-module at the powers of f, packaged as a ModuleCat.

noncomputable def QCohSheaves.toSpecGlobal {R : CommRingCat} (f : ↑R) : ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤))

Image of f ∈ R under the natural isomorphism R ≅ Γ(Spec R, 𝒪), producing a global section of the structure sheaf of Spec R.

noncomputable def QCohSheaves.basicOpenInclusion {R : CommRingCat} (f : ↑R) : ↑((AlgebraicGeometry.Spec R).basicOpen (toSpecGlobal f)) ⟶ AlgebraicGeometry.Spec R

Open immersion of the basic open D(f) into Spec R.

theorem QCohSheaves.prop16_pushforward_pullback_qc {R : CommRingCat} (M : ModuleCat ↑R) (f : ↑R) : CategoryTheory.IsIso ((AlgebraicGeometry.Scheme.Modules.pushforward (basicOpenInclusion f)).obj ((AlgebraicGeometry.Scheme.Modules.pullback (basicOpenInclusion f)).obj (AlgebraicGeometry.tilde M))).fromTildeΓ

Prop 16 (Lec 12) input: applying tilde to M, then restricting and pushing forward along D(f) ↪ Spec R, gives a sheaf whose fromTildeΓ counit is an isomorphism.

noncomputable def QCohSheaves.prop16_globalSections_iso {R : CommRingCat} (M : ModuleCat ↑R) (f : ↑R) : AlgebraicGeometry.moduleSpecΓFunctor.obj ((AlgebraicGeometry.Scheme.Modules.pushforward (basicOpenInclusion f)).obj ((AlgebraicGeometry.Scheme.Modules.pullback (basicOpenInclusion f)).obj (AlgebraicGeometry.tilde M))) ≅ localizedModuleCat M f

Global sections of the pushforward of M̃|_{D(f)} are naturally isomorphic to the localization M_f.

noncomputable def QCohSheaves.prop16_pushforward_pullback_tilde_iso {R : CommRingCat} (M : ModuleCat ↑R) (f : ↑R) : (AlgebraicGeometry.Scheme.Modules.pushforward (basicOpenInclusion f)).obj ((AlgebraicGeometry.Scheme.Modules.pullback (basicOpenInclusion f)).obj (AlgebraicGeometry.tilde M)) ≅ AlgebraicGeometry.tilde (localizedModuleCat M f)

Prop 16: pushforward-pullback of M̃ along D(f) ↪ Spec R is naturally isomorphic to the tilde of the localized module M_f.

theorem QCohSheaves.prop16_qcoh_fromTildeΓ_iso {R : CommRingCat} (F : (AlgebraicGeometry.Spec R).Modules) [SheafOfModules.IsQuasicoherent F] : CategoryTheory.IsIso F.fromTildeΓ

For any quasi-coherent sheaf on Spec R, the counit F̃Γ → F is an isomorphism (the affine reconstruction lemma underlying the equivalence).

noncomputable def QCohSheaves.prop16_pushforward_pullback_qcoh_iso {R : CommRingCat} (F : (AlgebraicGeometry.Spec R).Modules) [SheafOfModules.IsQuasicoherent F] (f : ↑R) : (AlgebraicGeometry.Scheme.Modules.pushforward (basicOpenInclusion f)).obj ((AlgebraicGeometry.Scheme.Modules.pullback (basicOpenInclusion f)).obj F) ≅ AlgebraicGeometry.tilde (localizedModuleCat (AlgebraicGeometry.moduleSpecΓFunctor.obj F) f)

Quasi-coherent version of Prop 16: pushforward-pullback of a quasi-coherent sheaf F along D(f) ↪ Spec R is isomorphic to the tilde of the localization of its global sections at f.

instance QCohSheaves.tilde_isQuasicoherent_goal94 {R : CommRingCat} (M : ModuleCat ↑R) : SheafOfModules.IsQuasicoherent (AlgebraicGeometry.tilde M)

The sheaf M̃ on Spec R is quasi-coherent (Cor 16, registered as an instance).

noncomputable def QCohSheaves.tilde_gamma_adjunction (R : CommRingCat) : AlgebraicGeometry.tilde.functor R ⊣ AlgebraicGeometry.moduleSpecΓFunctor

The adjunction tilde ⊣ Γ between modules over R and sheaves of modules on Spec R.

def QCohSheaves.IsQuasicoherentSheaf {X : AlgebraicGeometry.Scheme} (F : X.Modules) : Prop

Predicate version of quasi-coherence for a sheaf of modules on a scheme.