Module

Scheme_Modules_isInvertible_of_forall_exists_isFrameOn.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isInvertible_of_forall_exists_isFrameOn

1 declaration indexed from sourceView source ↗

Module documentation

Scheme Modules is Invertible of forall exists is Frame On

Imports7

Imported by4

theorem

isInvertible_of_forall_exists_isFrameOn

L38 ↗

AlgebraicGeometry.Scheme.Modules.isInvertible_of_forall_exists_isFrameOn

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.LocalFramesInvertible
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open AlgebraicGeometry AlgebraicGeometry.Scheme.Modules in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.isInvertible_of_forall_exists_isFrameOn {X :
  AlgebraicGeometry.Scheme.{u}} {M : X.Modules}
    (h : ∀ x : X, ∃ (U : X.Opens) (s : Γ(M, U)), x ∈ U ∧
      AlgebraicGeometry.Scheme.Modules.IsFrameOn s U) :
    AlgebraicGeometry.Scheme.Modules.IsInvertible M

Module documentation

Scheme Modules is Invertible of forall exists is Frame On

Declarations

isInvertible_of_forall_exists_isFrameOn