ModuleSubmoduleEmbeddedIso.lean
Nyll.SchemeTheory.Modules.SubmoduleEmbeddedIso
2 declarations indexed from sourceView source ↗ Module documentation
Literal equality from embedded submodule comparisons
An actual morphism commuting with the native inclusions gives pointwise containment. An actual isomorphism commuting with the inclusions therefore gives equality of the original native submodules. In particular, the embedded restriction comparison in the quasicoherent extension theorem can be used by submodule gluing without an assumed section comparison.
Imports1
- Mathlib.Algebra.Category.ModuleCat.Sheaf.Submodule
Imported by4
Declarations
SheafOfModules.Submodule.le_of_hom_ι
DocumentationA map of actual submodules commuting with their inclusions gives containment.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe v v₁ u₁ u
open CategoryTheory
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
{R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}
SheafOfModules.Submodule.eq_of_iso_ι
DocumentationAn isomorphism of submodules respecting their native embeddings gives equality of the actual submodules, including every section submodule.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe v v₁ u₁ u
open CategoryTheory
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
{R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}