AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullback_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.InverseUnique.inverseUnique
The isomorphism between two tensor inverses of the same object, constructed using the braiding and the specified evaluations.
Source context 15 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullback_dual_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace InverseUnique
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategoryLean 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'