noncomputable def QCohEquivalenceProof.inverse_from_local_data {R : Type u_1} [CommRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (η : M →ₗ[R] N) (h : ∀ (P : Ideal R) [inst : P.IsMaximal], Function.Bijective ⇑((LocalizedModule.map P.primeCompl) η)) : N →ₗ[R] M

Construct an inverse linear map from N to M assuming η : M → N becomes bijective after localization at every maximal ideal — used to invert maps via local data.

noncomputable def QCohEquivalenceProof.qcoh_mod_equivalence (R : CommRingCat) : ModuleCat ↑R ≌ (AlgebraicGeometry.tilde.functor R).EssImageSubcategory

Restricting the tilde functor to its essential image yields an equivalence Mod R ≃ EssImage(tilde), a step toward the equivalence with QCoh(Spec R).

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

M̃ is quasi-coherent for every R-module M (Cor 16).

theorem QCohEquivalenceProof.adjunction_equivalence_from_stalks {R : Type u_1} [CommRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (η : M →ₗ[R] N) (ε : N →ₗ[R] M) (h_comp_unit : ∀ (P : Ideal R) [inst : P.IsMaximal], (LocalizedModule.map P.primeCompl) (ε ∘ₗ η) = LinearMap.id) (h_comp_counit : ∀ (P : Ideal R) [inst : P.IsMaximal], (LocalizedModule.map P.primeCompl) (η ∘ₗ ε) = LinearMap.id) : ε ∘ₗ η = LinearMap.id ∧ η ∘ₗ ε = LinearMap.id

Reconstructs the equivalence-of-adjunction identity from local (stalkwise) data: maps that are inverse at every maximal localization are globally inverse.