A coherence tactic for monoidal categories, and ⊗≫ (composition up to associators)

We provide a coherence tactic, which proves equations where the two sides differ by replacing strings of monoidal structural morphisms with other such strings. (The replacements are always equalities by the monoidal coherence theorem.)

A simpler version of this tactic is pure_coherence, 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.

We also provide f ⊗≫ g, the monoidal_comp operation, which automatically inserts associators and unitors as needed to make the target of f match the source of g.

class Mathlib.Tactic.Coherence.LiftObj {C : Type u} (X : C) : Type u

• lift : CategoryTheory.FreeMonoidalCategory C

A typeclass carrying a choice of lift of an object from C to FreeMonoidalCategory C. It must be the case that projectObj id (LiftObj.lift x) = x by defeq.

instance Mathlib.Tactic.Coherence.LiftObj_unit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : Mathlib.Tactic.Coherence.LiftObj (CategoryTheory.MonoidalCategory.tensorUnit C)

Equations

• Mathlib.Tactic.Coherence.LiftObj_unit = { lift := CategoryTheory.FreeMonoidalCategory.Unit }

instance Mathlib.Tactic.Coherence.LiftObj_tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] : Mathlib.Tactic.Coherence.LiftObj (CategoryTheory.MonoidalCategory.tensorObj X Y)

Equations

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

instance Mathlib.Tactic.Coherence.LiftObj_of {C : Type u} (X : C) : Mathlib.Tactic.Coherence.LiftObj X

Equations

• Mathlib.Tactic.Coherence.LiftObj_of X = { lift := CategoryTheory.FreeMonoidalCategory.of X }

class Mathlib.Tactic.Coherence.LiftHom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] (f : X ⟶ Y) : Type u

• lift : Mathlib.Tactic.Coherence.LiftObj.lift X ⟶ Mathlib.Tactic.Coherence.LiftObj.lift Y

A typeclass carrying a choice of lift of a morphism from C to FreeMonoidalCategory C. It must be the case that projectMap id _ _ (LiftHom.lift f) = f by defeq.

instance Mathlib.Tactic.Coherence.LiftHom_id {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [Mathlib.Tactic.Coherence.LiftObj X] : Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.CategoryStruct.id X)

Equations

• Mathlib.Tactic.Coherence.LiftHom_id X = { lift := CategoryTheory.CategoryStruct.id (Mathlib.Tactic.Coherence.LiftObj.lift X) }

instance Mathlib.Tactic.Coherence.LiftHom_left_unitor_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mathlib.Tactic.Coherence.LiftObj X] : Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategory.leftUnitor X).hom

Equations

• Mathlib.Tactic.Coherence.LiftHom_left_unitor_hom X = { lift := (CategoryTheory.MonoidalCategory.leftUnitor (Mathlib.Tactic.Coherence.LiftObj.lift X)).hom }

instance Mathlib.Tactic.Coherence.LiftHom_left_unitor_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mathlib.Tactic.Coherence.LiftObj X] : Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategory.leftUnitor X).inv

Equations

• Mathlib.Tactic.Coherence.LiftHom_left_unitor_inv X = { lift := (CategoryTheory.MonoidalCategory.leftUnitor (Mathlib.Tactic.Coherence.LiftObj.lift X)).inv }

instance Mathlib.Tactic.Coherence.LiftHom_right_unitor_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mathlib.Tactic.Coherence.LiftObj X] : Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategory.rightUnitor X).hom

Equations

• Mathlib.Tactic.Coherence.LiftHom_right_unitor_hom X = { lift := (CategoryTheory.MonoidalCategory.rightUnitor (Mathlib.Tactic.Coherence.LiftObj.lift X)).hom }

instance Mathlib.Tactic.Coherence.LiftHom_right_unitor_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mathlib.Tactic.Coherence.LiftObj X] : Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategory.rightUnitor X).inv

Equations

• Mathlib.Tactic.Coherence.LiftHom_right_unitor_inv X = { lift := (CategoryTheory.MonoidalCategory.rightUnitor (Mathlib.Tactic.Coherence.LiftObj.lift X)).inv }

instance Mathlib.Tactic.Coherence.LiftHom_associator_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.LiftObj Z] : Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategory.associator X Y Z).hom

Equations

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

instance Mathlib.Tactic.Coherence.LiftHom_associator_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.LiftObj Z] : Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategory.associator X Y Z).inv

Equations

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

instance Mathlib.Tactic.Coherence.LiftHom_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.LiftObj Z] (f : X ⟶ Y) (g : Y ⟶ Z) [Mathlib.Tactic.Coherence.LiftHom f] [Mathlib.Tactic.Coherence.LiftHom g] : Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.CategoryStruct.comp f g)

