theorem adjunction_counit_isIso_of_conservative {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Full] [F.Faithful] [G.ReflectsIsomorphisms] (X : D) : CategoryTheory.IsIso (adj.counit.app X)

If F ⊣ G is an adjunction with F fully faithful and G conservative, then the counit is a natural isomorphism. This is a standard criterion for an adjunction to give an equivalence.

theorem Spec_isAffine' (R : CommRingCat) : AlgebraicGeometry.IsAffine (AlgebraicGeometry.Spec R)

Spec R is an affine scheme. Convenience wrapper around isAffine_Spec.

theorem restrictScalars_full_of_surjective {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (hf : Function.Surjective ⇑f) : (ModuleCat.restrictScalars f).Full

If f : R →+* S is surjective, then the restriction of scalars functor on module categories is full: every R-linear map between restricted S-modules lifts to an S-linear map.

theorem restrictScalars_essImage_annihilated {R : Type u_1} [CommRing R] (I : Ideal R) (M : ModuleCat R) (h : ∃ (N : ModuleCat (R ⧸ I)), Nonempty ((ModuleCat.restrictScalars (Ideal.Quotient.mk I)).obj N ≅ M)) (r : R) (m : ↑M) : r ∈ I → r • m = 0

If an R-module M is in the essential image of restriction along R → R/I, then I annihilates M.

theorem restrictScalars_essImage_of_annihilated {R : Type u_1} [CommRing R] (I : Ideal R) (M : ModuleCat R) (hann : ∀ (r : R) (m : ↑M), r ∈ I → r • m = 0) : ∃ (N : ModuleCat (R ⧸ I)), Nonempty ((ModuleCat.restrictScalars (Ideal.Quotient.mk I)).obj N ≅ M)

Conversely, an R-module annihilated by I is the restriction of scalars of some R/I-module; this characterizes the essential image of restriction along R → R/I.