Module

AffineOpenModuleEpi.lean

Nyll.SchemeTheory.Modules.AffineOpenModuleEpi

1 declaration indexed from sourceView source ↗

Module documentation

Epimorphisms over actual affine opens

Surjectivity on an affine open gives an epimorphism on its native slice site when the target is quasicoherent. The proof first uses the actual canonical spectrum of the affine open, then transports through restriction and the equivalence with the slice site.

Imports5

Nyll.SchemeTheory.Modules.AffineModuleEpi
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Mathlib.CategoryTheory.Functor.EpiMono

Imported by2

theorem

epi_over_of_surjective_app

L32 ↗

AlgebraicGeometry.Scheme.Modules.epi_over_of_surjective_app

Documentation

Surjectivity on an affine open implies that the actual restriction to its slice site is epimorphic, provided the target is quasicoherent.

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_over_of_surjective_app {X : Scheme.{u}} {M N : X.Modules}
    [N.IsQuasicoherent] (φ : M ⟶ N) (U : X.Opens) (hU : IsAffineOpen U)
    (hφ : Function.Surjective (φ.app U)) : Epi (SheafOfModules.Hom.over φ U)

Module documentation

Epimorphisms over actual affine opens

Declarations

epi_over_of_surjective_app