Module

Scheme_Modules_IsInvertible_tensor_monoidalV2.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_tensor_monoidalV2

2 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Invertible tensor monoidal V2

Imports8

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.CategoryTheory.Monoidal.Category
Nyll.AlgebraicCurves.Geometry.Picard.Functor
Nyll.SchemeTheory.Modules.PresheafInternalHom
Nyll.SchemeTheory.Modules.SheafificationMonoidal
Nyll.AlgebraicCurves.Foundations.Algebra.SheafOfModules_MonoidalV2
Nyll.SchemeTheory.Modules.PresheafPullbackMonoidal
Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesPullbackMonoidalV2

Imported by8

def

trivializationOfLE

L60 ↗

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

Documentation

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

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_tensor_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace 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_monoidalV2

L71 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.tensor_monoidalV2

Source context 7 commands