Theorems · Theorem · category theory

CategoryTheory.ExponentialIdeal.mk_of_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.MonoidalClosed C] [inst_4 : CategoryTheory.Reflective i]
  (h :
    (A : C) →
      i.comp ((CategoryTheory.ihom A).comp ((CategoryTheory.reflector i).comp i)) ≅ i.comp (CategoryTheory.ihom A)),
  CategoryTheory.ExponentialIdeal i

Given a natural isomorphism i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A, we can show i is an exponential ideal.

Defined in

Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.MonoidalClosedCategoryTheory.Reflective