doc-next-gen

Mathlib.Algebra.Module.Basic

Module docstring

{"# Further basic results about modules.

"}

Units.neg_smul theorem
[Ring R] [AddCommGroup M] [Module R M] (u : Rˣ) (x : M) : -u • x = -(u • x)
Full source 
@[simp]
theorem Units.neg_smul [Ring R] [AddCommGroup M] [Module R M] (u : Rˣ) (x : M) :
    -u • x = -(u • x) := by
  rw [Units.smul_def, Units.val_neg, _root_.neg_smul, Units.smul_def]
Negation of Scalar Multiplication by Unit Equals Scalar Multiplication by Negated Unit
Informal description
Let $R$ be a ring and $M$ an additive commutative group equipped with an $R$-module structure. For any unit $u \in R^\times$ and any element $x \in M$, we have: $$ - (u \cdot x) = -u \cdot x $$ where $\cdot$ denotes the scalar multiplication action of $R$ on $M$.
invOf_two_smul_add_invOf_two_smul theorem
(R) [Semiring R] [AddCommMonoid M] [Module R M] [Invertible (2 : R)] (x : M) : (⅟ 2 : R) • x + (⅟ 2 : R) • x = x
Full source 
@[simp]
theorem invOf_two_smul_add_invOf_two_smul (R) [Semiring R] [AddCommMonoid M] [Module R M]
    [Invertible (2 : R)] (x : M) :
    (⅟ 2 : R) • x + (⅟ 2 : R) • x = x :=
  Convex.combo_self invOf_two_add_invOf_two _
Inverse of Two Scalar Addition Identity: $(⅟ 2) \cdot x + (⅟ 2) \cdot x = x$
Informal description
Let $R$ be a semiring, $M$ an additive commutative monoid equipped with an $R$-module structure, and assume $2$ is invertible in $R$. Then for any $x \in M$, we have: $$(⅟ 2) \cdot x + (⅟ 2) \cdot x = x$$ where $⅟ 2$ denotes the multiplicative inverse of $2$ in $R$.
map_inv_natCast_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₂] (n : ℕ) (x : M) : f ((n⁻¹ : R) • x) = (n⁻¹ : S) • f x
Full source 
theorem map_inv_natCast_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₂] (n : ℕ) (x : M) : f ((n⁻¹ : R) • x) = (n⁻¹ : S) • f x := by
  by_cases hR : (n : R) = 0 <;> by_cases hS : (n : S) = 0
  · simp [hR, hS, map_zero f]
  · suffices ∀ y, f y = 0 by rw [this, this, smul_zero]
    clear x
    intro x
    rw [← inv_smul_smul₀ hS (f x), ← map_natCast_smul f R S]
    simp [hR, map_zero f]
  · suffices ∀ y, f y = 0 by simp [this]
    clear x
    intro x
    rw [← smul_inv_smul₀ hR x, map_natCast_smul f R S, hS, zero_smul]
  · rw [← inv_smul_smul₀ hS (f _), ← map_natCast_smul f R S, smul_inv_smul₀ hR]
Natural Number Inverse Scalar Multiplication Commutes with Additive Monoid Homomorphisms
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. For any division semirings $R$ and $S$ with module structures on $M$ and $M_2$ respectively, any natural number $n$, and any element $x \in M$, we have: \[ f\left((n^{-1} : R) \cdot x\right) = (n^{-1} : S) \cdot f(x). \]
map_inv_intCast_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₂] (z : ℤ) (x : M) : f ((z⁻¹ : R) • x) = (z⁻¹ : S) • f x
Full source 
theorem map_inv_intCast_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₂] (z : ℤ) (x : M) : f ((z⁻¹ : R) • x) = (z⁻¹ : S) • f x := by
  obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
  · rw [Int.cast_natCast, Int.cast_natCast, map_inv_natCast_smul _ R S]
  · simp_rw [Int.cast_neg, Int.cast_natCast, inv_neg, neg_smul, map_neg,
      map_inv_natCast_smul _ R S]
