Mathlib.Algebra.Module.Rat

map_nnratCast_smul theorem

 [AddCommMonoid M] [AddCommMonoid M₂] {F : Type*} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R S : Type*)
  [DivisionSemiring R] [DivisionSemiring S] [Module R M] [Module S M₂] (c : ℚ≥0) (x : M) :
  f ((c : R) • x) = (c : S) • f x

Full source

theorem map_nnratCast_smul [AddCommMonoid M] [AddCommMonoid M₂] {F : Type*} [FunLike F M M₂]
    [AddMonoidHomClass F M M₂] (f : F) (R S : Type*) [DivisionSemiring R] [DivisionSemiring S]
    [Module R M] [Module S M₂] (c : ℚ≥0) (x : M) :
    f ((c : R) • x) = (c : S) • f x := by
  rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_natCast_smul f R S, map_inv_natCast_smul f R S]

Compatibility of Additive Monoid Homomorphisms with Scalar Multiplication by Nonnegative Rationals

Informal description

Let $M$ and $M_2$ be additive commutative monoids, and let $F$ be a type of functions from $M$ to $M_2$ that are additive monoid homomorphisms. Let $R$ and $S$ be division semirings, and suppose $M$ is a module over $R$ and $M_2$ is a module over $S$. For any nonnegative rational number $c \in \mathbb{Q}_{\geq 0}$ and any $x \in M$, the function $f$ satisfies: \[ f(c \cdot x) = c \cdot f(x), \] where the scalar multiplication on the left is in $R$ and on the right is in $S$.

map_ratCast_smul theorem

 [AddCommGroup M] [AddCommGroup M₂] {F : Type*} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R S : Type*)
  [DivisionRing R] [DivisionRing S] [Module R M] [Module S M₂] (c : ℚ) (x : M) : f ((c : R) • x) = (c : S) • f x

Full source

theorem map_ratCast_smul [AddCommGroup M] [AddCommGroup M₂] {F : Type*} [FunLike F M M₂]
    [AddMonoidHomClass F M M₂] (f : F) (R S : Type*) [DivisionRing R] [DivisionRing S] [Module R M]
    [Module S M₂] (c : ℚ) (x : M) :
    f ((c : R) • x) = (c : S) • f x := by
  rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_intCast_smul f R S, map_inv_natCast_smul f R S]

Preservation of Rational Scalar Multiplication by Additive Monoid Homomorphisms

Informal description

Let $M$ and $M₂$ be additive commutative groups, and let $F$ be a type of functions from $M$ to $M₂$ that are additive monoid homomorphisms. Let $R$ and $S$ be division rings, and suppose $M$ is a module over $R$ and $M₂$ is a module over $S$. For any rational number $c \in \mathbb{Q}$ and any element $x \in M$, the function $f$ satisfies $f(c \cdot x) = c \cdot f(x)$, where the scalar multiplications are taken in the respective modules over $R$ and $S$.

map_nnrat_smul theorem

 [AddCommMonoid M] [AddCommMonoid M₂] [_instM : Module ℚ≥0 M] [_instM₂ : Module ℚ≥0 M₂] {F : Type*} [FunLike F M M₂]
  [AddMonoidHomClass F M M₂] (f : F) (c : ℚ≥0) (x : M) : f (c • x) = c • f x

Full source

theorem map_nnrat_smul [AddCommMonoid M] [AddCommMonoid M₂]
    [_instM : Module ℚ≥0 M] [_instM₂ : Module ℚ≥0 M₂]
    {F : Type*} [FunLike F M M₂] [AddMonoidHomClass F M M₂]
    (f : F) (c : ℚ≥0) (x : M) : f (c • x) = c • f x :=
  map_nnratCast_smul f ℚ≥0 ℚ≥0 c x

Preservation of Nonnegative Rational Scalar Multiplication by Additive Monoid Homomorphisms

Informal description

Let $M$ and $M_2$ be additive commutative monoids equipped with module structures over the nonnegative rationals $\mathbb{Q}_{\geq 0}$. Let $F$ be a type of functions from $M$ to $M_2$ that are additive monoid homomorphisms. Then for any nonnegative rational number $c \in \mathbb{Q}_{\geq 0}$ and any $x \in M$, the function $f$ satisfies: \[ f(c \cdot x) = c \cdot f(x). \]

