Module

Scheme_Modules_IsFrameOn_tensorPowSection.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_tensorPowSection

1 declaration indexed from sourceView source ↗

Module documentation

Scheme Modules Is Frame On tensor Pow Section

Imports6

Imported by4

theorem

tensorPowSection

L35 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.tensorPowSection

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorPowSection
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.IsFrameOn.tensorPowSection {X :
  AlgebraicGeometry.Scheme.{u}} {L : X.Modules} {U V : X.Opens} {s : Γ(L, U)}
    (hs : AlgebraicGeometry.Scheme.Modules.IsFrameOn s V) (n : ℕ) :
    AlgebraicGeometry.Scheme.Modules.IsFrameOn
      (AlgebraicGeometry.Scheme.Modules.tensorPowSection s n) V

Module documentation

Scheme Modules Is Frame On tensor Pow Section

Declarations

tensorPowSection