NYLL
Module

TensorSectionRightUnitor.lean

Nyll.SchemeTheory.Modules.TensorSectionRightUnitor
8 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules right Unitor hom app tensor Sections

Imports4
Imported by4

Declarations

abbrev

ι

L51 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_rightUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.ι
Documentation

The forgetful functor from scheme modules to their underlying presheaves of modules.

Source context 19 commands

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

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

adj

L55 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_rightUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.adj
Documentation

The sheafification adjunction for modules over the scheme structure sheaf.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_rightUnitor_hom_app_tensorSections
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 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

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_rightUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.sheafify_map_val_app_unit
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_rightUnitor_hom_app_tensorSections
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 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

L65 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_rightUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.counit_val_app_unit
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_rightUnitor_hom_app_tensorSections
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 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

tensorUnitIso

L73 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_rightUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.tensorUnitIso
Documentation

Compare sheafification of a module tensor the presheaf unit with the sheaf tensor unit.

Source context 20 commands

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

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

tensorUnitIso_hom_comp_rightUnitor_hom

L79 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_rightUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.tensorUnitIso_hom_comp_rightUnitor_hom
Source context 20 commands

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

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

rightUnitor_hom_app_tensorSections

L91 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_rightUnitor_hom_app_tensorSections.AlgebraicGeometry.Scheme.Modules.UnitorSections.rightUnitor_hom_app_tensorSections
Source context 20 commands

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

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

rightUnitor_hom_app_tensorSections

L124 ↗
AlgebraicGeometry.Scheme.Modules.rightUnitor_hom_app_tensorSections
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_rightUnitor_hom_app_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open CategoryTheory _root_.CategoryTheory.MonoidalCategory _root_.AlgebraicGeometry
  AlgebraicGeometry _root_.AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.rightUnitor_hom_app_tensorSections {X :
  AlgebraicGeometry.Scheme.{u}} {N : X.Modules} {U : X.Opens} (n : Γ(N, U)) (g : Γ(X, U)) :
    (ρ_ N).hom.app U
      (AlgebraicGeometry.Scheme.Modules.tensorSections (L := N) (M := 𝟙_ X.Modules) n g) = g • n

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