Semigroup of compositions

Stream: mathlib4

[Michael Lane]

Hi,

I am wondering if there is a type class of semigroups where the operation is function composition? Something like this:

/-- Elements of `F` can be injectively coerced to functions `X → X` so that coercion
commutes with composition. -/
class CompSemigroup
(F : Type*) (X : outParam Type*) [FunLike F X X] where
  comp : F → F → F
  coe_hom : ∀ f g : F, ⇑(comp f g) = ⇑f ∘ ⇑g

namespace CompSemigroup

theorem comp_assoc
{F X : Type*} [FunLike F X X ] [CompSemigroup F X]
: ∀ f g h : F, comp (comp f g) h = comp f (comp g h) := by
  intros
  apply DFunLike.coe_injective'
  repeat rw[coe_hom]
  rfl

end CompSemigroup

instance {F X : Type*} [FunLike F X X] [CompSemigroup F X]
: Semigroup F where
  mul := CompSemigroup.comp
  mul_assoc := CompSemigroup.comp_assoc

I wonder if mathlib already has this type class or something equivalent to it, because I need the following theorem, which converts a commutative semigroup operation to commutative function composition.

theorem commute_of_comm_compSemigroup
{F X : Type*} [FunLike F X X] [CompSemigroup F X] [IsMulCommutative F]
: ∀ f g : F, Function.Commute f g := by
  intro f g
  refine congrFun ?_
  calc ⇑f ∘ ⇑g
    _ = ⇑(f * g) := (CompSemigroup.coe_hom f g).symm
    _ = ⇑(g * f) := by rw[CommSemigroup.mul_comm f g]
    _ = ⇑g ∘ ⇑f := CompSemigroup.coe_hom g f

Thanks a lot!
Michael

[Johan Commelin]

@Michael Lane Hi! We don't have a typeclass for that. We do have docs#End which is a type that sets up the endomorphism monoid where the multiplication * is definitionally composition. And then there are some API lemmas for moving back and forth between multiplication and composition. I think that's the closest we have to what you're asking for.

It's not ideal. But I think it minimizes the amount setup and code duplication wrt Mathlib's algebraic hierarchy.

[Michael Lane]

Hi! Thank you. Your docs link is dead, there are several namespaces that have End type synonyms.

I am not sure what those API lemmas you mention are, for moving back and forth between multiplication and composition. Maybe you can help me with my specific use-case. I have the following type synonym:

namespace AffineMap

protected def End
(R : Type*) [Ring R] (V : Type*) [AddCommGroup V] [Module R V] :=
  V →ᵃ[R] V

end AffineMap

I could instance AffineMap.End as Semigroup (or as Monoid, if you prefer) and FunLike. Given M : Subsemigroup (AffineMap.End R V) and [IsMulCommutative M], what API lemmas do I use to prove ∀ f g : M, Function.Commute f g? By the way, there's nothing specific about AffineMap here, since we're just talking about function composition, I'm just using it for the sake of concreteness.

EDIT: I answered my own question, I found docs#Function.End.mul_def