Normalization of morphisms in monoidal categories

This file provides a tactic that normalizes morphisms in monoidal categories. This is used in the string diagram widget given in Mathlib.Tactic.StringDiagram. We say that the morphism η in a monoidal category is in normal form if

1. η is of the form α₀ ≫ η₀ ≫ α₁ ≫ η₁ ≫ ... αₘ ≫ ηₘ ≫ αₘ₊₁ where each αᵢ is a structural 2-morphism (consisting of associators and unitors),
2. each ηᵢ is a non-structural 2-morphism of the form f₁ ◁ ... ◁ fₘ ◁ θ, and
3. θ is of the form ι ▷ g₁ ▷ ... ▷ gₗ

Note that the structural morphisms αᵢ are not necessarily normalized, as the main purpose is to get a list of the non-structural morphisms out.

Currently, the primary application of the normalization tactic in mind is drawing string diagrams, which are graphical representations of morphisms in monoidal categories, in the infoview. When drawing string diagrams, we often ignore associators and unitors (i.e., drawing morphisms in strict monoidal categories). On the other hand, in Lean, it is considered difficult to formalize the concept of strict monoidal categories due to the feature of dependent type theory. The normalization tactic can remove associators and unitors from the expression, extracting the necessary data for drawing string diagrams.

The current plan on drawing string diagrams (#10581) is to use Penrose (https://github.com/penrose) via ProofWidget. However, it should be noted that the normalization procedure in this file does not rely on specific settings, allowing for broader application.

Future plans include the following. At least I (Yuma) would like to work on these in the future, but it might not be immediate. If anyone is interested, I would be happy to discuss.

• Currently (#10581), the string diagrams only do drawing. It would be better they also generate proofs. That is, by manipulating the string diagrams displayed in the infoview with a mouse to generate proofs. In #10581, the string diagram widget only uses the morphisms generated by the normalization tactic and does not use proof terms ensuring that the original morphism and the normalized morphism are equal. Proof terms will be necessary for proof generation.

• There is also the possibility of using homotopy.io (https://github.com/homotopy-io), a graphical proof assistant for category theory, from Lean. At this point, I have very few ideas regarding this approach.

• The normalization tactic allows for an alternative implementation of the coherent tactic.

Main definitions

• Tactic.Monoidal.eval: Given a Lean expression e that represents a morphism in a monoidal category, this function returns a pair of ⟨e', pf⟩ where e' is the normalized expression of e and pf is a proof that e = e'.

Implementation notes

The function Tactic.Monoidal.eval fails to produce a proof term when the environment cannot find the necessary MonoidalCategory C instance. This occurs when running the string diagram widget, and the error makes it impossible for the string diagram widget to generate the diagram. To work around the widget failure, if the proof generation fails when eval running, it returns a meaningless term mkConst ``True in place of the proof term.

structure Mathlib.Tactic.Monoidal.Context : Type

The context for evaluating expressions.

• C : Lean.Expr

  The expression for the underlying category.

def Mathlib.Tactic.Monoidal.mkContext (e : Lean.Expr) : Lean.MetaM Mathlib.Tactic.Monoidal.Context

Populate a context object for evaluating e.

Equations

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

@[reducible, inline]

abbrev Mathlib.Tactic.Monoidal.MonoidalM (α : Type) : Type

The monad for the normalization of 2-morphisms.

Equations

• Mathlib.Tactic.Monoidal.MonoidalM = ReaderT Mathlib.Tactic.Monoidal.Context Lean.MetaM

@[reducible, inline]

abbrev Mathlib.Tactic.Monoidal.MonoidalM.run {α : Type} (c : Mathlib.Tactic.Monoidal.Context) (m : Mathlib.Tactic.Monoidal.MonoidalM α) : Lean.MetaM α

Run a computation in the M monad.

Equations

• Mathlib.Tactic.Monoidal.MonoidalM.run c m = ReaderT.run m c

structure Mathlib.Tactic.Monoidal.Atom₁ : Type

Expressions for atomic 1-morphisms.

• e : Lean.Expr

  Extract a Lean expression from an Atom₁ expression.

inductive Mathlib.Tactic.Monoidal.Mor₁ : Type

Expressions for 1-morphisms.

• id: Mathlib.Tactic.Monoidal.Mor₁

  id is the expression for 𝟙_ C.

• comp: Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.Mor₁

  comp X Y is the expression for X ⊗ Y

• of: Mathlib.Tactic.Monoidal.Atom₁ → Mathlib.Tactic.Monoidal.Mor₁

  Construct the expression for an atomic 1-morphism.

instance Mathlib.Tactic.Monoidal.instInhabitedMor₁ : Inhabited Mathlib.Tactic.Monoidal.Mor₁

Equations

• Mathlib.Tactic.Monoidal.instInhabitedMor₁ = { default := Mathlib.Tactic.Monoidal.Mor₁.id }

def Mathlib.Tactic.Monoidal.Mor₁.toList : Mathlib.Tactic.Monoidal.Mor₁ → List Mathlib.Tactic.Monoidal.Atom₁

Converts a 1-morphism into a list of its components.

Equations

• Mathlib.Tactic.Monoidal.Mor₁.id.toList = []
• (f.comp g).toList = f.toList ++ g.toList
• (Mathlib.Tactic.Monoidal.Mor₁.of f).toList = [f]

def Mathlib.Tactic.Monoidal.isTensorUnit? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Returns 𝟙_ C if the expression e is of the form 𝟙_ C.

Equations

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

def Mathlib.Tactic.Monoidal.isTensorObj? (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Returns (f, g) if the expression e is of the form f ⊗ g.

Equations

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

partial def Mathlib.Tactic.Monoidal.toMor₁ (e : Lean.Expr) : Lean.MetaM Mathlib.Tactic.Monoidal.Mor₁

Construct a Mor₁ expression from a Lean expression.

inductive Mathlib.Tactic.Monoidal.StructuralAtom : Type

Expressions for atomic structural 2-morphisms.

• associator: Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.StructuralAtom

  The expression for the associator (α_ f g h).hom.

• associatorInv: Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.StructuralAtom

  The expression for the inverse of the associator (α_ f g h).inv.

• leftUnitor: Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.StructuralAtom

  The expression for the left unitor (λ_ f).hom.

• leftUnitorInv: Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.StructuralAtom

  The expression for the inverse of the left unitor (λ_ f).inv.

• rightUnitor: Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.StructuralAtom

  The expression for the right unitor (ρ_ f).hom.

• rightUnitorInv: Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.StructuralAtom

  The expression for the inverse of the right unitor (ρ_ f).inv.

instance Mathlib.Tactic.Monoidal.instInhabitedStructuralAtom : Inhabited Mathlib.Tactic.Monoidal.StructuralAtom

Equations

• Mathlib.Tactic.Monoidal.instInhabitedStructuralAtom = { default := Mathlib.Tactic.Monoidal.StructuralAtom.associator default default default }

def Mathlib.Tactic.Monoidal.structuralAtom? (e : Lean.Expr) : Lean.MetaM (Option Mathlib.Tactic.Monoidal.StructuralAtom)

Construct a StructuralAtom expression from a Lean expression.

Equations

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

structure Mathlib.Tactic.Monoidal.Atom : Type

Expressions for atomic non-structural 2-morphisms.

• e : Lean.Expr

  Extract a Lean expression from an Atom expression.

instance Mathlib.Tactic.Monoidal.instInhabitedAtom : Inhabited Mathlib.Tactic.Monoidal.Atom

Equations

• Mathlib.Tactic.Monoidal.instInhabitedAtom = { default := { e := default } }

inductive Mathlib.Tactic.Monoidal.WhiskerRightExpr : Type

Expressions of the form η ▷ f₁ ▷ ... ▷ fₙ.

• of: Mathlib.Tactic.Monoidal.Atom → Mathlib.Tactic.Monoidal.WhiskerRightExpr

  Construct the expression for an atomic 2-morphism.

• whisker: Mathlib.Tactic.Monoidal.WhiskerRightExpr → Mathlib.Tactic.Monoidal.Atom₁ → Mathlib.Tactic.Monoidal.WhiskerRightExpr

  Construct the expression for η ▷ f.

instance Mathlib.Tactic.Monoidal.instInhabitedWhiskerRightExpr : Inhabited Mathlib.Tactic.Monoidal.WhiskerRightExpr

Equations

• Mathlib.Tactic.Monoidal.instInhabitedWhiskerRightExpr = { default := Mathlib.Tactic.Monoidal.WhiskerRightExpr.of default }

inductive Mathlib.Tactic.Monoidal.WhiskerLeftExpr : Type

Expressions of the form f₁ ◁ ... ◁ fₙ ◁ η.

• of: Mathlib.Tactic.Monoidal.WhiskerRightExpr → Mathlib.Tactic.Monoidal.WhiskerLeftExpr

  Construct the expression for a right-whiskered 2-morphism.

• whisker: Mathlib.Tactic.Monoidal.Atom₁ → Mathlib.Tactic.Monoidal.WhiskerLeftExpr → Mathlib.Tactic.Monoidal.WhiskerLeftExpr

  Construct the expression for f ◁ η.

instance Mathlib.Tactic.Monoidal.instInhabitedWhiskerLeftExpr : Inhabited Mathlib.Tactic.Monoidal.WhiskerLeftExpr

Equations

• Mathlib.Tactic.Monoidal.instInhabitedWhiskerLeftExpr = { default := Mathlib.Tactic.Monoidal.WhiskerLeftExpr.of default }

inductive Mathlib.Tactic.Monoidal.Structural : Type

Expressions for structural 2-morphisms.

• atom: Mathlib.Tactic.Monoidal.StructuralAtom → Mathlib.Tactic.Monoidal.Structural

  Expressions for atomic structural 2-morphisms.

• id: Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.Structural

  Expressions for the identity 𝟙 f.

• comp: Mathlib.Tactic.Monoidal.Structural → Mathlib.Tactic.Monoidal.Structural → Mathlib.Tactic.Monoidal.Structural

  Expressions for the composition η ≫ θ.

• whiskerLeft: Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.Structural → Mathlib.Tactic.Monoidal.Structural

  Expressions for the left whiskering f ◁ η.

• whiskerRight: Mathlib.Tactic.Monoidal.Structural → Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.Structural

  Expressions for the right whiskering η ▷ f.

• monoidalCoherence: Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.Mor₁ → Lean.Expr → Mathlib.Tactic.Monoidal.Structural

  Expressions for α in the monoidal composition η ⊗≫ θ := η ≫ α ≫ θ.

instance Mathlib.Tactic.Monoidal.instInhabitedStructural : Inhabited Mathlib.Tactic.Monoidal.Structural

Equations

• Mathlib.Tactic.Monoidal.instInhabitedStructural = { default := Mathlib.Tactic.Monoidal.Structural.atom default }

inductive Mathlib.Tactic.Monoidal.NormalExpr : Type

Normalized expressions for 2-morphisms.

• nil: Mathlib.Tactic.Monoidal.Structural → Mathlib.Tactic.Monoidal.NormalExpr

  Construct the expression for a structural 2-morphism.

• cons: Mathlib.Tactic.Monoidal.Structural → Mathlib.Tactic.Monoidal.WhiskerLeftExpr → Mathlib.Tactic.Monoidal.NormalExpr → Mathlib.Tactic.Monoidal.NormalExpr

  Construct the normalized expression of 2-morphisms recursively.

instance Mathlib.Tactic.Monoidal.instInhabitedNormalExpr : Inhabited Mathlib.Tactic.Monoidal.NormalExpr

Equations

• Mathlib.Tactic.Monoidal.instInhabitedNormalExpr = { default := Mathlib.Tactic.Monoidal.NormalExpr.nil default }

def Mathlib.Tactic.Monoidal.src (η : Lean.Expr) : Lean.MetaM Mathlib.Tactic.Monoidal.Mor₁

The domain of a morphism.

Equations

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

def Mathlib.Tactic.Monoidal.tgt (η : Lean.Expr) : Lean.MetaM Mathlib.Tactic.Monoidal.Mor₁

The codomain of a morphism.

Equations

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

def Mathlib.Tactic.Monoidal.Atom.src (η : Mathlib.Tactic.Monoidal.Atom) : Lean.MetaM Mathlib.Tactic.Monoidal.Mor₁

The domain of a 2-morphism.

Equations

• η.src = Mathlib.Tactic.Monoidal.src η.e

def Mathlib.Tactic.Monoidal.Atom.tgt (η : Mathlib.Tactic.Monoidal.Atom) : Lean.MetaM Mathlib.Tactic.Monoidal.Mor₁

The codomain of a 2-morphism.

Equations

• η.tgt = Mathlib.Tactic.Monoidal.tgt η.e

def Mathlib.Tactic.Monoidal.WhiskerRightExpr.src : Mathlib.Tactic.Monoidal.WhiskerRightExpr → Lean.MetaM Mathlib.Tactic.Monoidal.Mor₁

The domain of a 2-morphism.

Equations

• (Mathlib.Tactic.Monoidal.WhiskerRightExpr.of η).src = η.src
• (η.whisker f).src = do let __do_lift ← η.src pure (__do_lift.comp (Mathlib.Tactic.Monoidal.Mor₁.of f))

def Mathlib.Tactic.Monoidal.WhiskerRightExpr.tgt : Mathlib.Tactic.Monoidal.WhiskerRightExpr → Lean.MetaM Mathlib.Tactic.Monoidal.Mor₁

The codomain of a 2-morphism.

Equations

• (Mathlib.Tactic.Monoidal.WhiskerRightExpr.of η).tgt = η.tgt
• (η.whisker f).tgt = do let __do_lift ← η.tgt pure (__do_lift.comp (Mathlib.Tactic.Monoidal.Mor₁.of f))

def Mathlib.Tactic.Monoidal.WhiskerLeftExpr.src : Mathlib.Tactic.Monoidal.WhiskerLeftExpr → Lean.MetaM Mathlib.Tactic.Monoidal.Mor₁

The domain of a 2-morphism.

Equations

• (Mathlib.Tactic.Monoidal.WhiskerLeftExpr.of η).src = η.src
• (Mathlib.Tactic.Monoidal.WhiskerLeftExpr.whisker f η).src = do let __do_lift ← η.src pure ((Mathlib.Tactic.Monoidal.Mor₁.of f).comp __do_lift)

def Mathlib.Tactic.Monoidal.WhiskerLeftExpr.tgt : Mathlib.Tactic.Monoidal.WhiskerLeftExpr → Lean.MetaM Mathlib.Tactic.Monoidal.Mor₁

The codomain of a 2-morphism.

Equations

• (Mathlib.Tactic.Monoidal.WhiskerLeftExpr.of η).tgt = η.tgt
• (Mathlib.Tactic.Monoidal.WhiskerLeftExpr.whisker f η).tgt = do let __do_lift ← η.tgt pure ((Mathlib.Tactic.Monoidal.Mor₁.of f).comp __do_lift)

def Mathlib.Tactic.Monoidal.StructuralAtom.src : Mathlib.Tactic.Monoidal.StructuralAtom → Mathlib.Tactic.Monoidal.Mor₁

The domain of a 2-morphism.

Equations

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

def Mathlib.Tactic.Monoidal.StructuralAtom.tgt : Mathlib.Tactic.Monoidal.StructuralAtom → Mathlib.Tactic.Monoidal.Mor₁

The codomain of a 2-morphism.

Equations

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

def Mathlib.Tactic.Monoidal.Structural.src : Mathlib.Tactic.Monoidal.Structural → Mathlib.Tactic.Monoidal.Mor₁

The domain of a 2-morphism.

Equations

• (Mathlib.Tactic.Monoidal.Structural.atom η).src = η.src
• (Mathlib.Tactic.Monoidal.Structural.id f).src = f
• (α.comp β).src = α.src
• (Mathlib.Tactic.Monoidal.Structural.whiskerLeft f η).src = f.comp η.src
• (η.whiskerRight f).src = η.src.comp f
• (Mathlib.Tactic.Monoidal.Structural.monoidalCoherence f g e).src = f

def Mathlib.Tactic.Monoidal.Structural.tgt : Mathlib.Tactic.Monoidal.Structural → Mathlib.Tactic.Monoidal.Mor₁

The codomain of a 2-morphism.

Equations

• (Mathlib.Tactic.Monoidal.Structural.atom η).tgt = η.tgt
• (Mathlib.Tactic.Monoidal.Structural.id f).tgt = f
• (α.comp β).tgt = β.tgt
• (Mathlib.Tactic.Monoidal.Structural.whiskerLeft f η).tgt = f.comp η.tgt
• (η.whiskerRight f).tgt = η.tgt.comp f
• (Mathlib.Tactic.Monoidal.Structural.monoidalCoherence f g e).tgt = g

def Mathlib.Tactic.Monoidal.NormalExpr.src : Mathlib.Tactic.Monoidal.NormalExpr → Mathlib.Tactic.Monoidal.Mor₁

The domain of a 2-morphism.

Equations

• x.src = match x with | Mathlib.Tactic.Monoidal.NormalExpr.nil η => η.src | Mathlib.Tactic.Monoidal.NormalExpr.cons α head tail => α.src

def Mathlib.Tactic.Monoidal.NormalExpr.tgt : Mathlib.Tactic.Monoidal.NormalExpr → Mathlib.Tactic.Monoidal.Mor₁

The codomain of a 2-morphism.

Equations

• (Mathlib.Tactic.Monoidal.NormalExpr.nil η).tgt = η.tgt
• (Mathlib.Tactic.Monoidal.NormalExpr.cons α head tail).tgt = tail.tgt

def Mathlib.Tactic.Monoidal.NormalExpr.associator (f : Mathlib.Tactic.Monoidal.Mor₁) (g : Mathlib.Tactic.Monoidal.Mor₁) (h : Mathlib.Tactic.Monoidal.Mor₁) : Mathlib.Tactic.Monoidal.NormalExpr

The associator as a term of normalExpr.

Equations

• Mathlib.Tactic.Monoidal.NormalExpr.associator f g h = Mathlib.Tactic.Monoidal.NormalExpr.nil (Mathlib.Tactic.Monoidal.Structural.atom (Mathlib.Tactic.Monoidal.StructuralAtom.associator f g h))

def Mathlib.Tactic.Monoidal.NormalExpr.associatorInv (f : Mathlib.Tactic.Monoidal.Mor₁) (g : Mathlib.Tactic.Monoidal.Mor₁) (h : Mathlib.Tactic.Monoidal.Mor₁) : Mathlib.Tactic.Monoidal.NormalExpr

The inverse of the associator as a term of normalExpr.

Equations

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

def Mathlib.Tactic.Monoidal.NormalExpr.leftUnitor (f : Mathlib.Tactic.Monoidal.Mor₁) : Mathlib.Tactic.Monoidal.NormalExpr

The left unitor as a term of normalExpr.

Equations

• Mathlib.Tactic.Monoidal.NormalExpr.leftUnitor f = Mathlib.Tactic.Monoidal.NormalExpr.nil (Mathlib.Tactic.Monoidal.Structural.atom (Mathlib.Tactic.Monoidal.StructuralAtom.leftUnitor f))

def Mathlib.Tactic.Monoidal.NormalExpr.leftUnitorInv (f : Mathlib.Tactic.Monoidal.Mor₁) : Mathlib.Tactic.Monoidal.NormalExpr

The inverse of the left unitor as a term of normalExpr.

Equations

• Mathlib.Tactic.Monoidal.NormalExpr.leftUnitorInv f = Mathlib.Tactic.Monoidal.NormalExpr.nil (Mathlib.Tactic.Monoidal.Structural.atom (Mathlib.Tactic.Monoidal.StructuralAtom.leftUnitorInv f))

def Mathlib.Tactic.Monoidal.NormalExpr.rightUnitor (f : Mathlib.Tactic.Monoidal.Mor₁) : Mathlib.Tactic.Monoidal.NormalExpr

The right unitor as a term of normalExpr.

Equations

• Mathlib.Tactic.Monoidal.NormalExpr.rightUnitor f = Mathlib.Tactic.Monoidal.NormalExpr.nil (Mathlib.Tactic.Monoidal.Structural.atom (Mathlib.Tactic.Monoidal.StructuralAtom.rightUnitor f))

def Mathlib.Tactic.Monoidal.NormalExpr.rightUnitorInv (f : Mathlib.Tactic.Monoidal.Mor₁) : Mathlib.Tactic.Monoidal.NormalExpr

The inverse of the right unitor as a term of normalExpr.

Equations

• Mathlib.Tactic.Monoidal.NormalExpr.rightUnitorInv f = Mathlib.Tactic.Monoidal.NormalExpr.nil (Mathlib.Tactic.Monoidal.Structural.atom (Mathlib.Tactic.Monoidal.StructuralAtom.rightUnitorInv f))

def Mathlib.Tactic.Monoidal.WhiskerRightExpr.atom : Mathlib.Tactic.Monoidal.WhiskerRightExpr → Mathlib.Tactic.Monoidal.Atom

Return η for η ▷ g₁ ▷ ... ▷ gₙ.

Equations

• (Mathlib.Tactic.Monoidal.WhiskerRightExpr.of η).atom = η
• (η.whisker f).atom = η.atom

def Mathlib.Tactic.Monoidal.WhiskerLeftExpr.atom : Mathlib.Tactic.Monoidal.WhiskerLeftExpr → Mathlib.Tactic.Monoidal.Atom

Return η for f₁ ◁ ... ◁ fₙ ◁ η ▷ g₁ ▷ ... ▷ gₙ.

Equations

• (Mathlib.Tactic.Monoidal.WhiskerLeftExpr.of η).atom = η.atom
• (Mathlib.Tactic.Monoidal.WhiskerLeftExpr.whisker f η).atom = η.atom

partial def Mathlib.Tactic.Monoidal.structural? (e : Lean.Expr) : Lean.MetaM Mathlib.Tactic.Monoidal.Structural

Construct a Structural expression from a Lean expression for a structural 2-morphism.

def Mathlib.Tactic.Monoidal.NormalExpr.of (η : Mathlib.Tactic.Monoidal.WhiskerLeftExpr) : Lean.MetaM Mathlib.Tactic.Monoidal.NormalExpr

Construct a NormalExpr expression from a WhiskerLeftExpr expression.

Equations

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

def Mathlib.Tactic.Monoidal.NormalExpr.ofExpr (η : Lean.Expr) : Lean.MetaM Mathlib.Tactic.Monoidal.NormalExpr

Construct a NormalExpr expression from a Lean expression for an atomic 2-morphism.

Equations

• Mathlib.Tactic.Monoidal.NormalExpr.ofExpr η = Mathlib.Tactic.Monoidal.NormalExpr.of (Mathlib.Tactic.Monoidal.WhiskerLeftExpr.of (Mathlib.Tactic.Monoidal.WhiskerRightExpr.of { e := η }))

def Mathlib.Tactic.Monoidal.structuralOfMonoidalComp (C : Lean.Expr) (e : Lean.Expr) : Lean.MetaM Mathlib.Tactic.Monoidal.Structural

If e is an expression of the form η ⊗≫ θ := η ≫ α ≫ θ in the monoidal category C, return the expression for α .

Equations

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

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

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

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

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

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

theorem Mathlib.Tactic.Monoidal.evalWhiskerLeft_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f : C} {g : C} {h : C} {i : C} {η : h ⟶ i} {θ : CategoryTheory.MonoidalCategory.tensorObj g h ⟶ CategoryTheory.MonoidalCategory.tensorObj g i} {ι : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g h) ⟶ CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g i)} {ι' : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g h) ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) i} {ι'' : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) h ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) i} (pf_θ : CategoryTheory.MonoidalCategory.whiskerLeft g η = θ) (pf_ι : CategoryTheory.MonoidalCategory.whiskerLeft f θ = ι) (pf_ι' : CategoryTheory.CategoryStruct.comp ι (CategoryTheory.MonoidalCategory.associator f g i).inv = ι') (pf_ι'' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f g h).hom ι' = ι'') : CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj f g) η = ι''

