Commit 2024-04-05 00:53 8b50609c

feat: MulActionHom in the semilinear style (#6057) Generalize MulActionHom so that it allows two different monoids acting, related by a morphism. This is inspired by the treatment of (semi)linear maps in mathlib, and allows to refactor them. Let M, N, X, Y be types, with SMul M X and SMul N Y, and let φ : M → N be a map.

• MulActionHom φ X Y, the type of equivariant functions from X to Y, consists of functions f : X → Y such that f (m • x) = (φ m) • (f x) for all m : M and x : X. Assume that we have Monoid M, Monoid N and that φ : M →* N. For A, B by types with AddMonoid A and AddMonoid B, endowed with DistribMulAction M A and DistribMulAction M B:
• DistribMulActionHom φ A B is the type of equivariant additive monoid homomorphisms from A to B. Similarly, when R and S are types with Semiring R, Semiring S, MulSemiringAction M R and MulSemiringAction N S
• SMulSemiringHom φ R S is the type of equivariant ring homomorphisms from R to S. The above types have corresponding classes:
• MulActionHomClass F φ X Y states that F is a type of bundled X → Y homs which are φ-equivariant
• DistribMulActionHomClass F φ A B states that F is a type of bundled A → B homs preserving the additive monoid structure and φ-equivariant
• SMulSemiringHomClass F φ R S states that F is a type of bundled R → S homs preserving the ring structure and φ-equivariant

Notation

We introduce the following notation to code equivariant maps (the subscript index ₑ is for equivariant) :

• X →ₑ[φ] Y is MulActionHom φ X Y.
• A →ₑ+[φ] B is DistribMulActionHom φ A B.
• R →ₑ+*[φ] S is MulSemiringActionHom φ R S. When M = N and φ = MonoidHom.id M, we provide the backward compatible notation :
• X →[M] Y is MulActionHom (@id M) X Y
• A →+[M] B is DistribMulActionHom (MonoidHom.id M) A B
• R →+*[M] S is MulSemiringActionHom (MonoidHom.id M) R S This more general definition is propagated all over mathlib, in particular to LinearMap. The treatment of composition of equivariant maps is inspired by that of semilinear maps. We provide classes CompTriple and MonoidHom.CompTriple of “composable triples`, and various instances for them.