NYLL
Module

Scheme_Modules_leftUnitor_hom_app_tensorSections.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_leftUnitor_hom_app_tensorSections
9 declarations indexed from sourceView source ↗

Module documentation

The left unitor on tensor sections

The left unitor evaluates a tensor of a scalar section with a module section as scalar multiplication.

Imports5
Imported by4

Declarations

instance

presheafSectionsModule

L36 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_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_leftUnitor_hom_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

ι

L60 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.ι
Documentation

The functor taking a module sheaf on a scheme to its underlying module presheaf.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_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 UnitorSections
open Opposite TensorProduct
variable {X : Scheme.{u}}
Lean source · statement
abbrev ι (X : Scheme.{u}) : X.Modules ⥤ X.PresheafOfModules
abbrev

adj

L64 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.adj
Documentation

The adjunction between module presheaf sheafification and passage to underlying presheaves.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_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 UnitorSections
open Opposite TensorProduct
variable {X : Scheme.{u}}
Lean source · statement
abbrev adj (X : Scheme.{u}) : Modules.sheafify X ⊣ ι X
lemma

sheafify_map_val_app_unit

L67 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.sheafify_map_val_app_unit
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_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 UnitorSections
open Opposite TensorProduct
variable {X : Scheme.{u}}
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)
lemma

counit_val_app_unit

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.counit_val_app_unit
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_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 UnitorSections
open Opposite TensorProduct
variable {X : Scheme.{u}}
Lean source · statement
lemma counit_val_app_unit (N : X.Modules) (V : (X.Opens)ᵒᵖ) (y : N.val.obj V) :
    (((adj X).counit.app N).val.app V) (((adj X).unit.app ((ι X).obj N)).app V y) = y
def

unitTensorIso

L83 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.unitTensorIso
Documentation

The comparison isomorphism from the sheafified tensor with the presheaf unit to the tensor with the sheaf unit.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_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 UnitorSections
open Opposite TensorProduct
variable {X : Scheme.{u}}
variable (N : X.Modules)
Lean source · statement
def unitTensorIso : (Modules.sheafify X).obj (𝟙_ X.PresheafOfModules ⊗ (ι X).obj N) ≅ 𝟙_ X.Modules ⊗
    N
lemma

unitTensorIso_hom_comp_leftUnitor_hom

L89 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.unitTensorIso_hom_comp_leftUnitor_hom
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_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 UnitorSections
open Opposite TensorProduct
variable {X : Scheme.{u}}
variable (N : X.Modules)
Lean source · statement
lemma unitTensorIso_hom_comp_leftUnitor_hom :
    (unitTensorIso N).hom ≫ (λ_ N).hom =
      (Modules.sheafify X).map (λ_ ((ι X).obj N)).hom ≫ (adj X).counit.app N
theorem

leftUnitor_hom_app_tensorSections

L101 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.leftUnitor_hom_app_tensorSections
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_leftUnitor_hom_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 UnitorSections
open Opposite TensorProduct
variable {X : Scheme.{u}}
variable (N : X.Modules)
Lean source · statement
theorem leftUnitor_hom_app_tensorSections {U : X.Opens} (g : Γ(X, U)) (n : Γ(N, U)) :
    (λ_ N).hom.app U (Modules.tensorSections (L := 𝟙_ X.Modules) (M := N) g n) = g • n
theorem

leftUnitor_hom_app_tensorSections

L130 ↗
AlgebraicGeometry.Scheme.Modules.leftUnitor_hom_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_leftUnitor_hom_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 CategoryTheory _root_.CategoryTheory.MonoidalCategory _root_.AlgebraicGeometry
    AlgebraicGeometry _root_.AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.leftUnitor_hom_app_tensorSections {X :
  AlgebraicGeometry.Scheme.{u}} {N : X.Modules} {U : X.Opens} (g : Γ(X, U)) (n : Γ(N, U)) :
    (λ_ N).hom.app U
      (AlgebraicGeometry.Scheme.Modules.tensorSections (L := 𝟙_ X.Modules) (M := N) g n) = g • n

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