Theorems · Definition · group theory

Units.mulDistribMulActionRight

{M : Type u_6} →
  {N : Type u_7} → [inst : Monoid M] → [inst_1 : Monoid N] → [MulDistribMulAction M N] → MulDistribMulAction M Nˣ

Note this has different defeqs than Units.mulAction', but doesn't create a diamond with it in non-degenerate situations. Indeed, to get a diamond on MulDistribMulAction G Mˣ, we would need both instances to fire. But Units.mulAction' assumes SMulCommClass G M M, i.e. ∀ (g : G) (m₁ m₂ : M), g • (m₁ * m₂) = m₁ * g • m₂), while Units.instMulDistribMulActionRight assumes MulDistribMulAction G M, i.e. ∀ (g : G) (m₁ m₂ : M), g • (m₁ * m₂) = g • m₁ * g • m₂. In particular, if M is cancellative, then we obtain ∀ (g : G) (m : M), g • m = m, i.e. the action is trivial! This however does create a (propeq) diamond for MulDistribMulAction (ConjAct Mˣ) Mˣ with ConjAct.unitsMulDistribMulAction and ConjAct.instMulDistribMulAction. Indeed, if we go down one way then u • v := ⟨ofConjAct u * v * ofConjAct u⁻¹, ofConjAct u * v⁻¹ * ofConjAct u⁻¹, _, _⟩, while the other way is u • v := ⟨ofConjAct u * v * ofConjAct u⁻¹, ofConjAct u * (v⁻¹ * ofConjAct u⁻¹), _, _⟩.

Defined in

Mathlib.Algebra.Group.Action.Units

Cited by

2 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

MonoidMonoidMulDistribMulAction