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 Kim Morrison in Lean 4.

source

theorem Tactic.Elementwise.forall_congr_forget_Type (α : Type u) (p : α → Prop) :

(∀ (x : (CategoryTheory.forget (Type u)).obj α), p x) ↔ ∀ (x : α), p x

source

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

⇑f = f

source

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

f x = g x

source

def Tactic.Elementwise.elementwiseThms :

List Lean.Name

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

source

def Tactic.Elementwise.elementwiseExpr (src : Lean.Name) (type pf : Lean.Expr) (simpSides : 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.

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

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

Lean.MetaM α

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

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.

Equations