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 #

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

List of simp lemmas to apply to the elementwise theorem.

Instances For

    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.

    Instances For

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

      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:

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


        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.

        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.

          Instances For