Module

AffineModuleEpi.lean

Nyll.SchemeTheory.Modules.AffineModuleEpi

1 declaration indexed from sourceView source ↗

Module documentation

Affine epimorphisms from actual global sections

Surjectivity on global sections of a morphism into a quasicoherent module over a spectrum implies that the actual sheaf morphism is epimorphic. The proof uses the native tilde--Gamma counit and preservation of epimorphisms by tilde; the source need not be quasicoherent.

Imports4

Mathlib.AlgebraicGeometry.Modules.Tilde
Mathlib.Algebra.Category.ModuleCat.EpiMono
Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.CategoryTheory.Functor.EpiMono

Imported by2

theorem

epi_of_surjective_moduleSpecΓ

L31 ↗

AlgebraicGeometry.Scheme.Modules.epi_of_surjective_moduleSpecΓ

Documentation

Surjectivity on actual affine global sections detects an epimorphism onto a quasicoherent module.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem epi_of_surjective_moduleSpecΓ {R : CommRingCat.{u}}
    {M N : (Spec R).Modules} [N.IsQuasicoherent] (φ : M ⟶ N)
    (hφ : Function.Surjective ((moduleSpecΓFunctor (R := R)).map φ)) : Epi φ

Module documentation

Affine epimorphisms from actual global sections

Declarations

epi_of_surjective_moduleSpecΓ