Mathlib.Algebra.GroupWithZero.Action.Defs

SMulZeroClass structure

(M A : Type*) [Zero A] extends SMul M A

Full source

/-- Typeclass for scalar multiplication that preserves `0` on the right. -/
class SMulZeroClass (M A : Type*) [Zero A] extends SMul M A where
  /-- Multiplying `0` by a scalar gives `0` -/
  smul_zero : ∀ a : M, a • (0 : A) = 0

Scalar multiplication preserving zero

Informal description

The structure `SMulZeroClass` represents a scalar multiplication operation `•` between types `M` and `A`, where `A` has a zero element `0`, such that the scalar multiplication preserves zero on the right, i.e., for any `a : M`, we have `a • (0 : A) = 0`.

smul_zero theorem

(a : M) : a • (0 : A) = 0

Full source

@[simp]
theorem smul_zero (a : M) : a • (0 : A) = 0 :=
  SMulZeroClass.smul_zero _

Scalar multiplication annihilates zero

Informal description

For any element $a$ of type $M$ and any zero element $0$ of type $A$, the scalar multiplication satisfies $a \cdot 0 = 0$.

smul_ite_zero theorem

(p : Prop) [Decidable p] (a : M) (b : A) : (a • if p then b else 0) = if p then a • b else 0

Full source

lemma smul_ite_zero (p : Prop) [Decidable p] (a : M) (b : A) :
    (a • if p then b else 0) = if p then a • b else 0 := by split_ifs <;> simp

Scalar Multiplication Distributes Over Conditional Zero

Informal description

For any proposition $p$ (with a decidability instance), any element $a$ of type $M$, and any element $b$ of type $A$, the scalar multiplication satisfies: \[ a \cdot (\text{if } p \text{ then } b \text{ else } 0) = \text{if } p \text{ then } a \cdot b \text{ else } 0 \]

smul_eq_zero_of_right theorem

(a : M) {b : A} (h : b = 0) : a • b = 0

Full source

lemma smul_eq_zero_of_right (a : M) {b : A} (h : b = 0) : a • b = 0 := h.symm ▸ smul_zero a

Scalar Multiplication of Zero Yields Zero

Informal description

For any element $a$ of type $M$ and any element $b$ of type $A$ such that $b = 0$, the scalar multiplication satisfies $a \cdot b = 0$.

right_ne_zero_of_smul theorem

{a : M} {b : A} : a • b ≠ 0 → b ≠ 0

Full source

lemma right_ne_zero_of_smul {a : M} {b : A} : a • b ≠ 0 → b ≠ 0 := mt <| smul_eq_zero_of_right a

Nonzero Scalar Product Implies Nonzero Operand

Informal description

For any elements $a \in M$ and $b \in A$, if the scalar multiplication $a \cdot b$ is nonzero, then $b$ is nonzero.

Function.Injective.smulZeroClass abbrev

 [Zero B] [SMul M B] (f : ZeroHom B A) (hf : Injective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) :
  SMulZeroClass M B

Full source

/-- Pullback a zero-preserving scalar multiplication along an injective zero-preserving map.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.smulZeroClass [Zero B] [SMul M B] (f : ZeroHom B A)
    (hf : Injective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) :
    SMulZeroClass M B where
  smul := (· • ·)
  smul_zero c := hf <| by simp only [smul, map_zero, smul_zero]

Pullback of Zero-Preserving Scalar Multiplication via Injective Zero Homomorphism

Informal description

Let $M$ and $A$ be types, where $A$ has a zero element, and let $B$ be another type with a zero element and a scalar multiplication operation $\bullet \colon M \times B \to B$. Given an injective zero-preserving homomorphism $f \colon B \to A$ such that for all $c \in M$ and $x \in B$, $f(c \bullet x) = c \bullet f(x)$, then the scalar multiplication on $B$ preserves zero, i.e., $c \bullet 0 = 0$ for all $c \in M$.

ZeroHom.smulZeroClass abbrev

[Zero B] [SMul M B] (f : ZeroHom A B) (smul : ∀ (c : M) (x), f (c • x) = c • f x) : SMulZeroClass M B

Full source

/-- Pushforward a zero-preserving scalar multiplication along a zero-preserving map.
See note [reducible non-instances]. -/
protected abbrev ZeroHom.smulZeroClass [Zero B] [SMul M B] (f : ZeroHom A B)
    (smul : ∀ (c : M) (x), f (c • x) = c • f x) :
    SMulZeroClass M B where
  -- Porting note: `simp` no longer works here.
  smul_zero c := by rw [← map_zero f, ← smul, smul_zero]

Pushforward of Zero-Preserving Scalar Multiplication via Zero Homomorphism

Informal description

Given a zero-preserving homomorphism $f \colon A \to B$ between types with zero elements, and a scalar multiplication operation $\bullet \colon M \times A \to A$ that preserves zero, if for all $c \in M$ and $x \in A$ we have $f(c \bullet x) = c \bullet f(x)$, then $M$ also acts on $B$ via a zero-preserving scalar multiplication defined by $c \bullet b := f(c \bullet f^{-1}(b))$ (where $f^{-1}$ is any preimage under $f$).

Function.Surjective.smulZeroClassLeft abbrev

 {R S M : Type*} [Zero M] [SMulZeroClass R M] [SMul S M] (f : R → S) (hf : Function.Surjective f)
  (hsmul : ∀ (c) (x : M), f c • x = c • x) : SMulZeroClass S M

Full source

/-- Push forward the multiplication of `R` on `M` along a compatible surjective map `f : R → S`.

See also `Function.Surjective.distribMulActionLeft`.
-/
abbrev Function.Surjective.smulZeroClassLeft {R S M : Type*} [Zero M] [SMulZeroClass R M]
    [SMul S M] (f : R → S) (hf : Function.Surjective f)
    (hsmul : ∀ (c) (x : M), f c • x = c • x) :
    SMulZeroClass S M where
  smul := (· • ·)
  smul_zero := hf.forall.mpr fun c => by rw [hsmul, smul_zero]

