NYLL
Module

Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
13 declarations indexed from sourceView source ↗

Module documentation

A frame trivializes pullback to an open

A section that is a frame on an open gives an isomorphism between the restricted pullback of the module and the unit module on every smaller open.

Imports6
Imported by15

Declarations

def

restrictRingCatSheafHom

L62 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry.Scheme.Modules.FrameBridge.restrictRingCatSheafHom
Documentation

The identity map of ring sheaves describing restriction to the scheme associated to an open subset.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open Opposite TopologicalSpace
variable {X : Scheme.{u}}
section restrict
variable (W : X.Opens)
Lean source · statement
def restrictRingCatSheafHom : (W : Scheme.{u}).ringCatSheaf ⟶
    (W.ι.opensFunctor.sheafPushforwardContinuous RingCat.{u}
      (Opens.grothendieckTopology (W : Scheme.{u})) (Opens.grothendieckTopology X)).obj
        X.ringCatSheaf
def

restrictFunctor'

L69 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry.Scheme.Modules.FrameBridge.restrictFunctor'
Documentation

Restriction of module sheaves to an open subset, expressed as a sheaf pushforward.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open Opposite TopologicalSpace
variable {X : Scheme.{u}}
section restrict
variable (W : X.Opens)
Lean source · statement
def restrictFunctor' : X.Modules ⥤ (W : Scheme.{u}).Modules
lemma

restrictFunctor'_eq

L72 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry.Scheme.Modules.FrameBridge.restrictFunctor'_eq
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open Opposite TopologicalSpace
variable {X : Scheme.{u}}
section restrict
variable (W : X.Opens)
Lean source · statement
lemma restrictFunctor'_eq : restrictFunctor' W = Modules.restrictFunctor W.ι
def

restrictFunctor'IsoPullback

L81 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry.Scheme.Modules.FrameBridge.restrictFunctor'IsoPullback
Documentation

The natural isomorphism identifying open restriction with pullback along its inclusion.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open Opposite TopologicalSpace
variable {X : Scheme.{u}}
section restrict
variable (W : X.Opens)
Lean source · statement
def restrictFunctor'IsoPullback : restrictFunctor' W ≅ Modules.pullback W.ι
lemma

image_le

L84 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry.Scheme.Modules.FrameBridge.image_le
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open Opposite TopologicalSpace
variable {X : Scheme.{u}}
section restrict
variable (W : X.Opens)
Lean source · statement
lemma image_le (W' : (W : Scheme.{u}).Opens) : W.ι ''ᵁ W' ≤ W
lemma

image_preimage_of_le

L88 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry.Scheme.Modules.FrameBridge.image_preimage_of_le
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open Opposite TopologicalSpace
variable {X : Scheme.{u}}
section restrict
variable (W : X.Opens)
variable {W} in
Lean source · statement
lemma image_preimage_of_le {W₂ : X.Opens} (h : W₂ ≤ W) : W.ι ''ᵁ (W.ι ⁻¹ᵁ W₂) = W₂
abbrev

secX

L94 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry.Scheme.Modules.FrameBridge.secX
Documentation

A section on the scheme associated to an open, regarded as a section on its image in the original scheme.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open Opposite TopologicalSpace
variable {X : Scheme.{u}}
section restrict
variable (W : X.Opens)
variable {W} in
Lean source · statement
abbrev secX (W' : (W : Scheme.{u}).Opens) (a : Γ(W, W')) : Γ(X, W.ι ''ᵁ W')
def

smulSectionHom

L103 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry.Scheme.Modules.FrameBridge.smulSectionHom
Documentation

The morphism from the unit sheaf defined by scalar multiplication by the restricted section.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open Opposite TopologicalSpace
variable {X : Scheme.{u}}
section smulHom
variable (N : X.Modules) (W : X.Opens) (τ : Γ(N, W))
Lean source · statement
def smulSectionHom : SheafOfModules.unit ((W : X.Opens) : Scheme.{u}).ringCatSheaf ⟶
    (restrictFunctor' W).obj N
lemma

smulSectionHom_app_apply

L128 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry.Scheme.Modules.FrameBridge.smulSectionHom_app_apply
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open Opposite TopologicalSpace
variable {X : Scheme.{u}}
section smulHom
variable (N : X.Modules) (W : X.Opens) (τ : Γ(N, W))
Lean source · statement
lemma smulSectionHom_app_apply (W' : (((W : X.Opens) : Scheme.{u}).Opens)ᵒᵖ) (a : Γ(W, W'.unop)) :
    (smulSectionHom N W τ).val.app W' a =
      secX W W'.unop a • N.presheaf.map (homOfLE (image_le W W'.unop)).op τ
lemma

isIso_smulSectionHom_of_bijective

L134 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry.Scheme.Modules.FrameBridge.isIso_smulSectionHom_of_bijective
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open Opposite TopologicalSpace
variable {X : Scheme.{u}}
section smulHom
variable (N : X.Modules) (W : X.Opens) (τ : Γ(N, W))
variable {N W τ}
Lean source · statement
lemma isIso_smulSectionHom_of_bijective
    (hb : ∀ W' : (((W : X.Opens) : Scheme.{u}).Opens)ᵒᵖ, Function.Bijective ((smulSectionHom N W
        τ).val.app W')) :
    IsIso (smulSectionHom N W τ)
theorem

isIso_smulSectionHom

L156 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry.Scheme.Modules.FrameBridge.isIso_smulSectionHom
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open Opposite TopologicalSpace
variable {X : Scheme.{u}}
variable {M : X.Modules} {U V : X.Opens} {s : Γ(M, U)}
Lean source · statement
theorem isIso_smulSectionHom (h : IsFrameOn s V) (W : X.Opens) (hWU : W ≤ U) (hWV : W ≤ V) :
    IsIso (smulSectionHom M W (M.presheaf.map (homOfLE hWU).op s))
theorem

nonempty_pullback_iso_unit

L169 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry.Scheme.Modules.FrameBridge.nonempty_pullback_iso_unit
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameBridge
open Opposite TopologicalSpace
variable {X : Scheme.{u}}
variable {M : X.Modules} {U V : X.Opens} {s : Γ(M, U)}
Lean source · statement
theorem nonempty_pullback_iso_unit (h : IsFrameOn s V) (W : X.Opens) (hWU : W ≤ U) (hWV : W ≤ V) :
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit (W :
        Scheme.{u}).ringCatSheaf)
theorem

nonempty_pullback_iso_unit

L188 ↗
AlgebraicGeometry.Scheme.Modules.IsFrameOn.nonempty_pullback_iso_unit
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
with_weak_namespace _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open _root_.AlgebraicGeometry
    Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry
    _root_.AlgebraicGeometry.Scheme.Modules
    Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit.AlgebraicGeometry.Scheme.Modules in
with_weak_namespace Scheme_Modules_IsFrameOn_nonempty_pullback_iso_unit
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsFrameOn.nonempty_pullback_iso_unit {X :
    AlgebraicGeometry.Scheme.{u}} {M : X.Modules} {U V : X.Opens} {s : Γ(M, U)}
    (h : AlgebraicGeometry.Scheme.Modules.IsFrameOn s V) (W : X.Opens) (hWU : W ≤ U) (hWV : W ≤ V) :
    Nonempty ((AlgebraicGeometry.Scheme.Modules.pullback W.ι).obj M ≅
      SheafOfModules.unit (W : AlgebraicGeometry.Scheme.{u}).ringCatSheaf)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.