Tools to reformulate category-theoretic lemmas in concrete categories

The elementwise attribute

The elementwise attribute generates lemmas for concrete categories from lemmas that equate morphisms in a category.

A sort of inverse to this for the Type* category is the @[higher_order] attribute.

For more details, see the documentation attached to the syntax declaration.

Main definitions

• The @[elementwise] attribute.

• The ``elementwise_of% h` term elaborator.

Implementation

This closely follows the implementation of the @[reassoc] attribute, due to Simon Hudon and reimplemented by Scott Morrison in Lean 4.

theorem Tactic.Elementwise.forall_congr_forget_Type (α : Type u) (p : α → Prop) : ((x : (CategoryTheory.forget (Type u)).obj α) → p x) ↔ (x : α) → p x

theorem Tactic.Elementwise.forget_hom_Type (α : Type u) (β : Type u) (f : α ⟶ β) : ↑f = f

theorem Tactic.Elementwise.hom_elementwise {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} {f : X ⟶ Y} {g : X ⟶ Y} (h : f = g) (x : (CategoryTheory.forget C).obj X) : ↑f x = ↑g x

def Tactic.Elementwise.elementwiseThms : List Lean.Name

List of simp lemmas to apply to the elementwise theorem.

def Tactic.Elementwise.elementwiseExpr (src : Lean.Name) (type : Lean.Expr) (pf : Lean.Expr) (simpSides : optParam Bool true) : Lean.MetaM (Lean.Expr × Option Lean.Level)

Given an equation f = g between morphisms X ⟶ Y in a category C (possibly after a ∀ binder), produce the equation ∀ (x : X), f x = g x or ∀ [ConcreteCategory C] (x : X), f x = g x as needed (after the ∀ binder), but with compositions fully right associated and identities removed.

Returns the proof of the new theorem along with (optionally) a new level metavariable for the first universe parameter to ConcreteCategory.

The simpSides option controls whether to simplify both sides of the equality, for simpNF purposes.

def Tactic.Elementwise.elementwiseExpr.extractCatInstance (eqTy : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Given an equality, extract a Category instance from it or raise an error. Returns the name of the category and its instance.

def Tactic.Elementwise.elementwiseExpr.mkHomElementwise {α : Type} (eqTy : Lean.Expr) (eqPf : Lean.Expr) (k : Lean.Expr → Option (Lean.Level × Lean.Expr) → Lean.MetaM α) : Lean.MetaM α

def Tactic.Elementwise.elementwise : Lean.ParserDescr

The elementwise attribute can be added to a lemma proving an equation of morphisms, and it creates a new lemma for a ConcreteCategory giving an equation with those morphisms applied to some value.

Syntax examples:

• @[elementwise]
• @[elementwise nosimp] to not use simp on both sides of the generated lemma
• @[elementwise (attr := simp)] to apply the simp attribute to both the generated lemma and the original lemma.

Example application of elementwise:

@[elementwise]
lemma some_lemma {C : Type*} [Category C]
    {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : X ⟶ Z) (w : ...) : f ≫ g = h := ...

produces

lemma some_lemma_apply {C : Type*} [Category C]
    {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : X ⟶ Z) (w : ...)
    [ConcreteCategory C] (x : X) : g (f x) = h x := ...

Here X is being coerced to a type via CategoryTheory.ConcreteCategory.hasCoeToSort and f, g, and h are being coerced to functions via CategoryTheory.ConcreteCategory.hasCoeToFun. Further, we simplify the type using CategoryTheory.coe_id : ((𝟙 X) : X → X) x = x and CategoryTheory.coe_comp : (f ≫ g) x = g (f x), replacing morphism composition with function composition.

The [ConcreteCategory C] argument will be omitted if it is possible to synthesize an instance.

The name of the produced lemma can be specified with @[elementwise other_lemma_name]. If simp is added first, the generated lemma will also have the simp attribute.

def Tactic.Elementwise.«termElementwise_of%_» : Lean.ParserDescr

elementwise_of% h, where h is a proof of an equation f = g between morphisms X ⟶ Y in a concrete category (possibly after a ∀ binder), produces a proof of equation ∀ (x : X), f x = g x, but with compositions fully right associated and identities removed.

A typical example is using elementwise_of% to dynamically generate rewrite lemmas:

example (M N K : MonCat) (f : M ⟶ N) (g : N ⟶ K) (h : M ⟶ K) (w : f ≫ g = h) (m : M) :
    g (f m) = h m := by rw [elementwise_of% w]

In this case, elementwise_of% w generates the lemma ∀ (x : M), f (g x) = h x.

Like the @[elementwise] attribute, elementwise_of% inserts a ConcreteCategory instance argument if it can't synthesize a relevant ConcreteCategory instance. (Technical note: The forgetful functor's universe variable is instantiated with a fresh level metavariable in this case.)

One difference between elementwise_of% and @[elementwise] is that @[elementwise] by default applies simp to both sides of the generated lemma to get something that is in simp normal form. elementwise_of% does not do this.

def Tactic.Elementwise.tacticElementwise___ : Lean.ParserDescr

def Tactic.Elementwise.tacticElementwise!___ : Lean.ParserDescr