NYLL
Module

TensorSections.lean

Nyll.SchemeTheory.Modules.TensorSections
29 declarations indexed from sourceView source ↗

Module documentation

Tensor products and frames of module sections

Local tensor sections and their iterated powers are compatible with restrictions and module operations; frames characterize sections freely generating smaller opens.

Imports4
Imported by116

Declarations

instance

tensorSectionsPresheafModule

L35 ↗
AlgebraicGeometry.Scheme.Modules.tensorSectionsPresheafModule
Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
Lean source · statement
instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U))
def

tensorSectionsHom

L44 ↗
AlgebraicGeometry.Scheme.Modules.tensorSectionsHom
Documentation

The canonical map from the tensor product of underlying presheaves to the sheaf tensor product.

Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Hom
variable (L M : X.Modules)
Lean source · full declaration
def tensorSectionsHom : L.val ⊗ M.val ⟶
    (SheafOfModules.toPMod (J := _root_.Opens.grothendieckTopology X)
      X.sheaf.obj X.ringCatSheaf.property : X.Modules ⥤ X.PresheafOfModules).obj (show X.Modules
          from L ⊗ M) :=
  (SheafOfModules.sheafifyAdj X.sheaf.obj X.ringCatSheaf.property).unit.app (L.val ⊗ M.val) ≫
    (SheafOfModules.toPMod (J := _root_.Opens.grothendieckTopology X)
      X.sheaf.obj X.ringCatSheaf.property : X.Modules ⥤ X.PresheafOfModules).map (tensorIsoSheafify
          L M).hom
def

tensorSections

L60 ↗
AlgebraicGeometry.Scheme.Modules.tensorSections
Documentation

The tensor product of two module sections over the same open subset.

Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
Lean source · statement
def tensorSections (s : Γ(L, U)) (t : Γ(M, U)) : Γ(L ⊗ M, U)
lemma

tensorSections_def

L65 ↗
AlgebraicGeometry.Scheme.Modules.tensorSections_def
Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
Lean source · full declaration
lemma tensorSections_def (s : Γ(L, U)) (t : Γ(M, U)) :
    tensorSections s t = DFunLike.coe (α := ((L.val ⊗ M.val).obj (op U) :)) (β := fun _ => Γ(L ⊗ M,
        U))
      ((tensorSectionsHom L M).app (op U)).hom
      ((s : L.val.obj (op U)) ⊗ₜ[Γ(X, U)] (t : M.val.obj (op U))) := rfl
lemma

tensorSections_add_left