map_rat_smul theorem

 [AddCommGroup M] [AddCommGroup M₂] [_instM : Module ℚ M] [_instM₂ : Module ℚ M₂] {F : Type*} [FunLike F M M₂]
  [AddMonoidHomClass F M M₂] (f : F) (c : ℚ) (x : M) : f (c • x) = c • f x

Full source

theorem map_rat_smul [AddCommGroup M] [AddCommGroup M₂]
    [_instM : Module ℚ M] [_instM₂ : Module ℚ M₂]
    {F : Type*} [FunLike F M M₂] [AddMonoidHomClass F M M₂]
    (f : F) (c : ℚ) (x : M) : f (c • x) = c • f x :=
  map_ratCast_smul f ℚ ℚ c x

$\mathbb{Q}$-linearity of additive monoid homomorphisms between $\mathbb{Q}$-modules

Informal description

Let $M$ and $M_2$ be additive commutative groups equipped with $\mathbb{Q}$-module structures. For any additive monoid homomorphism $f \colon M \to M_2$, rational number $c \in \mathbb{Q}$, and element $x \in M$, we have $f(c \cdot x) = c \cdot f(x)$.

subsingleton_nnrat_module instance

(E : Type*) [AddCommMonoid E] : Subsingleton (Module ℚ≥0 E)

Full source

