Commit 2025-02-25 19:33 b1f5b964

View on Github →

refactor(CategoryTheory/Action/*): make Action.rho a MonoidHom instead of a morphism in MonCat (#21652)

Estimated changes

modified def Action.res
modified def Action.resComp
modified def Action.resId
modified def Action.ρAut
modified theorem Action.ρ_one
modified structure Action
modified def Action.diagonal
modified def Action.leftRegular
modified def Action.ofMulAction
deleted theorem Action.tensorUnit_ρ'
deleted theorem Action.tensor_ρ'
modified theorem Rep.linearization_obj_ρ
modified theorem Rep.linearization_of
modified theorem Rep.linearization_single
modified theorem Rep.linearization_δ_hom
modified theorem Rep.linearization_μ_hom
deleted theorem Rep.of_ρ_apply