theorem Mathlib.Tactic.Monoidal.evalWhiskerLeft_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f : C} {g : C} {η : f ⟶ g} {η' : f ⟶ CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) g} {η'' : CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) f ⟶ CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) g} (pf_η' : CategoryTheory.CategoryStruct.comp η (CategoryTheory.MonoidalCategory.leftUnitor g).inv = η') (pf_η'' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor f).hom η' = η'') : CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) η = η''

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

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

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

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

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

theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f : C} {g : C} {h : C} {i : C} {j : C} (α : f ⟶ g) (η : g ⟶ h) {ηs : h ⟶ i} {θ : CategoryTheory.MonoidalCategory.tensorObj h j ⟶ CategoryTheory.MonoidalCategory.tensorObj i j} (pf_θ : CategoryTheory.MonoidalCategory.whiskerRight ηs j = θ) : CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp η ηs)) j = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight α j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight η j) θ)

theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_whisker {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f : C} {g : C} {h : C} {i : C} {j : C} {α : g ⟶ CategoryTheory.MonoidalCategory.tensorObj f h} {η : h ⟶ i} {ηs : CategoryTheory.MonoidalCategory.tensorObj f i ⟶ j} {k : C} {η₁ : CategoryTheory.MonoidalCategory.tensorObj h k ⟶ CategoryTheory.MonoidalCategory.tensorObj i k} {η₂ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj h k) ⟶ CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj i k)} {ηs₁ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f i) k ⟶ CategoryTheory.MonoidalCategory.tensorObj j k} {ηs₂ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj i k) ⟶ CategoryTheory.MonoidalCategory.tensorObj j k} {η₃ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj h k) ⟶ CategoryTheory.MonoidalCategory.tensorObj j k} {η₄ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f h) k ⟶ CategoryTheory.MonoidalCategory.tensorObj j k} {η₅ : CategoryTheory.MonoidalCategory.tensorObj g k ⟶ CategoryTheory.MonoidalCategory.tensorObj j k} (pf_η₁ : CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id h) (CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.id i))) k = η₁) (pf_η₂ : CategoryTheory.MonoidalCategory.whiskerLeft f η₁ = η₂) (pf_ηs₁ : CategoryTheory.MonoidalCategory.whiskerRight ηs k = ηs₁) (pf_ηs₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f i k).inv ηs₁ = ηs₂) (pf_η₃ : CategoryTheory.CategoryStruct.comp η₂ ηs₂ = η₃) (pf_η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f h k).hom η₃ = η₄) (pf_η₅ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight α k) η₄ = η₅) : CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft f η) ηs)) k = η₅

theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f : C} {f' : C} {g : C} {h : C} {η : f ⟶ f'} {η₁ : CategoryTheory.MonoidalCategory.tensorObj f g ⟶ CategoryTheory.MonoidalCategory.tensorObj f' g} {η₂ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) h ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f' g) h} {η₃ : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj f g) h ⟶ CategoryTheory.MonoidalCategory.tensorObj f' (CategoryTheory.MonoidalCategory.tensorObj g h)} {η₄ : CategoryTheory.MonoidalCategory.tensorObj f (CategoryTheory.MonoidalCategory.tensorObj g h) ⟶ CategoryTheory.MonoidalCategory.tensorObj f' (CategoryTheory.MonoidalCategory.tensorObj g h)} (pf_η₁ : CategoryTheory.MonoidalCategory.whiskerRight η g = η₁) (pf_η₂ : CategoryTheory.MonoidalCategory.whiskerRight η₁ h = η₂) (pf_η₃ : CategoryTheory.CategoryStruct.comp η₂ (CategoryTheory.MonoidalCategory.associator f' g h).hom = η₃) (pf_η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator f g h).inv η₃ = η₄) : CategoryTheory.MonoidalCategory.whiskerRight η (CategoryTheory.MonoidalCategory.tensorObj g h) = η₄

theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {f : C} {g : C} {η : f ⟶ g} {η₁ : f ⟶ CategoryTheory.MonoidalCategory.tensorObj g (𝟙_ C)} {η₂ : CategoryTheory.MonoidalCategory.tensorObj f (𝟙_ C) ⟶ CategoryTheory.MonoidalCategory.tensorObj g (𝟙_ C)} (pf_η₁ : CategoryTheory.CategoryStruct.comp η (CategoryTheory.MonoidalCategory.rightUnitor g).inv = η₁) (pf_η₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor f).hom η₁ = η₂) : CategoryTheory.MonoidalCategory.whiskerRight η (𝟙_ C) = η₂

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

def Mathlib.Tactic.Monoidal.Mor₁.e : Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.MonoidalM Lean.Expr

Extract a Lean expression from a Mor₁ expression.

Equations

• Mathlib.Tactic.Monoidal.Mor₁.id.e = do let ctx ← read liftM (Lean.Meta.mkAppOptM `CategoryTheory.MonoidalCategoryStruct.tensorUnit #[some ctx.C, none, none])
• (f.comp g).e = do let __do_lift ← f.e let __do_lift_1 ← g.e liftM (Lean.Meta.mkAppM `CategoryTheory.MonoidalCategoryStruct.tensorObj #[__do_lift, __do_lift_1])
• (Mathlib.Tactic.Monoidal.Mor₁.of f).e = pure f.e

def Mathlib.Tactic.Monoidal.StructuralAtom.e : Mathlib.Tactic.Monoidal.StructuralAtom → Mathlib.Tactic.Monoidal.MonoidalM Lean.Expr

Extract a Lean expression from a StructuralAtom expression.

Equations

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

partial def Mathlib.Tactic.Monoidal.Structural.e : Mathlib.Tactic.Monoidal.Structural → Mathlib.Tactic.Monoidal.MonoidalM Lean.Expr

Extract a Lean expression from a Structural expression.

def Mathlib.Tactic.Monoidal.WhiskerRightExpr.e : Mathlib.Tactic.Monoidal.WhiskerRightExpr → Mathlib.Tactic.Monoidal.MonoidalM Lean.Expr

Extract a Lean expression from a WhiskerRightExpr expression.

Equations

• (Mathlib.Tactic.Monoidal.WhiskerRightExpr.of η).e = pure η.e
• (η.whisker f).e = do let __do_lift ← η.e liftM (Lean.Meta.mkAppM `CategoryTheory.MonoidalCategoryStruct.whiskerRight #[__do_lift, f.e])

def Mathlib.Tactic.Monoidal.WhiskerLeftExpr.e : Mathlib.Tactic.Monoidal.WhiskerLeftExpr → Mathlib.Tactic.Monoidal.MonoidalM Lean.Expr

Extract a Lean expression from a WhiskerLeftExpr expression.

Equations

• (Mathlib.Tactic.Monoidal.WhiskerLeftExpr.of η).e = η.e
• (Mathlib.Tactic.Monoidal.WhiskerLeftExpr.whisker f η).e = do let __do_lift ← η.e liftM (Lean.Meta.mkAppM `CategoryTheory.MonoidalCategoryStruct.whiskerLeft #[f.e, __do_lift])

def Mathlib.Tactic.Monoidal.NormalExpr.e : Mathlib.Tactic.Monoidal.NormalExpr → Mathlib.Tactic.Monoidal.MonoidalM Lean.Expr

Extract a Lean expression from a NormalExpr expression.

Equations

• One or more equations did not get rendered due to their size.
• (Mathlib.Tactic.Monoidal.NormalExpr.nil η).e = η.e

structure Mathlib.Tactic.Monoidal.Result : Type

The result of evaluating an expression into normal form.

• expr : Mathlib.Tactic.Monoidal.NormalExpr

  The normalized expression of the 2-morphism.

• proof : Lean.Expr

  The proof that the normalized expression is equal to the original expression.

partial def Mathlib.Tactic.Monoidal.evalComp : Mathlib.Tactic.Monoidal.NormalExpr → Mathlib.Tactic.Monoidal.NormalExpr → Mathlib.Tactic.Monoidal.MonoidalM Mathlib.Tactic.Monoidal.Result

Evaluate the expression η ≫ θ into a normalized form.

partial def Mathlib.Tactic.Monoidal.evalWhiskerLeftExpr : Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.NormalExpr → Mathlib.Tactic.Monoidal.MonoidalM Mathlib.Tactic.Monoidal.Result

Evaluate the expression f ◁ η into a normalized form.

partial def Mathlib.Tactic.Monoidal.evalWhiskerRightExpr : Mathlib.Tactic.Monoidal.NormalExpr → Mathlib.Tactic.Monoidal.Mor₁ → Mathlib.Tactic.Monoidal.MonoidalM Mathlib.Tactic.Monoidal.Result

Evaluate the expression η ▷ f into a normalized form.

partial def Mathlib.Tactic.Monoidal.eval (e : Lean.Expr) : Mathlib.Tactic.Monoidal.MonoidalM Mathlib.Tactic.Monoidal.Result

Evaluate the expression of a 2-morphism into a normalized form.

def Mathlib.Tactic.Monoidal.NormalExpr.toList : Mathlib.Tactic.Monoidal.NormalExpr → List Mathlib.Tactic.Monoidal.WhiskerLeftExpr

Convert a NormalExpr expression into a list of WhiskerLeftExpr expressions.

Equations

• (Mathlib.Tactic.Monoidal.NormalExpr.nil η).toList = []
• (Mathlib.Tactic.Monoidal.NormalExpr.cons α head tail).toList = head :: tail.toList

def «termNormalize%_» : Lean.ParserDescr

normalize% η is the normalization of the 2-morphism η.

1. The normalized 2-morphism is of the form α₀ ≫ η₀ ≫ α₁ ≫ η₁ ≫ ... αₘ ≫ ηₘ ≫ αₘ₊₁ where each αᵢ is a structural 2-morphism (consisting of associators and unitors),
2. each ηᵢ is a non-structural 2-morphism of the form f₁ ◁ ... ◁ fₘ ◁ θ, and
3. θ is of the form ι ▷ g₁ ▷ ... ▷ gₗ

Equations

• «termNormalize%_» = Lean.ParserDescr.node `termNormalize%_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "normalize% ") (Lean.ParserDescr.cat `term 51))

theorem mk_eq {α : Type u_1} (a : α) (b : α) (a' : α) (b' : α) (ha : a = a') (hb : b = b') (h : a' = b') : a = b

def mkEq (e : Lean.Expr) : Lean.MetaM Lean.Expr

Transform an equality between 2-morphisms into the equality between their normalizations.

Equations

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

def tacticMonoidal_nf : Lean.ParserDescr

Normalize the both sides of an equality.

Equations

• tacticMonoidal_nf = Lean.ParserDescr.node `tacticMonoidal_nf 1024 (Lean.ParserDescr.nonReservedSymbol "monoidal_nf" false)