Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Modules.smul

{X : AlgebraicGeometry.Scheme} →
  {M : X.Modules} →
    {U : X.Opens} → ↑(X.presheaf.obj (Opposite.op U)) →+* CategoryTheory.End (M.presheaf.obj (Opposite.op U))

Scalar multiplication as an endomorphism of Γ(M, U).

Defined in

Mathlib.AlgebraicGeometry.Modules.Sheaf

Cited by

9 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound