Module

Frames.lean

Nyll.SchemeTheory.Modules.Frames

9 declarations indexed from sourceView source ↗

Module documentation

Local frames for scheme modules and their restrictions.

Imports1

Mathlib.AlgebraicGeometry.Modules.Sheaf

Imported by5

def

IsFrameOn

L27 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn

Documentation

A section is a local frame on an open subset when its restrictions freely generate all smaller section modules.

Source context 4 commands

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

universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} {U : X.Opens}

Lean source · statement

def IsFrameOn (s : Γ(M, U)) (V : X.Opens) : Prop

lemma

bijective

L35 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.bijective

Source context 6 commands

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

universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} {U : X.Opens}
namespace IsFrameOn
variable {s : Γ(M, U)} {V : X.Opens}

Lean source · full declaration

lemma bijective (h : IsFrameOn s V) {W : X.Opens} (hWU : W ≤ U) (hWV : W ≤ V) :
    Function.Bijective fun g : Γ(X, W) => g • (M.presheaf.map (homOfLE hWU).op s : Γ(M, W)) :=
  h hWU hWV

lemma

mono

L39 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.mono

Source context 6 commands

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

universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} {U : X.Opens}
namespace IsFrameOn
variable {s : Γ(M, U)} {V : X.Opens}

Lean source · statement

lemma mono (h : IsFrameOn s V) {V' : X.Opens} (hV' : V' ≤ V) : IsFrameOn s V'

lemma

of_inf

L42 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.of_inf

Source context 6 commands

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

universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} {U : X.Opens}
namespace IsFrameOn
variable {s : Γ(M, U)} {V : X.Opens}

Lean source · statement

lemma of_inf (h : IsFrameOn s (V ⊓ U)) : IsFrameOn s V

lemma

inf_iff

L45 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.inf_iff

Source context 6 commands

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

universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} {U : X.Opens}
namespace IsFrameOn
variable {s : Γ(M, U)} {V : X.Opens}

Lean source · statement

lemma inf_iff : IsFrameOn s (V ⊓ U) ↔ IsFrameOn s V

lemma

map

L48 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.map

Source context 6 commands

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

universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} {U : X.Opens}
namespace IsFrameOn
variable {s : Γ(M, U)} {V : X.Opens}

Lean source · statement

lemma map (h : IsFrameOn s V) {U' : X.Opens} (i : U' ⟶ U) :
    IsFrameOn (M.presheaf.map i.op s) V

lemma

existsUnique

L58 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.existsUnique

Source context 6 commands

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

universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} {U : X.Opens}
namespace IsFrameOn
variable {s : Γ(M, U)} {V : X.Opens}

Lean source · statement

lemma existsUnique (h : IsFrameOn s V) {W : X.Opens} (hWU : W ≤ U) (hWV : W ≤ V) (x : Γ(M, W)) :
    ∃! g : Γ(X, W), g • M.presheaf.map (homOfLE hWU).op s = x

lemma

smul_eq_zero_iff

L62 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.smul_eq_zero_iff

Source context 6 commands

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

universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} {U : X.Opens}
namespace IsFrameOn
variable {s : Γ(M, U)} {V : X.Opens}

Lean source · statement

lemma smul_eq_zero_iff (h : IsFrameOn s V) {W : X.Opens} (hWU : W ≤ U) (hWV : W ≤ V) (g : Γ(X, W)) :
    g • M.presheaf.map (homOfLE hWU).op s = 0 ↔ g = 0

lemma

map_iso

L74 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.map_iso

Source context 4 commands

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

universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} {U : X.Opens}

Lean source · statement

lemma IsFrameOn.map_iso {N : X.Modules} {s : Γ(M, U)} {V : X.Opens} (h : IsFrameOn s V) (e : M ≅ N)
  :
    IsFrameOn (e.hom.app U s) V

Module documentation

Declarations