instance QCohMathlib.tilde_functor_faithful {R : CommRingCat} : (AlgebraicGeometry.tilde.functor R).Faithful

The tilde functor Mod R → (Spec R).Modules is faithful.

instance QCohMathlib.tilde_functor_full {R : CommRingCat} : (AlgebraicGeometry.tilde.functor R).Full

The tilde functor Mod R → (Spec R).Modules is full.

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

Packaged fully-faithful structure for the tilde functor, exposing both fullness and faithfulness simultaneously.

instance QCohMathlib.tilde_isLeftAdjoint {R : CommRingCat} : (AlgebraicGeometry.tilde.functor R).IsLeftAdjoint

The tilde functor is the left adjoint of the tilde ⊣ Γ adjunction.

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

For every module M, the sheaf M̃ is quasi-coherent (Cor 16).

instance QCohMathlib.tilde_toEssImage_isEquivalence {R : CommRingCat} : (AlgebraicGeometry.tilde.functor R).toEssImage.IsEquivalence

The corestriction of tilde to its essential image is an equivalence of categories, since tilde is fully faithful.