/-- There can be at most one `Module ℚ≥0 E` structure on an additive commutative monoid. -/
instance subsingleton_nnrat_module (E : Type*) [AddCommMonoid E] : Subsingleton (Module ℚ≥0 E) :=
  ⟨fun P Q => (Module.ext' P Q) fun r x =>
    map_nnrat_smul (_instM := P) (_instM₂ := Q) (AddMonoidHom.id E) r x⟩

Uniqueness of Nonnegative Rational Module Structure on Additive Commutative Monoids

Informal description

For any additive commutative monoid $E$, there is at most one $\mathbb{Q}_{\geq 0}$-module structure on $E$.

subsingleton_rat_module instance

(E : Type*) [AddCommGroup E] : Subsingleton (Module ℚ E)

Full source

/-- There can be at most one `Module ℚ E` structure on an additive commutative group. -/
instance subsingleton_rat_module (E : Type*) [AddCommGroup E] : Subsingleton (Module ℚ E) :=
  ⟨fun P Q => (Module.ext' P Q) fun r x =>
    map_rat_smul (_instM := P) (_instM₂ := Q) (AddMonoidHom.id E) r x⟩

Uniqueness of $\mathbb{Q}$-module Structure on Additive Commutative Groups

Informal description

For any additive commutative group $E$, there is at most one $\mathbb{Q}$-module structure on $E$.

nnratCast_smul_eq theorem

 {E : Type*} (R S : Type*) [AddCommMonoid E] [DivisionSemiring R] [DivisionSemiring S] [Module R E] [Module S E]
  (r : ℚ≥0) (x : E) : (r : R) • x = (r : S) • x

Full source

/-- If `E` is a vector space over two division semirings `R` and `S`, then scalar multiplications
agree on non-negative rational numbers in `R` and `S`. -/
theorem nnratCast_smul_eq {E : Type*} (R S : Type*) [AddCommMonoid E] [DivisionSemiring R]
    [DivisionSemiring S] [Module R E] [Module S E] (r : ℚ≥0) (x : E) : (r : R) • x = (r : S) • x :=
  map_nnratCast_smul (AddMonoidHom.id E) R S r x

Scalar Multiplication by Nonnegative Rationals is Independent of Division Semiring

Informal description

Let $E$ be an additive commutative monoid, and let $R$ and $S$ be division semirings such that $E$ is a module over both $R$ and $S$. For any nonnegative rational number $r \in \mathbb{Q}_{\geq 0}$ and any element $x \in E$, the scalar multiplication of $r$ (viewed as an element of $R$) with $x$ is equal to the scalar multiplication of $r$ (viewed as an element of $S$) with $x$. That is, \[ (r : R) \cdot x = (r : S) \cdot x. \]

ratCast_smul_eq theorem

 {E : Type*} (R S : Type*) [AddCommGroup E] [DivisionRing R] [DivisionRing S] [Module R E] [Module S E] (r : ℚ)
  (x : E) : (r : R) • x = (r : S) • x

Full source

/-- If `E` is a vector space over two division rings `R` and `S`, then scalar multiplications
agree on rational numbers in `R` and `S`. -/
theorem ratCast_smul_eq {E : Type*} (R S : Type*) [AddCommGroup E] [DivisionRing R]
    [DivisionRing S] [Module R E] [Module S E] (r : ℚ) (x : E) : (r : R) • x = (r : S) • x :=
  map_ratCast_smul (AddMonoidHom.id E) R S r x

Rational Scalar Multiplication is Independent of Division Ring

Informal description

Let $E$ be an additive commutative group that is a module over two division rings $R$ and $S$. Then for any rational number $r \in \mathbb{Q}$ and any element $x \in E$, the scalar multiplication of $r$ (viewed as an element of $R$) with $x$ is equal to the scalar multiplication of $r$ (viewed as an element of $S$) with $x$, i.e., $(r : R) \cdot x = (r : S) \cdot x$.

IsScalarTower.nnrat instance

 {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module ℚ≥0 R] [Module ℚ≥0 M] :
  IsScalarTower ℚ≥0 R M

Full source

instance IsScalarTower.nnrat {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M]
    [Module ℚ≥0 R] [Module ℚ≥0 M] : IsScalarTower ℚ≥0 R M where
  smul_assoc r x y := map_nnrat_smul ((smulAddHom R M).flip y) r x

Tower Property for Nonnegative Rational Scalar Multiplication

Informal description

For any semiring $R$ and additive commutative monoid $M$ that are both modules over the nonnegative rationals $\mathbb{Q}_{\geq 0}$, the scalar multiplication operations satisfy the tower property. That is, for any $q \in \mathbb{Q}_{\geq 0}$, $r \in R$, and $m \in M$, we have: \[ q \cdot (r \cdot m) = (q \cdot r) \cdot m. \]

IsScalarTower.rat instance

{R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module ℚ R] [Module ℚ M] : IsScalarTower ℚ R M

Full source

instance IsScalarTower.rat {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M]
    [Module ℚ R] [Module ℚ M] : IsScalarTower ℚ R M where
  smul_assoc r x y := map_rat_smul ((smulAddHom R M).flip y) r x

Tower Property for Rational Scalar Multiplication

Informal description

For any ring $R$ and additive commutative group $M$ that are both modules over $\mathbb{Q}$, the scalar multiplication operations satisfy the tower property: for any $q \in \mathbb{Q}$, $r \in R$, and $m \in M$, we have $(q \cdot r) \cdot m = q \cdot (r \cdot m)$.

SMulCommClass.nnrat instance

[Monoid α] [AddCommMonoid M] [DistribMulAction α M] [Module ℚ≥0 M] : SMulCommClass ℚ≥0 α M

Full source

instance SMulCommClass.nnrat [Monoid α] [AddCommMonoid M] [DistribMulAction α M] [Module ℚ≥0 M] :
    SMulCommClass ℚ≥0 α M where
  smul_comm r x y := (map_nnrat_smul (DistribMulAction.toAddMonoidHom M x) r y).symm

Commutativity of Nonnegative Rational and Monoid Scalar Multiplications

Informal description

For any monoid $\alpha$ and additive commutative monoid $M$ equipped with a distributive multiplicative action of $\alpha$ on $M$ and a module structure over the nonnegative rationals $\mathbb{Q}_{\geq 0}$, the scalar multiplications by $\mathbb{Q}_{\geq 0}$ and $\alpha$ on $M$ commute. That is, for any $q \in \mathbb{Q}_{\geq 0}$, $a \in \alpha$, and $x \in M$, we have $q \cdot (a \cdot x) = a \cdot (q \cdot x)$.

SMulCommClass.rat instance

[Monoid α] [AddCommGroup M] [DistribMulAction α M] [Module ℚ M] : SMulCommClass ℚ α M

Full source

instance SMulCommClass.rat [Monoid α] [AddCommGroup M] [DistribMulAction α M] [Module ℚ M] :
    SMulCommClass ℚ α M where
  smul_comm r x y := (map_rat_smul (DistribMulAction.toAddMonoidHom M x) r y).symm

Commutativity of Rational and Monoid Scalar Multiplications

Informal description

For any monoid $\alpha$ and additive commutative group $M$ equipped with a distributive multiplicative action of $\alpha$ on $M$ and a $\mathbb{Q}$-module structure, the scalar multiplications by $\mathbb{Q}$ and $\alpha$ on $M$ commute. That is, for any $q \in \mathbb{Q}$, $a \in \alpha$, and $x \in M$, we have $q \cdot (a \cdot x) = a \cdot (q \cdot x)$.

SMulCommClass.nnrat' instance

[Monoid α] [AddCommMonoid M] [DistribMulAction α M] [Module ℚ≥0 M] : SMulCommClass α ℚ≥0 M

Full source

instance SMulCommClass.nnrat' [Monoid α] [AddCommMonoid M] [DistribMulAction α M] [Module ℚ≥0 M] :
    SMulCommClass α ℚ≥0 M :=
  SMulCommClass.symm _ _ _

Commutativity of Monoid and Nonnegative Rational Scalar Multiplications

Informal description

For any monoid $\alpha$ and additive commutative monoid $M$ equipped with a distributive multiplicative action of $\alpha$ on $M$ and a module structure over the nonnegative rationals $\mathbb{Q}_{\geq 0}$, the scalar multiplications by $\alpha$ and $\mathbb{Q}_{\geq 0}$ on $M$ commute. That is, for any $a \in \alpha$, $q \in \mathbb{Q}_{\geq 0}$, and $x \in M$, we have $a \cdot (q \cdot x) = q \cdot (a \cdot x)$.

SMulCommClass.rat' instance

[Monoid α] [AddCommGroup M] [DistribMulAction α M] [Module ℚ M] : SMulCommClass α ℚ M

Full source

instance SMulCommClass.rat' [Monoid α] [AddCommGroup M] [DistribMulAction α M] [Module ℚ M] :
    SMulCommClass α ℚ M :=
  SMulCommClass.symm _ _ _

Commutativity of Monoid and Rational Scalar Multiplications

Informal description

For any monoid $\alpha$ and additive commutative group $M$ equipped with a distributive multiplicative action of $\alpha$ on $M$ and a $\mathbb{Q}$-module structure, the scalar multiplications by $\alpha$ and $\mathbb{Q}$ on $M$ commute. That is, for any $a \in \alpha$, $q \in \mathbb{Q}$, and $x \in M$, we have $a \cdot (q \cdot x) = q \cdot (a \cdot x)$.

NNRatModule.noZeroSMulDivisors instance

[AddCommMonoid M] [Module ℚ≥0 M] : NoZeroSMulDivisors ℕ M

Full source

instance (priority := 100) NNRatModule.noZeroSMulDivisors [AddCommMonoid M] [Module ℚ≥0 M] :
    NoZeroSMulDivisors ℕ M :=
  ⟨fun {k} {x : M} h => by simpa [← Nat.cast_smul_eq_nsmul ℚ≥0 k x] using h⟩

No Zero Divisors for Natural Number Scalar Multiplication in Nonnegative Rational Modules

Informal description

For any additive commutative monoid $M$ equipped with a $\mathbb{Q}_{\geq 0}$-module structure, the scalar multiplication by natural numbers on $M$ has no zero divisors. That is, for any natural number $n$ and element $m \in M$, if $n \cdot m = 0$ then either $n = 0$ or $m = 0$.

RatModule.noZeroSMulDivisors instance

[AddCommGroup M] [Module ℚ M] : NoZeroSMulDivisors ℤ M

Full source

instance (priority := 100) RatModule.noZeroSMulDivisors [AddCommGroup M] [Module ℚ M] :
    NoZeroSMulDivisors ℤ M :=
  ⟨fun {k} {x : M} h => by simpa [← Int.cast_smul_eq_zsmul ℚ k x] using h⟩

No Zero Divisors for Integer Scalar Multiplication in Rational Modules

Informal description

For any additive commutative group $M$ equipped with a $\mathbb{Q}$-module structure, the scalar multiplication by integers on $M$ has no zero divisors. That is, for any integer $n$ and element $m \in M$, if $n \cdot m = 0$ then either $n = 0$ or $m = 0$.