Module

TensorSectionAssociator.lean

Nyll.SchemeTheory.Modules.TensorSectionAssociator

12 declarations indexed from sourceView source ↗

Module documentation

The associator on tensor sections

The formula is proved through the monoidal sheafification adjunction and naturality.

Imports5

Imported by2

abbrev

ι

L41 ↗

AlgebraicGeometry.Scheme.Modules.TensorSectionAssociator.ι

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
namespace TensorSectionAssociator
open Opposite TensorProduct
variable {X : Scheme.{u}}

Lean source · statement

abbrev ι (X : Scheme.{u}) : X.Modules ⥤ X.PresheafOfModules

abbrev

adj

L44 ↗

AlgebraicGeometry.Scheme.Modules.TensorSectionAssociator.adj

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
namespace TensorSectionAssociator
open Opposite TensorProduct
variable {X : Scheme.{u}}

Lean source · statement

abbrev adj (X : Scheme.{u}) : Modules.sheafify X ⊣ ι X

abbrev

eta

L47 ↗

AlgebraicGeometry.Scheme.Modules.TensorSectionAssociator.eta

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
namespace TensorSectionAssociator
open Opposite TensorProduct
variable {X : Scheme.{u}}

Lean source · statement

abbrev eta (P : X.PresheafOfModules) (U : X.Opens) (x : P.obj (op U)) :
    Γ((Modules.sheafify X).obj P, U)

lemma

comp_app_apply

L51 ↗

AlgebraicGeometry.Scheme.Modules.TensorSectionAssociator.comp_app_apply

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
namespace TensorSectionAssociator
open Opposite TensorProduct
variable {X : Scheme.{u}}

Lean source · statement

lemma comp_app_apply {A B C : X.Modules} (f : A ⟶ B) (g : B ⟶ C)
    (U : X.Opens) (a : Γ(A, U)) :
    (f ≫ g).app U a = g.app U (f.app U a)

lemma

id_app_apply

L55 ↗

AlgebraicGeometry.Scheme.Modules.TensorSectionAssociator.id_app_apply

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
namespace TensorSectionAssociator
open Opposite TensorProduct
variable {X : Scheme.{u}}

Lean source · statement

lemma id_app_apply {A : X.Modules} (U : X.Opens) (a : Γ(A, U)) :
    (𝟙 A : A ⟶ A).app U a = a

lemma

iso_app_injective

L58 ↗

AlgebraicGeometry.Scheme.Modules.TensorSectionAssociator.iso_app_injective

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
namespace TensorSectionAssociator
open Opposite TensorProduct
variable {X : Scheme.{u}}

Lean source · statement

lemma iso_app_injective {A B : X.Modules} (e : A ≅ B) (U : X.Opens) :
    Function.Injective (e.hom.app U)

lemma

whiskerLeft_app_tensorSections

L65 ↗

AlgebraicGeometry.Scheme.Modules.TensorSectionAssociator.whiskerLeft_app_tensorSections

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
namespace TensorSectionAssociator
open Opposite TensorProduct
variable {X : Scheme.{u}}

Lean source · statement

lemma whiskerLeft_app_tensorSections {L M M' : X.Modules} (f : M ⟶ M')
    {U : X.Opens} (s : Γ(L, U)) (t : Γ(M, U)) :
    (L ◁ f).app U (tensorSections s t) = tensorSections s (f.app U t)

lemma

whiskerRight_app_tensorSections

L71 ↗

AlgebraicGeometry.Scheme.Modules.TensorSectionAssociator.whiskerRight_app_tensorSections

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
namespace TensorSectionAssociator
open Opposite TensorProduct
variable {X : Scheme.{u}}

Lean source · statement

lemma whiskerRight_app_tensorSections {L L' M : X.Modules} (f : L ⟶ L')
    {U : X.Opens} (s : Γ(L, U)) (t : Γ(M, U)) :
    (f ▷ M).app U (tensorSections s t) = tensorSections (f.app U s) t

lemma

sheafify_map_app_eta

L77 ↗

AlgebraicGeometry.Scheme.Modules.TensorSectionAssociator.sheafify_map_app_eta

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
namespace TensorSectionAssociator
open Opposite TensorProduct
variable {X : Scheme.{u}}

Lean source · statement

lemma sheafify_map_app_eta {P P' : X.PresheafOfModules} (g : P ⟶ P')
    (U : X.Opens) (z : P.obj (op U)) :
    ((Modules.sheafify X).map g).app U (eta P U z) = eta P' U (g.app (op U) z)

lemma

counit_app_eta

L83 ↗

AlgebraicGeometry.Scheme.Modules.TensorSectionAssociator.counit_app_eta

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
namespace TensorSectionAssociator
open Opposite TensorProduct
variable {X : Scheme.{u}}

Lean source · statement

lemma counit_app_eta (N : X.Modules) (U : X.Opens) (y : Γ(N, U)) :
    Scheme.Modules.Hom.app (M := (Modules.sheafify X).obj ((ι X).obj N)) (N := N)
      ((adj X).counit.app N) U (eta ((ι X).obj N) U y) = y

theorem

associator_sheafify

L89 ↗

AlgebraicGeometry.Scheme.Modules.TensorSectionAssociator.associator_sheafify

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
namespace TensorSectionAssociator
open Opposite TensorProduct
variable {X : Scheme.{u}}

Lean source · statement

theorem associator_sheafify (P Q R : X.PresheafOfModules) (U : X.Opens)
    (x : P.obj (op U)) (y : Q.obj (op U)) (z : R.obj (op U)) :
    (α_ ((Modules.sheafify X).obj P) ((Modules.sheafify X).obj Q)
        ((Modules.sheafify X).obj R)).hom.app U
        (tensorSections (tensorSections (eta P U x) (eta Q U y)) (eta R U z)) =
      tensorSections (eta P U x) (tensorSections (eta Q U y) (eta R U z))

theorem

associator_hom_app_tensorSections

L121 ↗

AlgebraicGeometry.Scheme.Modules.associator_hom_app_tensorSections

Documentation

The associator sends a tensor of three local sections to the other parenthesization.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
open TensorSectionAssociator in

Lean source · statement

theorem associator_hom_app_tensorSections {L M N : X.Modules} {U : X.Opens}
    (l : Γ(L, U)) (m : Γ(M, U)) (n : Γ(N, U)) :
    (α_ L M N).hom.app U (tensorSections (L := L ⊗ M) (M := N) (tensorSections l m) n) =
      tensorSections (L := L) (M := M ⊗ N) l (tensorSections m n)

Module documentation

The associator on tensor sections

Declarations