Trivial actions

A trivial action of G on R, g • m = m for all g and m, given as a hypothesis rather than as an instance: this is how the trivial coefficient modules of group cohomology are handled, where the action of G on a ring of coefficients is a parameter and its triviality a hypothesis (TauCeti.cohomFpAddEquivH1).

When a construction demands an action as an instance and the ambient theory has none, the trivial action of a monoid G on a monoid M by monoid endomorphisms is supplied by TauCeti.trivialMulDistribMulAction, deliberately not an instance: it is installed locally where it is needed, as in the theory of projective representations and for central extensions such as 1 → ℤ/2 → ℤ/4 → ℤ/2 → 1.

Main results

• TauCeti.smul_mul_smul_of_smul_eq_self: for a trivial action on a multiplicative structure, multiplication is equivariant, g • m * g • n = g • (m * n).
• TauCeti.trivialMulDistribMulAction: the trivial action of a monoid on a monoid by monoid endomorphisms, with TauCeti.trivialMulDistribMulAction_smul: under it every element is fixed.

theorem TauCeti.smul_mul_smul_of_smul_eq_self {G : Type u_1} {R : Type u_2} [Mul R] [SMul G R] (htriv : ∀ (g : G) (m : R), g • m = m) (g : G) (m n : R) : g • m * g • n = g • (m * n)

For a trivial action of G on a multiplicative structure, multiplication is equivariant.

@[reducible, inline]

abbrev TauCeti.trivialMulDistribMulAction (G : Type u_3) (M : Type u_4) [Monoid G] [Monoid M] : MulDistribMulAction G M

The trivial action of a monoid G on a monoid M, g • a = a, obtained by composing the tautological action of MulAut M with the trivial homomorphism. It is the action for which the extension built from a factor set is central, so it is the one a projective representation's factor set is bundled over in TauCeti.IsProjectiveRep.exists_factorSet_linearization. It is reducible and deliberately not an instance, since the theory of factor sets is stated for an arbitrary action; it is only used to supply one where the ambient theory has none.

Equations

• TauCeti.trivialMulDistribMulAction G M = MulDistribMulAction.compHom M 1

@[simp]

theorem TauCeti.trivialMulDistribMulAction_smul {G : Type u_3} {M : Type u_4} [Monoid G] [Monoid M] (g : G) (a : M) : g • a = a

Under TauCeti.trivialMulDistribMulAction every element is fixed. This is the triviality hypothesis that TauCeti.FactorSet.isFactorSet_curry, TauCeti.IsFactorSet.toFactorSet and TauCeti.FactorSet.inl_range_le_center take, supplied once so that their callers can name a constant rather than an inlined proof.