Equations

• Mathlib.Tactic.Coherence.LiftHom_comp f g = { lift := CategoryTheory.CategoryStruct.comp (Mathlib.Tactic.Coherence.LiftHom.lift f) (Mathlib.Tactic.Coherence.LiftHom.lift g) }

instance Mathlib.Tactic.Coherence.LiftHom_tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {W : C} {X : C} {Y : C} {Z : C} [Mathlib.Tactic.Coherence.LiftObj W] [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.LiftObj Z] (f : W ⟶ X) (g : Y ⟶ Z) [Mathlib.Tactic.Coherence.LiftHom f] [Mathlib.Tactic.Coherence.LiftHom g] : Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategory.tensorHom f g)

Equations

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

class Mathlib.Tactic.Coherence.MonoidalCoherence {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] : Type v

• hom : X ⟶ Y
• isIso : CategoryTheory.IsIso Mathlib.Tactic.Coherence.MonoidalCoherence.hom

A typeclass carrying a choice of monoidal structural isomorphism between two objects. Used by the ⊗≫ monoidal composition operator, and the coherence tactic.

@[simp]

theorem Mathlib.Tactic.Coherence.MonoidalCoherence.refl_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [Mathlib.Tactic.Coherence.LiftObj X] : Mathlib.Tactic.Coherence.MonoidalCoherence.hom = CategoryTheory.CategoryStruct.id X

instance Mathlib.Tactic.Coherence.MonoidalCoherence.refl {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [Mathlib.Tactic.Coherence.LiftObj X] : Mathlib.Tactic.Coherence.MonoidalCoherence X X

Equations

• Mathlib.Tactic.Coherence.MonoidalCoherence.refl X = Mathlib.Tactic.Coherence.MonoidalCoherence.mk (CategoryTheory.CategoryStruct.id X)

@[simp]

theorem Mathlib.Tactic.Coherence.MonoidalCoherence.tensor_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.LiftObj Z] [Mathlib.Tactic.Coherence.MonoidalCoherence Y Z] : Mathlib.Tactic.Coherence.MonoidalCoherence.hom = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) Mathlib.Tactic.Coherence.MonoidalCoherence.hom

instance Mathlib.Tactic.Coherence.MonoidalCoherence.tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.LiftObj Z] [Mathlib.Tactic.Coherence.MonoidalCoherence Y Z] : Mathlib.Tactic.Coherence.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj X Y) (CategoryTheory.MonoidalCategory.tensorObj X Z)

Equations

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

@[simp]

theorem Mathlib.Tactic.Coherence.MonoidalCoherence.tensor_right_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorUnit C) Y] : Mathlib.Tactic.Coherence.MonoidalCoherence.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) Mathlib.Tactic.Coherence.MonoidalCoherence.hom)

instance Mathlib.Tactic.Coherence.MonoidalCoherence.tensor_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorUnit C) Y] : Mathlib.Tactic.Coherence.MonoidalCoherence X (CategoryTheory.MonoidalCategory.tensorObj X Y)

Equations

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

@[simp]

theorem Mathlib.Tactic.Coherence.MonoidalCoherence.tensor_right'_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence Y (CategoryTheory.MonoidalCategory.tensorUnit C)] : Mathlib.Tactic.Coherence.MonoidalCoherence.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) Mathlib.Tactic.Coherence.MonoidalCoherence.hom) (CategoryTheory.MonoidalCategory.rightUnitor X).hom

instance Mathlib.Tactic.Coherence.MonoidalCoherence.tensor_right' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence Y (CategoryTheory.MonoidalCategory.tensorUnit C)] : Mathlib.Tactic.Coherence.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj X Y) X

Equations

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

@[simp]

theorem Mathlib.Tactic.Coherence.MonoidalCoherence.left_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence X Y] : Mathlib.Tactic.Coherence.MonoidalCoherence.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom Mathlib.Tactic.Coherence.MonoidalCoherence.hom

instance Mathlib.Tactic.Coherence.MonoidalCoherence.left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence X Y] : Mathlib.Tactic.Coherence.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorUnit C) X) Y

Equations

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

@[simp]

theorem Mathlib.Tactic.Coherence.MonoidalCoherence.left'_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence X Y] : Mathlib.Tactic.Coherence.MonoidalCoherence.hom = CategoryTheory.CategoryStruct.comp Mathlib.Tactic.Coherence.MonoidalCoherence.hom (CategoryTheory.MonoidalCategory.leftUnitor Y).inv

instance Mathlib.Tactic.Coherence.MonoidalCoherence.left' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence X Y] : Mathlib.Tactic.Coherence.MonoidalCoherence X (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorUnit C) Y)

