NYLL
Module

TensorSectionMaps.lean

Nyll.SchemeTheory.Modules.TensorSectionMaps
9 declarations indexed from sourceView source ↗

Module documentation

Tensor morphisms on local tensor sections

The components of a tensor product of module morphisms act separately on the two factors of a local tensor section.

Imports4
Imported by10

Declarations

instance

presheafSectionsModule

L35 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections.presheafSectionsModule
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
Lean source · statement
instance presheafSectionsModule {X : Scheme.{u}}
    (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (Opposite.op U))
abbrev

ι

L59 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.TensorHomSections.ι
Documentation

The underlying presheaf functor in the native module category of the scheme.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
local instance presheafSectionsModule {X : Scheme.{u}}
    (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (Opposite.op U)) :=
  (P.obj (Opposite.op U)).isModule
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 TensorHomSections
open Opposite TensorProduct
variable {X : Scheme.{u}} {L L' M M' : X.Modules}
Lean source · statement
abbrev ι (X : Scheme.{u}) : X.Modules ⥤ X.PresheafOfModules
abbrev

adj

L63 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.TensorHomSections.adj
Documentation

The canonical adjunction between sheafification and the underlying presheaf functor.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
local instance presheafSectionsModule {X : Scheme.{u}}
    (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (Opposite.op U)) :=
  (P.obj (Opposite.op U)).isModule
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 TensorHomSections
open Opposite TensorProduct
variable {X : Scheme.{u}} {L L' M M' : X.Modules}
Lean source · statement
abbrev adj (X : Scheme.{u}) : Modules.sheafify X ⊣ ι X
def

sheafifyTensorIso

L70 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.TensorHomSections.sheafifyTensorIso
Documentation

The canonical comparison from the sheafified presheaf tensor product to the sheaf tensor product.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
local instance presheafSectionsModule {X : Scheme.{u}}
    (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (Opposite.op U)) :=
  (P.obj (Opposite.op U)).isModule
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 TensorHomSections
open Opposite TensorProduct
variable {X : Scheme.{u}} {L L' M M' : X.Modules}
variable (L M)
Lean source · statement
def sheafifyTensorIso : (Modules.sheafify X).obj ((ι X).obj L ⊗ (ι X).obj M) ≅ L ⊗ M
lemma

sheafifyTensorIso_hom_naturality

L77 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.TensorHomSections.sheafifyTensorIso_hom_naturality
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
local instance presheafSectionsModule {X : Scheme.{u}}
    (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (Opposite.op U)) :=
  (P.obj (Opposite.op U)).isModule
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 TensorHomSections
open Opposite TensorProduct
variable {X : Scheme.{u}} {L L' M M' : X.Modules}
variable (L M)
variable {L M}
Lean source · statement
lemma sheafifyTensorIso_hom_naturality (f : L ⟶ L') (g : M ⟶ M') :
    (Modules.sheafify X).map ((ι X).map f ⊗ₘ (ι X).map g) ≫ (sheafifyTensorIso L' M').hom =
      (sheafifyTensorIso L M).hom ≫ (f ⊗ₘ g)
lemma

tensorSections_eq

L92 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.TensorHomSections.tensorSections_eq
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
local instance presheafSectionsModule {X : Scheme.{u}}
    (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (Opposite.op U)) :=
  (P.obj (Opposite.op U)).isModule
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 TensorHomSections
open Opposite TensorProduct
variable {X : Scheme.{u}} {L L' M M' : X.Modules}
variable (L M)
variable {L M}
Lean source · statement
lemma tensorSections_eq {U : X.Opens} (s : Γ(L, U)) (t : Γ(M, U)) :
    Modules.tensorSections s t = (sheafifyTensorIso L M).hom.val.app (op U)
      (((adj X).unit.app ((ι X).obj L ⊗ (ι X).obj M)).app (op U)
        ((s : L.val.obj (op U)) ⊗ₜ[Γ(X, U)] (t : M.val.obj (op U))))
lemma

sheafify_map_val_app_unit

L97 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.TensorHomSections.sheafify_map_val_app_unit
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
local instance presheafSectionsModule {X : Scheme.{u}}
    (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (Opposite.op U)) :=
  (P.obj (Opposite.op U)).isModule
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 TensorHomSections
open Opposite TensorProduct
variable {X : Scheme.{u}} {L L' M M' : X.Modules}
variable (L M)
variable {L M}
Lean source · statement
lemma sheafify_map_val_app_unit {P P' : X.PresheafOfModules} (g : P ⟶ P') (V : (X.Opens)ᵒᵖ) (z :
  P.obj V) :
    (((Modules.sheafify X).map g).val.app V) (((adj X).unit.app P).app V z) =
      ((adj X).unit.app P').app V (g.app V z)
theorem

tensorHom_app_tensorSections

L104 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.TensorHomSections.tensorHom_app_tensorSections
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
local instance presheafSectionsModule {X : Scheme.{u}}
    (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (Opposite.op U)) :=
  (P.obj (Opposite.op U)).isModule
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 TensorHomSections
open Opposite TensorProduct
variable {X : Scheme.{u}} {L L' M M' : X.Modules}
variable (L M)
variable {L M}
Lean source · statement
theorem tensorHom_app_tensorSections (φ : L ⟶ L') (ψ : M ⟶ M') {U : X.Opens} (s : Γ(L, U)) (t : Γ(M,
  U)) :
    (φ ⊗ₘ ψ).app U (Modules.tensorSections s t) = Modules.tensorSections (φ.app U s) (ψ.app U t)
theorem

tensorHom_app_tensorSections

L134 ↗
AlgebraicGeometry.Scheme.Modules.tensorHom_app_tensorSections
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorHom_app_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
local instance presheafSectionsModule {X : Scheme.{u}}
    (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (Opposite.op U)) :=
  (P.obj (Opposite.op U)).isModule
open _root_.AlgebraicGeometry AlgebraicGeometry _root_.AlgebraicGeometry.Scheme.Modules
    AlgebraicGeometry.Scheme.Modules in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.tensorHom_app_tensorSections {X :
  AlgebraicGeometry.Scheme.{u}} {L L' M M' : X.Modules} (φ : L ⟶ L') (ψ : M ⟶ M') {U : X.Opens}
    (s : Γ(L, U)) (t : Γ(M, U)) :
    (φ ⊗ₘ ψ).app U (AlgebraicGeometry.Scheme.Modules.tensorSections s t) =
      AlgebraicGeometry.Scheme.Modules.tensorSections (φ.app U s) (ψ.app U t)

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