Mathlib.Algebra.GroupWithZero.Action.Units

Module docstring

{"# 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.

Let $G_0$ be a group with zero, $\alpha$ a type with a scalar multiplication action by $G_0$, and $g \in G_0$ a nonzero element. Then the scalar multiplication of $a \in \alpha$ by the unit $\text{mk0}(g, hg)$ (where $hg$ is a proof that $g \neq 0$) is equal to the scalar multiplication of $a$ by $g$ itself, i.e., $\text{mk0}(g, hg) \cdot a = g \cdot a$.

inv_smul_smul₀ theorem

(ha : a ≠ 0) (x : β) : a⁻¹ • a • x = x

Full source

@[simp] lemma inv_smul_smul₀ (ha : a ≠ 0) (x : β) : a⁻¹ • a • x = x :=
  inv_smul_smul (Units.mk0 a ha) x

Inverse Action Cancellation in Groups with Zero: $a^{-1} \cdot (a \cdot x) = x$

Informal description

For any nonzero element $a$ in a group with zero $G_0$ acting on a type $\beta$, and any element $x \in \beta$, the action of the inverse $a^{-1}$ followed by the action of $a$ on $x$ returns $x$, i.e., $a^{-1} \cdot (a \cdot x) = x$.

smul_inv_smul₀ theorem

(ha : a ≠ 0) (x : β) : a • a⁻¹ • x = x

Full source

@[simp]
lemma smul_inv_smul₀ (ha : a ≠ 0) (x : β) : a • a⁻¹ • x = x := smul_inv_smul (Units.mk0 a ha) x

Inverse Action Cancellation in Groups with Zero: $a \cdot (a^{-1} \cdot x) = x$

Informal description

For any nonzero element $a$ in a group with zero $G_0$ acting on a type $\beta$, and any element $x \in \beta$, the action of $a$ followed by the action of its inverse $a^{-1}$ on $x$ returns $x$, i.e., $a \cdot (a^{-1} \cdot x) = x$.

inv_smul_eq_iff₀ theorem

(ha : a ≠ 0) {x y : β} : a⁻¹ • x = y ↔ x = a • y

Full source

lemma inv_smul_eq_iff₀ (ha : a ≠ 0) {x y : β} : a⁻¹a⁻¹ • x = y ↔ x = a • y :=
  inv_smul_eq_iff (g := Units.mk0 a ha)

Inverse Action Equivalence in Groups with Zero: $a^{-1} \cdot x = y \leftrightarrow x = a \cdot y$

Informal description

For any nonzero element $a$ in a group with zero $G_0$ acting on a type $\beta$, and any elements $x, y \in \beta$, the action of the inverse $a^{-1}$ on $x$ equals $y$ if and only if $x$ equals the action of $a$ on $y$, i.e., $a^{-1} \cdot x = y \leftrightarrow x = a \cdot y$.

Commute.smul_right_iff₀ theorem

 [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β} (ha : a ≠ 0) : Commute x (a • y) ↔ Commute x y

Full source

@[simp]
lemma Commute.smul_right_iff₀ [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β}
    (ha : a ≠ 0) : CommuteCommute x (a • y) ↔ Commute x y := Commute.smul_right_iff (g := Units.mk0 a ha)

Scalar Multiplication Preserves Commutativity for Nonzero Scalars: $x \cdot (a \cdot y) = (a \cdot y) \cdot x \leftrightarrow x \cdot y = y \cdot x$

Informal description

Let $\alpha$ be a group with zero, $\beta$ be a multiplicative structure, and assume that the scalar multiplication actions of $\alpha$ and $\beta$ on $\beta$ commute and form a scalar tower. For any nonzero element $a \in \alpha$ and elements $x, y \in \beta$, the elements $x$ and $a \cdot y$ commute if and only if $x$ and $y$ commute, i.e., $x * (a \cdot y) = (a \cdot y) * x \leftrightarrow x * y = y * x$.

Commute.smul_left_iff₀ theorem

 [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β} (ha : a ≠ 0) : Commute (a • x) y ↔ Commute x y

Full source

@[simp]
lemma Commute.smul_left_iff₀ [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β}
    (ha : a ≠ 0) : CommuteCommute (a • x) y ↔ Commute x y := Commute.smul_left_iff (g := Units.mk0 a ha)

Scalar Multiplication Preserves Commutativity for Nonzero Scalars: $(a \cdot x) \cdot y = y \cdot (a \cdot x) \leftrightarrow x \cdot y = y \cdot x$

Informal description

Let $\alpha$ be a group with zero, $\beta$ be a multiplicative structure, and assume that the scalar multiplication actions of $\alpha$ and $\beta$ on $\beta$ commute and form a scalar tower. For any nonzero element $a \in \alpha$ and elements $x, y \in \beta$, the elements $a \cdot x$ and $y$ commute if and only if $x$ and $y$ commute, i.e., $(a \cdot x) * y = y * (a \cdot x) \leftrightarrow x * y = y * x$.

Equiv.smulRight definition

(ha : a ≠ 0) : β ≃ β

Full source

/-- Right scalar multiplication as an order isomorphism. -/
@[simps] def Equiv.smulRight (ha : a ≠ 0) : β ≃ β where
  toFun b := a • b
  invFun b := a⁻¹ • b
  left_inv := inv_smul_smul₀ ha
  right_inv := smul_inv_smul₀ ha

Right scalar multiplication bijection for nonzero elements

Informal description

Given a nonzero element $a$ in a group with zero $G_0$ acting on a type $\beta$, the function $b \mapsto a \cdot b$ is a bijection from $\beta$ to itself, with inverse given by $b \mapsto a^{-1} \cdot b$.

Units.instSMulZeroClass instance

[Monoid M] [Zero α] [SMulZeroClass M α] : SMulZeroClass Mˣ α

Full source

instance instSMulZeroClass [Monoid M] [Zero α] [SMulZeroClass M α] : SMulZeroClass Mˣ α where
  smul := (· • ·)
  smul_zero m := smul_zero (m : M)

Zero-Preserving Scalar Multiplication Action by Units of a Monoid

Informal description

For any monoid $M$ and any type $\alpha$ with a zero element and a scalar multiplication action by $M$ that preserves zero, the group of units $M^\times$ of $M$ also acts on $\alpha$ via scalar multiplication that preserves zero. Specifically, for any unit $m \in M^\times$ and any $a \in \alpha$, the action satisfies $m \cdot 0 = 0$.

Units.instDistribSMulUnits instance

[Monoid M] [AddZeroClass α] [DistribSMul M α] : DistribSMul Mˣ α

Full source

instance instDistribSMulUnits [Monoid M] [AddZeroClass α] [DistribSMul M α] :
    DistribSMul Mˣ α where smul_add m := smul_add (m : M)

Distributive Scalar Multiplication by Units of a Monoid

Informal description

For any monoid $M$ and any additive monoid $\alpha$ with a distributive scalar multiplication action by $M$, the group of units $M^\times$ of $M$ also acts distributively on $\alpha$. This means that for any unit $m \in M^\times$ and any elements $a, b \in \alpha$, the action satisfies $m \cdot (a + b) = m \cdot a + m \cdot b$ and $m \cdot 0 = 0$.

Units.instDistribMulAction instance

[Monoid M] [AddMonoid α] [DistribMulAction M α] : DistribMulAction Mˣ α

Full source

instance instDistribMulAction [Monoid M] [AddMonoid α] [DistribMulAction M α] :
    DistribMulAction Mˣ α where
  __ := instDistribSMulUnits
  one_smul := fun b => one_smul M b
  mul_smul := fun x y b => mul_smul (x : M) y b

Distributive Multiplicative Action of Units on an Additive Monoid

Informal description

For any monoid $M$ and any additive monoid $\alpha$ with a distributive multiplicative action by $M$, the group of units $M^\times$ of $M$ also has a distributive multiplicative action on $\alpha$. This means that for any unit $u \in M^\times$ and any elements $a, b \in \alpha$, the action satisfies $u \cdot (a + b) = u \cdot a + u \cdot b$ and $u \cdot 0 = 0$.

Units.instMulDistribMulAction instance

[Monoid M] [Monoid α] [MulDistribMulAction M α] : MulDistribMulAction Mˣ α

Full source

instance instMulDistribMulAction [Monoid M] [Monoid α] [MulDistribMulAction M α] :
    MulDistribMulAction Mˣ α where
  smul_mul m := smul_mul' (m : M)
  smul_one m := smul_one (m : M)

Multiplicative Distributive Action of Units on a Monoid

Informal description

For any monoid $M$ and any monoid $\alpha$ with a multiplicative distributive action by $M$, the group of units $M^\times$ of $M$ also has a multiplicative distributive action on $\alpha$. This means that for any unit $u \in M^\times$ and any elements $a, b \in \alpha$, the action satisfies $u \cdot (a * b) = (u \cdot a) * (u \cdot b)$.

Units.mulDistribMulAction' instance

[Group G] [Monoid M] [MulDistribMulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] : MulDistribMulAction G Mˣ

Full source

/-- A stronger form of `Units.mul_action'`. -/
instance mulDistribMulAction' [Group G] [Monoid M] [MulDistribMulAction G M] [SMulCommClass G M M]
    [IsScalarTower G M M] : MulDistribMulAction G Mˣ :=
  { Units.mulAction' with
    smul := (· • ·),
    smul_one := fun _ => Units.ext <| smul_one _,
    smul_mul := fun _ _ _ => Units.ext <| smul_mul' _ _ _ }

Multiplicative Distributive Action of a Group on Units of a Monoid

Informal description

For any group $G$ and monoid $M$ with a multiplicative distributive action of $G$ on $M$ that commutes with multiplication and satisfies the scalar tower property, there is an induced multiplicative distributive action of $G$ on the group of units $M^\times$ of $M$. More precisely, if $G$ acts on $M$ such that for all $g \in G$ and $m_1, m_2 \in M$ we have $g \cdot (m_1 * m_2) = (g \cdot m_1) * (g \cdot m_2)$, and this action satisfies the compatibility conditions $g \cdot (h \cdot m) = h \cdot (g \cdot m)$ and $g \cdot (h \cdot m) = (g \cdot h) \cdot m$ for all $g, h \in G$ and $m \in M$, then $G$ also acts multiplicatively and distributively on $M^\times$ via the same action.

IsUnit.smul_eq_zero theorem

(hu : IsUnit u) : u • x = 0 ↔ x = 0

Full source

@[simp] lemma IsUnit.smul_eq_zero (hu : IsUnit u) : u • x = 0 ↔ x = 0 := smul_eq_zero_iff_eq hu.unit

Scalar Multiplication by a Unit Annihilates Zero if and only if Element is Zero

Informal description

For any element $u$ in a monoid $M$ that is a unit (i.e., invertible), and any element $x$ in an additive monoid $\alpha$ with a distributive multiplicative action by $M$, the scalar multiplication satisfies $u \cdot x = 0$ if and only if $x = 0$.

See also