Seeking comment for PR: FunLike monoid with nice composition

Stream: mathlib4

[Michael Lane]

Hi, I'm new here. I am planning on making a series of PRs towards the Markov-Kakutani fixed-point theorem. The first of these PRs are the definitions of a few type classes that provide an interface between the algebraic and set-theoretic properties of composing self-maps, as well as a few basic results. I first posted about this idea here.

Here is the commit to my side branch.

For your convenience, here is the commit message (I plan on making this the PR title/description as well):

feat(Dynamics): type classes for FunLike monoids with nice composition

The type synonyms Function.End, Monoid.End, Module.End, etc. all instance Monoid in the same manner, where the mul field is composition (of bundled endomorphisms), one is the identity endomorphism, and mul_assoc is the proof that function composition is associative. Making a Monoid instance for each End type synonym in this manner is not difficult. However, it is tedious to translate algebraic properties of the monoid to set-theoretic properties of the unbundled endomorphisms. The type classes CompSemigroup and its extensions make this translation easier.

Here is the description at the top of the new file Mathlib/Dynamics/Algebra.lean:

Monoids of functions with composition.

This module is an interface between the algebraic and set-theoretic properties of composing self-maps. The basic type class of this module is CompSemigroup. A type F can instance CompSemigroup whenever F consists of bundled functions and composing elements of F agrees with composing the unbundled functions. For example, the type F := V →ₗ[R] V of R-linear endomorphisms of a vector space V can instance CompSemigroup because LinearMap.comp merely composes the unbundled linear maps.

My phrasing feels sorta tortured, so please let me know if you have a better description. Also, I put the definitions in the new file Mathlib/Dynamics/Algebra.lean, please let me know if you think they should go elsewhere.

[Eric Wieser]

I would guess that it becomes quite annoying switching back and forth between CompMonoid.comp and MonoidHom.comp, and similarly for id.

[Eric Wieser]

One solution to that is to make comp and id outParams, though that might bring other challenges

[Eric Wieser]

Another would be to characterize it as (f * g) x = f (g x) without reference to comp : F -> F -> F at all

[Yaël Dillies]

If I may, I should warn you that this sort of change is hugely distracting. Here you have a nice end result which doesn't seem to need any "composition monoid"; where do you use them?

[Eric Wieser]

(Yael is an expert in being hugely distracted)

[Michael Lane]

Here you have a nice end result which doesn't seem to need any "composition monoid"; where do you use them?

One of the inputs of the Markov-Kakutani theorem is a commuting collection of continuous affine maps. WLOG, we may assume instead that we have a commuting monoid of continuous affine maps, hence CompMonoid.

It is very common in dynamics to assume that you have a commuting collection/semigroup/monoid/group/whatever of transformations. One reason for this assumption is that the fixed points of a transformation are invariant under another transformation, if the two transformations commute (docs#Function.Semiconj.mapsTo_fixedPoints). This fact is used in the proof of Markov-Kakutani.

So in general, say we had a different type of bundled functions (smooth, Lipschitz, linear, ....). For every such type, we would need a theorem matching the following blueprint:

theorem jointFixedPoints_of_commuting
-- inputs: some bundled functions and a proof that they commute
: -- Prop : The intersection of all fixedPoints is invariant under every function

The proof of every such theorem would basically be the same: Coerce to functions and apply docs#Set.mapsTo_iInter_iInter, docs#Function.Semiconj.mapsTo_fixedPoints, and CompSemigroup.function_commute_iff_commute (or rather, its proof). CompSemigroup can do all these at once:

def jointFixedPoints
(F : Type*) {X : Type*} [FunLike F X X] :=
  ⋂ f : F, Function.fixedPoints f

theorem jointFixedPoints_of_commuting
{F X : Type*} [FunLike F X X] [CompSemigroup F X] [IsMulCommutative F] (f : F)
: Set.MapsTo f (jointFixedPoints F) (jointFixedPoints F) := by
  apply Set.mapsTo_iInter_iInter
  intro g
  refine Function.Semiconj.mapsTo_fixedPoints ?_
  refine (CompSemigroup.function_commute_iff_commute f g).mpr ?_
  exact IsMulCommutative.is_comm.comm f g

[Michael Lane]

I would guess that it becomes quite annoying switching back and forth between CompMonoid.comp and MonoidHom.comp, and similarly for id.

I haven't encountered this difficulty yet, although I've only applied CompSemigroup to the Markov-Kakutani proof.