AlgebraicGeometry.Scheme.Modules.tensorPowAdd_hom_app_tensorSections_tensorPowSection
The addition comparison multiplies powers of the same local section.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.ModulesLean source · statement
theorem tensorPowAdd_hom_app_tensorSections_tensorPowSection
{X : Scheme.{u}} {L : X.Modules} {U : X.Opens} (g : Γ(L, U)) (m n : ℕ) :
(Scheme.Modules.tensorPowAdd L m n).hom.app U
(Scheme.Modules.tensorSections (L := L.tensorPow m) (M := L.tensorPow n)
(Scheme.Modules.tensorPowSection g m) (Scheme.Modules.tensorPowSection g n)) =
Scheme.Modules.tensorPowSection g (m + n)