Module

Scheme_Modules_IsInvertible_nonempty_rigidify_pullback_tensor_iso.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_rigidify_pullback_tensor_iso

2 declarations indexed from sourceView source ↗

Module documentation

Rigidification removes a tensor factor from the base

Rigidifying the tensor product of an invertible module with a module pulled back from the base yields a module isomorphic to the rigidification of the original module.

Imports5

Imported by10

def

lbTB_tensorExchange

L39 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_nonempty_rigidify_pullback_tensor_iso.lbTB_tensorExchange

Documentation

The braided tensor interchange that exchanges the two middle factors of a fourfold tensor product.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_nonempty_rigidify_pullback_tensor_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry

Lean source · statement

def lbTB_tensorExchange {V : Type*} [Category V] [MonoidalCategory V] [BraidedCategory V]
    (A B C D : V) : (A ⊗ B) ⊗ (C ⊗ D) ≅ (A ⊗ C) ⊗ (B ⊗ D)

theorem

nonempty_rigidify_pullback_tensor_iso

L44 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.nonempty_rigidify_pullback_tensor_iso