CategoryTheory.forgetEnrichment_comp
theorem CategoryTheory.forgetEnrichment_comp :
ā {C : Type uā} (W : Type (v + 1)) [inst : CategoryTheory.Category.{v, v + 1} W]
[inst_1 : CategoryTheory.MonoidalCategory W] [inst_2 : CategoryTheory.EnrichedCategory W C]
{X Y Z : CategoryTheory.ForgetEnrichment W C} (f : X ā¶ Y) (g : Y ā¶ Z),
CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.CategoryStruct.comp f g) =
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (š_ W)).inv
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.ForgetEnrichment.homTo W f)
(CategoryTheory.ForgetEnrichment.homTo W g)))
(CategoryTheory.eComp W (CategoryTheory.ForgetEnrichment.to W X) (CategoryTheory.ForgetEnrichment.to W Y)
(CategoryTheory.ForgetEnrichment.to W Z))
The theorem `CategoryTheory.forgetEnrichment_comp` states that for any enriched category C over a monoidal category W, and any three objects X, Y, Z in the forgetful enrichment of C, the composition of two morphisms f: X ā¶ Y and g: Y ā¶ Z in this enriched category is equal to the composition of certain other specific morphisms in the underlying category W. These specific morphisms involve the inverse of the left unitor of the identity morphism in W, the tensor product of the morphisms f and g when regarded as morphisms in W, and the enriched composition of the objects X, Y, Z. This theorem effectively describes how to compute the composition of morphisms in the enriched category in terms of compositions of morphisms in the underlying monoidal category.
More concisely: For any enriched category C over a monoidal category W and objects X, Y, Z in C, the composition of morphisms f: X ā¶ Y and g: Y ā¶ Z in the forgetful enrichment of C is equal to the tensor product of f and g in W followed by the composition of Z, Y, X using the inverse of the left unitor of the identity morphism in W.
|
CategoryTheory.forgetEnrichment_id
theorem CategoryTheory.forgetEnrichment_id :
ā {C : Type uā} (W : Type (v + 1)) [inst : CategoryTheory.Category.{v, v + 1} W]
[inst_1 : CategoryTheory.MonoidalCategory W] [inst_2 : CategoryTheory.EnrichedCategory W C]
(X : CategoryTheory.ForgetEnrichment W C),
CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.CategoryStruct.id X) =
CategoryTheory.eId W (CategoryTheory.ForgetEnrichment.to W X)
This theorem, `CategoryTheory.forgetEnrichment_id`, states that for any type `C` and `W` where `W` is a monoidal category and `C` is enriched over `W`, and any object `X` in the category given by forgetting the enrichment of `C` over `W`, the identity morphism on `X` in the "underlying" category (obtained by applying `CategoryTheory.ForgetEnrichment.homTo W` to `CategoryTheory.CategoryStruct.id X`) is equal to the identity morphism in the enriched category on the object obtained by checking `X` as an object of `C` (given by `CategoryTheory.eId W (CategoryTheory.ForgetEnrichment.to W X)`). This captures the idea that the process of 'forgetting the enrichment' preserves the identity morphism.
More concisely: For any monoidal category `W` and an enriched category `C` over `W`, the identity morphism of an object `X` in the forgetten category is equal to the identity morphism of `X` in `C`.
|