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.MonoidalCategory.tensorObj p f ≅ pf)
(η_g : CategoryTheory.MonoidalCategory.tensorObj pf g ≅ pfg)
:
The composition of the normalizing isomorphisms η_f : p ⊗ f ≅ pf and η_g : pf ⊗ g ≅ pfg.
Equations
- Mathlib.Tactic.Monoidal.normalizeIsoComp η_f η_g = (CategoryTheory.MonoidalCategory.associator p f g).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso η_f g ≪≫ η_g
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.MonoidalCategory.tensorObj p f ≅ pf)
(η_g : CategoryTheory.MonoidalCategory.tensorObj pf g ≅ pfg)
(η_h : CategoryTheory.MonoidalCategory.tensorObj pfg h ≅ pfgh)
:
theorem
Mathlib.Tactic.Monoidal.naturality_leftUnitor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{p f pf : C}
(η_f : CategoryTheory.MonoidalCategory.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.MonoidalCategory.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.MonoidalCategory.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.MonoidalCategory.tensorObj p f ≅ pf)
(η_g : CategoryTheory.MonoidalCategory.tensorObj p g ≅ pf)
(η_h : CategoryTheory.MonoidalCategory.tensorObj p h ≅ pf)
(ih_η : CategoryTheory.MonoidalCategory.whiskerLeftIso p η ≪≫ η_g = η_f)
(ih_θ : CategoryTheory.MonoidalCategory.whiskerLeftIso p θ ≪≫ η_h = η_g)
:
CategoryTheory.MonoidalCategory.whiskerLeftIso p (η ≪≫ θ) ≪≫ η_h = η_f
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.MonoidalCategory.tensorObj p f ≅ pf)
(η_fg : CategoryTheory.MonoidalCategory.tensorObj pf g ≅ pfg)
(η_fh : CategoryTheory.MonoidalCategory.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.MonoidalCategory.tensorObj p f ≅ pf)
(η_g : CategoryTheory.MonoidalCategory.tensorObj p g ≅ pf)
(η_fh : CategoryTheory.MonoidalCategory.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.MonoidalCategory.tensorObj p f₁ ≅ pf₁)
(η_g₁ : CategoryTheory.MonoidalCategory.tensorObj p g₁ ≅ pf₁)
(η_f₂ : CategoryTheory.MonoidalCategory.tensorObj pf₁ f₂ ≅ pf₁f₂)
(η_g₂ : CategoryTheory.MonoidalCategory.tensorObj pf₁ g₂ ≅ pf₁f₂)
(ih_η : CategoryTheory.MonoidalCategory.whiskerLeftIso p η ≪≫ η_g₁ = η_f₁)
(ih_θ : CategoryTheory.MonoidalCategory.whiskerLeftIso pf₁ θ ≪≫ η_g₂ = η_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.MonoidalCategory.tensorObj p f ≅ pf)
(η_g : CategoryTheory.MonoidalCategory.tensorObj p g ≅ pf)
(ih : CategoryTheory.MonoidalCategory.whiskerLeftIso p η ≪≫ η_g = η_f)
:
CategoryTheory.MonoidalCategory.whiskerLeftIso p η.symm ≪≫ η_f = η_g
Equations
- One or more equations did not get rendered due to their size.
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.MonoidalCategory.tensorObj (𝟙_ C) f ≅ f')
(η_g : CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) g ≅ f')
(h_η : CategoryTheory.MonoidalCategory.whiskerLeftIso (𝟙_ C) η ≪≫ η_g = η_f)
(h_θ : CategoryTheory.MonoidalCategory.whiskerLeftIso (𝟙_ 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.MonoidalCategory.tensorObj (𝟙_ C) f ≅ f')
(η_g : CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) g ≅ f')
(η_hom : η'.hom = η)
(Θ_hom : θ'.hom = θ)
(Hη : CategoryTheory.MonoidalCategory.whiskerLeftIso (𝟙_ C) η' ≪≫ η_g = η_f)
(Hθ : CategoryTheory.MonoidalCategory.whiskerLeftIso (𝟙_ C) θ' ≪≫ η_g = η_f)
:
η = θ
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- Mathlib.Tactic.Monoidal.tacticMonoidal_coherence = Lean.ParserDescr.node `Mathlib.Tactic.Monoidal.tacticMonoidal_coherence 1024 (Lean.ParserDescr.nonReservedSymbol "monoidal_coherence" false)