Integer Inverse Scalar Multiplication Commutes with Additive Monoid Homomorphisms
Informal description
Let $M$ and $M_2$ be additive commutative groups, and let $F$ be a type of functions from $M$ to $M_2$ that are additive monoid homomorphisms. For any division rings $R$ and $S$ with module structures on $M$ and $M_2$ respectively, any integer $z$, and any element $x \in M$, we have: \[ f\left((z^{-1} : R) \cdot x\right) = (z^{-1} : S) \cdot f(x). \]
inv_natCast_smul_eq theorem
{E : Type*} (R S : Type*) [AddCommMonoid E] [DivisionSemiring R] [DivisionSemiring S] [Module R E] [Module S E] (n : ℕ) (x : E) : (n⁻¹ : R) • x = (n⁻¹ : S) • x
Full source 
/-- If `E` is a vector space over two division semirings `R` and `S`, then scalar multiplications
agree on inverses of natural numbers in `R` and `S`. -/
theorem inv_natCast_smul_eq {E : Type*} (R S : Type*) [AddCommMonoid E] [DivisionSemiring R]
    [DivisionSemiring S] [Module R E] [Module S E] (n : ℕ) (x : E) :
    (n⁻¹ : R) • x = (n⁻¹ : S) • x :=
  map_inv_natCast_smul (AddMonoidHom.id E) R S n x
Agreement of Scalar Multiplication by Natural Number Inverses in Different Division Semirings
Informal description
Let $E$ be an additive commutative monoid equipped with module structures over two division semirings $R$ and $S$. For any natural number $n$ and any element $x \in E$, the scalar multiplication by the inverse of $n$ in $R$ and $S$ agree, i.e., \[ (n^{-1} : R) \cdot x = (n^{-1} : S) \cdot x. \]
inv_intCast_smul_eq theorem
{E : Type*} (R S : Type*) [AddCommGroup E] [DivisionRing R] [DivisionRing S] [Module R E] [Module S E] (n : ℤ) (x : E) : (n⁻¹ : R) • x = (n⁻¹ : S) • x
Full source 
/-- If `E` is a vector space over two division rings `R` and `S`, then scalar multiplications
agree on inverses of integer numbers in `R` and `S`. -/
theorem inv_intCast_smul_eq {E : Type*} (R S : Type*) [AddCommGroup E] [DivisionRing R]
    [DivisionRing S] [Module R E] [Module S E] (n : ℤ) (x : E) : (n⁻¹ : R) • x = (n⁻¹ : S) • x :=
  map_inv_intCast_smul (AddMonoidHom.id E) R S n x
Agreement of Scalar Multiplication by Integer Inverses in Different Division Rings
Informal description
Let $E$ be an additive commutative group equipped with module structures over two division rings $R$ and $S$. For any integer $n$ and any element $x \in E$, the scalar multiplication by the inverse of $n$ in $R$ and $S$ agree, i.e., \[ (n^{-1} : R) \cdot x = (n^{-1} : S) \cdot x. \]
inv_natCast_smul_comm theorem
{α E : Type*} (R : Type*) [AddCommMonoid E] [DivisionSemiring R] [Monoid α] [Module R E] [DistribMulAction α E] (n : ℕ) (s : α) (x : E) : (n⁻¹ : R) • s • x = s • (n⁻¹ : R) • x
Full source 
/-- If `E` is a vector space over a division semiring `R` and has a monoid action by `α`, then that
action commutes by scalar multiplication of inverses of natural numbers in `R`. -/
theorem inv_natCast_smul_comm {α E : Type*} (R : Type*) [AddCommMonoid E] [DivisionSemiring R]
    [Monoid α] [Module R E] [DistribMulAction α E] (n : ℕ) (s : α) (x : E) :
    (n⁻¹ : R) • s • x = s • (n⁻¹ : R) • x :=
  (map_inv_natCast_smul (DistribMulAction.toAddMonoidHom E s) R R n x).symm
