Normalization of morphisms in monoidal categories #

This file provides the implementation of the normalization given in Mathlib/Tactic/CategoryTheory/Coherence/Normalize.lean. See this file for more details.

source

theorem Mathlib.Tactic.Monoidal.evalComp_nil_nil {C : Type u} [CategoryTheory.Category.{v, u} C] {f g h : C} (α : f ≅ g) (β : g ≅ h) :

(α ≪≫ β).hom = (α ≪≫ β).hom

source

theorem Mathlib.Tactic.Monoidal.evalComp_nil_cons {C : Type u} [CategoryTheory.Category.{v, u} C] {f g h i 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)

source

theorem Mathlib.Tactic.Monoidal.evalComp_cons {C : Type u} [CategoryTheory.Category.{v, u} C] {f g h i j : C} (α : f ≅ g) (η : g ⟶ h) {ηs : h ⟶ i} {θ : i ⟶ j} {ι : h ⟶ j} (e_ι : CategoryTheory.CategoryStruct.comp ηs θ = ι) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) θ = CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ι)

source

theorem Mathlib.Tactic.Monoidal.eval_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {f g h : C} {η η' : f ⟶ g} {θ θ' : g ⟶ h} {ι : f ⟶ h} (e_η : η = η') (e_θ : θ = θ') (e_ηθ : CategoryTheory.CategoryStruct.comp η' θ' = ι) :

CategoryTheory.CategoryStruct.comp η θ = ι

source

theorem Mathlib.Tactic.Monoidal.eval_of {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : C} (η : f ⟶ g) :

η = CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl f).hom (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl g).hom)

source

theorem Mathlib.Tactic.Monoidal.eval_monoidalComp {C : Type u} [CategoryTheory.Category.{v, u} C] {f g h i : C} {η η' : f ⟶ g} {α : g ≅ h} {θ θ' : h ⟶ i} {αθ : g ⟶ i} {ηαθ : f ⟶ i} (e_η : η = η') (e_θ : θ = θ') (e_αθ : CategoryTheory.CategoryStruct.comp α.hom θ' = αθ) (e_ηαθ : CategoryTheory.CategoryStruct.comp η' αθ = ηαθ) :

CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp α.hom θ) = ηαθ

source

theorem Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (f : C) {g h : C} (α : g ≅ h) :

(CategoryTheory.MonoidalCategory.whiskerLeftIso f α).hom = (CategoryTheory.MonoidalCategory.whiskerLeftIso f α).hom

source

theorem Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f g h i j : C} (α : g ≅ h) (η : h ⟶ i) {ηs : i ⟶ j} {θ : CategoryTheory.MonoidalCategoryStruct.tensorObj f i ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj f j} (e_θ : CategoryTheory.MonoidalCategoryStruct.whiskerLeft f ηs = θ) :

CategoryTheory.MonoidalCategoryStruct.whiskerLeft f (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeftIso f α).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η) θ)

source

CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj f g) η = η₄

source

theorem Mathlib.Tactic.Monoidal.evalWhiskerLeft_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f g : C} {η : f ⟶ g} {η₁ : f ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) g} {η₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) g} (e_η₁ : CategoryTheory.CategoryStruct.comp η (CategoryTheory.MonoidalCategoryStruct.leftUnitor g).inv = η₁) (e_η₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor f).hom η₁ = η₂) :

CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) η = η₂

source

theorem Mathlib.Tactic.Monoidal.eval_whiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f g h : C} {η η' : g ⟶ h} {θ : CategoryTheory.MonoidalCategoryStruct.tensorObj f g ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj f h} (e_η : η = η') (e_θ : CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η' = θ) :

CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η = θ

source

theorem Mathlib.Tactic.Monoidal.eval_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f g h : C} {η η' : f ⟶ g} {θ : CategoryTheory.MonoidalCategoryStruct.tensorObj f h ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj g h} (e_η : η = η') (e_θ : CategoryTheory.MonoidalCategoryStruct.whiskerRight η' h = θ) :

CategoryTheory.MonoidalCategoryStruct.whiskerRight η h = θ

source

theorem Mathlib.Tactic.Monoidal.eval_tensorHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f g h i : C} {η η' : f ⟶ g} {θ θ' : h ⟶ i} {ι : CategoryTheory.MonoidalCategoryStruct.tensorObj f h ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj g i} (e_η : η = η') (e_θ : θ = θ') (e_ι : CategoryTheory.MonoidalCategoryStruct.tensorHom η' θ' = ι) :

