Theorems · Theorem · category theory

CategoryTheory.prodComparison_iso

∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_3 : CategoryTheory.Reflective i] [inst_4 : CategoryTheory.MonoidalClosed C]
  [inst_5 : CategoryTheory.CartesianMonoidalCategory D] [CategoryTheory.ExponentialIdeal i]
  [CategoryTheory.BraidedCategory C] (A B : C),
  CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison (CategoryTheory.reflector i) A B)

The bijection allows us to show that prodComparison L A B is an isomorphism, where the inverse is the forward map of the identity morphism.

Defined in

Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Cited by

0 results in Mathlib

Foundations

Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.ReflectiveCategoryTheory.MonoidalClosedCategoryTheory.CartesianMonoidalCategoryCategoryTheory.ExponentialIdealCategoryTheory.BraidedCategory