Coordinates of mulAutArrow #
Mathlib's mulAutArrow lets a group G acting on A act on A → M by multiplicative
automorphisms. This file records that action's evaluation formula in plain coordinates, supporting
coordinate calculations in semidirect products built from mulAutArrow, particularly
arbitrary-action permutation wreath products.
Main results #
TauCeti.mulAutArrow_apply_apply_eq_apply_inv_smul:mulAutArrow g f a = f (g⁻¹ • a).
@[simp]
theorem
TauCeti.mulAutArrow_apply_apply_eq_apply_inv_smul
{G : Type u_1}
{M : Type u_2}
{A : Type u_3}
[Group G]
[MulAction G A]
[Monoid M]
(g : G)
(f : A → M)
(a : A)
:
The automorphism mulAutArrow g of A → M evaluates coordinates through g⁻¹:
mulAutArrow g f a = f (g⁻¹ • a).