CategoryTheory.MonoidalCategoryStruct.tensorHom η θ = ι

source

theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_nil {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f g : C} (α : f ≅ g) (h : C) :

(CategoryTheory.MonoidalCategory.whiskerRightIso α h).hom = (CategoryTheory.MonoidalCategory.whiskerRightIso α h).hom

source

CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) j = η₃

source

CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η) ηs)) k = η₅

source

CategoryTheory.MonoidalCategoryStruct.whiskerRight η (CategoryTheory.MonoidalCategoryStruct.tensorObj g h) = η₄

source

CategoryTheory.MonoidalCategoryStruct.whiskerRight η (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = η₂

source

theorem Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f g : C} (η : f ⟶ g) (h : C) :

CategoryTheory.MonoidalCategoryStruct.whiskerRight η h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj f h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight η h) (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj g h)).hom)

source

CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom η ηs) f = η₃

source

CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) f = η₃

source

theorem Mathlib.Tactic.Monoidal.evalHorizontalCompAux_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f g h i : C} (η : f ⟶ g) (θ : h ⟶ i) :

CategoryTheory.MonoidalCategoryStruct.tensorHom η θ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj f h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom η θ) (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj g i)).hom)

source

CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom η ηs) θ = ηθ₂

source

CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η) θ = η₃

source

CategoryTheory.MonoidalCategoryStruct.tensorHom η (CategoryTheory.MonoidalCategoryStruct.whiskerLeft f θ) = ηθ₂

source

theorem Mathlib.Tactic.Monoidal.evalHorizontalComp_nil_nil {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f g h i : C} (α : f ≅ g) (β : h ≅ i) :

(CategoryTheory.MonoidalCategory.tensorIso α β).hom = (CategoryTheory.MonoidalCategory.tensorIso α β).hom

source

CategoryTheory.MonoidalCategoryStruct.tensorHom α.hom (CategoryTheory.CategoryStruct.comp β.hom (CategoryTheory.CategoryStruct.comp η ηs)) = η₃

source

CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) β.hom = η₃

source

CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) (CategoryTheory.CategoryStruct.comp β.hom (CategoryTheory.CategoryStruct.comp θ θs)) = ηθ₂

source

@[instance_reducible]

instance Mathlib.Tactic.Monoidal.instMkEvalCompMonoidalM :

BicategoryLike.MkEvalComp MonoidalM

Equations

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

source

@[instance_reducible]

instance Mathlib.Tactic.Monoidal.instMkEvalWhiskerLeftMonoidalM :

BicategoryLike.MkEvalWhiskerLeft MonoidalM

Equations

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

source

@[instance_reducible]

instance Mathlib.Tactic.Monoidal.instMkEvalWhiskerRightMonoidalM :

BicategoryLike.MkEvalWhiskerRight MonoidalM

Equations

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

source

@[instance_reducible]

instance Mathlib.Tactic.Monoidal.instMkEvalHorizontalCompMonoidalM :

BicategoryLike.MkEvalHorizontalComp MonoidalM

Equations

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

source

@[instance_reducible]

instance Mathlib.Tactic.Monoidal.instMkEvalMonoidalM :

BicategoryLike.MkEval MonoidalM

Equations

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

source

@[instance_reducible]

instance Mathlib.Tactic.Monoidal.instMonadNormalExprMonoidalM :

BicategoryLike.MonadNormalExpr MonoidalM

Equations

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

source

@[instance_reducible]

instance Mathlib.Tactic.Monoidal.instMkMor₂MonoidalM_1 :

BicategoryLike.MkMor₂ MonoidalM

Equations

Mathlib.Tactic.Monoidal.instMkMor₂MonoidalM_1 = { ofExpr := Mathlib.Tactic.Monoidal.Mor₂OfExpr }

Documentation

Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Normalization of morphisms in monoidal categories #