ModuleQuasicoherentCokernel.lean
Nyll.SchemeTheory.Modules.QuasicoherentCokernel
3 declarations indexed from sourceView source ↗ Module documentation
Quasicoherence of actual cokernels
On an affine scheme, the actual morphism is transported through its canonical tilde isomorphisms. The existing tilde adjunction preserves its cokernel. Restriction and the shared affine-presentation criterion then give the result on arbitrary schemes.
Declarations
AlgebraicGeometry.Scheme.Modules.affineTildeIso
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Modules
AlgebraicGeometry.Scheme.Modules.isQuasicoherent_cokernel_toSpec
DocumentationThe actual cokernel of a morphism between quasicoherent modules on an affine scheme is quasicoherent.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Modules
AlgebraicGeometry.Scheme.Modules.isQuasicoherent_cokernel
DocumentationThe actual categorical cokernel of a morphism between quasicoherent modules on any scheme is quasicoherent.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Modules