Commutation of Inverse Natural Number Scalar Multiplication with Monoid Action
Informal description
Let $E$ be an additive commutative monoid equipped with a module structure over a division semiring $R$, and let $\alpha$ be a monoid acting distributively on $E$. For any natural number $n$, element $s \in \alpha$, and $x \in E$, the scalar multiplication by the inverse of $n$ in $R$ commutes with the action of $s$: \[ (n^{-1} : R) \cdot (s \cdot x) = s \cdot (n^{-1} : R \cdot x). \]
inv_intCast_smul_comm theorem
{α E : Type*} (R : Type*) [AddCommGroup E] [DivisionRing R] [Monoid α] [Module R E] [DistribMulAction α E] (n : ℤ) (s : α) (x : E) : (n⁻¹ : R) • s • x = s • (n⁻¹ : R) • x
Full source 
/-- If `E` is a vector space over a division ring `R` and has a monoid action by `α`, then that
action commutes by scalar multiplication of inverses of integers in `R` -/
theorem inv_intCast_smul_comm {α E : Type*} (R : Type*) [AddCommGroup E] [DivisionRing R]
    [Monoid α] [Module R E] [DistribMulAction α E] (n : ℤ) (s : α) (x : E) :
    (n⁻¹ : R) • s • x = s • (n⁻¹ : R) • x :=
  (map_inv_intCast_smul (DistribMulAction.toAddMonoidHom E s) R R n x).symm
