Direct sums of 𝒪ₓ-modules

The site-level closure properties of direct sums of sheaves of modules (TauCeti/Algebra/Category/ModuleCat/Sheaf/Quasicoherent/Biprod.lean) specialize to a scheme X by taking the sheaf of rings to be the structure sheaf of X. Since X.Modules carries its own category and abelian structures, instance search does not find the site-level instances for M ⊞ N, and they are restated here.

Main declarations

• AlgebraicGeometry.Scheme.Modules.isQuasicoherent_biprod, AlgebraicGeometry.Scheme.Modules.isFiniteType_biprod, AlgebraicGeometry.Scheme.Modules.isFinitePresentation_biprod and AlgebraicGeometry.Scheme.Modules.isLocallyFree_biprod: the direct sum of two quasi-coherent (respectively finite type, finitely presented, locally free) 𝒪ₓ-modules is again so. In particular, direct sums of finite locally free 𝒪ₓ-modules are finite locally free.

instance AlgebraicGeometry.Scheme.Modules.isQuasicoherent_biprod {X : Scheme} (M N : X.Modules) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] : SheafOfModules.IsQuasicoherent (M ⊞ N)

The direct sum of two quasi-coherent 𝒪ₓ-modules is quasi-coherent.

instance AlgebraicGeometry.Scheme.Modules.isFiniteType_biprod {X : Scheme} (M N : X.Modules) [SheafOfModules.IsFiniteType M] [SheafOfModules.IsFiniteType N] : SheafOfModules.IsFiniteType (M ⊞ N)

The direct sum of two 𝒪ₓ-modules of finite type is of finite type.

instance AlgebraicGeometry.Scheme.Modules.isFinitePresentation_biprod {X : Scheme} (M N : X.Modules) [SheafOfModules.IsFinitePresentation M] [SheafOfModules.IsFinitePresentation N] : SheafOfModules.IsFinitePresentation (M ⊞ N)

The direct sum of two finitely presented 𝒪ₓ-modules is finitely presented.

instance AlgebraicGeometry.Scheme.Modules.isLocallyFree_biprod {X : Scheme} (M N : X.Modules) [SheafOfModules.IsLocallyFree M] [SheafOfModules.IsLocallyFree N] : SheafOfModules.IsLocallyFree (M ⊞ N)

The direct sum of two locally free 𝒪ₓ-modules is locally free.