Coherence tactic for monoidal categories #
We provide a monoidal_coherence tactic,
which proves that any two morphisms (with the same source and target)
in a monoidal category which are built out of associators and unitors
are equal.
@[reducible, inline]
abbrev
Mathlib.Tactic.Monoidal.normalizeIsoComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{p f g pf pfg : C}
(η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
(η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj pf g ≅ pfg)
:
The composition of the normalizing isomorphisms η_f : p ⊗ f ≅ pf and η_g : pf ⊗ g ≅ pfg.
Equations
Instances For
theorem
Mathlib.Tactic.Monoidal.naturality_associator
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{p f g h pf pfg pfgh : C}
(η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
(η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj pf g ≅ pfg)
(η_h : CategoryTheory.MonoidalCategoryStruct.tensorObj pfg h ≅ pfgh)
:
CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.MonoidalCategoryStruct.associator f g h) ≪≫ normalizeIsoComp η_f (normalizeIsoComp η_g η_h) = normalizeIsoComp (normalizeIsoComp η_f η_g) η_h
theorem
Mathlib.Tactic.Monoidal.naturality_leftUnitor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{p f pf : C}
(η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
:
theorem
Mathlib.Tactic.Monoidal.naturality_rightUnitor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{p f pf : C}
(η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
:
theorem
Mathlib.Tactic.Monoidal.naturality_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{p f pf : C}
(η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
:
theorem
Mathlib.Tactic.Monoidal.naturality_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{p f g h pf : C}
{η : f ≅ g}
{θ : g ≅ h}
(η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
(η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj p g ≅ pf)
(η_h : CategoryTheory.MonoidalCategoryStruct.tensorObj p h ≅ pf)
(ih_η : CategoryTheory.MonoidalCategory.whiskerLeftIso p η ≪≫ η_g = η_f)
(ih_θ : CategoryTheory.MonoidalCategory.whiskerLeftIso p θ ≪≫ η_h = η_g)
:
theorem
Mathlib.Tactic.Monoidal.naturality_whiskerLeft
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{p f g h pf pfg : C}
{η : g ≅ h}
(η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
(η_fg : CategoryTheory.MonoidalCategoryStruct.tensorObj pf g ≅ pfg)
(η_fh : CategoryTheory.MonoidalCategoryStruct.tensorObj pf h ≅ pfg)
(ih_η : CategoryTheory.MonoidalCategory.whiskerLeftIso pf η ≪≫ η_fh = η_fg)
:
theorem
Mathlib.Tactic.Monoidal.naturality_whiskerRight
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{p f g h pf pfh : C}
{η : f ≅ g}
(η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
(η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj p g ≅ pf)
(η_fh : CategoryTheory.MonoidalCategoryStruct.tensorObj pf h ≅ pfh)
(ih_η : CategoryTheory.MonoidalCategory.whiskerLeftIso p η ≪≫ η_g = η_f)
:
theorem
Mathlib.Tactic.Monoidal.naturality_tensorHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C}
{η : f₁ ≅ g₁}
{θ : f₂ ≅ g₂}
(η_f₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj p f₁ ≅ pf₁)
(η_g₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj p g₁ ≅ pf₁)
(η_f₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj pf₁ f₂ ≅ pf₁f₂)
(η_g₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj pf₁ g₂ ≅ pf₁f₂)
(ih_η : CategoryTheory.MonoidalCategory.whiskerLeftIso p η ≪≫ η_g₁ = η_f₁)
(ih_θ : CategoryTheory.MonoidalCategory.whiskerLeftIso pf₁ θ ≪≫ η_g₂ = η_f₂)
:
CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.MonoidalCategory.tensorIso η θ) ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_f₁ η_f₂
theorem
Mathlib.Tactic.Monoidal.naturality_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{p f g pf : C}
{η : f ≅ g}
(η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
(η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj p g ≅ pf)
(ih : CategoryTheory.MonoidalCategory.whiskerLeftIso p η ≪≫ η_g = η_f)
:
theorem
Mathlib.Tactic.Monoidal.of_normalize_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f g f' : C}
{η θ : f ≅ g}
(η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f ≅ f')
(η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) g ≅ f')
(h_η :
CategoryTheory.MonoidalCategory.whiskerLeftIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) η ≪≫ η_g = η_f)
(h_θ :
CategoryTheory.MonoidalCategory.whiskerLeftIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) θ ≪≫ η_g = η_f)
:
theorem
Mathlib.Tactic.Monoidal.mk_eq_of_naturality
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{f g f' : C}
{η θ : f ⟶ g}
{η' θ' : f ≅ g}
(η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f ≅ f')
(η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) g ≅ f')
(η_hom : η'.hom = η)
(Θ_hom : θ'.hom = θ)
(Hη :
CategoryTheory.MonoidalCategory.whiskerLeftIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) η' ≪≫ η_g = η_f)
(Hθ :
CategoryTheory.MonoidalCategory.whiskerLeftIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) θ' ≪≫ η_g = η_f)
:
Close the goal of the form η = θ, where η and θ are 2-isomorphisms made up only of
associators, unitors, and identities.
example {C : Type} [Category C] [MonoidalCategory C] :
(λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom := by
monoidal_coherence
Equations
Instances For
Close the goal of the form η = θ, where η and θ are 2-isomorphisms made up only of
associators, unitors, and identities.
example {C : Type} [Category C] [MonoidalCategory C] :
(λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom := by
monoidal_coherence