Module

Scheme_Modules_whiskerRight_app_tensorSections.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_whiskerRight_app_tensorSections

1 declaration indexed from sourceView source ↗

Module documentation

Whiskering morphisms on tensor sections

Right whiskering acts on the first factor of a local tensor section.

Imports6

Imported by3

theorem

whiskerRight_app_tensorSections

L38 ↗

AlgebraicGeometry.Scheme.Modules.whiskerRight_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_whiskerRight_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.whiskerRight_app_tensorSections
    {X : AlgebraicGeometry.Scheme.{u}} {L L' : X.Modules} (φ : L ⟶ L') (M : X.Modules) {U : X.Opens}
    (s : Γ(L, U)) (t : Γ(M, U)) :
    (φ ▷ M).app U (AlgebraicGeometry.Scheme.Modules.tensorSections s t) =
      AlgebraicGeometry.Scheme.Modules.tensorSections (φ.app U s) t

Module documentation

Whiskering morphisms on tensor sections

Declarations

whiskerRight_app_tensorSections