Mathlib.LinearAlgebra.Basis.SMul

Basis.instSMul instance

: SMul G (Basis ι R M)

Full source

/-- The action on a `Basis` by acting on each element.

See also `Basis.unitsSMul` and `Basis.groupSMul`, for the cases when a different action is applied
to each basis element. -/
instance : SMul G (Basis ι R M) where
  smul g b := b.map <| DistribMulAction.toLinearEquiv _ _ g

Scalar Multiplication of Basis Vectors by Group Elements

Informal description

For any group $G$ acting on a module $M$ over a ring $R$ with basis indexed by $\iota$, there is a natural action of $G$ on the basis vectors where each basis vector is scaled by the corresponding group element. Specifically, if $b$ is a basis of $M$ and $g \in G$, then the action $g \cdot b$ is defined by $(g \cdot b)(i) = g \cdot b(i)$ for each index $i \in \iota$.

Basis.smul_apply theorem

(g : G) (b : Basis ι R M) (i : ι) : (g • b) i = g • b i

Full source

@[simp]
theorem smul_apply (g : G) (b : Basis ι R M) (i : ι) : (g • b) i = g • b i := rfl

Scalar Action on Basis Vectors: $(g \cdot b)(i) = g \cdot b(i)$

Informal description

Let $G$ be a group acting on a module $M$ over a ring $R$ with basis $\{b_i\}_{i \in \iota}$. For any $g \in G$, basis $b$, and index $i \in \iota$, the $i$-th basis vector of the scaled basis $g \cdot b$ is equal to $g$ acting on the $i$-th basis vector of $b$, i.e., $(g \cdot b)(i) = g \cdot b(i)$.

Basis.coe_smul theorem

(g : G) (b : Basis ι R M) : ⇑(g • b) = g • ⇑b

Full source

@[norm_cast] theorem coe_smul (g : G) (b : Basis ι R M) : ⇑(g • b) = g • ⇑b := rfl

Scalar Multiplication of Basis Vectors Preserves Function Representation

Informal description

For any group element $g \in G$ and basis $b$ of a module $M$ over a ring $R$ indexed by $\iota$, the function representation of the scaled basis $g \cdot b$ is equal to the pointwise scalar multiplication of $g$ with the function representation of $b$. That is, $(g \cdot b)(i) = g \cdot b(i)$ for all $i \in \iota$.

Basis.smul_eq_map theorem

(g : M ≃ₗ[R] M) (b : Basis ι R M) : g • b = b.map g

Full source

/-- When the group in question is the automorphisms, `•` coincides with `Basis.map`. -/
@[simp]
theorem smul_eq_map (g : M ≃ₗ[R] M) (b : Basis ι R M) : g • b = b.map g := rfl

Scalar Multiplication of Basis by Automorphism Equals Basis Mapping

Informal description

For any linear automorphism $g : M \simeq_{R} M$ and any basis $b$ of an $R$-module $M$ indexed by $\iota$, the scalar multiplication of $b$ by $g$ is equal to the basis obtained by applying $g$ to each basis vector of $b$, i.e., $g \cdot b = b.map\, g$.

Basis.repr_smul theorem

(g : G) (b : Basis ι R M) : (g • b).repr = (DistribMulAction.toLinearEquiv _ _ g).symm.trans b.repr

Full source

@[simp] theorem repr_smul (g : G) (b : Basis ι R M) :
    (g • b).repr = (DistribMulAction.toLinearEquiv _ _ g).symm.trans b.repr := rfl

Representation Isomorphism of Scaled Basis

Informal description

Let $G$ be a group acting on a module $M$ over a ring $R$ with basis $b$ indexed by $\iota$. For any $g \in G$, the representation isomorphism of the scaled basis $g \cdot b$ is equal to the composition of the inverse of the linear equivalence induced by the group action $g$ with the representation isomorphism of the original basis $b$. In other words, the following equality holds: $$(g \cdot b)^\text{repr} = (\text{DistribMulAction.toLinearEquiv}_R^M g)^{-1} \circ b^\text{repr}.$$

