Further results on (semi)linear maps #

source

def LinearMap.ltoFun (R : Type u_6) (M : Type u_7) (N : Type u_8) (A : Type u_9) [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module A N] [SMulCommClass R A N] :

(M →ₗ[R] N) →ₗ[A] M → N

A-linearly coerce an R-linear map from M to N to a function, when N has commuting R-module and A-module structures.

Equations

LinearMap.ltoFun R M N A = { toFun := fun (f : M →ₗ[R] N) => f.toFun, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem LinearMap.ltoFun_apply {R : Type u_6} {M : Type u_7} {N : Type u_8} {A : Type u_9} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module A N] [SMulCommClass R A N] {f : M →ₗ[R] N} :

(ltoFun R M N A) f = ⇑f

source

@[implicit_reducible]

instance LinearMap.instSMulDomMulAct {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] :

SMul S'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M')

Equations

LinearMap.instSMulDomMulAct = { smul := fun (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M') => { toFun := a • ⇑f, map_add' := ⋯, map_smul' := ⋯ } }

source

theorem DomMulAct.smul_linearMap_apply {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M') (x : M) :

(a • f) x = f (mk.symm a • x)

source

@[simp]

theorem DomMulAct.mk_smul_linearMap_apply {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S') (f : M →ₛₗ[σ₁₂] M') (x : M) :

(mk a • f) x = f (a • x)

source

theorem DomMulAct.coe_smul_linearMap {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M') :

⇑(a • f) = a • ⇑f

source

instance LinearMap.instSMulCommClassDomMulAct {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} {T' : Type u_7} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] [Monoid T'] [DistribMulAction T' M] [SMulCommClass R T' M] [SMulCommClass S' T' M] :

SMulCommClass S'ᵈᵐᵃ T'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M')

source

@[implicit_reducible]

instance LinearMap.instDistribMulActionDomMulActOfSMulCommClass {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] :

DistribMulAction S'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M')

Equations

LinearMap.instDistribMulActionDomMulActOfSMulCommClass = { toSMul := LinearMap.instSMulDomMulAct, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

source

instance LinearMap.instIsTorsionFree {R : Type u_1} {R' : Type u_2} {S : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} [Semiring S] [Module S M'] [SMulCommClass R' S M'] [Module.IsTorsionFree S M'] :

Module.IsTorsionFree S (M →ₛₗ[σ₁₂] M')

source

@[implicit_reducible]

instance LinearMap.instModuleDomMulActOfSMulCommClass {R : Type u_1} {R' : Type u_2} {S : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} [Semiring S] [Module S M] [SMulCommClass R S M] :

Module Sᵈᵐᵃ (M →ₛₗ[σ₁₂] M')

Equations

LinearMap.instModuleDomMulActOfSMulCommClass = { toDistribMulAction := LinearMap.instDistribMulActionDomMulActOfSMulCommClass, add_smul := ⋯, zero_smul := ⋯ }

source

@[simp]

theorem LinearMap.mulLeft_mul (R : Type u_6) (A : Type u_7) [Semiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] (a b : A) :

mulLeft R (a * b) = mulLeft R a ∘ₗ mulLeft R b

source

@[simp]

theorem LinearMap.mulRight_mul (R : Type u_6) (A : Type u_7) [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] (a b : A) :

mulRight R (a * b) = mulRight R b ∘ₗ mulRight R a

source

@[simp]

theorem LinearMap.mulLeft_inj {R : Type u_6} {A : Type u_7} [Semiring R] [NonAssocSemiring A] [Module R A] [SMulCommClass R A A] {a b : A} :

mulLeft R a = mulLeft R b ↔ a = b

source

@[simp]

theorem LinearMap.mulRight_inj {R : Type u_6} {A : Type u_7} [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] {a b : A} :

mulRight R a = mulRight R b ↔ a = b

source

@[simp]

theorem LinearMap.mulLeft_one (R : Type u_6) (A : Type u_7) [Semiring R] [NonAssocSemiring A] [Module R A] [SMulCommClass R A A] :

mulLeft R 1 = id

source

@[simp]

theorem LinearMap.mulLeft_eq_zero_iff (R : Type u_6) (A : Type u_7) [Semiring R] [NonAssocSemiring A] [Module R A] [SMulCommClass R A A] (a : A) :

mulLeft R a = 0 ↔ a = 0

source

@[simp]

theorem LinearMap.mulRight_one (R : Type u_6) (A : Type u_7) [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] :

mulRight R 1 = id

source

@[simp]

theorem LinearMap.mulRight_eq_zero_iff (R : Type u_6) (A : Type u_7) [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] (a : A) :

mulRight R a = 0 ↔ a = 0

source

def Sum.elimZeroLeft {ι : Type u_6} {κ : Type u_7} {R : Type u_8} [Semiring R] :

(ι → R) →ₗ[R] κ ⊕ ι → R

The map Sum.elim specialised with zero in the first argument, as a linear map.

Equations

Sum.elimZeroLeft = { toFun := Sum.elim 0, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem Sum.elimZeroLeft_apply {ι : Type u_6} {κ : Type u_7} {R : Type u_8} [Semiring R] (g : ι → R) (a✝ : κ ⊕ ι) :

elimZeroLeft g a✝ = Sum.elim 0 g a✝

source

def Sum.elimZeroRight {ι : Type u_6} {κ : Type u_7} {R : Type u_8} [Semiring R] :

(ι → R) →ₗ[R] ι ⊕ κ → R

The map Sum.elim specialised with zero in the second argument, as a linear map.

Equations

Sum.elimZeroRight = { toFun := fun (f : ι → R) => Sum.elim f 0, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem Sum.elimZeroRight_apply {ι : Type u_6} {κ : Type u_7} {R : Type u_8} [Semiring R] (f : ι → R) (a✝ : ι ⊕ κ) :

elimZeroRight f a✝ = Sum.elim f 0 a✝

Documentation

Mathlib.Algebra.Module.LinearMap.Basic

Further results on (semi)linear maps #