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')
[CategoryTheory.Category.{v', u'} V]
[CategoryTheory.MonoidalCategory V]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.EnrichedOrdinaryCategory V C]
{X Y X₁ Y₁ : C}
(α : X ≅ X₁)
(β : Y ≅ 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₁.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Iso.eHomCongr_inv
(V : Type u')
[CategoryTheory.Category.{v', u'} V]
[CategoryTheory.MonoidalCategory V]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.EnrichedOrdinaryCategory V C]
{X Y X₁ Y₁ : C}
(α : X ≅ X₁)
(β : Y ≅ Y₁)
:
(CategoryTheory.Iso.eHomCongr V α β).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V α.hom Y₁)
(CategoryTheory.eHomWhiskerLeft V X β.inv)
@[simp]
theorem
CategoryTheory.Iso.eHomCongr_hom
(V : Type u')
[CategoryTheory.Category.{v', u'} V]
[CategoryTheory.MonoidalCategory V]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.EnrichedOrdinaryCategory V C]
{X Y X₁ Y₁ : C}
(α : X ≅ X₁)
(β : Y ≅ Y₁)
:
(CategoryTheory.Iso.eHomCongr V α β).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V α.inv Y)
(CategoryTheory.eHomWhiskerLeft V X₁ β.hom)
theorem
CategoryTheory.Iso.eHomCongr_refl
(V : Type u')
[CategoryTheory.Category.{v', u'} V]
[CategoryTheory.MonoidalCategory V]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.EnrichedOrdinaryCategory V C]
(X Y : C)
:
theorem
CategoryTheory.Iso.eHomCongr_trans
(V : Type u')
[CategoryTheory.Category.{v', u'} V]
[CategoryTheory.MonoidalCategory V]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.EnrichedOrdinaryCategory V C]
{X₁ Y₁ X₂ Y₂ X₃ Y₃ : C}
(α₁ : X₁ ≅ X₂)
(β₁ : Y₁ ≅ Y₂)
(α₂ : X₂ ≅ X₃)
(β₂ : Y₂ ≅ Y₃)
:
CategoryTheory.Iso.eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂) = CategoryTheory.Iso.eHomCongr V α₁ β₁ ≪≫ CategoryTheory.Iso.eHomCongr V α₂ β₂
theorem
CategoryTheory.Iso.eHomCongr_symm
(V : Type u')
[CategoryTheory.Category.{v', u'} V]
[CategoryTheory.MonoidalCategory V]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.EnrichedOrdinaryCategory V C]
{X Y X₁ Y₁ : C}
(α : X ≅ X₁)
(β : Y ≅ Y₁)
:
(CategoryTheory.Iso.eHomCongr V α β).symm = CategoryTheory.Iso.eHomCongr V α.symm β.symm
theorem
CategoryTheory.Iso.eHomCongr_comp
(V : Type u')
[CategoryTheory.Category.{v', u'} V]
[CategoryTheory.MonoidalCategory V]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.EnrichedOrdinaryCategory V C]
{X Y Z X₁ Y₁ Z₁ : C}
(α : X ≅ X₁)
(β : Y ≅ Y₁)
(γ : Z ≅ Z₁)
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g))
(CategoryTheory.Iso.eHomCongr V α γ).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ V)).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) f) (CategoryTheory.Iso.eHomCongr V α β).hom)
(𝟙_ V))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom X₁ Y₁)
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) g)
(CategoryTheory.Iso.eHomCongr V β γ).hom))
(CategoryTheory.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')
[CategoryTheory.Category.{v', u'} V]
[CategoryTheory.MonoidalCategory V]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.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 : CategoryTheory.EnrichedCategory.Hom X₁ Z₁ ⟶ Z✝)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.eHomCongr V α γ).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ V)).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) f) (CategoryTheory.Iso.eHomCongr V α β).hom)
(𝟙_ V))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom X₁ Y₁)
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) g)
(CategoryTheory.Iso.eHomCongr V β γ).hom))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X₁ Y₁ Z₁) h)))
theorem
CategoryTheory.Iso.eHomCongr_inv_comp
(V : Type u')
[CategoryTheory.Category.{v', u'} V]
[CategoryTheory.MonoidalCategory V]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.EnrichedOrdinaryCategory V C]
{X Y Z X₁ Y₁ Z₁ : C}
(α : X ≅ X₁)
(β : Y ≅ Y₁)
(γ : Z ≅ Z₁)
(f : X₁ ⟶ Y₁)
(g : Y₁ ⟶ Z₁)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g))
(CategoryTheory.Iso.eHomCongr V α γ).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ V)).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) f) (CategoryTheory.Iso.eHomCongr V α β).inv)
(𝟙_ V))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom X Y)
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) g)
(CategoryTheory.Iso.eHomCongr V β γ).inv))
(CategoryTheory.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')
[CategoryTheory.Category.{v', u'} V]
[CategoryTheory.MonoidalCategory V]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.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 : CategoryTheory.EnrichedCategory.Hom X Z ⟶ Z✝)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.eHomCongr V α γ).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ V)).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) f) (CategoryTheory.Iso.eHomCongr V α β).inv)
(𝟙_ V))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom X Y)
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) g)
(CategoryTheory.Iso.eHomCongr V β γ).inv))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) h)))