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) : CategoryTheory.MonoidalCategoryStruct.tensorObj p (CategoryTheory.MonoidalCategoryStruct.tensorObj f 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.MonoidalCategoryStruct.associator p f g).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso η_f g ≪≫ η_g

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) : CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.MonoidalCategoryStruct.leftUnitor f) ≪≫ η_f = normalizeIsoComp (CategoryTheory.MonoidalCategoryStruct.rightUnitor p) η_f

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) : CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.MonoidalCategoryStruct.rightUnitor f) ≪≫ η_f = normalizeIsoComp η_f (CategoryTheory.MonoidalCategoryStruct.rightUnitor 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) : CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.Iso.refl f) ≪≫ η_f = η_f

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) : 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.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) : CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.MonoidalCategory.whiskerLeftIso f η) ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f η_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) : CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.MonoidalCategory.whiskerRightIso η h) ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp η_f η_fh

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) : CategoryTheory.MonoidalCategory.whiskerLeftIso p η.symm ≪≫ η_f = η_g

instance Mathlib.Tactic.Monoidal.instMonadNormalizeNaturalityMonoidalM : BicategoryLike.MonadNormalizeNaturality MonoidalM

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.MonoidalCategoryStruct.tensorObj (𝟙_ C) f ≅ f') (η_g : CategoryTheory.MonoidalCategoryStruct.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.MonoidalCategoryStruct.tensorObj (𝟙_ C) f ≅ f') (η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj (𝟙_ C) g ≅ f') (η_hom : η'.hom = η) (Θ_hom : θ'.hom = θ) (Hη : CategoryTheory.MonoidalCategory.whiskerLeftIso (𝟙_ C) η' ≪≫ η_g = η_f) (Hθ : CategoryTheory.MonoidalCategory.whiskerLeftIso (𝟙_ C) θ' ≪≫ η_g = η_f) : η = θ

instance Mathlib.Tactic.Monoidal.instMkEqOfNaturalityMonoidalM : BicategoryLike.MkEqOfNaturality MonoidalM

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Monoidal.pureCoherence (mvarId : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

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.pureCoherence mvarId = Mathlib.Tactic.BicategoryLike.pureCoherence Mathlib.Tactic.Monoidal.Context `monoidal mvarId

def Mathlib.Tactic.Monoidal.tacticMonoidal_coherence : Lean.ParserDescr

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)