# 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 : .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} [] {X : C} {Y : C} {f : X Y} {g : X Y} (h : f = g) (x : .obj X) :
f x = g x

List of simp lemmas to apply to the elementwise theorem.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Tactic.Elementwise.elementwiseExpr (src : Lean.Name) (type : Lean.Expr) (pf : Lean.Expr) (simpSides : ) :

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.

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

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

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

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.

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

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.

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