Module

SubmoduleCoverEquality.lean

Nyll.SchemeTheory.Modules.SubmoduleCoverEquality

2 declarations indexed from sourceView source ↗

Module documentation

Equality of actual submodules from an open cover

Containment of the actual restricted submodules is local on an open cover. The proof uses the native membership locality axiom on the intersections of each test open with the cover. This turns the finite principal-open equalities of affine extraction into equality on their quasi-compact union.

Imports2

Nyll.SchemeTheory.Modules.SubmoduleGluingQuasicoherent
Mathlib.CategoryTheory.Sites.Spaces

Imported by2

theorem

le_over_of_iSup_eq

L34 ↗

SheafOfModules.Submodule.le_over_of_iSup_eq

Documentation

Native submodule containment on a union follows from containment on every member of its actual open cover.

Source context 5 commands

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

noncomputable section
universe u v w t
open CategoryTheory Opposite TopologicalSpace
namespace SheafOfModules.Submodule
variable {X : Type u} [TopologicalSpace X]
  {R : Sheaf (Opens.grothendieckTopology X) RingCat.{v}}
  {M : SheafOfModules.{w} R}

Lean source · statement

theorem le_over_of_iSup_eq (N P : M.Submodule) (U : Opens X)
    {ι : Type t} (V : ι → Opens X) (hCover : (⨆ i, V i) = U)
    (h : ∀ i : ι, N.over (V i) ≤ P.over (V i)) : N.over U ≤ P.over U

theorem

over_eq_of_iSup_eq

L56 ↗

SheafOfModules.Submodule.over_eq_of_iSup_eq