Module

Scheme_Modules_IsInvertible_pullback_dual.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_pullback_dual

2 declarations indexed from sourceView source ↗

Module documentation

Pullback of the dual of an invertible module

Uniqueness of a tensor inverse identifies the pullback of the dual with the dual of the pullback of an invertible module.

Imports7

Imported by15

def

inverseUnique

L52 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullback_dual.AlgebraicGeometry.Scheme.Modules.InverseUnique.inverseUnique

Documentation

The isomorphism identifying two tensor inverses of the same object.

Source context 17 commands

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

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

Lean source · statement

def inverseUnique {C : Type*} [Category C] [MonoidalCategory C] [BraidedCategory C]
    {L M M' : C} (e : L ⊗ M ≅ 𝟙_ C) (e' : L ⊗ M' ≅ 𝟙_ C) : M ≅ M'

theorem

pullback_dual

L61 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.pullback_dual

Source context 6 commands