Pushforward of Zero-Preserving Scalar Multiplication via Surjective Map

Informal description

Let $R$, $S$, and $M$ be types, where $M$ has a zero element and is equipped with a scalar multiplication operation $\bullet$ from $R$ to $M$ that preserves zero. Given a surjective function $f : R \to S$ and a scalar multiplication operation $\bullet$ from $S$ to $M$ such that for all $c \in R$ and $x \in M$, $f(c) \bullet x = c \bullet x$, then $S$ also acts on $M$ via a zero-preserving scalar multiplication.

SMulZeroClass.compFun abbrev

(f : N → M) : SMulZeroClass N A

Full source

/-- Compose a `SMulZeroClass` with a function, with scalar multiplication `f r' • m`.
See note [reducible non-instances]. -/
abbrev SMulZeroClass.compFun (f : N → M) :
    SMulZeroClass N A where
  smul := SMul.comp.smul f
  smul_zero x := smul_zero (f x)

Composition of Zero-Preserving Scalar Multiplication via a Function

Informal description

Given a scalar multiplication operation `•` between types `M` and `A` that preserves zero (i.e., `a • (0 : A) = 0` for any `a : M`), and a function `f : N → M`, we can define a new scalar multiplication operation between `N` and `A` by composition, where `n • a := f(n) • a`. This operation also preserves zero.

SMulZeroClass.toZeroHom definition

(x : M) : ZeroHom A A

Full source

/-- Each element of the scalars defines a zero-preserving map. -/
@[simps]
def SMulZeroClass.toZeroHom (x : M) :
    ZeroHom A A where
  toFun := (x • ·)
  map_zero' := smul_zero x

Zero-preserving homomorphism induced by scalar multiplication

Informal description

For any element $ x $ of the scalar type $ M $, the function $ a \mapsto x \bullet a $ is a zero-preserving homomorphism from $ A $ to $ A $, where $ \bullet $ denotes the scalar multiplication operation.

SMulWithZero structure

[Zero M₀] [Zero A] extends SMulZeroClass M₀ A

Full source

/-- `SMulWithZero` is a class consisting of a Type `M₀` with `0 ∈ M₀` and a scalar multiplication
of `M₀` on a Type `A` with `0`, such that the equality `r • m = 0` holds if at least one among `r`
or `m` equals `0`. -/
class SMulWithZero [Zero M₀] [Zero A] extends SMulZeroClass M₀ A where
  /-- Scalar multiplication by the scalar `0` is `0`. -/
  zero_smul : ∀ m : A, (0 : M₀) • m = 0

Scalar Multiplication with Zero

Informal description

The structure `SMulWithZero` consists of a type `M₀` with a zero element and a scalar multiplication operation of `M₀` on a type `A` with a zero element, such that the equality `r • m = 0` holds if at least one of `r` or `m` is zero.

MulZeroClass.toSMulWithZero instance

[MulZeroClass M₀] : SMulWithZero M₀ M₀

Full source

instance MulZeroClass.toSMulWithZero [MulZeroClass M₀] : SMulWithZero M₀ M₀ where
  smul := (· * ·)
  smul_zero := mul_zero
  zero_smul := zero_mul

Scalar Multiplication with Zero from MulZeroClass

Informal description

For any type $M₀$ with a multiplication operation and a zero element satisfying $0 \cdot a = 0$ and $a \cdot 0 = 0$ for all $a \in M₀$, there is a scalar multiplication operation of $M₀$ on itself that preserves zero.

MulZeroClass.toOppositeSMulWithZero instance

[MulZeroClass M₀] : SMulWithZero M₀ᵐᵒᵖ M₀

Full source

/-- Like `MulZeroClass.toSMulWithZero`, but multiplies on the right. -/
instance MulZeroClass.toOppositeSMulWithZero [MulZeroClass M₀] : SMulWithZero M₀ᵐᵒᵖ M₀ where
  smul := (· • ·)
  smul_zero _ := zero_mul _
  zero_smul := mul_zero

Scalar Multiplication with Zero via Opposite from MulZeroClass

Informal description

For any type $M₀$ with a multiplication operation and a zero element satisfying $0 \cdot a = 0$ and $a \cdot 0 = 0$ for all $a \in M₀$, there is a scalar multiplication operation of the multiplicative opposite $M₀^\text{op}$ on $M₀$ that preserves zero.

zero_smul theorem

(m : A) : (0 : M₀) • m = 0

Full source

@[simp]
theorem zero_smul (m : A) : (0 : M₀) • m = 0 :=
  SMulWithZero.zero_smul m

Zero Scalar Multiplication Yields Zero: $0 \cdot m = 0$

Informal description

For any element $m$ in an additive monoid $A$ with a zero element, and for the zero element $0$ in a type $M₀$ with a zero element, the scalar multiplication of $0$ and $m$ equals the zero element of $A$, i.e., $0 \cdot m = 0$.

smul_eq_zero_of_left theorem

(h : a = 0) (b : A) : a • b = 0

Full source

lemma smul_eq_zero_of_left (h : a = 0) (b : A) : a • b = 0 := h.symm ▸ zero_smul _ b

Zero scalar yields zero multiplication: $a = 0 \implies a \bullet b = 0$

Informal description

For any element $b$ in an additive monoid $A$ and any scalar $a$ in a type $M₀$ with a zero element, if $a = 0$, then the scalar multiplication $a \bullet b$ equals the zero element of $A$, i.e., $a \bullet b = 0$.

left_ne_zero_of_smul theorem

: a • b ≠ 0 → a ≠ 0

Full source

lemma left_ne_zero_of_smul : a • b ≠ 0 → a ≠ 0 := mt fun h ↦ smul_eq_zero_of_left h b

Nonzero Scalar Multiplication Implies Nonzero Scalar: $a \bullet b \neq 0 \implies a \neq 0$

Informal description

For any scalar $a$ in a type $M₀$ and any element $b$ in an additive monoid $A$, if the scalar multiplication $a \bullet b$ is not equal to zero, then $a$ is not equal to zero.

