The trivial action of a monoid on ZMod n

The trivial action g • m = m of a monoid F on ZMod n, as a DistribMulAction. It is the coefficient action that a statement about the cohomology of trivial ZMod n-coefficients installs locally when no action of F appears in its conclusion; the statements of TauCeti.Topology.Algebra.Group.Profinite.ProP.Relation.Rank that carry an action of F on ZMod n as an instance together with the hypothesis that it is trivial then apply to it.

Main definitions

• TauCeti.trivialZModAction: the trivial action of a monoid on ZMod n.

@[reducible, inline]

abbrev TauCeti.trivialZModAction (n : ℕ) (F : Type u_1) [Monoid F] : DistribMulAction F (ZMod n)

The trivial action g • m = m of a monoid F on ZMod n. It is the coefficient action of a statement about the cohomology of trivial ZMod n-coefficients whose conclusion mentions no action of F.

Equations

• TauCeti.trivialZModAction n F = { smul := fun (x : F) (m : ZMod n) => m, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }