Commit 2025-02-16 20:14 9c88c8f9

View on Github →

refactor(CategoryTheory): redefine action of endomorphisms on morphisms (#21917) Right now the End X-action on X ⟶ Y is defined as

instance mulActionLeft {X : Cᵒᵖ} {Y : C} : MulAction (End X) (unop X ⟶ Y) where
  smul r f := r.unop ≫ f
  one_smul := Category.id_comp
  mul_smul _ _ _ := Category.assoc _ _ _

which works really badly in practice. One big reason is that not all hom-sets get the action, so while you have unop (op X) ⟶ Y you have the module structure, but if you dsimp this you suddenly have X ⟶ Y which isn't a module anymore. But even if things work out syntactically, things go wrong, as the following example shows:

import Mathlib
open CategoryTheory Opposite
variable {C : Type u} [Category.{v} C] [Preadditive C] {X Y : C}
example : Module (End (op X)) (unop (op X) ⟶ Y) := inferInstance -- failed to synthesize
example : Module (End (op X)) (unop (op X) ⟶ Y) := moduleEndLeft _ -- works

Even if you remind Lean what the action is, you get mysterious problem like simp lemmas not firing even though rw works. I clearly remember this action being a pain to work with in Lean 3, and it is still bad in Lean 4. This PR redefines the action as

instance mulActionLeft {X Y : C} : MulAction (End X)ᵐᵒᵖ (X ⟶ Y) where
  smul r f := r.unop ≫ f
  one_smul := Category.id_comp
  mul_smul _ _ _ := Category.assoc _ _ _

which makes all these problems go away in my applications. The diff is pretty small, and I don't think many people are using this action, so I don't think there will be many problems caused by this change.

Estimated changes