Precomposing an internal Hom with an isomorphism or an epimorphism

MonoidalClosed.pre_isIso states that precomposition by an isomorphism of objects is an isomorphism of internal Hom functors, and MonoidalClosed.mono_pre_app that, in a braided closed monoidal category, precomposition by an epimorphism is a monomorphism of internal Homs: [-, X] is contravariant and turns epimorphisms into monomorphisms.

Use MonoidalClosed.pre_isIso when an isomorphism of source objects identifies the two internal Hom functors appearing in a comparison, so that invertibility, or any other isomorphism-level property, can be read across that identification. For instance it is how the invertibility of one internal-Hom comparison is transported to an isomorphic source object in CategoryTheory.Functor.ihomComparison_isIso_of_iso. It is Mathlib's isomorphism instance CategoryTheory.conjugateEquiv_iso specialized to MonoidalClosed.pre.

Main declarations

• MonoidalClosed.pre_isIso;
• MonoidalClosed.mono_pre_app.

theorem CategoryTheory.MonoidalClosed.pre_isIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} (e : A ≅ B) [Closed A] [Closed B] : IsIso (pre e.hom)

Precomposition with an isomorphism, as a natural transformation between internal Hom functors, is an isomorphism.

instance CategoryTheory.MonoidalClosed.mono_pre_app {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] {A B : C} (f : B ⟶ A) [Epi f] (X : C) : Mono ((pre f).app X)

In a braided closed monoidal category, precomposition of internal Homs with an epimorphism f : B ⟶ A is a monomorphism (A ⟶[C] X) ⟶ (B ⟶[C] X).