AlgebraicGeometry.Scheme.Modules.isInvertible_glueOfCocycle
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isInvertible_glueOfCocycle
open _root_.CategoryTheory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
universe uLean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.isInvertible_glueOfCocycle
{X : Scheme.{u}} {ι : Type u} {U : ι → X.Opens} (hU : ⨆ i, U i = ⊤) (c :
Scheme.Modules.UnitCocycle U) :
Scheme.Modules.IsInvertible (Scheme.Modules.glueOfCocycle c)