CategoryTheory.whiskerRight_id'
theorem CategoryTheory.whiskerRight_id' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor C D} (F : CategoryTheory.Functor D E),
CategoryTheory.whiskerRight (CategoryTheory.CategoryStruct.id G) F =
CategoryTheory.CategoryStruct.id (G.comp F)
This theorem is stating that in the context of three categories `C`, `D`, and `E`, and two functors `G` from `C` to `D` and `F` from `D` to `E`, the operation of "whiskering" the identity morphism on `G` on the right by `F` is equivalent to the identity morphism on the composition of the functors `G` and `F`. In other words, "whiskering" the identity doesn't change the functorial composition. In mathematical terms, this can be expressed as `CategoryTheory.whiskerRight (CategoryTheory.CategoryStruct.id G) F = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.comp G F)`.
More concisely: The operation of whiskering the identity morphism of a functor `G` on the right by another functor `F` is equal to the identity morphism of the composite functor `G ∘ F`.
|
CategoryTheory.whiskerRight_comp
theorem CategoryTheory.whiskerRight_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
{G H K : CategoryTheory.Functor C D} (α : G ⟶ H) (β : H ⟶ K) (F : CategoryTheory.Functor D E),
CategoryTheory.whiskerRight (CategoryTheory.CategoryStruct.comp α β) F =
CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight α F) (CategoryTheory.whiskerRight β F)
The theorem `CategoryTheory.whiskerRight_comp` in Lean 4 states that for any three categories `C`, `D`, and `E`, and any three functors `G`, `H`, and `K` from `C` to `D` (with corresponding morphisms `α : G ⟶ H` and `β : H ⟶ K`), and any functor `F` from `D` to `E`, the operation of "whiskering on the right" by `F` preserves the composition of morphisms. This means that whiskering the composition of `α` and `β` is the same as the composition of the whiskerings of `α` and `β`. In mathematical notation, we have `(α ≫ β) ⊗ F = (α ⊗ F) ≫ (β ⊗ F)`, where `≫` denotes composition and `⊗` denotes whiskering on the right.
More concisely: For any functors G, H, K from category C to categories D and E, and functor F from D to E, the right whiskering of the composition of G and H with F is equal to the composition of the right whiskerings of G and H with F. In other words, (G ⊗ F) ≫ (H ⊗ F) = (G ≫ H) ⊗ F.
|