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

The localisation M[f⁻¹] of an R-module M at the powers of f, packaged as a ModuleCat R.

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

The image of f ∈ R as a global section of Spec R via the canonical isomorphism Γ(Spec R, ⊤) ≅ R.

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

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

theorem PushforwardDirectLimit.isIso_fromTildeΓ_pushforward_pullback {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Γ

For any module M, the canonical map tildeΓ → id is an isomorphism on f_* f^* (M̃), where f : D(f) ↪ Spec R.

noncomputable def PushforwardDirectLimit.globalSections_pushforward_pullback_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

The global sections of f_* f^* M̃ are isomorphic to the localisation M[f⁻¹].

theorem PushforwardDirectLimit.isIso_fromTildeΓ_qcoh_spec {R : CommRingCat} (F : (AlgebraicGeometry.Spec R).Modules) [SheafOfModules.IsQuasicoherent F] : CategoryTheory.IsIso F.fromTildeΓ

Quasicoherence implies the canonical map tildeΓ → id is an isomorphism on Spec R.

noncomputable def PushforwardDirectLimit.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)

For a basic open D(f) ↪ Spec R, pushforward followed by pullback of M̃ identifies with the tilde of the localisation M[f⁻¹].

noncomputable def PushforwardDirectLimit.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)

For a quasicoherent F on Spec R and a basic open D(f), the composite f_* f^* F is isomorphic to the tilde of the localisation of Γ(F) at f.