Documentation

Mathlib.Tactic.CategoryTheory.Elementwise

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.

Equations
  • One or more equations did not get rendered due to their size.
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.

    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