Congruence of enriched homs

Recall that when C is both a category and a V-enriched category, we say it is an EnrichedOrdinaryCategory if it comes equipped with a sufficiently compatible equivalence between morphisms X ⟶ Y in C and morphisms 𝟙_ V ⟶ (X ⟶[V] Y) in V.

In such a V-enriched ordinary category C, isomorphisms in C induce isomorphisms between hom-objects in V. We define this isomorphism in CategoryTheory.Iso.eHomCongr and prove that it respects composition in C.

The treatment here parallels that for unenriched categories in Mathlib/CategoryTheory/HomCongr.lean and that for sorts in Mathlib/Logic/Equiv/Defs.lean (cf. Equiv.arrowCongr). Note, however, that they construct equivalences between Types and Sorts, respectively, while in this file we construct isomorphisms between objects in V.

def CategoryTheory.Iso.eHomCongr (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) : (X ⟶[V] Y) ≅ X₁ ⟶[V] Y₁

Given isomorphisms α : X ≅ X₁ and β : Y ≅ Y₁ in C, we can construct an isomorphism between V objects X ⟶[V] Y and X₁ ⟶[V] Y₁.

@[simp]

theorem CategoryTheory.Iso.eHomCongr_inv (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) : (eHomCongr V α β).inv = CategoryStruct.comp (eHomWhiskerRight V α.hom Y₁) (eHomWhiskerLeft V X β.inv)

@[simp]

theorem CategoryTheory.Iso.eHomCongr_hom (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) : (eHomCongr V α β).hom = CategoryStruct.comp (eHomWhiskerRight V α.inv Y) (eHomWhiskerLeft V X₁ β.hom)

theorem CategoryTheory.Iso.eHomCongr_refl (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X Y : C) : eHomCongr V (refl X) (refl Y) = refl (X ⟶[V] Y)

theorem CategoryTheory.Iso.eHomCongr_trans (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X₁ Y₁ X₂ Y₂ X₃ Y₃ : C} (α₁ : X₁ ≅ X₂) (β₁ : Y₁ ≅ Y₂) (α₂ : X₂ ≅ X₃) (β₂ : Y₂ ≅ Y₃) : eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂) = eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂

theorem CategoryTheory.Iso.eHomCongr_symm (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) : (eHomCongr V α β).symm = eHomCongr V α.symm β.symm

theorem CategoryTheory.Iso.eHomCongr_comp (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryStruct.comp ((eHomEquiv V) (CategoryStruct.comp f g)) (eHomCongr V α γ).hom = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit V)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp ((eHomEquiv V) f) (eHomCongr V α β).hom) (MonoidalCategoryStruct.tensorUnit V)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X₁ ⟶[V] Y₁) (CategoryStruct.comp ((eHomEquiv V) g) (eHomCongr V β γ).hom)) (eComp V X₁ Y₁ Z₁)))

eHomCongr respects composition of morphisms. Recall that for any composable pair of arrows f : X ⟶ Y and g : Y ⟶ Z in C, the composite f ≫ g in C defines a morphism 𝟙_ V ⟶ (X ⟶[V] Z) in V. Composing with the isomorphism eHomCongr V α γ yields a morphism in V that can be factored through the enriched composition map as shown: 𝟙_ V ⟶ 𝟙_ V ⊗ 𝟙_ V ⟶ (X₁ ⟶[V] Y₁) ⊗ (Y₁ ⟶[V] Z₁) ⟶ (X₁ ⟶[V] Z₁).

theorem CategoryTheory.Iso.eHomCongr_comp_assoc (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : V} (h : (X₁ ⟶[V] Z₁) ⟶ Z✝) : CategoryStruct.comp ((eHomEquiv V) (CategoryStruct.comp f g)) (CategoryStruct.comp (eHomCongr V α γ).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit V)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp ((eHomEquiv V) f) (eHomCongr V α β).hom) (MonoidalCategoryStruct.tensorUnit V)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X₁ ⟶[V] Y₁) (CategoryStruct.comp ((eHomEquiv V) g) (eHomCongr V β γ).hom)) (CategoryStruct.comp (eComp V X₁ Y₁ Z₁) h)))

eHomCongr respects composition of morphisms. Recall that for any composable pair of arrows f : X ⟶ Y and g : Y ⟶ Z in C, the composite f ≫ g in C defines a morphism 𝟙_ V ⟶ (X ⟶[V] Z) in V. Composing with the isomorphism eHomCongr V α γ yields a morphism in V that can be factored through the enriched composition map as shown: 𝟙_ V ⟶ 𝟙_ V ⊗ 𝟙_ V ⟶ (X₁ ⟶[V] Y₁) ⊗ (Y₁ ⟶[V] Z₁) ⟶ (X₁ ⟶[V] Z₁).

theorem CategoryTheory.Iso.eHomCongr_inv_comp (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X₁ ⟶ Y₁) (g : Y₁ ⟶ Z₁) : CategoryStruct.comp ((eHomEquiv V) (CategoryStruct.comp f g)) (eHomCongr V α γ).inv = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit V)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp ((eHomEquiv V) f) (eHomCongr V α β).inv) (MonoidalCategoryStruct.tensorUnit V)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryStruct.comp ((eHomEquiv V) g) (eHomCongr V β γ).inv)) (eComp V X Y Z)))

The inverse map defined by eHomCongr respects composition of morphisms.

theorem CategoryTheory.Iso.eHomCongr_inv_comp_assoc (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X₁ ⟶ Y₁) (g : Y₁ ⟶ Z₁) {Z✝ : V} (h : (X ⟶[V] Z) ⟶ Z✝) : CategoryStruct.comp ((eHomEquiv V) (CategoryStruct.comp f g)) (CategoryStruct.comp (eHomCongr V α γ).inv h) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit V)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp ((eHomEquiv V) f) (eHomCongr V α β).inv) (MonoidalCategoryStruct.tensorUnit V)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryStruct.comp ((eHomEquiv V) g) (eHomCongr V β γ).inv)) (CategoryStruct.comp (eComp V X Y Z) h)))

The inverse map defined by eHomCongr respects composition of morphisms.