Normalization of morphisms in monoidal categories #
This file provides the implementation of the normalization given in
Mathlib.Tactic.CategoryTheory.Coherence.Normalize. See this file for more details.
theorem
Mathlib.Tactic.Monoidal.evalComp_nil_nil
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : C}
{g : C}
{h : C}
(α : f ≅ g)
(β : g ≅ h)
:
theorem
Mathlib.Tactic.Monoidal.evalComp_nil_cons
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : C}
{g : C}
{h : C}
{i : C}
{j : C}
(α : f ≅ g)
(β : g ≅ h)
(η : h ⟶ i)
(ηs : i ⟶ j)
:
CategoryTheory.CategoryStruct.comp α.hom
(CategoryTheory.CategoryStruct.comp β.hom (CategoryTheory.CategoryStruct.comp η ηs)) = CategoryTheory.CategoryStruct.comp (α ≪≫ β).hom (CategoryTheory.CategoryStruct.comp η ηs)
theorem
Mathlib.Tactic.Monoidal.evalComp_cons
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : C}
{g : C}
{h : C}
{i : C}
{j : C}
(α : f ≅ g)
(η : g ⟶ h)
{ηs : h ⟶ i}
{θ : i ⟶ j}
{ι : h ⟶ j}
(e_ι : CategoryTheory.CategoryStruct.comp ηs θ = ι)
:
theorem
Mathlib.Tactic.Monoidal.eval_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : C}
{g : C}
{h : C}
{η : f ⟶ g}
{η' : f ⟶ g}
{θ : g ⟶ h}
{θ' : g ⟶ h}
{ι : f ⟶ h}
(e_η : η = η')
(e_θ : θ = θ')
(e_ηθ : CategoryTheory.CategoryStruct.comp η' θ' = ι)
:
theorem
Mathlib.Tactic.Monoidal.eval_of
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : C}
{g : C}
(η : f ⟶ g)
:
theorem
Mathlib.Tactic.Monoidal.eval_monoidalComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : C}
{g : C}
{h : C}
{i : C}
{η : f ⟶ g}
{η' : f ⟶ g}
{α : g ≅ h}
{θ : h ⟶ i}
{θ' : h ⟶ i}
{αθ : g ⟶ i}
{ηαθ : f ⟶ i}
(e_η : η = η')
(e_θ : θ = θ')
(e_αθ : CategoryTheory.CategoryStruct.comp α.hom θ' = αθ)
(e_ηαθ : CategoryTheory.CategoryStruct.comp η' αθ = ηαθ)
:
CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp α.hom θ) = ηαθ
theorem
Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(f : C)
{g : C}
{h : C}
(α : g ≅ h)
:
theorem
Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
{h : C}
{i : C}
{j : C}
(α : g ≅ h)
(η : h ⟶ i)
{ηs : i ⟶ j}
{θ : CategoryTheory.MonoidalCategory.tensorObj f i ⟶ CategoryTheory.MonoidalCategory.tensorObj f j}
(e_θ : CategoryTheory.MonoidalCategory.whiskerLeft f ηs = θ)
:
CategoryTheory.MonoidalCategory.whiskerLeft f
(CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeftIso f α).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft f η) θ)
theorem
Mathlib.Tactic.Monoidal.evalWhiskerLeft_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
{h : C}
{i : C}
{η : h ⟶ i}
{η₁ : CategoryTheory.MonoidalCategory.tensorObj g h ⟶ CategoryTheory.MonoidalCategory.tensorObj g i}
{η₂ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g h) ⟶ CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g i)}
{η₃ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g h) ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) i}
{η₄ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) h ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) i}
(e_η₁ : CategoryTheory.MonoidalCategory.whiskerLeft g η = η₁)
(e_η₂ : CategoryTheory.MonoidalCategory.whiskerLeft f η₁ = η₂)
(e_η₃ : CategoryTheory.CategoryStruct.comp η₂ (CategoryTheory.MonoidalCategory.associator f g i).inv = η₃)
(e_η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f g h).hom η₃ = η₄)
:
theorem
Mathlib.Tactic.Monoidal.evalWhiskerLeft_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
{η : f ⟶ g}
{η₁ : f ⟶ CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) g}
{η₂ : CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) f ⟶ CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) g}
(e_η₁ : CategoryTheory.CategoryStruct.comp η (CategoryTheory.MonoidalCategory.leftUnitor g).inv = η₁)
(e_η₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor f).hom η₁ = η₂)
:
CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) η = η₂
theorem
Mathlib.Tactic.Monoidal.eval_whiskerLeft
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
{h : C}
{η : g ⟶ h}
{η' : g ⟶ h}
{θ : CategoryTheory.MonoidalCategory.tensorObj f g ⟶ CategoryTheory.MonoidalCategory.tensorObj f h}
(e_η : η = η')
(e_θ : CategoryTheory.MonoidalCategory.whiskerLeft f η' = θ)
:
theorem
Mathlib.Tactic.Monoidal.eval_whiskerRight
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
{h : C}
{η : f ⟶ g}
{η' : f ⟶ g}
{θ : CategoryTheory.MonoidalCategory.tensorObj f h ⟶ CategoryTheory.MonoidalCategory.tensorObj g h}
(e_η : η = η')
(e_θ : CategoryTheory.MonoidalCategory.whiskerRight η' h = θ)
:
theorem
Mathlib.Tactic.Monoidal.eval_tensorHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
{h : C}
{i : C}
{η : f ⟶ g}
{η' : f ⟶ g}
{θ : h ⟶ i}
{θ' : h ⟶ i}
{ι : CategoryTheory.MonoidalCategory.tensorObj f h ⟶ CategoryTheory.MonoidalCategory.tensorObj g i}
(e_η : η = η')
(e_θ : θ = θ')
(e_ι : CategoryTheory.MonoidalCategory.tensorHom η' θ' = ι)
:
theorem
Mathlib.Tactic.Monoidal.evalWhiskerRight_nil
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
(α : f ≅ g)
(h : C)
:
theorem
Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
{h : C}
{i : C}
{j : C}
{α : f ≅ g}
{η : g ⟶ h}
{ηs : h ⟶ i}
{ηs₁ : CategoryTheory.MonoidalCategory.tensorObj h j ⟶ CategoryTheory.MonoidalCategory.tensorObj i j}
{η₁ : CategoryTheory.MonoidalCategory.tensorObj g j ⟶ CategoryTheory.MonoidalCategory.tensorObj h j}
{η₂ : CategoryTheory.MonoidalCategory.tensorObj g j ⟶ CategoryTheory.MonoidalCategory.tensorObj i j}
{η₃ : CategoryTheory.MonoidalCategory.tensorObj f j ⟶ CategoryTheory.MonoidalCategory.tensorObj i j}
(e_ηs₁ : CategoryTheory.MonoidalCategory.whiskerRight ηs j = ηs₁)
(e_η₁ : CategoryTheory.MonoidalCategory.whiskerRight η j = η₁)
(e_η₂ : CategoryTheory.CategoryStruct.comp η₁ ηs₁ = η₂)
(e_η₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRightIso α j).hom η₂ = η₃)
:
theorem
Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_whisker
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
{h : C}
{i : C}
{j : C}
{k : C}
{α : g ≅ CategoryTheory.MonoidalCategory.tensorObj f h}
{η : h ⟶ i}
{ηs : CategoryTheory.MonoidalCategory.tensorObj f i ⟶ j}
{η₁ : CategoryTheory.MonoidalCategory.tensorObj h k ⟶ CategoryTheory.MonoidalCategory.tensorObj i k}
{η₂ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj h k) ⟶ CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj i k)}
{ηs₁ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f i) k ⟶ CategoryTheory.MonoidalCategory.tensorObj j k}
{ηs₂ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj i k) ⟶ CategoryTheory.MonoidalCategory.tensorObj j k}
{η₃ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj h k) ⟶ CategoryTheory.MonoidalCategory.tensorObj j k}
{η₄ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f h) k ⟶ CategoryTheory.MonoidalCategory.tensorObj j k}
{η₅ : CategoryTheory.MonoidalCategory.tensorObj g k ⟶ CategoryTheory.MonoidalCategory.tensorObj j k}
(e_η₁ : CategoryTheory.MonoidalCategory.whiskerRight
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl h).hom
(CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl i).hom))
k = η₁)
(e_η₂ : CategoryTheory.MonoidalCategory.whiskerLeft f η₁ = η₂)
(e_ηs₁ : CategoryTheory.MonoidalCategory.whiskerRight ηs k = ηs₁)
(e_ηs₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f i k).inv ηs₁ = ηs₂)
(e_η₃ : CategoryTheory.CategoryStruct.comp η₂ ηs₂ = η₃)
(e_η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f h k).hom η₃ = η₄)
(e_η₅ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRightIso α k).hom η₄ = η₅)
:
theorem
Mathlib.Tactic.Monoidal.evalWhiskerRight_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{f' : C}
{g : C}
{h : C}
{η : f ⟶ f'}
{η₁ : CategoryTheory.MonoidalCategory.tensorObj f g ⟶ CategoryTheory.MonoidalCategory.tensorObj f' g}
{η₂ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) h ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f' g) h}
{η₃ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) h ⟶ CategoryTheory.MonoidalCategory.tensorObj f' (CategoryTheory.MonoidalCategory.tensorObj g h)}
{η₄ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g h) ⟶ CategoryTheory.MonoidalCategory.tensorObj f' (CategoryTheory.MonoidalCategory.tensorObj g h)}
(e_η₁ : CategoryTheory.MonoidalCategory.whiskerRight η g = η₁)
(e_η₂ : CategoryTheory.MonoidalCategory.whiskerRight η₁ h = η₂)
(e_η₃ : CategoryTheory.CategoryStruct.comp η₂ (CategoryTheory.MonoidalCategory.associator f' g h).hom = η₃)
(e_η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f g h).inv η₃ = η₄)
:
theorem
Mathlib.Tactic.Monoidal.evalWhiskerRight_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
{η : f ⟶ g}
{η₁ : f ⟶ CategoryTheory.MonoidalCategory.tensorObj g (𝟙_ C)}
{η₂ : CategoryTheory.MonoidalCategory.tensorObj f (𝟙_ C) ⟶ CategoryTheory.MonoidalCategory.tensorObj g (𝟙_ C)}
(e_η₁ : CategoryTheory.CategoryStruct.comp η (CategoryTheory.MonoidalCategory.rightUnitor g).inv = η₁)
(e_η₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor f).hom η₁ = η₂)
:
CategoryTheory.MonoidalCategory.whiskerRight η (𝟙_ C) = η₂
theorem
Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
(η : f ⟶ g)
(h : C)
:
CategoryTheory.MonoidalCategory.whiskerRight η h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategory.tensorObj f h)).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight η h)
(CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategory.tensorObj g h)).hom)
theorem
Mathlib.Tactic.Monoidal.evalWhiskerRightAux_cons
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
{h : C}
{i : C}
{j : C}
{η : g ⟶ h}
{ηs : i ⟶ j}
{ηs' : CategoryTheory.MonoidalCategory.tensorObj i f ⟶ CategoryTheory.MonoidalCategory.tensorObj j f}
{η₁ : CategoryTheory.MonoidalCategory.tensorObj g (CategoryTheory.MonoidalCategory.tensorObj i f) ⟶ CategoryTheory.MonoidalCategory.tensorObj h (CategoryTheory.MonoidalCategory.tensorObj j f)}
{η₂ : CategoryTheory.MonoidalCategory.tensorObj g (CategoryTheory.MonoidalCategory.tensorObj i f) ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj h j) f}
{η₃ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj g i) f ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj h j) f}
(e_ηs' : CategoryTheory.MonoidalCategory.whiskerRight ηs f = ηs')
(e_η₁ : CategoryTheory.MonoidalCategory.tensorHom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl g).hom
(CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl h).hom))
ηs' = η₁)
(e_η₂ : CategoryTheory.CategoryStruct.comp η₁ (CategoryTheory.MonoidalCategory.associator h j f).inv = η₂)
(e_η₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator g i f).hom η₂ = η₃)
:
theorem
Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{f' : C}
{g : C}
{h : C}
{i : C}
{α : f' ≅ g}
{η : g ⟶ h}
{ηs : h ⟶ i}
{ηs₁ : CategoryTheory.MonoidalCategory.tensorObj h f ⟶ CategoryTheory.MonoidalCategory.tensorObj i f}
{η₁ : CategoryTheory.MonoidalCategory.tensorObj g f ⟶ CategoryTheory.MonoidalCategory.tensorObj h f}
{η₂ : CategoryTheory.MonoidalCategory.tensorObj g f ⟶ CategoryTheory.MonoidalCategory.tensorObj i f}
{η₃ : CategoryTheory.MonoidalCategory.tensorObj f' f ⟶ CategoryTheory.MonoidalCategory.tensorObj i f}
(e_ηs₁ : CategoryTheory.MonoidalCategory.whiskerRight ηs f = ηs₁)
(e_η₁ : CategoryTheory.MonoidalCategory.whiskerRight η f = η₁)
(e_η₂ : CategoryTheory.CategoryStruct.comp η₁ ηs₁ = η₂)
(e_η₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRightIso α f).hom η₂ = η₃)
:
theorem
Mathlib.Tactic.Monoidal.evalHorizontalCompAux_of
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
{h : C}
{i : C}
(η : f ⟶ g)
(θ : h ⟶ i)
:
CategoryTheory.MonoidalCategory.tensorHom η θ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategory.tensorObj f h)).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom η θ)
(CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategory.tensorObj g i)).hom)
theorem
Mathlib.Tactic.Monoidal.evalHorizontalCompAux_cons
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{f' : C}
{g : C}
{g' : C}
{h : C}
{i : C}
{η : f ⟶ g}
{ηs : f' ⟶ g'}
{θ : h ⟶ i}
{ηθ : CategoryTheory.MonoidalCategory.tensorObj f' h ⟶ CategoryTheory.MonoidalCategory.tensorObj g' i}
{η₁ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj f' h) ⟶ CategoryTheory.MonoidalCategory.tensorObj g (CategoryTheory.MonoidalCategory.tensorObj g' i)}
{ηθ₁ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj f' h) ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj g g') i}
{ηθ₂ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f f') h ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj g g') i}
(e_ηθ : CategoryTheory.MonoidalCategory.tensorHom ηs θ = ηθ)
(e_η₁ : CategoryTheory.MonoidalCategory.tensorHom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl f).hom
(CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl g).hom))
ηθ = η₁)
(e_ηθ₁ : CategoryTheory.CategoryStruct.comp η₁ (CategoryTheory.MonoidalCategory.associator g g' i).inv = ηθ₁)
(e_ηθ₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f f' h).hom ηθ₁ = ηθ₂)
:
theorem
Mathlib.Tactic.Monoidal.evalHorizontalCompAux'_whisker
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{f' : C}
{g : C}
{g' : C}
{h : C}
{η : g ⟶ h}
{θ : f' ⟶ g'}
{ηθ : CategoryTheory.MonoidalCategory.tensorObj g f' ⟶ CategoryTheory.MonoidalCategory.tensorObj h g'}
{η₁ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g f') ⟶ CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj h g')}
{η₂ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g f') ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f h) g'}
{η₃ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) f' ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f h) g'}
(e_ηθ : CategoryTheory.MonoidalCategory.tensorHom η θ = ηθ)
(e_η₁ : CategoryTheory.MonoidalCategory.whiskerLeft f ηθ = η₁)
(e_η₂ : CategoryTheory.CategoryStruct.comp η₁ (CategoryTheory.MonoidalCategory.associator f h g').inv = η₂)
(e_η₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f g f').hom η₂ = η₃)
:
theorem
Mathlib.Tactic.Monoidal.evalHorizontalCompAux'_of_whisker
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{f' : C}
{g : C}
{g' : C}
{h : C}
{η : g ⟶ h}
{θ : f' ⟶ g'}
{η₁ : CategoryTheory.MonoidalCategory.tensorObj g f ⟶ CategoryTheory.MonoidalCategory.tensorObj h f}
{ηθ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj g f) f' ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj h f) g'}
{ηθ₁ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj g f) f' ⟶ CategoryTheory.MonoidalCategory.tensorObj h (CategoryTheory.MonoidalCategory.tensorObj f g')}
{ηθ₂ : CategoryTheory.MonoidalCategory.tensorObj g (CategoryTheory.MonoidalCategory.tensorObj f f') ⟶ CategoryTheory.MonoidalCategory.tensorObj h (CategoryTheory.MonoidalCategory.tensorObj f g')}
(e_η₁ : CategoryTheory.MonoidalCategory.whiskerRight η f = η₁)
(e_ηθ : CategoryTheory.MonoidalCategory.tensorHom η₁
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl f').hom
(CategoryTheory.CategoryStruct.comp θ (CategoryTheory.Iso.refl g').hom)) = ηθ)
(e_ηθ₁ : CategoryTheory.CategoryStruct.comp ηθ (CategoryTheory.MonoidalCategory.associator h f g').hom = ηθ₁)
(e_ηθ₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator g f f').inv ηθ₁ = ηθ₂)
:
theorem
Mathlib.Tactic.Monoidal.evalHorizontalComp_nil_nil
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{g : C}
{h : C}
{i : C}
(α : f ≅ g)
(β : h ≅ i)
:
theorem
Mathlib.Tactic.Monoidal.evalHorizontalComp_nil_cons
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{f' : C}
{g : C}
{g' : C}
{h : C}
{i : C}
{α : f ≅ g}
{β : f' ≅ g'}
{η : g' ⟶ h}
{ηs : h ⟶ i}
{η₁ : CategoryTheory.MonoidalCategory.tensorObj g g' ⟶ CategoryTheory.MonoidalCategory.tensorObj g h}
{ηs₁ : CategoryTheory.MonoidalCategory.tensorObj g h ⟶ CategoryTheory.MonoidalCategory.tensorObj g i}
{η₂ : CategoryTheory.MonoidalCategory.tensorObj g g' ⟶ CategoryTheory.MonoidalCategory.tensorObj g i}
{η₃ : CategoryTheory.MonoidalCategory.tensorObj f f' ⟶ CategoryTheory.MonoidalCategory.tensorObj g i}
(e_η₁ : CategoryTheory.MonoidalCategory.whiskerLeft g
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl g').hom
(CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl h).hom)) = η₁)
(e_ηs₁ : CategoryTheory.MonoidalCategory.whiskerLeft g ηs = ηs₁)
(e_η₂ : CategoryTheory.CategoryStruct.comp η₁ ηs₁ = η₂)
(e_η₃ : CategoryTheory.CategoryStruct.comp (α ⊗ β).hom η₂ = η₃)
:
theorem
Mathlib.Tactic.Monoidal.evalHorizontalComp_cons_nil
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{f' : C}
{g : C}
{g' : C}
{h : C}
{i : C}
{α : f ≅ g}
{η : g ⟶ h}
{ηs : h ⟶ i}
{β : f' ≅ g'}
{η₁ : CategoryTheory.MonoidalCategory.tensorObj g g' ⟶ CategoryTheory.MonoidalCategory.tensorObj h g'}
{ηs₁ : CategoryTheory.MonoidalCategory.tensorObj h g' ⟶ CategoryTheory.MonoidalCategory.tensorObj i g'}
{η₂ : CategoryTheory.MonoidalCategory.tensorObj g g' ⟶ CategoryTheory.MonoidalCategory.tensorObj i g'}
{η₃ : CategoryTheory.MonoidalCategory.tensorObj f f' ⟶ CategoryTheory.MonoidalCategory.tensorObj i g'}
(e_η₁ : CategoryTheory.MonoidalCategory.whiskerRight
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl g).hom
(CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl h).hom))
g' = η₁)
(e_ηs₁ : CategoryTheory.MonoidalCategory.whiskerRight ηs g' = ηs₁)
(e_η₂ : CategoryTheory.CategoryStruct.comp η₁ ηs₁ = η₂)
(e_η₃ : CategoryTheory.CategoryStruct.comp (α ⊗ β).hom η₂ = η₃)
:
theorem
Mathlib.Tactic.Monoidal.evalHorizontalComp_cons_cons
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f : C}
{f' : C}
{g : C}
{g' : C}
{h : C}
{h' : C}
{i : C}
{i' : C}
{α : f ≅ g}
{η : g ⟶ h}
{ηs : h ⟶ i}
{β : f' ≅ g'}
{θ : g' ⟶ h'}
{θs : h' ⟶ i'}
{ηθ : CategoryTheory.MonoidalCategory.tensorObj g g' ⟶ CategoryTheory.MonoidalCategory.tensorObj h h'}
{ηθs : CategoryTheory.MonoidalCategory.tensorObj h h' ⟶ CategoryTheory.MonoidalCategory.tensorObj i i'}
{ηθ₁ : CategoryTheory.MonoidalCategory.tensorObj g g' ⟶ CategoryTheory.MonoidalCategory.tensorObj i i'}
{ηθ₂ : CategoryTheory.MonoidalCategory.tensorObj f f' ⟶ CategoryTheory.MonoidalCategory.tensorObj i i'}
(e_ηθ : CategoryTheory.MonoidalCategory.tensorHom η θ = ηθ)
(e_ηθs : CategoryTheory.MonoidalCategory.tensorHom ηs θs = ηθs)
(e_ηθ₁ : CategoryTheory.CategoryStruct.comp ηθ ηθs = ηθ₁)
(e_ηθ₂ : CategoryTheory.CategoryStruct.comp (α ⊗ β).hom ηθ₁ = ηθ₂)
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.