Module

Scheme_Modules_Hom_epi_iff_locallySurjective.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_Hom_epi_iff_locallySurjective

2 declarations indexed from sourceView source ↗

Module documentation

Epimorphisms and locally surjective module maps

A morphism of module sheaves is an epimorphism precisely when sections locally lift through its components.

Imports5

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.CategoryTheory.Sites.EpiMono
Mathlib.Algebra.Category.Grp.EpiMono
Mathlib.Algebra.Category.Grp.Abelian
Mathlib.Topology.Sheaves.Abelian

Imported by8

theorem

epi_toSheaf_map_of_epi

L47 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_Hom_epi_iff_locallySurjective.SheafOfModules.epi_toSheaf_map_of_epi

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_Hom_epi_iff_locallySurjective
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe v v' u'
namespace SheafOfModules
open _root_.SheafOfModules
open _root_.SheafOfModules
variable {C : Type u'} [Category.{v'} C] {J : GrothendieckTopology C} {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{v}] [J.WEqualsLocallyBijective AddCommGrpCat.{v}]

Lean source · statement

theorem epi_toSheaf_map_of_epi {M N : SheafOfModules.{v} R} (φ : M ⟶ N) [Epi φ] :
    Epi ((toSheaf R).map φ)

theorem

epi_iff_locallySurjective

L113 ↗

AlgebraicGeometry.Scheme.Modules.Hom.epi_iff_locallySurjective

Source context 19 commands