Bases and scalar multiplication #

This file defines the scalar multiplication of bases by multiplying each basis vector.

instance Basis.instSMul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_7} [Group G] [DistribMulAction G M] [SMulCommClass G R M] :

SMul G (Basis ι R M)

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.

Equations

source

@[simp]

theorem Basis.smul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_7} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) (b : Basis ι R M) (i : ι) :

(g • b) i = g • b i

source

theorem Basis.coe_smul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_7} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) (b : Basis ι R M) :

⇑(g • b) = g • ⇑b

source

@[simp]

theorem Basis.smul_eq_map {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (g : M ≃ₗ[R] M) (b : Basis ι R M) :

g • b = b.map g

When the group in question is the automorphisms, • coincides with Basis.map.

source

@[simp]

theorem Basis.repr_smul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_7} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) (b : Basis ι R M) :

(g • b).repr = (DistribMulAction.toLinearEquiv R M g).symm ≪≫ₗ b.repr

source

instance Basis.instMulAction {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_7} [Group G] [DistribMulAction G M] [SMulCommClass G R M] :

MulAction G (Basis ι R M)

Equations

source

instance Basis.instSMulCommClass {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_7} {G' : Type u_8} [Group G] [Group G'] [DistribMulAction G M] [DistribMulAction G' M] [SMulCommClass G R M] [SMulCommClass G' R M] [SMulCommClass G G' M] :

SMulCommClass G G' (Basis ι R M)

source

instance Basis.instIsScalarTower {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_7} {G' : Type u_8} [Group G] [Group G'] [DistribMulAction G M] [DistribMulAction G' M] [SMulCommClass G R M] [SMulCommClass G' R M] [SMul G G'] [IsScalarTower G G' M] :

IsScalarTower G G' (Basis ι R M)

source

theorem Basis.groupSMul_span_eq_top {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_7} [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)) = ⊤

source

def Basis.groupSMul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_7} [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

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.

Equations

Instances For

source

theorem Basis.groupSMul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_7} [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) i

source

theorem Basis.units_smul_span_eq_top {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) {w : ι → Rˣ} :

Submodule.span R (Set.range (w • v)) = ⊤

source

def Basis.unitsSMul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (v : Basis ι R M) (w : ι → Rˣ) :

Basis ι R M

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.

Equations

Instances For

source

theorem Basis.unitsSMul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : Basis ι R M} {w : ι → Rˣ} (i : ι) :

(v.unitsSMul w) i = w i • v i

source

@[simp]

theorem Basis.coord_unitsSMul {ι : Type u_1} {R₂ : Type u_4} {M : Type u_5} [AddCommMonoid M] [CommSemiring R₂] [Module R₂ M] (e : Basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) :

(e.unitsSMul w).coord i = (w i)⁻¹ • e.coord i

source

@[simp]

theorem Basis.repr_unitsSMul {ι : Type u_1} {R₂ : Type u_4} {M : Type u_5} [AddCommMonoid M] [CommSemiring R₂] [Module R₂ M] (e : Basis ι R₂ M) (w : ι → R₂ˣ) (v : M) (i : ι) :

((e.unitsSMul w).repr v) i = (w i)⁻¹ • (e.repr v) i

source

def Basis.isUnitSMul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (v : Basis ι R M) {w : ι → R} (hw : ∀ (i : ι), IsUnit (w i)) :

Basis ι R M

A version of unitsSMul that uses IsUnit.

Equations

Instances For

source

theorem Basis.isUnitSMul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : Basis ι R M} {w : ι → R} (hw : ∀ (i : ι), IsUnit (w i)) (i : ι) :

(v.isUnitSMul hw) i = w i • v i

source

theorem Basis.repr_isUnitSMul {ι : Type u_1} {R₂ : Type u_4} {M : Type u_5} [AddCommMonoid M] [CommSemiring R₂] [Module R₂ M] {v : Basis ι R₂ M} {w : ι → R₂} (hw : ∀ (i : ι), IsUnit (w i)) (x : M) (i : ι) :

((v.isUnitSMul hw).repr x) i = ⋯.unit⁻¹ • (v.repr x) i

Documentation

Mathlib.LinearAlgebra.Basis.SMul

Bases and scalar multiplication #