Module

Scheme_Modules_IsInvertible_tensor.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_tensor

2 declarations indexed from sourceView source ↗

Module documentation

Tensor products of invertible module sheaves

Restrict local trivializations to their common open subset and tensor them to prove that the tensor product of two invertible modules is invertible.

Imports6

Imported by113

def

trivializationOfLE

L48 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_tensor.AlgebraicGeometry.Scheme.Modules.trivializationOfLE

Documentation

Pull a trivialization of L back from U to the smaller open V.

Source context 15 commands

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

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

Lean source · statement

def trivializationOfLE {X : Scheme.{u}} {U V : X.Opens} (h : V ≤ U) (L : X.Modules)
    (e : (Modules.pullback U.ι).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf) :
    (Modules.pullback V.ι).obj L ≅ SheafOfModules.unit (V : Scheme.{u}).ringCatSheaf

theorem

tensor

L59 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.tensor

Source context 7 commands