L71 ↗
AlgebraicGeometry.Scheme.Modules.tensorSections_add_left
Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
Lean source · statement
lemma tensorSections_add_left (s s' : Γ(L, U)) (t : Γ(M, U)) :
    tensorSections (s + s') t = tensorSections s t + tensorSections s' t
lemma

tensorSections_add_right

L77 ↗
AlgebraicGeometry.Scheme.Modules.tensorSections_add_right
Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
Lean source · statement
lemma tensorSections_add_right (s : Γ(L, U)) (t t' : Γ(M, U)) :
    tensorSections s (t + t') = tensorSections s t + tensorSections s t'
lemma

tensorSections_smul_left

L83 ↗
AlgebraicGeometry.Scheme.Modules.tensorSections_smul_left
Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
Lean source · statement
lemma tensorSections_smul_left (g : Γ(X, U)) (s : Γ(L, U)) (t : Γ(M, U)) :
    tensorSections (g • s) t = g • tensorSections s t
lemma

tensorSections_smul_right

L90 ↗
AlgebraicGeometry.Scheme.Modules.tensorSections_smul_right
Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
Lean source · statement
lemma tensorSections_smul_right (g : Γ(X, U)) (s : Γ(L, U)) (t : Γ(M, U)) :
    tensorSections s (g • t) = g • tensorSections s t
lemma

tensorSections_zero_left

L97 ↗
AlgebraicGeometry.Scheme.Modules.tensorSections_zero_left
Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
Lean source · statement
lemma tensorSections_zero_left (t : Γ(M, U)) : tensorSections (0 : Γ(L, U)) t = 0
lemma

tensorSections_zero_right

L102 ↗
AlgebraicGeometry.Scheme.Modules.tensorSections_zero_right
Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
Lean source · statement
lemma tensorSections_zero_right (s : Γ(L, U)) : tensorSections s (0 : Γ(M, U)) = 0
lemma

tensorSections_neg_left

L107 ↗
AlgebraicGeometry.Scheme.Modules.tensorSections_neg_left
Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
Lean source · statement
lemma tensorSections_neg_left (s : Γ(L, U)) (t : Γ(M, U)) :
    tensorSections (-s) t = -tensorSections s t
lemma

tensorSections_neg_right

L111 ↗
AlgebraicGeometry.Scheme.Modules.tensorSections_neg_right
Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
Lean source · statement
lemma tensorSections_neg_right (s : Γ(L, U)) (t : Γ(M, U)) :
    tensorSections s (-t) = -tensorSections s t
lemma

tensorSections_sum_left

L115 ↗
AlgebraicGeometry.Scheme.Modules.tensorSections_sum_left
Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
Lean source · statement
lemma tensorSections_sum_left {ι : Type*} (S : Finset ι) (s : ι → Γ(L, U)) (t : Γ(M, U)) :
    tensorSections (∑ i ∈ S, s i) t = ∑ i ∈ S, tensorSections (s i) t
lemma

tensorSections_sum_right

L122 ↗
AlgebraicGeometry.Scheme.Modules.tensorSections_sum_right
Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
Lean source · statement
lemma tensorSections_sum_right {ι : Type*} (S : Finset ι) (s : Γ(L, U)) (t : ι → Γ(M, U)) :
    tensorSections s (∑ i ∈ S, t i) = ∑ i ∈ S, tensorSections s (t i)
def

tensorSectionsBilin

L132 ↗
AlgebraicGeometry.Scheme.Modules.tensorSectionsBilin
Documentation

The bilinear map on local sections induced by the sheaf tensor product.

Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
variable (L M U) in
Lean source · statement
def tensorSectionsBilin : Γ(L, U) →ₗ[Γ(X, U)] Γ(M, U) →ₗ[Γ(X, U)] Γ(L ⊗ M, U)
lemma

tensorSectionsBilin_apply

L136 ↗
AlgebraicGeometry.Scheme.Modules.tensorSectionsBilin_apply
Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
variable (L M U) in
Lean source · statement
lemma tensorSectionsBilin_apply (s : Γ(L, U)) (t : Γ(M, U)) :
    tensorSectionsBilin L M U s t = tensorSections s t
lemma

map_tensorSections

L139 ↗
AlgebraicGeometry.Scheme.Modules.map_tensorSections
Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
variable (L M U) in
Lean source · statement
lemma map_tensorSections {V : X.Opens} (i : V ⟶ U) (s : Γ(L, U)) (t : Γ(M, U)) :
    (L ⊗ M).presheaf.map i.op (tensorSections s t) =
      tensorSections (L.presheaf.map i.op s) (M.presheaf.map i.op t)
lemma

map_homOfLE_tensorSections

L148 ↗
AlgebraicGeometry.Scheme.Modules.map_homOfLE_tensorSections
Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Sections
variable {L M : X.Modules} {U : X.Opens}
variable (L M U) in
Lean source · statement
lemma map_homOfLE_tensorSections {V : X.Opens} (h : V ≤ U) (s : Γ(L, U)) (t : Γ(M, U)) :
    (L ⊗ M).presheaf.map (homOfLE h).op (tensorSections s t) =
      tensorSections (L.presheaf.map (homOfLE h).op s) (M.presheaf.map (homOfLE h).op t)
def

unitSection

L161 ↗
AlgebraicGeometry.Scheme.Modules.unitSection
Documentation

The section of the unit module represented by the constant function one.

Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Pow
variable {L : X.Modules} {U : X.Opens}
variable (U) in
Lean source · statement
def unitSection : Γ(𝟙_ X.Modules, U)
lemma

unitSection_def

L163 ↗
AlgebraicGeometry.Scheme.Modules.unitSection_def
Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Pow
variable {L : X.Modules} {U : X.Opens}
variable (U) in
Lean source · statement
lemma unitSection_def : (unitSection U : Γ(𝟙_ X.Modules, U)) = (1 : Γ(X, U))
lemma

map_unitSection

L165 ↗
AlgebraicGeometry.Scheme.Modules.map_unitSection
Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Pow
variable {L : X.Modules} {U : X.Opens}
variable (U) in
Lean source · statement
lemma map_unitSection {V : X.Opens} (i : V ⟶ U) :
    (𝟙_ X.Modules).presheaf.map i.op (unitSection U) = unitSection V
lemma

smul_unitSection

L169 ↗
AlgebraicGeometry.Scheme.Modules.smul_unitSection
Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Pow
variable {L : X.Modules} {U : X.Opens}
variable (U) in
Lean source · statement
lemma smul_unitSection (g : Γ(X, U)) : g • unitSection U = (g : Γ(X, U))
lemma

smul_unitSection_bijective

L172 ↗
AlgebraicGeometry.Scheme.Modules.smul_unitSection_bijective
Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Pow
variable {L : X.Modules} {U : X.Opens}
variable (U) in
Lean source · full declaration
lemma smul_unitSection_bijective : Function.Bijective fun g : Γ(X, U) => g • unitSection U := by
  refine Function.bijective_iff_has_inverse.2 ⟨fun x => (x : Γ(X, U)), fun g => ?_, fun x => ?_⟩
  · exact mul_one g
  · exact mul_one (show Γ(X, U) from x)
def

tensorPowSection

L178 ↗
AlgebraicGeometry.Scheme.Modules.tensorPowSection
Documentation

The iterated tensor power of a section, with the unit section in degree zero.

Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Pow
variable {L : X.Modules} {U : X.Opens}
variable (U) in
Lean source · full declaration
def tensorPowSection (s : Γ(L, U)) : (n : ℕ) → Γ(L.tensorPow n, U)
  | 0 => unitSection U
  | n + 1 => tensorSections (L := L.tensorPow n) (M := L) (tensorPowSection s n) s
lemma

tensorPowSection_zero

L182 ↗
AlgebraicGeometry.Scheme.Modules.tensorPowSection_zero
Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Pow
variable {L : X.Modules} {U : X.Opens}
variable (U) in
Lean source · statement
lemma tensorPowSection_zero (s : Γ(L, U)) : tensorPowSection s 0 = unitSection U
lemma

tensorPowSection_succ

L184 ↗
AlgebraicGeometry.Scheme.Modules.tensorPowSection_succ
Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Pow
variable {L : X.Modules} {U : X.Opens}
variable (U) in
Lean source · statement
lemma tensorPowSection_succ (s : Γ(L, U)) (n : ℕ) :
    tensorPowSection s (n + 1) = tensorSections (L := L.tensorPow n) (M := L) (tensorPowSection s n)
        s
lemma

tensorPowSection_one

L188 ↗
AlgebraicGeometry.Scheme.Modules.tensorPowSection_one
Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Pow
variable {L : X.Modules} {U : X.Opens}
variable (U) in
Lean source · statement
lemma tensorPowSection_one (s : Γ(L, U)) :
    tensorPowSection s 1 = tensorSections (L := 𝟙_ X.Modules) (M := L) (unitSection U) s
lemma

map_tensorPowSection

L191 ↗
AlgebraicGeometry.Scheme.Modules.map_tensorPowSection
Source context 9 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Pow
variable {L : X.Modules} {U : X.Opens}
variable (U) in
Lean source · statement
lemma map_tensorPowSection {V : X.Opens} (i : V ⟶ U) (s : Γ(L, U)) (n : ℕ) :
    (L.tensorPow n).presheaf.map i.op (tensorPowSection s n) =
      tensorPowSection (L.presheaf.map i.op s) n
lemma

isFrameOn_unitSection

L206 ↗
AlgebraicGeometry.Scheme.Modules.isFrameOn_unitSection
Source context 8 commands

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

universe u
open CategoryTheory MonoidalCategory Opposite TensorProduct
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
local instance tensorSectionsPresheafModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section Frame
variable {M : X.Modules} {U : X.Opens}
Lean source · statement
lemma isFrameOn_unitSection (V : X.Opens) : IsFrameOn (unitSection U) V

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