Module

Scheme_Modules_epi_sheafification_map_of_locallySurjective.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_epi_sheafification_map_of_locallySurjective

2 declarations indexed from sourceView source ↗

Module documentation

Epimorphisms induced by locally surjective presheaf maps

Sheafification turns a locally surjective morphism of module presheaves into an epimorphism.

Imports3

Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
Mathlib.AlgebraicGeometry.Modules.Presheaf
Mathlib.AlgebraicGeometry.Modules.Sheaf

Imported by2

theorem

epi_sheafification_map_of_isLocallySurjective

L47 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_epi_sheafification_map_of_locallySurjective.PresheafOfModules.epi_sheafification_map_of_isLocallySurjective

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_epi_sheafification_map_of_locallySurjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe v v' u'
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type u'} [Category.{v'} C] {J : GrothendieckTopology C}
  {R₀ : Cᵒᵖ ⥤ RingCat.{u}} {R : Sheaf J RingCat.{u}} (α : R₀ ⟶ R.obj)
  [Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
  [HasSheafify J AddCommGrpCat.{v}] [J.WEqualsLocallyBijective AddCommGrpCat.{v}]

Lean source · statement

theorem epi_sheafification_map_of_isLocallySurjective {P Q : PresheafOfModules.{v} R₀}
    (ψ : P ⟶ Q) [Presheaf.IsLocallySurjective J ((toPresheaf R₀).map ψ)] :
    Epi ((sheafification.{v} α).map ψ)

theorem

epi_sheafification_map_of_locallySurjective

L78 ↗

AlgebraicGeometry.Scheme.Modules.epi_sheafification_map_of_locallySurjective

Source context 20 commands