Commutation of Inverse Integer Scalar Multiplication with Monoid Action
Informal description
Let $E$ be an additive commutative group equipped with a module structure over a division ring $R$, and let $\alpha$ be a monoid acting distributively on $E$. For any integer $n$, element $s \in \alpha$, and $x \in E$, the scalar multiplication by the inverse of $n$ in $R$ commutes with the action of $s$: \[ (n^{-1} : R) \cdot (s \cdot x) = s \cdot (n^{-1} : R \cdot x). \]
Function.support_smul_subset_left theorem
[Zero R] [Zero M] [SMulWithZero R M] (f : α → R) (g : α → M) : support (f • g) ⊆ support f
Full source 
lemma support_smul_subset_left [Zero R] [Zero M] [SMulWithZero R M] (f : α → R) (g : α → M) :
    supportsupport (f • g) ⊆ support f := fun x hfg hf ↦
  hfg <| by rw [Pi.smul_apply', hf, zero_smul]
Support of Scalar Product is Contained in Support of Scalar Function
Informal description
Let $R$ and $M$ be types with zero elements, equipped with a scalar multiplication operation `[SMulWithZero R M]`. For any functions $f : \alpha \to R$ and $g : \alpha \to M$, the support of the scalar product function $f \bullet g$ is contained in the support of $f$, i.e., $\mathrm{supp}(f \bullet g) \subseteq \mathrm{supp}(f)$.
Function.support_smul_subset_right theorem
[Zero M] [SMulZeroClass R M] (f : α → R) (g : α → M) : support (f • g) ⊆ support g
Full source 
lemma support_smul_subset_right [Zero M] [SMulZeroClass R M] (f : α → R) (g : α → M) :
    supportsupport (f • g) ⊆ support g :=
  fun x hbf hf ↦ hbf <| by rw [Pi.smul_apply', hf, smul_zero]
Support of Scalar Product is Contained in Support of Function
Informal description
Let $M$ be a type with a zero element and $R$ a type equipped with a scalar multiplication operation on $M$ (`[SMulZeroClass R M]`). For any functions $f : \alpha \to R$ and $g : \alpha \to M$, the support of the pointwise scalar product $f \cdot g$ is a subset of the support of $g$, i.e., \[ \mathrm{supp}(f \cdot g) \subseteq \mathrm{supp}(g). \]
Function.support_const_smul_of_ne_zero theorem
[Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] (c : R) (g : α → M) (hc : c ≠ 0) : support (c • g) = support g
Full source 
lemma support_const_smul_of_ne_zero [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M]
    (c : R) (g : α → M) (hc : c ≠ 0) : support (c • g) = support g :=
  ext fun x ↦ by simp only [hc, mem_support, Pi.smul_apply, Ne, smul_eq_zero, false_or]
Support of Scalar Multiple Equals Support of Function for Nonzero Scalar
Informal description
Let $R$ and $M$ be types with zero elements, equipped with a scalar multiplication operation `[SMulWithZero R M]` such that $R$ has no zero divisors with respect to $M$ (`[NoZeroSMulDivisors R M]`). For any nonzero scalar $c \in R$ (where $c \neq 0$) and any function $g : \alpha \to M$, the support of the scalar multiple function $c \cdot g$ is equal to the support of $g$, i.e., $\mathrm{supp}(c \cdot g) = \mathrm{supp}(g)$.
Function.support_smul theorem
[Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] (f : α → R) (g : α → M) : support (f • g) = support f ∩ support g
Full source 
lemma support_smul [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] (f : α → R)
    (g : α → M) : support (f • g) = supportsupport f ∩ support g :=
  ext fun _ => smul_ne_zero_iff
Support of Pointwise Scalar Product Equals Intersection of Supports
Informal description
Let $R$ and $M$ be types with zero elements, equipped with a scalar multiplication operation $[SMulWithZero R M]$ such that $R$ has no zero divisors with respect to $M$ ($[NoZeroSMulDivisors R M]$). For any functions $f : \alpha \to R$ and $g : \alpha \to M$, the support of the pointwise scalar product $f \cdot g$ is equal to the intersection of the supports of $f$ and $g$, i.e., \[ \mathrm{supp}(f \cdot g) = \mathrm{supp}(f) \cap \mathrm{supp}(g). \]
Function.support_const_smul_subset theorem
[Zero M] [SMulZeroClass R M] (a : R) (f : α → M) : support (a • f) ⊆ support f
Full source 
lemma support_const_smul_subset [Zero M] [SMulZeroClass R M] (a : R) (f : α → M) :
    supportsupport (a • f) ⊆ support f := support_smul_subset_right (fun _ ↦ a) f
Support of Scalar Multiple is Subset of Support of Function
Informal description
Let $M$ be a type with a zero element and $R$ a type equipped with a scalar multiplication operation on $M$ (`[SMulZeroClass R M]`). For any scalar $a \in R$ and any function $f : \alpha \to M$, the support of the scalar multiple function $a \cdot f$ is a subset of the support of $f$, i.e., \[ \mathrm{supp}(a \cdot f) \subseteq \mathrm{supp}(f). \]
Set.indicator_smul_apply theorem
(s : Set α) (r : α → R) (f : α → M) (a : α) : indicator s (fun a ↦ r a • f a) a = r a • indicator s f a
Full source 
lemma indicator_smul_apply (s : Set α) (r : α → R) (f : α → M) (a : α) :
    indicator s (fun a ↦ r a • f a) a = r a • indicator s f a := by
  dsimp only [indicator]
  split_ifs
  exacts [rfl, (smul_zero (r a)).symm]
Pointwise Scalar Multiplication Commutes with Indicator Function
Informal description
For any set $s$ in a type $\alpha$, scalar-valued function $r : \alpha \to R$, vector-valued function $f : \alpha \to M$, and element $a \in \alpha$, the indicator function of $s$ evaluated at the pointwise scalar multiplication $r \cdot f$ at $a$ equals the scalar multiplication of $r(a)$ with the indicator function of $s$ evaluated at $f$ at $a$. That is, \[ \mathbf{1}_s(r \cdot f)(a) = r(a) \cdot \mathbf{1}_s(f)(a). \]
Set.indicator_smul theorem
(s : Set α) (r : α → R) (f : α → M) : indicator s (fun a ↦ r a • f a) = fun a ↦ r a • indicator s f a
Full source 
lemma indicator_smul (s : Set α) (r : α → R) (f : α → M) :
    indicator s (fun a ↦ r a • f a) = fun a ↦ r a • indicator s f a :=
  funext <| indicator_smul_apply s r f
Indicator Function Commutes with Pointwise Scalar Multiplication
Informal description
For any set $s \subseteq \alpha$, scalar-valued function $r : \alpha \to R$, and vector-valued function $f : \alpha \to M$, the indicator function of $s$ applied to the pointwise scalar multiplication $r \cdot f$ equals the pointwise scalar multiplication of $r$ with the indicator function of $s$ applied to $f$. That is, \[ \mathbf{1}_s(r \cdot f) = r \cdot \mathbf{1}_s(f). \]
Set.indicator_const_smul_apply theorem
(s : Set α) (r : R) (f : α → M) (a : α) : indicator s (r • f ·) a = r • indicator s f a
Full source 
lemma indicator_const_smul_apply (s : Set α) (r : R) (f : α → M) (a : α) :
    indicator s (r • f ·) a = r • indicator s f a :=
  indicator_smul_apply s (fun _ ↦ r) f a
Indicator Function Commutes with Constant Scalar Multiplication at a Point
Informal description
For any set $s \subseteq \alpha$, constant scalar $r \in R$, function $f \colon \alpha \to M$, and element $a \in \alpha$, the indicator function of $s$ evaluated at the constant scalar multiple $r \cdot f$ at $a$ equals the scalar multiple $r$ of the indicator function of $s$ evaluated at $f$ at $a$. That is, \[ \mathbf{1}_s(r \cdot f)(a) = r \cdot \mathbf{1}_s(f)(a). \]
Set.indicator_const_smul theorem
(s : Set α) (r : R) (f : α → M) : indicator s (r • f ·) = (r • indicator s f ·)
Full source 
lemma indicator_const_smul (s : Set α) (r : R) (f : α → M) :
    indicator s (r • f ·) = (r • indicator s f ·) :=
  funext <| indicator_const_smul_apply s r f
Indicator Function Commutes with Constant Scalar Multiplication (Global Version)
Informal description
For any set $s \subseteq \alpha$, constant scalar $r \in R$, and function $f \colon \alpha \to M$, the indicator function of $s$ applied to the constant scalar multiple $r \cdot f$ equals the constant scalar multiple $r$ of the indicator function of $s$ applied to $f$. That is, \[ \mathbf{1}_s(r \cdot f) = r \cdot \mathbf{1}_s(f). \]
Set.indicator_smul_apply_left theorem
(s : Set α) (r : α → R) (f : α → M) (a : α) : indicator s (fun a ↦ r a • f a) a = indicator s r a • f a
Full source 
lemma indicator_smul_apply_left (s : Set α) (r : α → R) (f : α → M) (a : α) :
    indicator s (fun a ↦ r a • f a) a = indicator s r a • f a := by
  dsimp only [indicator]
  split_ifs
  exacts [rfl, (zero_smul _ (f a)).symm]
Indicator Function Commutes with Pointwise Scalar Multiplication
Informal description
For any set $s$ over a type $\alpha$, scalar-valued function $r : \alpha \to R$, vector-valued function $f : \alpha \to M$, and element $a \in \alpha$, the indicator function of $s$ applied to the pointwise scalar multiplication $r(a) \cdot f(a)$ evaluated at $a$ equals the scalar multiplication of the indicator function of $s$ applied to $r$ evaluated at $a$ with $f(a)$. In symbols: $$ \mathbf{1}_s(r \cdot f)(a) = \mathbf{1}_s(r)(a) \cdot f(a) $$ where $\mathbf{1}_s$ denotes the indicator function of the set $s$.
Set.indicator_smul_left theorem
(s : Set α) (r : α → R) (f : α → M) : indicator s (fun a ↦ r a • f a) = fun a ↦ indicator s r a • f a
Full source 
lemma indicator_smul_left (s : Set α) (r : α → R) (f : α → M) :
    indicator s (fun a ↦ r a • f a) = fun a ↦ indicator s r a • f a :=
  funext <| indicator_smul_apply_left _ _ _
Indicator Function Commutes with Pointwise Scalar Multiplication (Global Version)
Informal description
For any set $s$ over a type $\alpha$, scalar-valued function $r : \alpha \to R$, and vector-valued function $f : \alpha \to M$, the indicator function of $s$ applied to the pointwise scalar multiplication $r \cdot f$ equals the pointwise scalar multiplication of the indicator function of $s$ applied to $r$ with $f$. In symbols: $$ \mathbf{1}_s(r \cdot f) = \mathbf{1}_s(r) \cdot f $$ where $\mathbf{1}_s$ denotes the indicator function of the set $s$.
Set.indicator_smul_const_apply theorem
(s : Set α) (r : α → R) (m : M) (a : α) : indicator s (r · • m) a = indicator s r a • m
Full source 
lemma indicator_smul_const_apply (s : Set α) (r : α → R) (m : M) (a : α) :
    indicator s (r · • m) a = indicator s r a • m := indicator_smul_apply_left _ _ _ _
Indicator Function Commutes with Constant Scalar Multiplication (Pointwise Version)
Informal description
For any set $s$ over a type $\alpha$, scalar-valued function $r : \alpha \to R$, element $m \in M$, and point $a \in \alpha$, the indicator function of $s$ applied to the scalar multiplication $r(a) \cdot m$ evaluated at $a$ equals the scalar multiplication of the indicator function of $s$ applied to $r$ evaluated at $a$ with $m$. In symbols: $$ \mathbf{1}_s(r \cdot m)(a) = \mathbf{1}_s(r)(a) \cdot m $$ where $\mathbf{1}_s$ denotes the indicator function of the set $s$.
Set.indicator_smul_const theorem
(s : Set α) (r : α → R) (m : M) : indicator s (r · • m) = (indicator s r · • m)
Full source 
lemma indicator_smul_const (s : Set α) (r : α → R) (m : M) :
    indicator s (r · • m) = (indicator s r · • m) :=
  funext <| indicator_smul_const_apply _ _ _
Indicator Function Commutes with Constant Scalar Multiplication (Global Version)
Informal description
For any set $s$ over a type $\alpha$, scalar-valued function $r : \alpha \to R$, and element $m \in M$, the indicator function of $s$ applied to the scalar multiplication $r \cdot m$ equals the scalar multiplication of the indicator function of $s$ applied to $r$ with $m$. In symbols: $$ \mathbf{1}_s(r \cdot m) = \mathbf{1}_s(r) \cdot m $$ where $\mathbf{1}_s$ denotes the indicator function of the set $s$.
Set.smul_indicator_one_apply theorem
(s : Set α) (r : R) (a : α) : r • s.indicator (1 : α → R) a = s.indicator (fun _ ↦ r) a
Full source 
lemma smul_indicator_one_apply (s : Set α) (r : R) (a : α) :
    r • s.indicator (1 : α → R) a = s.indicator (fun _ ↦ r) a := by
  simp_rw [← indicator_const_smul_apply, Pi.one_apply, smul_eq_mul, mul_one]
Scalar Multiplication of Indicator Function with Constant One Equals Constant Scalar Indicator Function
Informal description
For any set $s$ over a type $\alpha$, scalar $r \in R$, and point $a \in \alpha$, the scalar multiplication of $r$ with the indicator function of $s$ evaluated at $a$ (where the indicator function takes the value $1$ on $s$ and $0$ otherwise) equals the indicator function of $s$ evaluated at $a$ (where the indicator function takes the constant value $r$ on $s$ and $0$ otherwise). In symbols: $$ r \cdot \mathbf{1}_s(1)(a) = \mathbf{1}_s(\lambda \_. r)(a) $$ where $\mathbf{1}_s$ denotes the indicator function of the set $s$.