Documentation

Mathlib.Tactic.CategoryTheory.Coherence

A coherence tactic for monoidal categories #

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.

class Mathlib.Tactic.Coherence.LiftObj {C : Type u} (X : 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.

Instances
    Equations
    • Mathlib.Tactic.Coherence.LiftObj_unit = { lift := CategoryTheory.FreeMonoidalCategory.unit }

    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.

    Instances

      Helper function for throwing exceptions.

      Equations
      Instances For

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

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

          Auxiliary definition for monoidal_coherence.

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

            Coherence tactic for monoidal categories.

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

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

              Equations
              Instances For

                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
                Instances For

                  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.

                  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
                  Instances For

                    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.
                    Instances For

                      The main part of coherence tactic.

                      Equations
                      Instances For

                        Simp lemmas for rewriting a hom in monoical categories into a normal form.

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

                          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
                          Instances For