ModuleImageSubmoduleRestriction.lean
Nyll.SchemeTheory.Modules.ImageSubmoduleRestriction
2 declarations indexed from sourceView source ↗ Module documentation
The actual image on an open where its source generates
If a morphism into a prescribed native submodule becomes epimorphic on an open, the image of its composite into the ambient sheaf restricts to that exact prescribed submodule. The reverse inclusion is constructed by the epimorphism--monomorphism lifting property in the actual sheaf category.
Declarations
SheafOfModules.overSheafIso_inv_ι
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open CategoryTheory
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
{R : Sheaf J RingCat.{u}}
SheafOfModules.imageSubmodule_over_eq_of_epi
DocumentationAn actual local epimorphism onto P gives literal equality between P and the restriction of its image in the ambient sheaf.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open CategoryTheory
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
{R : Sheaf J RingCat.{u}}
variable [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
[∀ U : C, HasSheafify (J.over U) AddCommGrpCat.{u}]
[∀ U : C, (J.over U).WEqualsLocallyBijective AddCommGrpCat.{u}]