Cartesian closed categories

A cartesian closed category is a category with CartesianMonoidalCategory and MonoidalClosed instances. There used to be a separate definition CartesianClosed, with its own API, but over time this ended up as a duplicate of the former. Now, CartesianClosed and the surrounding API has been deprecated, and the API for MonoidalClosed should be used instead. This file now contains a few basic constructions for cartesian closed categories.

instance CategoryTheory.CartesianMonoidalCategory.isLeftAdjoint_prod_functor {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : C) [Closed A] : (Limits.prod.functor.obj A).IsLeftAdjoint

def CategoryTheory.CartesianClosed.«term_⟹_» : Lean.TrailingParserDescr

Morphisms obtained using an exponentiable object.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.CartesianClosed.delabFunctorObjExp : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for Functor.obj

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.CartesianClosed.«term_^^_» : Lean.TrailingParserDescr

Morphisms from an exponentiable object.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.internalizeHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A Y : C} [Closed A] (f : A ⟶ Y) : MonoidalCategoryStruct.tensorUnit C ⟶ A ⟹ Y

The internal element which points at the given morphism.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.zeroMul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A : C} [Closed A] {I : C} (t : Limits.IsInitial I) : MonoidalCategoryStruct.tensorObj A I ≅ I

If an initial object I exists in a CCC, then A ⨯ I ≅ I.

Equations

• CategoryTheory.zeroMul t = { hom := CategoryTheory.SemiCartesianMonoidalCategory.snd A I, inv := t.to (CategoryTheory.MonoidalCategoryStruct.tensorObj A I), hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.zeroMul_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A : C} [Closed A] {I : C} (t : Limits.IsInitial I) : (zeroMul t).hom = SemiCartesianMonoidalCategory.snd A I

@[simp]

theorem CategoryTheory.zeroMul_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A : C} [Closed A] {I : C} (t : Limits.IsInitial I) : (zeroMul t).inv = t.to (MonoidalCategoryStruct.tensorObj A I)

def CategoryTheory.mulZero {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A : C} [Closed A] [BraidedCategory C] {I : C} (t : Limits.IsInitial I) : MonoidalCategoryStruct.tensorObj I A ≅ I

If an initial object 0 exists in a CCC, then 0 ⨯ A ≅ 0.

Equations

• CategoryTheory.mulZero t = β_ I A ≪≫ CategoryTheory.zeroMul t