Function.Injective.smulWithZero abbrev

(f : ZeroHom A' A) (hf : Injective f) (smul : ∀ (a : M₀) (b), f (a • b) = a • f b) : SMulWithZero M₀ A'

Full source

/-- Pullback a `SMulWithZero` structure along an injective zero-preserving homomorphism. -/
-- See note [reducible non-instances]
protected abbrev Function.Injective.smulWithZero (f : ZeroHom A' A) (hf : Injective f)
    (smul : ∀ (a : M₀) (b), f (a • b) = a • f b) : SMulWithZero M₀ A' where
  smul := (· • ·)
  zero_smul a := hf <| by simp [smul]
  smul_zero a := hf <| by simp [smul]

Pullback of Scalar Multiplication with Zero Along Injective Zero-Preserving Homomorphism

Informal description

Given an injective zero-preserving homomorphism $f \colon A' \to A$ between types with zero elements, and a scalar multiplication operation $\bullet \colon M_0 \times A \to A$ that satisfies $f(a \bullet b) = a \bullet f(b)$ for all $a \in M_0$ and $b \in A'$, the type $A'$ inherits a scalar multiplication with zero structure from $A$ via $f$.

Function.Surjective.smulWithZero abbrev

(f : ZeroHom A A') (hf : Surjective f) (smul : ∀ (a : M₀) (b), f (a • b) = a • f b) : SMulWithZero M₀ A'

Full source

/-- Pushforward a `SMulWithZero` structure along a surjective zero-preserving homomorphism. -/
-- See note [reducible non-instances]
protected abbrev Function.Surjective.smulWithZero (f : ZeroHom A A') (hf : Surjective f)
    (smul : ∀ (a : M₀) (b), f (a • b) = a • f b) : SMulWithZero M₀ A' where
  smul := (· • ·)
  zero_smul m := by
    rcases hf m with ⟨x, rfl⟩
    simp [← smul]
  smul_zero c := by rw [← f.map_zero, ← smul, smul_zero]

Pushforward of Scalar Multiplication with Zero Along Surjective Zero-Preserving Homomorphism

Informal description

Given a surjective zero-preserving homomorphism $f \colon A \to A'$ between types with zero elements, and a scalar multiplication operation $\bullet \colon M_0 \times A \to A$ that satisfies $f(a \bullet b) = a \bullet f(b)$ for all $a \in M_0$ and $b \in A$, the type $A'$ inherits a `SMulWithZero` structure from $A$ via $f$.

SMulWithZero.compHom definition

(f : ZeroHom M₀' M₀) : SMulWithZero M₀' A

Full source

/-- Compose a `SMulWithZero` with a `ZeroHom`, with action `f r' • m` -/
def SMulWithZero.compHom (f : ZeroHom M₀' M₀) : SMulWithZero M₀' A where
  smul := (f · • ·)
  smul_zero m := smul_zero (f m)
  zero_smul m := by show (f 0) • m = 0; rw [map_zero, zero_smul]

Composition of Scalar Multiplication with Zero via Zero-Preserving Homomorphism

Informal description

Given a zero-preserving homomorphism $f \colon M_0' \to M_0$ between types with zero elements, the structure `SMulWithZero M_0' A` is defined with scalar multiplication given by composing $f$ with the original scalar multiplication, i.e., $m' \bullet a = f(m') \bullet a$ for $m' \in M_0'$ and $a \in A$. This operation preserves the zero element in both arguments.

AddMonoid.natSMulWithZero instance

[AddMonoid A] : SMulWithZero ℕ A

Full source

instance AddMonoid.natSMulWithZero [AddMonoid A] : SMulWithZero ℕ A where
  smul_zero := _root_.nsmul_zero
  zero_smul := zero_nsmul

Natural Number Scalar Multiplication with Zero on Additive Monoids

Informal description

For any additive monoid $A$, there is a scalar multiplication operation $\mathbb{N} \times A \to A$ that preserves the zero element in both arguments. That is, $0 \bullet a = 0$ for all $a \in A$ and $n \bullet 0 = 0$ for all $n \in \mathbb{N}$.

AddGroup.intSMulWithZero instance

[AddGroup A] : SMulWithZero ℤ A

Full source

instance AddGroup.intSMulWithZero [AddGroup A] : SMulWithZero ℤ A where
  smul_zero := zsmul_zero
  zero_smul := zero_zsmul

Integer Scalar Multiplication with Zero on Additive Groups

Informal description

For any additive group $A$, there is a scalar multiplication operation $\mathbb{Z} \times A \to A$ that preserves the zero element in both arguments. That is, $0 \bullet a = 0$ for all $a \in A$ and $n \bullet 0 = 0$ for all $n \in \mathbb{Z}$.

MulActionWithZero structure

extends MulAction M₀ A

Full source

/-- An action of a monoid with zero `M₀` on a Type `A`, also with `0`, extends `MulAction` and
is compatible with `0` (both in `M₀` and in `A`), with `1 ∈ M₀`, and with associativity of
multiplication on the monoid `A`. -/
class MulActionWithZero extends MulAction M₀ A where
  -- these fields are copied from `SMulWithZero`, as `extends` behaves poorly
  /-- Scalar multiplication by any element send `0` to `0`. -/
  smul_zero : ∀ r : M₀, r • (0 : A) = 0
  /-- Scalar multiplication by the scalar `0` is `0`. -/
  zero_smul : ∀ m : A, (0 : M₀) • m = 0

Multiplicative Action with Zero

Informal description

A *multiplicative action with zero* is an action of a monoid with zero `M₀` on a type `A` (also equipped with a zero element) that extends a multiplicative action and satisfies the following properties: 1. The action is compatible with the zero element in `M₀` (i.e., `0 • a = 0` for all `a ∈ A`), 2. The action is compatible with the zero element in `A` (i.e., `m • 0 = 0` for all `m ∈ M₀`), 3. The action preserves the multiplicative identity (i.e., `1 • a = a` for all `a ∈ A`), 4. The action is associative with respect to multiplication in `M₀` (i.e., `(m₁ * m₂) • a = m₁ • (m₂ • a)` for all `m₁, m₂ ∈ M₀` and `a ∈ A`).

MulActionWithZero.toSMulWithZero instance

(M₀ A) {_ : MonoidWithZero M₀} {_ : Zero A} [m : MulActionWithZero M₀ A] : SMulWithZero M₀ A

Full source

instance (priority := 100) MulActionWithZero.toSMulWithZero (M₀ A) {_ : MonoidWithZero M₀}
    {_ : Zero A} [m : MulActionWithZero M₀ A] : SMulWithZero M₀ A :=
  { m with }

Multiplicative Action with Zero Induces Scalar Multiplication with Zero

Informal description

For any monoid with zero $M₀$ and any type $A$ with a zero element, a multiplicative action with zero of $M₀$ on $A$ induces a scalar multiplication with zero structure on $A$.

MonoidWithZero.toMulActionWithZero instance

: MulActionWithZero M₀ M₀

Full source

/-- See also `Semiring.toModule` -/
instance MonoidWithZero.toMulActionWithZero : MulActionWithZero M₀ M₀ :=
  { MulZeroClass.toSMulWithZero M₀, Monoid.toMulAction M₀ with }

Left Multiplication Action of a Monoid with Zero on Itself

Informal description

Every monoid with zero $M₀$ acts on itself by left multiplication, where the action preserves the zero element and satisfies $0 \cdot a = 0$ and $a \cdot 0 = 0$ for all $a \in M₀$.

MonoidWithZero.toOppositeMulActionWithZero instance

: MulActionWithZero M₀ᵐᵒᵖ M₀

Full source

/-- Like `MonoidWithZero.toMulActionWithZero`, but multiplies on the right. See also
`Semiring.toOppositeModule` -/
instance MonoidWithZero.toOppositeMulActionWithZero : MulActionWithZero M₀ᵐᵒᵖ M₀ :=
  { MulZeroClass.toOppositeSMulWithZero M₀, Monoid.toOppositeMulAction with }

Right Multiplication Action with Zero by the Multiplicative Opposite of a Monoid with Zero

Informal description

For any monoid with zero $M₀$, the multiplicative opposite $M₀^\text{op}$ acts on $M₀$ with zero, where the action is defined by right multiplication and preserves the zero element. Specifically, for $a \in M₀^\text{op}$ and $b \in M₀$, the action is given by $a \cdot b = b \cdot \text{op}^{-1}(a)$, and it satisfies $0 \cdot b = 0$ and $a \cdot 0 = 0$ for all $a \in M₀^\text{op}$ and $b \in M₀$.

MulActionWithZero.subsingleton theorem

[MulActionWithZero M₀ A] [Subsingleton M₀] : Subsingleton A

Full source

protected lemma MulActionWithZero.subsingleton [MulActionWithZero M₀ A] [Subsingleton M₀] :
    Subsingleton A where
  allEq x y := by
    rw [← one_smul M₀ x, ← one_smul M₀ y, Subsingleton.elim (1 : M₀) 0, zero_smul, zero_smul]

Subsingleton Propagation under Zero-Preserving Monoid Action

Informal description

If a monoid with zero $M₀$ acts on a type $A$ with zero (i.e., $M₀$ is a `MulActionWithZero` on $A$) and $M₀$ is a subsingleton (has at most one element), then $A$ is also a subsingleton.

MulActionWithZero.nontrivial theorem

[MulActionWithZero M₀ A] [Nontrivial A] : Nontrivial M₀

Full source

protected lemma MulActionWithZero.nontrivial
    [MulActionWithZero M₀ A] [Nontrivial A] : Nontrivial M₀ :=
  (subsingleton_or_nontrivial M₀).resolve_left fun _ =>
    not_subsingleton A <| MulActionWithZero.subsingleton M₀ A

Nontriviality Propagation under Zero-Preserving Monoid Action

Informal description

If a monoid with zero $M₀$ acts on a type $A$ with zero (i.e., $M₀$ is a `MulActionWithZero` on $A$) and $A$ is nontrivial (contains at least two distinct elements), then $M₀$ is also nontrivial.

ite_zero_smul theorem

(a : M₀) (b : A) : (if p then a else 0 : M₀) • b = if p then a • b else 0

Full source

lemma ite_zero_smul (a : M₀) (b : A) : (if p then a else 0 : M₀) • b = if p then a • b else 0 := by
  rw [ite_smul, zero_smul]

Conditional Scalar Multiplication: $(if p then a else 0) \cdot b = if p then a \cdot b else 0$

Informal description

For any element $a$ in a monoid with zero $M₀$ and any element $b$ in an additive monoid $A$ with a zero element, the scalar multiplication of the conditional expression `if p then a else 0` (where $p$ is a proposition) with $b$ is equal to the conditional expression `if p then a • b else 0$.

boole_smul theorem

(a : A) : (if p then 1 else 0 : M₀) • a = if p then a else 0

Full source

lemma boole_smul (a : A) : (if p then 1 else 0 : M₀) • a = if p then a else 0 := by simp

Conditional Scalar Multiplication by Boolean: $(\text{if } p \text{ then } 1 \text{ else } 0) \cdot a = \text{if } p \text{ then } a \text{ else } 0$

Informal description

For any element $a$ in an additive monoid $A$ with a zero element, and for any proposition $p$, the scalar multiplication of the conditional element (which is $1$ if $p$ holds and $0$ otherwise) with $a$ equals $a$ if $p$ holds and $0$ otherwise. That is: $$(\text{if } p \text{ then } 1 \text{ else } 0) \cdot a = \text{if } p \text{ then } a \text{ else } 0$$

Pi.single_apply_smul theorem

{ι : Type*} [DecidableEq ι] (x : A) (i j : ι) : (Pi.single i 1 : ι → M₀) j • x = (Pi.single i x : ι → A) j

Full source

lemma Pi.single_apply_smul {ι : Type*} [DecidableEq ι] (x : A) (i j : ι) :
    (Pi.single i 1 : ι → M₀) j • x = (Pi.single i x : ι → A) j := by
  rw [single_apply, ite_smul, one_smul, zero_smul, single_apply]

Scalar Multiplication of Indicator Function with Identity and Zero

Informal description

For any type $\iota$ with decidable equality, any element $x$ in an additive monoid $A$ with a zero element, and any indices $i, j \in \iota$, the scalar multiplication of the $j$-th component of the function `Pi.single i 1` (which is $1$ at $i$ and $0$ elsewhere) with $x$ equals the $j$-th component of the function `Pi.single i x` (which is $x$ at $i$ and $0$ elsewhere). In other words, $$(\text{Pi.single}_i\, 1)_j \cdot x = (\text{Pi.single}_i\, x)_j.$$

Function.Injective.mulActionWithZero abbrev

(f : ZeroHom A' A) (hf : Injective f) (smul : ∀ (a : M₀) (b), f (a • b) = a • f b) : MulActionWithZero M₀ A'

Full source

/-- Pullback a `MulActionWithZero` structure along an injective zero-preserving homomorphism. -/
-- See note [reducible non-instances]
protected abbrev Function.Injective.mulActionWithZero (f : ZeroHom A' A) (hf : Injective f)
    (smul : ∀ (a : M₀) (b), f (a • b) = a • f b) : MulActionWithZero M₀ A' :=
  { hf.mulAction f smul, hf.smulWithZero f smul with }

Injective Pullback of Multiplicative Action with Zero

Informal description

Given a monoid with zero $M₀$ acting on a type $A$ with a zero element, and an injective zero-preserving homomorphism $f \colon A' \to A$ such that $f(a \cdot b) = a \cdot f(b)$ for all $a \in M₀$ and $b \in A'$, then $A'$ inherits a multiplicative action with zero structure from $A$ via $f$.

Function.Surjective.mulActionWithZero abbrev

(f : ZeroHom A A') (hf : Surjective f) (smul : ∀ (a : M₀) (b), f (a • b) = a • f b) : MulActionWithZero M₀ A'

Full source

/-- Pushforward a `MulActionWithZero` structure along a surjective zero-preserving homomorphism. -/
-- See note [reducible non-instances]
protected abbrev Function.Surjective.mulActionWithZero (f : ZeroHom A A') (hf : Surjective f)
   (smul : ∀ (a : M₀) (b), f (a • b) = a • f b) : MulActionWithZero M₀ A' :=
  { hf.mulAction f smul, hf.smulWithZero f smul with }

Pushforward of Multiplicative Action with Zero Along Surjective Zero-Preserving Homomorphism

Informal description

Given a monoid with zero $M₀$ and types $A$ and $A'$ each equipped with a zero element, if there exists a surjective zero-preserving homomorphism $f \colon A \to A'$ such that $f(a \cdot b) = a \cdot f(b)$ for all $a \in M₀$ and $b \in A$, then $A'$ inherits a multiplicative action with zero structure from $A$ via $f$.

MulActionWithZero.compHom definition

(f : M₀' →*₀ M₀) : MulActionWithZero M₀' A

Full source

/-- Compose a `MulActionWithZero` with a `MonoidWithZeroHom`, with action `f r' • m` -/
def MulActionWithZero.compHom (f : M₀' →*₀ M₀) : MulActionWithZero M₀' A where
  __ := SMulWithZero.compHom A f.toZeroHom
  mul_smul r s m := by show f (r * s) • m = f r • f s • m; simp [mul_smul]
  one_smul m := by show f 1 • m = m; simp

Composition of multiplicative action with zero via monoid with zero homomorphism

Informal description

Given a monoid with zero homomorphism $f \colon M_0' \to M_0$, the structure `MulActionWithZero M_0' A` is defined with scalar multiplication given by composing $f$ with the original scalar multiplication, i.e., $m' \bullet a = f(m') \bullet a$ for $m' \in M_0'$ and $a \in A$. This operation preserves the zero element in both arguments and is compatible with the multiplicative structure of $M_0'$.

smul_inv₀ theorem

(c : G₀) (x : G₀') : (c • x)⁻¹ = c⁻¹ • x⁻¹

Full source

lemma smul_inv₀ (c : G₀) (x : G₀') : (c • x)⁻¹ = c⁻¹ • x⁻¹ := by
  obtain rfl | hc := eq_or_ne c 0
  · simp only [inv_zero, zero_smul]
  obtain rfl | hx := eq_or_ne x 0
  · simp only [inv_zero, smul_zero]
  · refine inv_eq_of_mul_eq_one_left ?_
    rw [smul_mul_smul_comm, inv_mul_cancel₀ hc, inv_mul_cancel₀ hx, one_smul]

Inverse of Scalar Multiplication: $(c \cdot x)^{-1} = c^{-1} \cdot x^{-1}$

Informal description

For any element $c$ in a group with zero $G₀$ and any element $x$ in a type $G₀'$ with a multiplicative inverse, the inverse of the scalar multiplication $c \cdot x$ is equal to the scalar multiplication of the inverse of $c$ and the inverse of $x$, i.e., $(c \cdot x)^{-1} = c^{-1} \cdot x^{-1}$.

DistribSMul structure

(M A : Type*) [AddZeroClass A] extends SMulZeroClass M A

Full source

/-- Typeclass for scalar multiplication that preserves `0` and `+` on the right.

This is exactly `DistribMulAction` without the `MulAction` part.
-/
@[ext]
class DistribSMul (M A : Type*) [AddZeroClass A] extends SMulZeroClass M A where
  /-- Scalar multiplication distributes across addition -/
  smul_add : ∀ (a : M) (x y : A), a • (x + y) = a • x + a • y

Distributive Scalar Multiplication

Informal description

The structure `DistribSMul M A` represents a scalar multiplication operation `•` of elements of `M` on elements of `A`, where `A` is an additive monoid (i.e., has a zero element and addition). This operation preserves zero (`a • 0 = 0` for all `a ∈ M`) and is right-distributive over addition (`a • (b₁ + b₂) = a • b₁ + a • b₂` for all `a ∈ M` and `b₁, b₂ ∈ A`).

smul_add theorem

(a : M) (b₁ b₂ : A) : a • (b₁ + b₂) = a • b₁ + a • b₂

Full source

theorem smul_add (a : M) (b₁ b₂ : A) : a • (b₁ + b₂) = a • b₁ + a • b₂ :=
  DistribSMul.smul_add _ _ _

Distributivity of Scalar Multiplication over Addition ($a \bullet (b_1 + b_2) = a \bullet b_1 + a \bullet b_2$)

Informal description

For any scalar $a$ in $M$ and any elements $b_1, b_2$ in an additive monoid $A$, the scalar multiplication operation satisfies the distributive property: $$a \bullet (b_1 + b_2) = a \bullet b_1 + a \bullet b_2$$

AddMonoidHom.smulZeroClass instance

[AddZeroClass B] : SMulZeroClass M (B →+ A)

Full source

instance AddMonoidHom.smulZeroClass [AddZeroClass B] : SMulZeroClass M (B →+ A) where
  smul r f :=
    { toFun := fun a => r • (f a)
      map_zero' := by simp only [map_zero, smul_zero]
      map_add' := fun x y => by simp only [map_add, smul_add] }
  smul_zero _ := ext fun _ => smul_zero _

Scalar Multiplication on Homomorphisms Preserving Zero

Informal description

For any additive monoid $B$, the type of additive monoid homomorphisms from $B$ to an additive monoid $A$ forms a scalar multiplication structure that preserves zero. That is, for any scalar $m \in M$ and homomorphism $f : B \to A$, the operation $m \bullet f$ is defined pointwise as $(m \bullet f)(x) = m \bullet f(x)$, and this operation satisfies $m \bullet 0 = 0$ for the zero homomorphism.

Function.Injective.distribSMul abbrev

 [AddZeroClass B] [SMul M B] (f : B →+ A) (hf : Injective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) :
  DistribSMul M B

Full source

/-- Pullback a distributive scalar multiplication along an injective additive monoid
homomorphism.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.distribSMul [AddZeroClass B] [SMul M B] (f : B →+ A)
    (hf : Injective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) : DistribSMul M B :=
  { hf.smulZeroClass f.toZeroHom smul with
    smul_add := fun c x y => hf <| by simp only [smul, map_add, smul_add] }

Pullback of Distributive Scalar Multiplication via Injective Additive Monoid Homomorphism

Informal description

Let $M$ and $A$ be types, where $A$ is an additive monoid (i.e., has a zero element and addition), and let $B$ be another additive monoid with a scalar multiplication operation $\bullet \colon M \times B \to B$. Given an injective additive monoid homomorphism $f \colon B \to A$ such that for all $c \in M$ and $x \in B$, $f(c \bullet x) = c \bullet f(x)$, then the scalar multiplication on $B$ is distributive, i.e., it satisfies: 1. $c \bullet (x + y) = c \bullet x + c \bullet y$ for all $c \in M$ and $x, y \in B$ 2. $c \bullet 0 = 0$ for all $c \in M$

Function.Surjective.distribSMul abbrev

 [AddZeroClass B] [SMul M B] (f : A →+ B) (hf : Surjective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) :
  DistribSMul M B

Full source

/-- Pushforward a distributive scalar multiplication along a surjective additive monoid
homomorphism.
See note [reducible non-instances]. -/
protected abbrev Function.Surjective.distribSMul [AddZeroClass B] [SMul M B] (f : A →+ B)
    (hf : Surjective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) : DistribSMul M B :=
  { f.toZeroHom.smulZeroClass smul with
    smul_add := fun c x y => by
      rcases hf x with ⟨x, rfl⟩
      rcases hf y with ⟨y, rfl⟩
      simp only [smul_add, ← smul, ← map_add] }

Pushforward of Distributive Scalar Multiplication via Surjective Additive Monoid Homomorphism

Informal description

Let $A$ and $B$ be additive monoids, and let $M$ be a type with a scalar multiplication operation on $B$. Given a surjective additive monoid homomorphism $f \colon A \to B$ such that for all $c \in M$ and $x \in A$, we have $f(c \bullet x) = c \bullet f(x)$, then $M$ acts distributively on $B$ via the scalar multiplication induced by $f$.

Function.Surjective.distribSMulLeft abbrev

 {R S M : Type*} [AddZeroClass M] [DistribSMul R M] [SMul S M] (f : R → S) (hf : Function.Surjective f)
  (hsmul : ∀ (c) (x : M), f c • x = c • x) : DistribSMul S M

Full source

/-- Push forward the multiplication of `R` on `M` along a compatible surjective map `f : R → S`.

See also `Function.Surjective.distribMulActionLeft`.
-/
abbrev Function.Surjective.distribSMulLeft {R S M : Type*} [AddZeroClass M] [DistribSMul R M]
    [SMul S M] (f : R → S) (hf : Function.Surjective f)
    (hsmul : ∀ (c) (x : M), f c • x = c • x) : DistribSMul S M :=
  { hf.smulZeroClassLeft f hsmul with
    smul_add := hf.forall.mpr fun c x y => by simp only [hsmul, smul_add] }

Pushforward of Distributive Scalar Multiplication via Surjective Map

Informal description

Let $R$, $S$, and $M$ be types, where $M$ is an additive monoid (i.e., has a zero element and addition). Suppose $R$ acts on $M$ via a distributive scalar multiplication (preserving zero and addition), and $S$ has a scalar multiplication on $M$. Given a surjective function $f : R \to S$ such that $f(c) \bullet x = c \bullet x$ for all $c \in R$ and $x \in M$, then $S$ also acts on $M$ via a distributive scalar multiplication.

DistribSMul.compFun abbrev

(f : N → M) : DistribSMul N A

Full source

/-- Compose a `DistribSMul` with a function, with scalar multiplication `f r' • m`.
See note [reducible non-instances]. -/
abbrev DistribSMul.compFun (f : N → M) : DistribSMul N A :=
  { SMulZeroClass.compFun A f with
    smul_add := fun x => smul_add (f x) }

Composition of Distributive Scalar Multiplication via a Function

Informal description

Given a function $f : N \to M$ and a distributive scalar multiplication operation $\bullet : M \times A \to A$ (where $A$ is an additive monoid), we can define a new distributive scalar multiplication operation $\circ : N \times A \to A$ by $n \circ a := f(n) \bullet a$. This operation preserves zero and distributes over addition in $A$.

DistribSMul.toAddMonoidHom definition

(x : M) : A →+ A

Full source

/-- Each element of the scalars defines an additive monoid homomorphism. -/
@[simps]
def DistribSMul.toAddMonoidHom (x : M) : A →+ A :=
  { SMulZeroClass.toZeroHom A x with toFun := (x • ·), map_add' := smul_add x }

Additive monoid homomorphism induced by scalar multiplication

Informal description

For any element $ x $ of the scalar type $ M $, the function $ a \mapsto x \bullet a $ is an additive monoid homomorphism from $ A $ to $ A $, where $ \bullet $ denotes the scalar multiplication operation. This means it preserves both the zero element ($ x \bullet 0 = 0 $) and addition ($ x \bullet (a + b) = x \bullet a + x \bullet b $ for all $ a, b \in A $).

DistribMulAction structure

(M A : Type*) [Monoid M] [AddMonoid A] extends MulAction M A

Full source

/-- Typeclass for multiplicative actions on additive structures. This generalizes group modules. -/
@[ext]
class DistribMulAction (M A : Type*) [Monoid M] [AddMonoid A] extends MulAction M A where
  /-- Multiplying `0` by a scalar gives `0` -/
  smul_zero : ∀ a : M, a • (0 : A) = 0
  /-- Scalar multiplication distributes across addition -/
  smul_add : ∀ (a : M) (x y : A), a • (x + y) = a • x + a • y

Distributive multiplicative action

Informal description

A structure representing a multiplicative action of a monoid $M$ on an additive monoid $A$ that distributes over addition and preserves zero. Specifically, for all $a \in M$ and $b, c \in A$, the action satisfies $a \cdot (b + c) = a \cdot b + a \cdot c$ and $a \cdot 0 = 0$.

DistribMulAction.toDistribSMul instance

: DistribSMul M A

Full source

instance (priority := 100) DistribMulAction.toDistribSMul : DistribSMul M A :=
  { ‹DistribMulAction M A› with }

Distributive Multiplicative Action Induces Distributive Scalar Multiplication

Informal description

Every distributive multiplicative action of a monoid $M$ on an additive monoid $A$ induces a distributive scalar multiplication structure on $A$.

Function.Injective.distribMulAction abbrev

 [AddMonoid B] [SMul M B] (f : B →+ A) (hf : Injective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) :
  DistribMulAction M B

Full source

/-- Pullback a distributive multiplicative action along an injective additive monoid
homomorphism.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.distribMulAction [AddMonoid B] [SMul M B] (f : B →+ A)
    (hf : Injective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) : DistribMulAction M B :=
  { hf.distribSMul f smul, hf.mulAction f smul with }

Injective Pullback of Distributive Multiplicative Action via Additive Monoid Homomorphism

Informal description

Let $M$ be a monoid and $A$, $B$ be additive monoids. Given an injective additive monoid homomorphism $f \colon B \to A$ and a scalar multiplication operation $\bullet \colon M \times B \to B$ such that for all $c \in M$ and $x \in B$, $f(c \bullet x) = c \bullet f(x)$, then $B$ inherits a distributive multiplicative action of $M$ via $f$. That is, the action satisfies: 1. $c \bullet (x + y) = c \bullet x + c \bullet y$ for all $c \in M$ and $x, y \in B$ 2. $c \bullet 0 = 0$ for all $c \in M$

Function.Surjective.distribMulAction abbrev

 [AddMonoid B] [SMul M B] (f : A →+ B) (hf : Surjective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) :
  DistribMulAction M B

Full source

/-- Pushforward a distributive multiplicative action along a surjective additive monoid
homomorphism.
See note [reducible non-instances]. -/
protected abbrev Function.Surjective.distribMulAction [AddMonoid B] [SMul M B] (f : A →+ B)
    (hf : Surjective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) : DistribMulAction M B :=
  { hf.distribSMul f smul, hf.mulAction f smul with }

Pushforward of Distributive Multiplicative Action via Surjective Additive Monoid Homomorphism

Informal description

Let $A$ and $B$ be additive monoids, and let $M$ be a monoid with a scalar multiplication operation on $B$. Given a surjective additive monoid homomorphism $f \colon A \to B$ such that for all $c \in M$ and $x \in A$, we have $f(c \bullet x) = c \bullet f(x)$, then $M$ acts distributively on $B$ via the scalar multiplication induced by $f$. That is, for all $a, b \in B$ and $m \in M$, we have $m \bullet (a + b) = m \bullet a + m \bullet b$ and $m \bullet 0 = 0$.

DistribMulAction.toAddMonoidHom definition

(x : M) : A →+ A

Full source

/-- Each element of the monoid defines an additive monoid homomorphism. -/
@[simps!]
def DistribMulAction.toAddMonoidHom (x : M) : A →+ A :=
  DistribSMul.toAddMonoidHom A x

Additive monoid homomorphism induced by scalar multiplication

Informal description

For any element $ x $ of the monoid $ M $, the function $ a \mapsto x \cdot a $ is an additive monoid homomorphism from $ A $ to $ A $, where $ \cdot $ denotes the scalar multiplication operation. This means it preserves both the zero element ($ x \cdot 0 = 0 $) and addition ($ x \cdot (a + b) = x \cdot a + x \cdot b $ for all $ a, b \in A $).

DistribMulAction.toAddMonoidEnd definition

: M →* AddMonoid.End A

Full source

/-- Each element of the monoid defines an additive monoid homomorphism. -/
@[simps]
def DistribMulAction.toAddMonoidEnd :
    M →* AddMonoid.End A where
  toFun := DistribMulAction.toAddMonoidHom A
  map_one' := AddMonoidHom.ext <| one_smul M
  map_mul' x y := AddMonoidHom.ext <| mul_smul x y

Monoid homomorphism to additive monoid endomorphisms induced by scalar multiplication

Informal description

The function maps each element $x$ of the monoid $M$ to the additive monoid endomorphism $a \mapsto x \cdot a$ on $A$, where $\cdot$ denotes the scalar multiplication operation. This function preserves the monoid structure, meaning it maps the identity element of $M$ to the identity endomorphism and the product of two elements in $M$ to the composition of their corresponding endomorphisms.

AddMonoid.nat_smulCommClass instance

: SMulCommClass ℕ M A

Full source

instance AddMonoid.nat_smulCommClass :
    SMulCommClass ℕ M
      A where smul_comm n x y := ((DistribMulAction.toAddMonoidHom A x).map_nsmul y n).symm

Commutativity of Natural Number and Monoid Actions on Additive Monoids

Informal description

For any additive monoid $A$ and monoid $M$ acting distributively on $A$, the scalar multiplications by natural numbers and by $M$ on $A$ commute. That is, for any $n \in \mathbb{N}$, $m \in M$, and $a \in A$, we have $n \cdot (m \cdot a) = m \cdot (n \cdot a)$.

AddMonoid.nat_smulCommClass' instance

: SMulCommClass M ℕ A

Full source

instance AddMonoid.nat_smulCommClass' : SMulCommClass M ℕ A :=
  SMulCommClass.symm _ _ _

Commutativity of Monoid and Natural Number Actions on Additive Monoids

Informal description

For any additive monoid $A$ and monoid $M$ acting distributively on $A$, the scalar multiplications by $M$ and by natural numbers on $A$ commute. That is, for any $m \in M$, $n \in \mathbb{N}$, and $a \in A$, we have $m \cdot (n \cdot a) = n \cdot (m \cdot a)$.

AddGroup.int_smulCommClass instance

: SMulCommClass ℤ M A

Full source

instance AddGroup.int_smulCommClass : SMulCommClass ℤ M A where
  smul_comm n x y := ((DistribMulAction.toAddMonoidHom A x).map_zsmul y n).symm

Commutativity of Integer and Monoid Actions on Additive Groups

Informal description

For any additive group $A$ and monoid $M$ acting distributively on $A$, the scalar multiplications by integers and by $M$ on $A$ commute. That is, for any $n \in \mathbb{Z}$, $m \in M$, and $a \in A$, we have $n \cdot (m \cdot a) = m \cdot (n \cdot a)$.

AddGroup.int_smulCommClass' instance

: SMulCommClass M ℤ A

Full source

instance AddGroup.int_smulCommClass' : SMulCommClass M ℤ A :=
  SMulCommClass.symm _ _ _

Commutativity of Monoid and Integer Actions on Additive Groups

Informal description

For any additive group $A$ and monoid $M$ acting distributively on $A$, the scalar multiplications by $M$ and by integers on $A$ commute. That is, for any $m \in M$, $n \in \mathbb{Z}$, and $a \in A$, we have $m \cdot (n \cdot a) = n \cdot (m \cdot a)$.

smul_neg theorem

(r : M) (x : A) : r • -x = -(r • x)

Full source

@[simp]
theorem smul_neg (r : M) (x : A) : r • -x = -(r • x) :=
  eq_neg_of_add_eq_zero_left <| by rw [← smul_add, neg_add_cancel, smul_zero]

Scalar Multiplication Commutes with Negation: $r \cdot (-x) = -(r \cdot x)$

Informal description

For any scalar $r$ in a monoid $M$ and any element $x$ in an additive group $A$, the scalar multiplication satisfies $r \cdot (-x) = -(r \cdot x)$.

smul_sub theorem

(r : M) (x y : A) : r • (x - y) = r • x - r • y

Full source

theorem smul_sub (r : M) (x y : A) : r • (x - y) = r • x - r • y := by
  rw [sub_eq_add_neg, sub_eq_add_neg, smul_add, smul_neg]

Scalar Multiplication Distributes over Subtraction: $r \cdot (x - y) = r \cdot x - r \cdot y$

Informal description

For any scalar $r$ in a monoid $M$ and any elements $x, y$ in an additive group $A$, the scalar multiplication satisfies $r \cdot (x - y) = r \cdot x - r \cdot y$.

smul_eq_zero_iff_eq theorem

(a : α) {x : β} : a • x = 0 ↔ x = 0

Full source

lemma smul_eq_zero_iff_eq (a : α) {x : β} : a • x = 0 ↔ x = 0 :=
  ⟨fun h => by rw [← inv_smul_smul a x, h, smul_zero], fun h => h.symm ▸ smul_zero _⟩

Scalar Multiplication Annihilates Zero if and only if Element is Zero

Informal description

For any scalar $a$ in a monoid $\alpha$ acting on an additive monoid $\beta$, and any element $x \in \beta$, the scalar multiplication satisfies $a \cdot x = 0$ if and only if $x = 0$.

smul_ne_zero_iff_ne theorem

(a : α) {x : β} : a • x ≠ 0 ↔ x ≠ 0

Full source

lemma smul_ne_zero_iff_ne (a : α) {x : β} : a • x ≠ 0a • x ≠ 0 ↔ x ≠ 0 :=
  not_congr <| smul_eq_zero_iff_eq a

Nonzero Scalar Multiplication Preserves Nonzero Elements: $a \cdot x \neq 0 \leftrightarrow x \neq 0$

Informal description

For any scalar $a$ in a monoid $\alpha$ acting on an additive monoid $\beta$, and any element $x \in \beta$, the scalar multiplication satisfies $a \cdot x \neq 0$ if and only if $x \neq 0$.

Mathlib.Algebra.GroupWithZero.Action.Defs

Notation

Implementation details

Tags