Module

Scheme_Modules_FiniteBySections_of_finiteBySections_unit.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_of_finiteBySections_unit

1 declaration indexed from sourceView source ↗

Module documentation

Scheme Modules Finite By Sections of finite By Sections unit

Imports5

Imported by2

theorem

of_finiteBySections_unit

L35 ↗

AlgebraicGeometry.Scheme.Modules.FiniteBySections.of_finiteBySections_unit

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_finiteBySections_unit
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.FiniteBySections.of_finiteBySections_unit
    {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [IsProper f]
    (h𝒪 : Scheme.Modules.FiniteBySections (SheafOfModules.unit X.ringCatSheaf : X.Modules) f)
    (M : X.Modules) (hM : Scheme.Modules.IsInvertible M) :
    Scheme.Modules.FiniteBySections M f

Module documentation

Scheme Modules Finite By Sections of finite By Sections unit

Declarations

of_finiteBySections_unit