Module

SubmoduleOverEquality.lean

Nyll.SchemeTheory.Modules.SubmoduleOverEquality

4 declarations indexed from sourceView source ↗

Module documentation

Exact restriction equalities for the finite-open induction

Equality on a slice gives equality of every actual section submodule below that slice. It is therefore inherited by smaller slices, and the native gluing has the exact prescribed restrictions on both opens.

Imports1

Nyll.SchemeTheory.Modules.SubmoduleGluingQuasicoherent

Imported by4

theorem

obj_eq_of_over_eq

L29 ↗

SheafOfModules.Submodule.obj_eq_of_over_eq

Documentation

Exact equality on a slice identifies every section submodule below it.

Source context 5 commands

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

noncomputable section
universe v v₁ u₁ u
open CategoryTheory Opposite
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}

Lean source · statement

theorem obj_eq_of_over_eq {N P : M.Submodule} {U : C}
    (h : N.over U = P.over U) (V : C) (f : V ⟶ U) :
    N.toSubmodule.obj (op V) = P.toSubmodule.obj (op V)

theorem

over_eq_of_over_eq

L35 ↗

SheafOfModules.Submodule.over_eq_of_over_eq

Documentation

Literal equality of native submodules persists under further restriction.

Source context 5 commands

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

noncomputable section
universe v v₁ u₁ u
open CategoryTheory Opposite
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}

Lean source · statement

theorem over_eq_of_over_eq {N P : M.Submodule} {U V : C}
    (h : N.over V = P.over V) (f : U ⟶ V) : N.over U = P.over U

theorem

glueOn_over_eq_left

L42 ↗

SheafOfModules.Submodule.glueOn_over_eq_left

Documentation

The constructed gluing has exactly the first prescribed native restriction.

Source context 5 commands

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

noncomputable section
universe v v₁ u₁ u
open CategoryTheory Opposite
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}

Lean source · statement

theorem glueOn_over_eq_left (N P : M.Submodule) (U V : C)
    (h : ∀ (Z : C) (_a : Z ⟶ U) (_b : Z ⟶ V),
      N.toSubmodule.obj (op Z) = P.toSubmodule.obj (op Z)) :
    (glueOn N P U V).over U = N.over U

theorem

glueOn_over_eq_right

L51 ↗

SheafOfModules.Submodule.glueOn_over_eq_right

Documentation

The constructed gluing has exactly the second prescribed native restriction.

Source context 5 commands

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

noncomputable section
universe v v₁ u₁ u
open CategoryTheory Opposite
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}

Lean source · statement

theorem glueOn_over_eq_right (N P : M.Submodule) (U V : C)
    (h : ∀ (Z : C) (_a : Z ⟶ U) (_b : Z ⟶ V),
      N.toSubmodule.obj (op Z) = P.toSubmodule.obj (op Z)) :
    (glueOn N P U V).over V = P.over V

Module documentation

Exact restriction equalities for the finite-open induction

Declarations

obj_eq_of_over_eq

over_eq_of_over_eq

glueOn_over_eq_left

glueOn_over_eq_right