Module

Scheme_Modules_nonempty_pullback_tensor_pullback_iso_of_trivial_on_open.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_tensor_pullback_iso_of_trivial_on_open

1 declaration indexed from sourceView source ↗

Module documentation

Tensoring with a module trivial on an open

Over the inverse image of an open where a module is trivial, tensoring with its pullback preserves the restricted pullback of the other module up to isomorphism.

Imports5

Imported by4

theorem

nonempty_pullback_tensor_pullback_iso_of_trivial_on_open

L39 ↗

AlgebraicGeometry.Scheme.Modules.nonempty_pullback_tensor_pullback_iso_of_trivial_on_open

Source context 8 commands

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

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

Lean source · statement

theorem
    _root_.AlgebraicGeometry.Scheme.Modules.nonempty_pullback_tensor_pullback_iso_of_trivial_on_open
    {Y T : AlgebraicGeometry.Scheme.{u}} (q : Y ⟶ T) (V : T.Opens) (L : Y.Modules) (N : T.Modules)
    (eN : (AlgebraicGeometry.Scheme.Modules.pullback V.ι).obj N ≅ 𝟙_ ((V :
        AlgebraicGeometry.Scheme.{u}).Modules)) :
    Nonempty ((AlgebraicGeometry.Scheme.Modules.pullback (q ⁻¹ᵁ V).ι).obj
        (L ⊗ (AlgebraicGeometry.Scheme.Modules.pullback q).obj N) ≅
      (AlgebraicGeometry.Scheme.Modules.pullback (q ⁻¹ᵁ V).ι).obj L)

Module documentation

Tensoring with a module trivial on an open

Declarations

nonempty_pullback_tensor_pullback_iso_of_trivial_on_open