theorem Prop19.pushforward_characterization {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : I ≤ Module.annihilator R M ↔ ∀ (r : R) (m : M), r ∈ I → r • m = 0

Reformulation: an ideal I annihilates a module M iff each element of I acts as zero on every element of M.

theorem Prop19.pushforward_fullyFaithful (R : Type u_1) [CommRing R] (I : Ideal R) : (ModuleCat.restrictScalars (Ideal.Quotient.mk I)).Full ∧ (ModuleCat.restrictScalars (Ideal.Quotient.mk I)).Faithful

Algebraic version of Proposition 19: restriction of scalars along R → R/I is a full and faithful functor from Mod(R/I) into Mod(R).

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

Essential image (algebraic version): an R-module is a restriction of scalars of an R/I-module iff every element of I annihilates M.

theorem Prop19.pushforward_full_embedding_scheme {X Z : AlgebraicGeometry.Scheme} (i : Z ⟶ X) [AlgebraicGeometry.IsClosedImmersion i] : (AlgebraicGeometry.Scheme.Modules.pushforward i).Full ∧ (AlgebraicGeometry.Scheme.Modules.pushforward i).Faithful

Proposition 19 (scheme version): for a closed immersion i : Z → X, the pushforward i_* : QCoh(Z) → QCoh(X) is a fully faithful functor.

theorem Prop19.essential_image_scheme {X Z : AlgebraicGeometry.Scheme} (i : Z ⟶ X) [AlgebraicGeometry.IsClosedImmersion i] (F : X.Modules) : (∃ (G : Z.Modules), Nonempty ((AlgebraicGeometry.Scheme.Modules.pushforward i).obj G ≅ F)) ↔ ∀ (U : ↑X.affineOpens), (AlgebraicGeometry.Scheme.Hom.ker i).ideal U ≤ Module.annihilator ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(F.val.obj (Opposite.op ↑U))

Proposition 19 (essential image, scheme version): a quasicoherent sheaf F on X is pushed forward from Z iff the ideal sheaf I_Z of the closed immersion annihilates F on every affine open.