Bases and scalar multiplication

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

@[instance_reducible]

noncomputable instance Module.Basis.instSMul {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_5} [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

• Module.Basis.instSMul = { smul := fun (g : G) (b : Module.Basis ι R M) => b.map (DistribMulAction.toLinearEquiv R M g) }

@[simp]

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

theorem Module.Basis.coe_smul {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_5} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) (b : Basis ι R M) : ⇑(g • b) = g • ⇑b

@[simp]

theorem Module.Basis.smul_eq_map {ι : Type u_1} {R : Type u_2} {M : Type u_4} [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.

@[simp]

theorem Module.Basis.repr_smul {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_5} [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

@[instance_reducible]

noncomputable instance Module.Basis.instMulAction {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_5} [Group G] [DistribMulAction G M] [SMulCommClass G R M] : MulAction G (Basis ι R M)

Equations

• Module.Basis.instMulAction = Function.Injective.mulAction DFunLike.coe ⋯ ⋯

instance Module.Basis.instSMulCommClass {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_5} {G' : Type u_6} [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)

instance Module.Basis.instIsScalarTower {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_5} {G' : Type u_6} [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)

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

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

• v.groupSMul w = Module.Basis.mk ⋯ ⋯

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

theorem Module.Basis.units_smul_span_eq_top {ι : Type u_1} {R : Type u_2} {M : Type u_4} [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)) = ⊤

noncomputable def Module.Basis.unitsSMul {ι : Type u_1} {R : Type u_2} {M : Type u_4} [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

• v.unitsSMul w = Module.Basis.mk ⋯ ⋯

theorem Module.Basis.unitsSMul_apply {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {v : Basis ι R M} {w : ι → Rˣ} (i : ι) : (v.unitsSMul w) i = w i • v i

@[simp]

theorem Module.Basis.coord_unitsSMul {ι : Type u_1} {R₂ : Type u_3} {M : Type u_4} [AddCommMonoid M] [CommSemiring R₂] [Module R₂ M] (e : Basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) : (e.unitsSMul w).coord i = (w i)⁻¹ • e.coord i

@[simp]

theorem Module.Basis.repr_unitsSMul {ι : Type u_1} {R₂ : Type u_3} {M : Type u_4} [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

noncomputable def Module.Basis.isUnitSMul {ι : Type u_1} {R : Type u_2} {M : Type u_4} [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

• v.isUnitSMul hw = v.unitsSMul fun (i : ι) => ⋯.unit

theorem Module.Basis.isUnitSMul_apply {ι : Type u_1} {R : Type u_2} {M : Type u_4} [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

theorem Module.Basis.repr_isUnitSMul {ι : Type u_1} {R₂ : Type u_3} {M : Type u_4} [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