Basis.instMulAction instance

: MulAction G (Basis ι R M)

Full source

instance : MulAction G (Basis ι R M) :=
  Function.Injective.mulAction _ DFunLike.coe_injective coe_smul

Multiplicative Group Action on Bases of a Module

Informal description

For any group $G$ acting on a module $M$ over a ring $R$ with basis indexed by $\iota$, the set of bases of $M$ forms a multiplicative $G$-action, where the action of $G$ on a basis $b$ is given by $(g \cdot b)(i) = g \cdot b(i)$ for each $g \in G$ and each index $i \in \iota$.

Basis.instSMulCommClass instance

[SMulCommClass G G' M] : SMulCommClass G G' (Basis ι R M)

Full source

instance [SMulCommClass G G' M] : SMulCommClass G G' (Basis ι R M) where
  smul_comm _g _g' _b := DFunLike.ext _ _ fun _ => smul_comm _ _ _

Commuting Scalar Actions on a Basis

Informal description

For any two scalar actions $G$ and $G'$ on a module $M$ over a ring $R$ that commute with each other, the induced scalar actions on a basis $\iota$ of $M$ also commute.

Basis.instIsScalarTower instance

[SMul G G'] [IsScalarTower G G' M] : IsScalarTower G G' (Basis ι R M)

Full source

instance [SMul G G'] [IsScalarTower G G' M] : IsScalarTower G G' (Basis ι R M) where
  smul_assoc _g _g' _b := DFunLike.ext _ _ fun _ => smul_assoc _ _ _

Compatibility of Scalar Actions on Basis Vectors

Informal description

For any groups $G$ and $G'$ acting on a module $M$ over a ring $R$ with basis indexed by $\iota$, if the scalar multiplication of $G$ and $G'$ on $M$ is compatible (i.e., $g \cdot (g' \cdot m) = (g \cdot g') \cdot m$ for all $g \in G$, $g' \in G'$, and $m \in M$), then the induced scalar multiplication on the basis vectors is also compatible. Specifically, for any basis $b$ of $M$, the action satisfies $(g \cdot (g' \cdot b))(i) = (g \cdot g') \cdot b(i)$ for each index $i \in \iota$.

Basis.groupSMul_span_eq_top theorem

 {G : Type*} [Group G] [SMul G R] [MulAction G M] [IsScalarTower G R M] {v : ι → M}
  (hv : Submodule.span R (Set.range v) = ⊤) {w : ι → G} : Submodule.span R (Set.range (w • v)) = ⊤

Full source

theorem groupSMul_span_eq_top {G : Type*} [Group G] [SMul G R] [MulAction G M]
    [IsScalarTower G R M] {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) {w : ι → G} :
    Submodule.span R (Set.range (w • v)) = ⊤ := by
  rw [eq_top_iff]
  intro j hj
  rw [← hv] at hj
  rw [Submodule.mem_span] at hj ⊢
  refine fun p hp => hj p fun u hu => ?_
  obtain ⟨i, rfl⟩ := hu
  have : ((w i)⁻¹ • (1 : R)) • w i • v i ∈ p := p.smul_mem ((w i)⁻¹ • (1 : R)) (hp ⟨i, rfl⟩)
  rwa [smul_one_smul, inv_smul_smul] at this

Span Preservation under Group Action on Basis Vectors

Informal description

Let $G$ be a group acting on a module $M$ over a ring $R$ such that the action is compatible with the scalar multiplication (i.e., $[IsScalarTower\, G\, R\, M]$). Suppose $v : \iota \to M$ is a family of vectors whose $R$-linear span is the entire module $M$ (i.e., $\text{span}_R (\text{range}\, v) = \top$). Then for any family of group elements $w : \iota \to G$, the $R$-linear span of the family $w \cdot v$ (where $\cdot$ denotes the scalar multiplication) is also the entire module $M$, i.e., $\text{span}_R (\text{range}\, (w \cdot v)) = \top$.

Basis.groupSMul definition

 {G : Type*} [Group G] [DistribMulAction G R] [DistribMulAction G M] [IsScalarTower G R M] [SMulCommClass G R M]
  (v : Basis ι R M) (w : ι → G) : Basis ι R M

Full source

/-- Given a basis `v` and a map `w` such that for all `i`, `w i` are elements of a group,
`groupSMul` provides the basis corresponding to `w • v`. -/
def groupSMul {G : Type*} [Group G] [DistribMulAction G R] [DistribMulAction G M]
    [IsScalarTower G R M] [SMulCommClass G R M] (v : Basis ι R M) (w : ι → G) : Basis ι R M :=
  Basis.mk (LinearIndependent.group_smul v.linearIndependent w) (groupSMul_span_eq_top v.span_eq).ge

Basis scaled by group elements

Informal description

Given a basis $v$ of a module $M$ over a ring $R$ indexed by a type $\iota$, and a family of group elements $w : \iota \to G$ where $G$ is a group acting distributively on both $R$ and $M$ with compatible scalar multiplication (i.e., $[IsScalarTower\, G\, R\, M]$ and $[SMulCommClass\, G\, R\, M]$), the function `Basis.groupSMul` constructs a new basis for $M$ where each basis vector $v_i$ is scaled by the corresponding group element $w_i$.

Basis.groupSMul_apply theorem

 {G : Type*} [Group G] [DistribMulAction G R] [DistribMulAction G M] [IsScalarTower G R M] [SMulCommClass G R M]
  {v : Basis ι R M} {w : ι → G} (i : ι) : v.groupSMul w i = (w • (v : ι → M)) i

Full source

theorem groupSMul_apply {G : Type*} [Group G] [DistribMulAction G R] [DistribMulAction G M]
    [IsScalarTower G R M] [SMulCommClass G R M] {v : Basis ι R M} {w : ι → G} (i : ι) :
    v.groupSMul w i = (w • (v : ι → M)) i :=
  mk_apply (LinearIndependent.group_smul v.linearIndependent w)
    (groupSMul_span_eq_top v.span_eq).ge i

Scaled Basis Vector Formula: $(v.\text{groupSMul}\, w)_i = w_i \cdot v_i$

Informal description

Let $G$ be a group acting distributively on a ring $R$ and a module $M$ over $R$, with compatible scalar multiplication (i.e., $[IsScalarTower\, G\, R\, M]$ and $[SMulCommClass\, G\, R\, M]$). Given a basis $v$ of $M$ indexed by $\iota$ and a family of group elements $w : \iota \to G$, the $i$-th basis vector of the scaled basis $v.\text{groupSMul}\, w$ is equal to $w_i \cdot v_i$, where $\cdot$ denotes the scalar multiplication. In other words, $(v.\text{groupSMul}\, w)_i = w_i \cdot v_i$ for all $i \in \iota$.

Basis.units_smul_span_eq_top theorem

 {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) {w : ι → Rˣ} : Submodule.span R (Set.range (w • v)) = ⊤

Full source

theorem units_smul_span_eq_top {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) {w : ι → Rˣ} :
    Submodule.span R (Set.range (w • v)) = ⊤ :=
  groupSMul_span_eq_top hv

Span Preservation under Unit Scalar Multiplication of Basis Vectors

Informal description

Let $R$ be a ring and $M$ an $R$-module. Given a family of vectors $v : \iota \to M$ whose $R$-linear span is the entire module $M$ (i.e., $\text{span}_R (\text{range}\, v) = \top$), then for any family of units $w : \iota \to R^\times$ in $R$, the $R$-linear span of the family $w \cdot v$ (where $\cdot$ denotes the scalar multiplication) is also the entire module $M$, i.e., $\text{span}_R (\text{range}\, (w \cdot v)) = \top$.

Basis.unitsSMul definition

(v : Basis ι R M) (w : ι → Rˣ) : Basis ι R M

Full source

/-- Given a basis `v` and a map `w` such that for all `i`, `w i` is a unit, `unitsSMul`
provides the basis corresponding to `w • v`. -/
def unitsSMul (v : Basis ι R M) (w : ι → Rˣ) : Basis ι R M :=
  Basis.mk (LinearIndependent.units_smul v.linearIndependent w)
    (units_smul_span_eq_top v.span_eq).ge

Basis scaled by units

Informal description

Given a basis $v$ of a module $M$ over a ring $R$ indexed by a type $\iota$ and a family of units $w : \iota \to R^\times$, the function `unitsSMul` constructs a new basis for $M$ where each basis vector $v_i$ is scaled by the corresponding unit $w_i$. The resulting basis vectors are given by $w_i \cdot v_i$ for each $i \in \iota$.

Basis.unitsSMul_apply theorem

{v : Basis ι R M} {w : ι → Rˣ} (i : ι) : unitsSMul v w i = w i • v i

Full source

theorem unitsSMul_apply {v : Basis ι R M} {w : ι → Rˣ} (i : ι) : unitsSMul v w i = w i • v i :=
  mk_apply (LinearIndependent.units_smul v.linearIndependent w)
    (units_smul_span_eq_top v.span_eq).ge i

Basis Vector Scaling by Units: $(\text{unitsSMul}\, v\, w)_i = w_i \cdot v_i$

Informal description

Let $M$ be a module over a ring $R$ with basis $v$ indexed by $\iota$, and let $w : \iota \to R^\times$ be a family of units in $R$. For any index $i \in \iota$, the $i$-th basis vector of the scaled basis $\text{unitsSMul}\, v\, w$ is equal to $w_i \cdot v_i$, i.e., $$(\text{unitsSMul}\, v\, w)_i = w_i \cdot v_i.$$

Basis.coord_unitsSMul theorem

(e : Basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) : (unitsSMul e w).coord i = (w i)⁻¹ • e.coord i

Full source

@[simp]
theorem coord_unitsSMul (e : Basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) :
    (unitsSMul e w).coord i = (w i)⁻¹ • e.coord i := by
  classical
    apply e.ext
    intro j
    trans ((unitsSMul e w).coord i) ((w j)⁻¹ • (unitsSMul e w) j)
    · congr
      simp [Basis.unitsSMul, ← mul_smul]
    simp only [Basis.coord_apply, LinearMap.smul_apply, Basis.repr_self, Units.smul_def,
      map_smul, Finsupp.single_apply]
    split_ifs with h <;> simp [h]

Coordinate Function of Scaled Basis: $(\text{unitsSMul}\, e\, w).\text{coord}\, i = (w_i)^{-1} \cdot (e.\text{coord}\, i)$

Informal description

Let $M$ be a module over a ring $R_2$ with basis $e$ indexed by $\iota$, and let $w : \iota \to R_2^\times$ be a family of units in $R_2$. For any index $i \in \iota$, the coordinate function of the scaled basis $\text{unitsSMul}\, e\, w$ at $i$ is given by $(w_i)^{-1}$ times the coordinate function of the original basis $e$ at $i$, i.e., $$(\text{unitsSMul}\, e\, w).\text{coord}\, i = (w_i)^{-1} \cdot (e.\text{coord}\, i).$$

Basis.repr_unitsSMul theorem

(e : Basis ι R₂ M) (w : ι → R₂ˣ) (v : M) (i : ι) : (e.unitsSMul w).repr v i = (w i)⁻¹ • e.repr v i

Full source

@[simp]
theorem repr_unitsSMul (e : Basis ι R₂ M) (w : ι → R₂ˣ) (v : M) (i : ι) :
    (e.unitsSMul w).repr v i = (w i)⁻¹ • e.repr v i :=
  congr_arg (fun f : M →ₗ[R₂] R₂ => f v) (e.coord_unitsSMul w i)

Coordinate Representation in Scaled Basis: $(\text{unitsSMul}\, e\, w).\text{repr}\, v\, i = (w_i)^{-1} \cdot (e.\text{repr}\, v\, i)$

Informal description

Let $M$ be a module over a ring $R_2$ with basis $e$ indexed by $\iota$, and let $w : \iota \to R_2^\times$ be a family of units in $R_2$. For any vector $v \in M$ and any index $i \in \iota$, the $i$-th coordinate of $v$ in the scaled basis $\text{unitsSMul}\, e\, w$ is equal to $(w_i)^{-1}$ times the $i$-th coordinate of $v$ in the original basis $e$, i.e., $$(\text{unitsSMul}\, e\, w).\text{repr}\, v\, i = (w_i)^{-1} \cdot (e.\text{repr}\, v\, i).$$

Basis.isUnitSMul definition

(v : Basis ι R M) {w : ι → R} (hw : ∀ i, IsUnit (w i)) : Basis ι R M

Full source

/-- A version of `unitsSMul` that uses `IsUnit`. -/
def isUnitSMul (v : Basis ι R M) {w : ι → R} (hw : ∀ i, IsUnit (w i)) : Basis ι R M :=
  unitsSMul v fun i => (hw i).unit

Basis scaled by units (using `IsUnit`)

Informal description

Given a basis $v$ of a module $M$ over a ring $R$ indexed by a type $\iota$ and a family of elements $w : \iota \to R$ where each $w_i$ is a unit, the function `isUnitSMul` constructs a new basis for $M$ where each basis vector $v_i$ is scaled by the corresponding unit $w_i$. The resulting basis vectors are given by $w_i \cdot v_i$ for each $i \in \iota$.

Basis.isUnitSMul_apply theorem

{v : Basis ι R M} {w : ι → R} (hw : ∀ i, IsUnit (w i)) (i : ι) : v.isUnitSMul hw i = w i • v i

Full source

theorem isUnitSMul_apply {v : Basis ι R M} {w : ι → R} (hw : ∀ i, IsUnit (w i)) (i : ι) :
    v.isUnitSMul hw i = w i • v i :=
  unitsSMul_apply i

Basis Vector Scaling by Units: $(v.\text{isUnitSMul}\, hw)_i = w_i \cdot v_i$

Informal description

Let $M$ be a module over a ring $R$ with basis $v$ indexed by $\iota$, and let $w : \iota \to R$ be a family of elements where each $w_i$ is a unit. For any index $i \in \iota$, the $i$-th basis vector of the scaled basis $v.\text{isUnitSMul}\, hw$ is equal to $w_i \cdot v_i$, i.e., $$(v.\text{isUnitSMul}\, hw)_i = w_i \cdot v_i.$$

Basis.repr_isUnitSMul theorem

 {v : Basis ι R₂ M} {w : ι → R₂} (hw : ∀ i, IsUnit (w i)) (x : M) (i : ι) :
  (v.isUnitSMul hw).repr x i = (hw i).unit⁻¹ • v.repr x i

Full source

theorem repr_isUnitSMul {v : Basis ι R₂ M} {w : ι → R₂} (hw : ∀ i, IsUnit (w i)) (x : M) (i : ι) :
    (v.isUnitSMul hw).repr x i = (hw i).unit⁻¹ • v.repr x i :=
  repr_unitsSMul _ _ _ _

Coordinate Representation in Unit-Scaled Basis: $(v.\text{isUnitSMul}\, hw).\text{repr}\, x\, i = (hw_i).\text{unit}^{-1} \cdot (v.\text{repr}\, x\, i)$

Informal description

Let $M$ be a module over a ring $R_2$ with basis $v$ indexed by $\iota$, and let $w : \iota \to R_2$ be a family of elements where each $w_i$ is a unit. For any vector $x \in M$ and any index $i \in \iota$, the $i$-th coordinate of $x$ in the scaled basis $v.\text{isUnitSMul}\, hw$ is equal to the inverse of the unit $(hw_i).\text{unit}$ multiplied by the $i$-th coordinate of $x$ in the original basis $v$, i.e., $$(v.\text{isUnitSMul}\, hw).\text{repr}\, x\, i = (hw_i).\text{unit}^{-1} \cdot (v.\text{repr}\, x\, i).$$