Module

Scheme_Modules_whiskerLeft_app_tensorSections.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_whiskerLeft_app_tensorSections

1 declaration indexed from sourceView source ↗

Module documentation

Scheme Modules whisker Left app tensor Sections

Imports7

Imported by2

theorem

whiskerLeft_app_tensorSections

L39 ↗

AlgebraicGeometry.Scheme.Modules.whiskerLeft_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_whiskerLeft_app_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open AlgebraicGeometry AlgebraicGeometry.Scheme.Modules in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.whiskerLeft_app_tensorSections
    {X : AlgebraicGeometry.Scheme.{u}} (L : X.Modules) {M M' : X.Modules} (ψ : M ⟶ M') {U : X.Opens}
    (s : Γ(L, U)) (t : Γ(M, U)) :
    (L ◁ ψ).app U (AlgebraicGeometry.Scheme.Modules.tensorSections s t) =
      AlgebraicGeometry.Scheme.Modules.tensorSections s (ψ.app U t)

Module documentation

Scheme Modules whisker Left app tensor Sections

Declarations

whiskerLeft_app_tensorSections