def CategoryTheory.powZero {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {B : C} [BraidedCategory C] {I : C} (t : Limits.IsInitial I) [MonoidalClosed C] : I ⟹ B ≅ MonoidalCategoryStruct.tensorUnit C

If an initial object 0 exists in a CCC then 0^B ≅ 1 for any B.

Equations

• One or more equations did not get rendered due to their size.

@[deprecated "No replacement: use `asIso (coprodComparison (tensorLeft Z) _ _)` instead." (since := "2025-12-22")]

noncomputable def CategoryTheory.prodCoprodDistrib {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [MonoidalClosed C] (X Y Z : C) : MonoidalCategoryStruct.tensorObj Z X ⨿ MonoidalCategoryStruct.tensorObj Z Y ≅ MonoidalCategoryStruct.tensorObj Z (X ⨿ Y)

In a CCC with binary coproducts, the distribution morphism is an isomorphism.

Equations

• CategoryTheory.prodCoprodDistrib X Y Z = CategoryTheory.asIso (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft Z) X Y)

theorem CategoryTheory.strict_initial {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A : C} [Closed A] {I : C} (t : Limits.IsInitial I) (f : A ⟶ I) : IsIso f

If an initial object I exists in a CCC then it is a strict initial object, i.e. any morphism to I is an iso. This actually shows a slightly stronger version: any morphism to an initial object from an exponentiable object is an isomorphism.

instance CategoryTheory.to_initial_isIso {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A : C} [Closed A] [Limits.HasInitial C] (f : A ⟶ ⊥_ C) : IsIso f

theorem CategoryTheory.initial_mono {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {I : C} (B : C) (t : Limits.IsInitial I) [MonoidalClosed C] : Mono (t.to B)

If an initial object 0 exists in a CCC then every morphism from it is monic.

instance CategoryTheory.Initial.mono_to {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [Limits.HasInitial C] (B : C) [MonoidalClosed C] : Mono (Limits.initial.to B)

noncomputable def CategoryTheory.cartesianClosedOfEquiv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (e : C ≌ D) [MonoidalClosed C] : MonoidalClosed D

Transport the property of being Cartesian closed across an equivalence of categories.

Note we didn't require any coherence between the choice of finite products here, since we transport along the prodComparison isomorphism.

Equations

• CategoryTheory.cartesianClosedOfEquiv e = CategoryTheory.MonoidalClosed.ofEquiv e.inverse e.symm.toAdjunction

@[deprecated CategoryTheory.Closed (since := "2025-12-22")]

def CategoryTheory.Exponentiable {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X : C) : Type (max u v)

Alias of CategoryTheory.Closed.

Equations

• @CategoryTheory.Exponentiable = @CategoryTheory.Closed

@[deprecated CategoryTheory.Closed.mk (since := "2025-12-22")]

def CategoryTheory.Exponentiable.mk {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X : C} (rightAdj : Functor C C) (adj : MonoidalCategory.tensorLeft X ⊣ rightAdj) : Closed X

Alias of CategoryTheory.Closed.mk.

Equations

• @CategoryTheory.Exponentiable.mk = @CategoryTheory.Closed.mk

@[deprecated CategoryTheory.tensorClosed (since := "2025-12-22")]

def CategoryTheory.binaryProductExponentiable {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} (hX : Closed X) (hY : Closed Y) : Closed (MonoidalCategoryStruct.tensorObj X Y)

Alias of CategoryTheory.tensorClosed.

Equations

• @CategoryTheory.binaryProductExponentiable = @CategoryTheory.tensorClosed

@[deprecated CategoryTheory.unitClosed (since := "2025-12-22")]

def CategoryTheory.terminalExponentiable {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : Closed (MonoidalCategoryStruct.tensorUnit C)

Alias of CategoryTheory.unitClosed.

Equations

• @CategoryTheory.terminalExponentiable = @CategoryTheory.unitClosed

@[deprecated CategoryTheory.MonoidalClosed (since := "2025-12-22")]

def CategoryTheory.CartesianClosed (C : Type u) [Category.{v, u} C] [MonoidalCategory C] : Type (max u v)

Alias of CategoryTheory.MonoidalClosed.

Equations

• CategoryTheory.CartesianClosed = CategoryTheory.MonoidalClosed

@[deprecated CategoryTheory.MonoidalClosed.mk (since := "2025-12-22")]

def CategoryTheory.CartesianClosed.mk {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (closed : (X : C) → Closed X := by infer_instance) : MonoidalClosed C

Alias of CategoryTheory.MonoidalClosed.mk.

Equations

• @CategoryTheory.CartesianClosed.mk = @CategoryTheory.MonoidalClosed.mk

@[deprecated CategoryTheory.ihom (since := "2025-12-22")]

def CategoryTheory.exp {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : Functor C C

Alias of CategoryTheory.ihom.

Equations

• @CategoryTheory.exp = @CategoryTheory.ihom

@[deprecated CategoryTheory.ihom.adjunction (since := "2025-12-22")]

def CategoryTheory.exp.adjunction {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : MonoidalCategory.tensorLeft A ⊣ ihom A

Alias of CategoryTheory.ihom.adjunction.

Equations

• @CategoryTheory.exp.adjunction = @CategoryTheory.ihom.adjunction

@[deprecated CategoryTheory.ihom.ev (since := "2025-12-22")]

def CategoryTheory.exp.ev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : (ihom A).comp (MonoidalCategory.tensorLeft A) ⟶ Functor.id C

Alias of CategoryTheory.ihom.ev.

Equations

• @CategoryTheory.exp.ev = @CategoryTheory.ihom.ev

@[deprecated CategoryTheory.ihom.coev (since := "2025-12-22")]

def CategoryTheory.exp.coev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : Functor.id C ⟶ (MonoidalCategory.tensorLeft A).comp (ihom A)

Alias of CategoryTheory.ihom.coev.

Equations

• @CategoryTheory.exp.coev = @CategoryTheory.ihom.coev

@[deprecated CategoryTheory.ihom.ev_coev (since := "2025-12-22")]

theorem CategoryTheory.exp.ev_coev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : C) [Closed A] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A ((ihom.coev A).app B)) ((ihom.ev A).app (MonoidalCategoryStruct.tensorObj A B)) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj A B)

Alias of CategoryTheory.ihom.ev_coev.

@[deprecated CategoryTheory.ihom.coev_ev (since := "2025-12-22")]

theorem CategoryTheory.exp.coev_ev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : C) [Closed A] : CategoryStruct.comp ((ihom.coev A).app (A ⟹ B)) ((ihom A).map ((ihom.ev A).app B)) = CategoryStruct.id (A ⟹ B)

Alias of CategoryTheory.ihom.coev_ev.

@[deprecated CategoryTheory.ihom.ev_coev_assoc (since := "2025-12-22")]

theorem CategoryTheory.exp.ev_coev_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : C) [Closed A] {Z : C} (h : MonoidalCategoryStruct.tensorObj A B ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A ((ihom.coev A).app B)) (CategoryStruct.comp ((ihom.ev A).app (MonoidalCategoryStruct.tensorObj A B)) h) = h

Alias of CategoryTheory.ihom.ev_coev_assoc.

@[deprecated CategoryTheory.ihom.coev_ev_assoc (since := "2025-12-22")]

theorem CategoryTheory.exp.coev_ev_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : C) [Closed A] {Z : C} (h : A ⟹ B ⟶ Z) : CategoryStruct.comp ((ihom.coev A).app (A ⟹ B)) (CategoryStruct.comp ((ihom A).map ((ihom.ev A).app B)) h) = h

Alias of CategoryTheory.ihom.coev_ev_assoc.

@[deprecated CategoryTheory.MonoidalClosed.curry (since := "2025-12-22")]

def CategoryTheory.CartesianClosed.curry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] : (MonoidalCategoryStruct.tensorObj A Y ⟶ X) → (Y ⟶ A ⟹ X)

