@[reducible, inline]

abbrev QCohLocalization.ModuleTilde (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (f : R) : Type (max u_2 u_1)

The localized module M_f := S^{-1} M at the powers of f, encoding the value Γ(D(f), M̃) of the tilde sheaf on a principal open.

theorem QCohLocalization.localization_preserves_injective {R : Type u_1} [CommRing R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) : Function.Injective ⇑((LocalizedModule.map S) f)

Localization is left exact: it preserves injectivity of module maps.

theorem QCohLocalization.localization_preserves_surjective {R : Type u_1} [CommRing R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑((LocalizedModule.map S) f)

Localization is right exact: it preserves surjectivity of module maps.

theorem QCohLocalization.localization_exact_middle {R : Type u_1} [CommRing R] (S : Submonoid R) {M' : Type u_2} {M : Type u_3} {M'' : Type u_4} [AddCommGroup M'] [Module R M'] [AddCommGroup M] [Module R M] [AddCommGroup M''] [Module R M''] (f : M' →ₗ[R] M) (g : M →ₗ[R] M'') (hex : Function.Exact ⇑f ⇑g) : Function.Exact ⇑((LocalizedModule.map S) f) ⇑((LocalizedModule.map S) g)

Localization is exact in the middle: it preserves exactness of a pair f, g of consecutive linear maps.

theorem QCohLocalization.localization_preserves_exactness {R : Type u_1} [CommRing R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hfg : Function.Exact ⇑f ⇑g) : Function.Exact ⇑((LocalizedModule.map S) f) ⇑((LocalizedModule.map S) g)

Localization functor S^{-1}(−) is exact: it preserves exact sequences, the key property powering the tilde-functor proofs.

theorem tildeSpec_qcoh_essImage {R : CommRingCat} (F : (AlgebraicGeometry.Spec R).Modules) [SheafOfModules.IsQuasicoherent F] : (AlgebraicGeometry.tilde.functor R).essImage F

Every quasi-coherent sheaf on Spec R lies in the essential image of the tilde functor (the Thm 12.1 direction).

noncomputable def tildeSpec_globalSectionsModule {R : CommRingCat} (F : (AlgebraicGeometry.Spec R).Modules) : ModuleCat ↑R

Global sections of a sheaf of modules on Spec R, viewed as an R-module through the natural Γ functor.

instance tildeSpec_unitIso {R : CommRingCat} : CategoryTheory.IsIso AlgebraicGeometry.tilde.adjunction.unit

The unit of the tilde ⊣ Γ adjunction is an isomorphism, expressing the identity Γ(M̃) ≅ M.

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

The sheaf M̃ on Spec R is quasi-coherent for any R-module M.