Exact tensoring by an invertible module sheaf

This file is the neutral exact-functor owner for tensoring module sheaves by a line bundle. The construction belongs under Modules/Tensor: divisor sequences, filtrations, and future moduli constructions are consumers of the same exact functor rather than separate owners of it.

The generic tensorLeftFunctor L, its colimit preservation, additivity, and free-sheaf comparison come from Monoidal and Colimits. For an invertible L, local rank-one trivializations show that it also preserves monomorphisms; hence it preserves homology and all finite limits.

theorem AlgebraicGeometry.Scheme.Modules.mono_tensorHom_id_of_invertible {X : Scheme} (L : X.Modules) [(have this := L; this).IsInvertible] {M N : X.Modules} (f : M ⟶ N) [CategoryTheory.Mono f] : CategoryTheory.Mono (tensorHom (CategoryTheory.CategoryStruct.id L) f)

Tensoring a monomorphism by an invertible module sheaf remains a monomorphism.

instance AlgebraicGeometry.Scheme.Modules.tensorLeftFunctor_preservesMonomorphisms {X : Scheme} (L : X.Modules) [(have this := L; this).IsInvertible] : L.tensorLeftFunctor.PreservesMonomorphisms

instance AlgebraicGeometry.Scheme.Modules.tensorLeftFunctor_preservesHomology {X : Scheme} (L : X.Modules) [(have this := L; this).IsInvertible] : L.tensorLeftFunctor.PreservesHomology

instance AlgebraicGeometry.Scheme.Modules.tensorLeftFunctor_preservesFiniteLimits {X : Scheme} (L : X.Modules) [(have this := L; this).IsInvertible] : CategoryTheory.Limits.PreservesFiniteLimits L.tensorLeftFunctor

Tensoring by an invertible module sheaf preserves finite limits.

theorem AlgebraicGeometry.Scheme.Modules.isFinitePresentation_tensorObj_left_of_isInvertible {X : Scheme} (L M : X.Modules) [(have this := L; this).IsInvertible] (hM : (have this := M; this).IsFinitePresentation) : (have this := L.tensorObj M; this).IsFinitePresentation

Tensoring a finitely presented module sheaf by an invertible one preserves finite presentation.

On a rank-one trivializing cover for L, the restriction of L ⊗ M is isomorphic to the restriction of M: commute the two tensor factors and use the right-factor trivialization. Finite presentation restricts to each cover member and descends from that cover.

theorem AlgebraicGeometry.Scheme.Modules.epi_tensorHom_id_of_invertible {X : Scheme} (L : X.Modules) [(have this := L; this).IsInvertible] {M N : X.Modules} (f : M ⟶ N) [CategoryTheory.Epi f] : CategoryTheory.Epi (tensorHom (CategoryTheory.CategoryStruct.id L) f)

Tensoring an epimorphism by an invertible module sheaf remains an epimorphism.

Finite colimits are preserved, so pushouts are, and a morphism is an epimorphism exactly when its pushout along itself is the identity square. The companion of mono_tensorHom_id_of_invertible, and the step that carries Serre's surjection free I ↠ F(N) across O(-N).

theorem AlgebraicGeometry.Scheme.Modules.shortExact_map_tensorLeft_of_invertible {X : Scheme} (L : X.Modules) [(have this := L; this).IsInvertible] (S : CategoryTheory.ShortComplex X.Modules) (hS : S.ShortExact) : (S.map L.tensorLeftFunctor).ShortExact

Tensoring a short exact sequence by an invertible module sheaf remains short exact.