Alias of CategoryTheory.MonoidalClosed.curry.

Equations

• @CategoryTheory.CartesianClosed.curry = @CategoryTheory.MonoidalClosed.curry

@[deprecated CategoryTheory.MonoidalClosed.uncurry (since := "2025-12-22")]

def CategoryTheory.CartesianClosed.uncurry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] : (Y ⟶ A ⟹ X) → (MonoidalCategoryStruct.tensorObj A Y ⟶ X)

Alias of CategoryTheory.MonoidalClosed.uncurry.

Equations

• @CategoryTheory.CartesianClosed.uncurry = @CategoryTheory.MonoidalClosed.uncurry

@[deprecated CategoryTheory.MonoidalClosed.homEquiv_apply_eq (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.homEquiv_apply_eq {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (f : MonoidalCategoryStruct.tensorObj A Y ⟶ X) : ((ihom.adjunction A).homEquiv Y X) f = MonoidalClosed.curry f

Alias of CategoryTheory.MonoidalClosed.homEquiv_apply_eq.

@[deprecated CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.homEquiv_symm_apply_eq {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (f : Y ⟶ A ⟹ X) : ((ihom.adjunction A).homEquiv Y X).symm f = MonoidalClosed.uncurry f

Alias of CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq.

@[deprecated CategoryTheory.MonoidalClosed.curry_natural_left (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.curry_natural_left {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X X' Y : C} [Closed A] (f : X ⟶ X') (g : MonoidalCategoryStruct.tensorObj A X' ⟶ Y) : MonoidalClosed.curry (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A f) g) = CategoryStruct.comp f (MonoidalClosed.curry g)

Alias of CategoryTheory.MonoidalClosed.curry_natural_left.

@[deprecated CategoryTheory.MonoidalClosed.curry_natural_left_assoc (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.curry_natural_left_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X X' Y : C} [Closed A] (f : X ⟶ X') (g : MonoidalCategoryStruct.tensorObj A X' ⟶ Y) {Z : C} (h : A ⟹ Y ⟶ Z) : CategoryStruct.comp (MonoidalClosed.curry (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A f) g)) h = CategoryStruct.comp f (CategoryStruct.comp (MonoidalClosed.curry g) h)

Alias of CategoryTheory.MonoidalClosed.curry_natural_left_assoc.

@[deprecated CategoryTheory.MonoidalClosed.curry_natural_right (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.curry_natural_right {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y Y' : C} [Closed A] (f : MonoidalCategoryStruct.tensorObj A X ⟶ Y) (g : Y ⟶ Y') : MonoidalClosed.curry (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalClosed.curry f) ((ihom A).map g)

Alias of CategoryTheory.MonoidalClosed.curry_natural_right.

@[deprecated CategoryTheory.MonoidalClosed.curry_natural_right_assoc (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.curry_natural_right_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y Y' : C} [Closed A] (f : MonoidalCategoryStruct.tensorObj A X ⟶ Y) (g : Y ⟶ Y') {Z : C} (h : A ⟹ Y' ⟶ Z) : CategoryStruct.comp (MonoidalClosed.curry (CategoryStruct.comp f g)) h = CategoryStruct.comp (MonoidalClosed.curry f) (CategoryStruct.comp ((ihom A).map g) h)

Alias of CategoryTheory.MonoidalClosed.curry_natural_right_assoc.

@[deprecated CategoryTheory.MonoidalClosed.uncurry_natural_right (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.uncurry_natural_right {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y Y' : C} [Closed A] (f : X ⟶ A ⟹ Y) (g : Y ⟶ Y') : MonoidalClosed.uncurry (CategoryStruct.comp f ((ihom A).map g)) = CategoryStruct.comp (MonoidalClosed.uncurry f) g

Alias of CategoryTheory.MonoidalClosed.uncurry_natural_right.

@[deprecated CategoryTheory.MonoidalClosed.uncurry_natural_right_assoc (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.uncurry_natural_right_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y Y' : C} [Closed A] (f : X ⟶ A ⟹ Y) (g : Y ⟶ Y') {Z : C} (h : Y' ⟶ Z) : CategoryStruct.comp (MonoidalClosed.uncurry (CategoryStruct.comp f ((ihom A).map g))) h = CategoryStruct.comp (MonoidalClosed.uncurry f) (CategoryStruct.comp g h)

Alias of CategoryTheory.MonoidalClosed.uncurry_natural_right_assoc.

@[deprecated CategoryTheory.MonoidalClosed.uncurry_natural_left (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.uncurry_natural_left {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X X' Y : C} [Closed A] (f : X ⟶ X') (g : X' ⟶ A ⟹ Y) : MonoidalClosed.uncurry (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A f) (MonoidalClosed.uncurry g)

Alias of CategoryTheory.MonoidalClosed.uncurry_natural_left.

@[deprecated CategoryTheory.MonoidalClosed.uncurry_natural_left_assoc (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.uncurry_natural_left_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X X' Y : C} [Closed A] (f : X ⟶ X') (g : X' ⟶ A ⟹ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (MonoidalClosed.uncurry (CategoryStruct.comp f g)) h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A f) (CategoryStruct.comp (MonoidalClosed.uncurry g) h)

Alias of CategoryTheory.MonoidalClosed.uncurry_natural_left_assoc.

@[deprecated CategoryTheory.MonoidalClosed.uncurry_curry (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.uncurry_curry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (f : MonoidalCategoryStruct.tensorObj A X ⟶ Y) : MonoidalClosed.uncurry (MonoidalClosed.curry f) = f

Alias of CategoryTheory.MonoidalClosed.uncurry_curry.

@[deprecated CategoryTheory.MonoidalClosed.curry_uncurry (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.curry_uncurry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (f : X ⟶ A ⟹ Y) : MonoidalClosed.curry (MonoidalClosed.uncurry f) = f

Alias of CategoryTheory.MonoidalClosed.curry_uncurry.

@[deprecated CategoryTheory.MonoidalClosed.curry_eq_iff (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.curry_eq_iff {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (f : MonoidalCategoryStruct.tensorObj A Y ⟶ X) (g : Y ⟶ A ⟹ X) : MonoidalClosed.curry f = g ↔ f = MonoidalClosed.uncurry g

Alias of CategoryTheory.MonoidalClosed.curry_eq_iff.

@[deprecated CategoryTheory.MonoidalClosed.eq_curry_iff (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.eq_curry_iff {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (f : MonoidalCategoryStruct.tensorObj A Y ⟶ X) (g : Y ⟶ A ⟹ X) : g = MonoidalClosed.curry f ↔ MonoidalClosed.uncurry g = f

Alias of CategoryTheory.MonoidalClosed.eq_curry_iff.

@[deprecated CategoryTheory.MonoidalClosed.uncurry_eq (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.uncurry_eq {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (g : Y ⟶ A ⟹ X) : MonoidalClosed.uncurry g = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A g) ((ihom.ev A).app X)

Alias of CategoryTheory.MonoidalClosed.uncurry_eq.

@[deprecated CategoryTheory.MonoidalClosed.curry_eq (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.curry_eq {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (g : MonoidalCategoryStruct.tensorObj A Y ⟶ X) : MonoidalClosed.curry g = CategoryStruct.comp ((ihom.coev A).app Y) ((ihom A).map g)

Alias of CategoryTheory.MonoidalClosed.curry_eq.

@[deprecated CategoryTheory.MonoidalClosed.uncurry_id_eq_ev (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.uncurry_id_eq_ev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A X : C) [Closed A] : MonoidalClosed.uncurry (CategoryStruct.id (A ⟹ X)) = (ihom.ev A).app X

Alias of CategoryTheory.MonoidalClosed.uncurry_id_eq_ev.

@[deprecated CategoryTheory.MonoidalClosed.curry_id_eq_coev (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.curry_id_eq_coev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A X : C) [Closed A] : MonoidalClosed.curry (CategoryStruct.id (MonoidalCategoryStruct.tensorObj A ((Functor.id C).obj X))) = (ihom.coev A).app X

Alias of CategoryTheory.MonoidalClosed.curry_id_eq_coev.

@[deprecated CategoryTheory.MonoidalClosed.curry_injective (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.curry_injective {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] : Function.Injective MonoidalClosed.curry

Alias of CategoryTheory.MonoidalClosed.curry_injective.

@[deprecated CategoryTheory.MonoidalClosed.uncurry_injective (since := "2025-12-22")]

theorem CategoryTheory.CartesianClosed.uncurry_injective {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] : Function.Injective MonoidalClosed.uncurry

Alias of CategoryTheory.MonoidalClosed.uncurry_injective.

@[deprecated CategoryTheory.MonoidalClosed.unitNatIso (since := "2025-12-22")]

def CategoryTheory.expUnitNatIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Closed (MonoidalCategoryStruct.tensorUnit C)] : Functor.id C ≅ ihom (MonoidalCategoryStruct.tensorUnit C)

Alias of CategoryTheory.MonoidalClosed.unitNatIso.

Equations

• @CategoryTheory.expUnitNatIso = @CategoryTheory.MonoidalClosed.unitNatIso

@[deprecated CategoryTheory.MonoidalClosed.unitIsoSelf (since := "2025-12-22")]

def CategoryTheory.expUnitIsoSelf {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X : C) [Closed (MonoidalCategoryStruct.tensorUnit C)] : MonoidalCategoryStruct.tensorUnit C ⟹ X ≅ X

Alias of CategoryTheory.MonoidalClosed.unitIsoSelf.

Equations

• @CategoryTheory.expUnitIsoSelf = @CategoryTheory.MonoidalClosed.unitIsoSelf

@[deprecated CategoryTheory.MonoidalClosed.pre (since := "2025-12-22")]

def CategoryTheory.pre {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} [Closed A] [Closed B] (f : B ⟶ A) : ihom A ⟶ ihom B

Alias of CategoryTheory.MonoidalClosed.pre.

Equations

• @CategoryTheory.pre = @CategoryTheory.MonoidalClosed.pre

@[deprecated CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev (since := "2025-12-22")]

theorem CategoryTheory.prod_map_pre_app_comp_ev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} [Closed A] [Closed B] (f : B ⟶ A) (X : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft B ((MonoidalClosed.pre f).app X)) ((ihom.ev B).app X) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (A ⟹ X)) ((ihom.ev A).app X)

Alias of CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev.

@[deprecated CategoryTheory.MonoidalClosed.uncurry_pre (since := "2025-12-22")]

theorem CategoryTheory.uncurry_pre {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} [Closed A] [Closed B] (f : B ⟶ A) (X : C) : MonoidalClosed.uncurry ((MonoidalClosed.pre f).app X) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (A ⟹ X)) ((ihom.ev A).app X)

Alias of CategoryTheory.MonoidalClosed.uncurry_pre.

@[deprecated CategoryTheory.MonoidalClosed.coev_app_comp_pre_app (since := "2025-12-22")]

theorem CategoryTheory.coev_app_comp_pre_app {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} (X : C) [Closed A] [Closed B] (f : B ⟶ A) : CategoryStruct.comp ((ihom.coev A).app X) ((MonoidalClosed.pre f).app (MonoidalCategoryStruct.tensorObj A X)) = CategoryStruct.comp ((ihom.coev B).app X) ((ihom B).map (MonoidalCategoryStruct.whiskerRight f X))

Alias of CategoryTheory.MonoidalClosed.coev_app_comp_pre_app.

@[deprecated CategoryTheory.MonoidalClosed.pre_id (since := "2025-12-22")]

theorem CategoryTheory.pre_id {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : MonoidalClosed.pre (CategoryStruct.id A) = CategoryStruct.id (ihom A)

Alias of CategoryTheory.MonoidalClosed.pre_id.

@[deprecated CategoryTheory.MonoidalClosed.pre_map (since := "2025-12-22")]

theorem CategoryTheory.pre_map {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A₁ A₂ A₃ : C} [Closed A₁] [Closed A₂] [Closed A₃] (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) : MonoidalClosed.pre (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalClosed.pre g) (MonoidalClosed.pre f)

Alias of CategoryTheory.MonoidalClosed.pre_map.

@[deprecated CategoryTheory.MonoidalClosed.internalHom (since := "2025-12-22")]

def CategoryTheory.internalHom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] : Functor Cᵒᵖ (Functor C C)

Alias of CategoryTheory.MonoidalClosed.internalHom.

Equations

• @CategoryTheory.internalHom = @CategoryTheory.MonoidalClosed.internalHom