Multiplicative actions with zero on and by Mˣ

This file provides the multiplicative actions with zero of a unit on a type α, SMul Mˣ α, in the presence of SMulWithZero M α, with the obvious definition stated in Units.smul_def.

Additionally, a MulDistribMulAction G M for some group G satisfying some additional properties admits a MulDistribMulAction G Mˣ structure, again with the obvious definition stated in Units.coe_smul. This instance uses a primed name.

Implementation notes

We previously had

instance mulDistribMulAction' [Group G] [Monoid M] [MulDistribMulAction G M] [SMulCommClass G M M]
  [IsScalarTower G M M] : MulDistribMulAction G Mˣ

as a strengthening of Units.mulAction', but in fact this instance (almost) never applies! MulDistribMulAction G M means ∀ (g : G) (m₁ m₂ : M), g • (m₁ * m₂) = g • m₁ * g • m₂, while SMulCommClass G M M means ∀ (g : G) (m₁ m₂ : M), g • (m₁ * m₂) = 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!

See also

• Algebra.GroupWithZero.Action.Opposite
• Algebra.GroupWithZero.Action.Pi
• Algebra.GroupWithZero.Action.Prod

@[simp]

theorem Units.smul_mk0 {G₀ : Type u_1} [GroupWithZero G₀] {α : Type u_6} [SMul G₀ α] {g : G₀} (hg : g ≠ 0) (a : α) : mk0 g hg • a = g • a

@[simp]

theorem inv_smul_smul₀ {α : Type u_4} {β : Type u_5} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (x : β) : a⁻¹ • a • x = x

@[simp]

theorem smul_inv_smul₀ {α : Type u_4} {β : Type u_5} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (x : β) : a • a⁻¹ • x = x

theorem inv_smul_eq_iff₀ {α : Type u_4} {β : Type u_5} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) {x y : β} : a⁻¹ • x = y ↔ x = a • y

theorem eq_inv_smul_iff₀ {α : Type u_4} {β : Type u_5} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) {x y : β} : x = a⁻¹ • y ↔ a • x = y

@[simp]

theorem Commute.smul_right_iff₀ {α : Type u_4} {β : Type u_5} [GroupWithZero α] [MulAction α β] {a : α} [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β} (ha : a ≠ 0) : Commute x (a • y) ↔ Commute x y

@[simp]

theorem Commute.smul_left_iff₀ {α : Type u_4} {β : Type u_5} [GroupWithZero α] [MulAction α β] {a : α} [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β} (ha : a ≠ 0) : Commute (a • x) y ↔ Commute x y

def Equiv.smulRight {α : Type u_4} {β : Type u_5} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) : β ≃ β

Right scalar multiplication as an order isomorphism.

Equations

• Equiv.smulRight ha = { toFun := fun (b : β) => a • b, invFun := fun (b : β) => a⁻¹ • b, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.smulRight_symm_apply {α : Type u_4} {β : Type u_5} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (b : β) : (smulRight ha).symm b = a⁻¹ • b

@[simp]

theorem Equiv.smulRight_apply {α : Type u_4} {β : Type u_5} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (b : β) : (smulRight ha) b = a • b

Action of the units of M on a type α

instance Units.instSMulZeroClass {M : Type u_3} {α : Type u_4} [Monoid M] [Zero α] [SMulZeroClass M α] : SMulZeroClass Mˣ α

Equations

• Units.instSMulZeroClass = { toSMul := Units.instSMul, smul_zero := ⋯ }

instance Units.instDistribSMulUnits {M : Type u_3} {α : Type u_4} [Monoid M] [AddZeroClass α] [DistribSMul M α] : DistribSMul Mˣ α

Equations

• Units.instDistribSMulUnits = { toSMulZeroClass := Units.instSMulZeroClass, smul_add := ⋯ }

instance Units.instDistribMulAction {M : Type u_3} {α : Type u_4} [Monoid M] [AddMonoid α] [DistribMulAction M α] : DistribMulAction Mˣ α

Equations

• Units.instDistribMulAction = { toSMul := Units.instDistribSMulUnits.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

instance Units.instMulDistribMulAction {M : Type u_3} {α : Type u_4} [Monoid M] [Monoid α] [MulDistribMulAction M α] : MulDistribMulAction Mˣ α

Equations

• Units.instMulDistribMulAction = { toMulAction := Units.instMulAction, smul_mul := ⋯, smul_one := ⋯ }

@[simp]

theorem IsUnit.smul_eq_zero {G : Type u_2} {M : Type u_3} [Monoid G] [AddMonoid M] [DistribMulAction G M] {u : G} {x : M} (hu : IsUnit u) : u • x = 0 ↔ x = 0