Equations

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

@[simp]

theorem Mathlib.Tactic.Coherence.MonoidalCoherence.right_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence X Y] : Mathlib.Tactic.Coherence.MonoidalCoherence.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom Mathlib.Tactic.Coherence.MonoidalCoherence.hom

instance Mathlib.Tactic.Coherence.MonoidalCoherence.right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence X Y] : Mathlib.Tactic.Coherence.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorUnit C)) Y

Equations

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

@[simp]

theorem Mathlib.Tactic.Coherence.MonoidalCoherence.right'_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence X Y] : Mathlib.Tactic.Coherence.MonoidalCoherence.hom = CategoryTheory.CategoryStruct.comp Mathlib.Tactic.Coherence.MonoidalCoherence.hom (CategoryTheory.MonoidalCategory.rightUnitor Y).inv

instance Mathlib.Tactic.Coherence.MonoidalCoherence.right' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence X Y] : Mathlib.Tactic.Coherence.MonoidalCoherence X (CategoryTheory.MonoidalCategory.tensorObj Y (CategoryTheory.MonoidalCategory.tensorUnit C))

Equations

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

@[simp]

theorem Mathlib.Tactic.Coherence.MonoidalCoherence.assoc_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) (W : C) [Mathlib.Tactic.Coherence.LiftObj W] [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.LiftObj Z] [Mathlib.Tactic.Coherence.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) W] : Mathlib.Tactic.Coherence.MonoidalCoherence.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom Mathlib.Tactic.Coherence.MonoidalCoherence.hom

instance Mathlib.Tactic.Coherence.MonoidalCoherence.assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) (W : C) [Mathlib.Tactic.Coherence.LiftObj W] [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.LiftObj Z] [Mathlib.Tactic.Coherence.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) W] : Mathlib.Tactic.Coherence.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) W

Equations

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

@[simp]

theorem Mathlib.Tactic.Coherence.MonoidalCoherence.assoc'_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (W : C) (X : C) (Y : C) (Z : C) [Mathlib.Tactic.Coherence.LiftObj W] [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.LiftObj Z] [Mathlib.Tactic.Coherence.MonoidalCoherence W (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z))] : Mathlib.Tactic.Coherence.MonoidalCoherence.hom = CategoryTheory.CategoryStruct.comp Mathlib.Tactic.Coherence.MonoidalCoherence.hom (CategoryTheory.MonoidalCategory.associator X Y Z).inv

instance Mathlib.Tactic.Coherence.MonoidalCoherence.assoc' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (W : C) (X : C) (Y : C) (Z : C) [Mathlib.Tactic.Coherence.LiftObj W] [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.LiftObj Z] [Mathlib.Tactic.Coherence.MonoidalCoherence W (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z))] : Mathlib.Tactic.Coherence.MonoidalCoherence W (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z)

Equations

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

def Mathlib.Tactic.Coherence.monoidalIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : C) [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence X Y] : X ≅ Y

Construct an isomorphism between two objects in a monoidal category out of unitors and associators.

Equations

• Mathlib.Tactic.Coherence.monoidalIso X Y = CategoryTheory.asIso Mathlib.Tactic.Coherence.MonoidalCoherence.hom

def Mathlib.Tactic.Coherence.monoidalComp {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence X Y] (f : W ⟶ X) (g : Y ⟶ Z) : W ⟶ Z

Compose two morphisms in a monoidal category, inserting unitors and associators between as necessary.

Equations

• Mathlib.Tactic.Coherence.monoidalComp f g = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp Mathlib.Tactic.Coherence.MonoidalCoherence.hom g)

def CategoryTheory.MonoidalCategory.«term_⊗≫_» : Lean.TrailingParserDescr

Compose two morphisms in a monoidal category, inserting unitors and associators between as necessary.

Equations

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

noncomputable def Mathlib.Tactic.Coherence.monoidalIsoComp {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] [Mathlib.Tactic.Coherence.MonoidalCoherence X Y] (f : W ≅ X) (g : Y ≅ Z) : W ≅ Z

Compose two isomorphisms in a monoidal category, inserting unitors and associators between as necessary.

Equations

• Mathlib.Tactic.Coherence.monoidalIsoComp f g = f ≪≫ CategoryTheory.asIso Mathlib.Tactic.Coherence.MonoidalCoherence.hom ≪≫ g

def CategoryTheory.MonoidalCategory.«term_≪⊗≫_» : Lean.TrailingParserDescr

Compose two isomorphisms in a monoidal category, inserting unitors and associators between as necessary.

Equations

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

@[simp]

theorem Mathlib.Tactic.Coherence.monoidalComp_refl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : Mathlib.Tactic.Coherence.monoidalComp f g = CategoryTheory.CategoryStruct.comp f g

def Mathlib.Tactic.Coherence.exception {α : Type} (g : Lean.MVarId) (msg : Lean.MessageData) : Lean.MetaM α

Helper function for throwing exceptions.

Equations

• Mathlib.Tactic.Coherence.exception g msg = Lean.Meta.throwTacticEx `monoidal_coherence g msg

def Mathlib.Tactic.Coherence.exception' (msg : Lean.MessageData) : Lean.Elab.Tactic.TacticM Unit

Helper function for throwing exceptions with respect to the main goal.

Equations

• Mathlib.Tactic.Coherence.exception' msg = tryCatch (Lean.Elab.Tactic.liftMetaTactic fun g => Mathlib.Tactic.Coherence.exception g msg) fun x => Lean.throwError msg

def Mathlib.Tactic.Coherence.mkProjectMapExpr (e : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Auxiliary definition for monoidal_coherence.

Equations

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

def Mathlib.Tactic.Coherence.monoidal_coherence (g : Lean.MVarId) : Lean.Elab.TermElabM Unit

Coherence tactic for monoidal categories.

Equations

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

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

Coherence tactic for monoidal categories. Use pure_coherence instead, which is a frontend to this one.

Equations

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

def Mathlib.Tactic.Coherence.pure_coherence : Lean.ParserDescr

pure_coherence uses the coherence theorem for monoidal categories to prove the goal. It can prove any equality made up only of associators, unitors, and identities.

example {C : Type} [Category C] [MonoidalCategory C] :
  (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom :=
by pure_coherence

Users will typically just use the coherence tactic, which can also cope with identities of the form a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c' where a = a', b = b', and c = c' can be proved using pure_coherence

Equations

• Mathlib.Tactic.Coherence.pure_coherence = Lean.ParserDescr.node `Mathlib.Tactic.Coherence.pure_coherence 1024 (Lean.ParserDescr.nonReservedSymbol "pure_coherence" false)

theorem Mathlib.Tactic.Coherence.assoc_liftHom {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} [Mathlib.Tactic.Coherence.LiftObj W] [Mathlib.Tactic.Coherence.LiftObj X] [Mathlib.Tactic.Coherence.LiftObj Y] (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) [Mathlib.Tactic.Coherence.LiftHom f] [Mathlib.Tactic.Coherence.LiftHom g] : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h

Auxiliary simp lemma for the coherence tactic: this moves brackets to the left in order to expose a maximal prefix built out of unitors and associators.

def Mathlib.Tactic.Coherence.liftable_prefixes : Lean.ParserDescr

Internal tactic used in coherence.

Rewrites an equation f = g as f₀ ≫ f₁ = g₀ ≫ g₁, where f₀ and g₀ are maximal prefixes of f and g (possibly after reassociating) which are "liftable" (i.e. expressible as compositions of unitors and associators).

Equations

• Mathlib.Tactic.Coherence.liftable_prefixes = Lean.ParserDescr.node `Mathlib.Tactic.Coherence.liftable_prefixes 1024 (Lean.ParserDescr.nonReservedSymbol "liftable_prefixes" false)

theorem Mathlib.Tactic.Coherence.insert_id_lhs {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) (w : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = g) : f = g

theorem Mathlib.Tactic.Coherence.insert_id_rhs {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) (w : f = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id Y)) : f = g

def Mathlib.Tactic.Coherence.insertTrailingIds (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

If either the lhs or rhs is not a composition, compose it on the right with an identity.

Equations

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

def Mathlib.Tactic.Coherence.coherence_loop (maxSteps : optParam ℕ 37) : Lean.Elab.Tactic.TacticM Unit

The main part of coherence tactic.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Coherence.coherence_loop 0 = Mathlib.Tactic.Coherence.exception' ((Lean.MessageData.ofFormat ∘ Std.format) "`coherence` tactic reached iteration limit")

def Mathlib.Tactic.Coherence.coherence : Lean.ParserDescr

Use the coherence theorem for monoidal categories to solve equations in a monoidal equation, where the two sides only differ by replacing strings of monoidal structural morphisms (that is, associators, unitors, and identities) with different strings of structural morphisms with the same source and target.

That is, coherence can handle goals of the form a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c' where a = a', b = b', and c = c' can be proved using pure_coherence.

(If you have very large equations on which coherence is unexpectedly failing, you may need to increase the typeclass search depth, using e.g. set_option synthInstance.maxSize 500.)

Equations

• Mathlib.Tactic.Coherence.coherence = Lean.ParserDescr.node `Mathlib.Tactic.Coherence.coherence 1024 (Lean.ParserDescr.nonReservedSymbol "coherence" false)