noncomputable def tildeΓAdjunction {R : CommRingCat} : AlgebraicGeometry.tilde.functor R ⊣ AlgebraicGeometry.moduleSpecΓFunctor

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

noncomputable def tildeFullyFaithful {R : CommRingCat} : (AlgebraicGeometry.tilde.functor R).FullyFaithful

The tilde functor is fully faithful, the categorical input to the equivalence Mod R ≃ QCoh(Spec R).

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

For every R-module M, the sheaf M̃ on Spec R is quasi-coherent.

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

The unit of the tilde ⊣ Γ adjunction is an isomorphism (the affine reconstruction Γ(M̃) ≅ M).

noncomputable def tildeEssImageEquiv {R : CommRingCat} : ModuleCat ↑R ≌ (AlgebraicGeometry.tilde.functor R).EssImageSubcategory

Equivalence of categories between Mod R and the essential image of the tilde functor, packaging the fully-faithful corestriction.

theorem tilde_essImage_iff_isIso_counit {R : CommRingCat} (M : (AlgebraicGeometry.Spec (CommRingCat.of ↑R)).Modules) : (AlgebraicGeometry.tilde.functor R).essImage M ↔ CategoryTheory.IsIso M.fromTildeΓ

A sheaf M on Spec R lies in the essential image of the tilde functor iff the affine counit fromTildeΓ M is an isomorphism.

theorem tilde_counit_isIso_of_presentation {R : CommRingCat} (M : (AlgebraicGeometry.Spec R).Modules) (P : SheafOfModules.Presentation M) : CategoryTheory.IsIso M.fromTildeΓ

If a sheaf of modules on Spec R admits a presentation, then the affine counit fromTildeΓ is an isomorphism.