(Semi)linear maps

In this file we define

• LinearMap σ M M₂, M →ₛₗ[σ] M₂ : a semilinear map between two Modules. Here, σ is a RingHom from R to R₂ and an f : M →ₛₗ[σ] M₂ satisfies f (c • x) = (σ c) • (f x). We recover plain linear maps by choosing σ to be RingHom.id R. This is denoted by M →ₗ[R] M₂. We also add the notation M →ₗ⋆[R] M₂ for star-linear maps.

• IsLinearMap R f : predicate saying that f : M → M₂ is a linear map. (Note that this was not generalized to semilinear maps.)

We then provide LinearMap with the following instances:

• LinearMap.addCommMonoid and LinearMap.addCommGroup: the elementwise addition structures corresponding to addition in the codomain
• LinearMap.distribMulAction and LinearMap.module: the elementwise scalar action structures corresponding to applying the action in the codomain.

Implementation notes

To ensure that composition works smoothly for semilinear maps, we use the typeclasses RingHomCompTriple, RingHomInvPair and RingHomSurjective from Mathlib.Algebra.Ring.CompTypeclasses.

Notation

• Throughout the file, we denote regular linear maps by fₗ, gₗ, etc, and semilinear maps by f, g, etc.

TODO

• Parts of this file have not yet been generalized to semilinear maps (i.e. CompatibleSMul)

Tags

linear map

structure IsLinearMap (R : Type u) {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M → M₂) : Prop

A map f between modules over a semiring is linear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = c • f x. The predicate IsLinearMap R f asserts this property. A bundled version is available with LinearMap, and should be favored over IsLinearMap most of the time.

• map_add : ∀ (x y : M), f (x + y) = f x + f y

  A linear map preserves addition.

• map_smul : ∀ (c : R) (x : M), f (c • x) = c • f x

  A linear map preserves scalar multiplication.

theorem IsLinearMap.map_add {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {f : M → M₂} (self : IsLinearMap R f) (x : M) (y : M) : f (x + y) = f x + f y

A linear map preserves addition.

theorem IsLinearMap.map_smul {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {f : M → M₂} (self : IsLinearMap R f) (c : R) (x : M) : f (c • x) = c • f x

A linear map preserves scalar multiplication.

structure LinearMap {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type u_16) (M₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends AddHom , MulActionHom : Type (max u_16 u_17)

A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x. Elements of LinearMap σ M M₂ (available under the notation M →ₛₗ[σ] M₂) are bundled versions of such maps. For plain linear maps (i.e. for which σ = RingHom.id R), the notation M →ₗ[R] M₂ is available. An unbundled version of plain linear maps is available with the predicate IsLinearMap, but it should be avoided most of the time.

@[reducible]

abbrev LinearMap.toMulActionHom {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] {σ : R →+* S} {M : Type u_16} {M₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] (self : M →ₛₗ[σ] M₂) : M →ₑ[⇑σ] M₂

The MulActionHom underlying a LinearMap.

Equations

• self.toMulActionHom = { toFun := self.toFun, map_smul' := ⋯ }

def «term_→ₛₗ[_]_» : Lean.TrailingParserDescr

M →ₛₗ[σ] N is the type of σ-semilinear maps from M to N.

Equations

• One or more equations did not get rendered due to their size.

def «term_→ₗ[_]_» : Lean.TrailingParserDescr

M →ₗ[R] N is the type of R-linear maps from M to N.

Equations

• One or more equations did not get rendered due to their size.

class SemilinearMapClass (F : Type u_14) {R : outParam (Type u_15)} {S : outParam (Type u_16)} [Semiring R] [Semiring S] (σ : outParam (R →+* S)) (M : outParam (Type u_17)) (M₂ : outParam (Type u_18)) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] [FunLike F M M₂] extends AddHomClass , MulActionSemiHomClass : Prop

SemilinearMapClass F σ M M₂ asserts F is a type of bundled σ-semilinear maps M → M₂.

See also LinearMapClass F R M M₂ for the case where σ is the identity map on R.

A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

@[reducible, inline]

abbrev LinearMapClass (F : Type u_14) (R : outParam (Type u_15)) (M : Type u_16) (M₂ : Type u_17) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [FunLike F M M₂] : Prop

LinearMapClass F R M M₂ asserts F is a type of bundled R-linear maps M → M₂.

This is an abbreviation for SemilinearMapClass F (RingHom.id R) M M₂.

Equations

• LinearMapClass F R M M₂ = SemilinearMapClass F (RingHom.id R) M M₂

theorem LinearMapClass.map_smul {R : outParam (Type u_14)} {M : outParam (Type u_15)} {M₂ : outParam (Type u_16)} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {F : Type u_17} [FunLike F M M₂] [LinearMapClass F R M M₂] (f : F) (r : R) (x : M) : f (r • x) = r • f x

@[instance 100]

instance SemilinearMapClass.instAddMonoidHomClass {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} (F : Type u_14) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] : AddMonoidHomClass F M M₃

Equations

• ⋯ = ⋯

@[instance 100]

instance SemilinearMapClass.distribMulActionSemiHomClass {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} (F : Type u_14) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] : DistribMulActionSemiHomClass F (⇑σ) M M₃

Equations

• ⋯ = ⋯

theorem SemilinearMapClass.map_smul_inv {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} {F : Type u_14} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : F) [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) : c • f x = f (σ' c • x)

def SemilinearMapClass.semilinearMap {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} {F : Type u_14} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : F) [FunLike F M M₃] [SemilinearMapClass F σ M M₃] : M →ₛₗ[σ] M₃

Reinterpret an element of a type of semilinear maps as a semilinear map.

Equations

• ↑f = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯ }

instance SemilinearMapClass.instCoeToSemilinearMap {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} {F : Type u_14} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] : CoeHead F (M →ₛₗ[σ] M₃)

Reinterpret an element of a type of semilinear maps as a semilinear map.

Equations

• SemilinearMapClass.instCoeToSemilinearMap = { coe := fun (f : F) => ↑f }

@[reducible, inline]

abbrev LinearMapClass.linearMap {R : Type u_1} {M₁ : Type u_9} {M₂ : Type u_10} {F : Type u_14} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (f : F) [FunLike F M₁ M₂] [LinearMapClass F R M₁ M₂] : M₁ →ₗ[R] M₂

Reinterpret an element of a type of linear maps as a linear map.

Equations

• LinearMapClass.linearMap f = ↑f

instance LinearMapClass.instCoeToLinearMap {R : Type u_1} {M₁ : Type u_9} {M₂ : Type u_10} {F : Type u_14} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [FunLike F M₁ M₂] [LinearMapClass F R M₁ M₂] : CoeHead F (M₁ →ₗ[R] M₂)

Reinterpret an element of a type of linear maps as a linear map.

Equations

• LinearMapClass.instCoeToLinearMap = { coe := fun (f : F) => ↑f }

instance LinearMap.instFunLike {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} : FunLike (M →ₛₗ[σ] M₃) M M₃

Equations

• LinearMap.instFunLike = { coe := fun (f : M →ₛₗ[σ] M₃) => f.toFun, coe_injective' := ⋯ }

instance LinearMap.semilinearMapClass {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃

Equations

• ⋯ = ⋯

@[simp]

theorem LinearMap.coe_coe {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {F : Type u_14} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f : F} : ⇑↑f = ⇑f

def LinearMap.toDistribMulActionHom {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) : M →ₑ+[↑σ] M₃

The DistribMulActionHom underlying a LinearMap.

Equations

• f.toDistribMulActionHom = { toFun := f.toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem LinearMap.coe_toAddHom {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) : ⇑f.toAddHom = ⇑f

theorem LinearMap.toFun_eq_coe {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} : f.toFun = ⇑f

theorem LinearMap.ext {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {g : M →ₛₗ[σ] M₃} (h : ∀ (x : M), f x = g x) : f = g

def LinearMap.copy {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : M →ₛₗ[σ] M₃

Copy of a LinearMap with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

• f.copy f' h = { toFun := f', map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.coe_copy {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem LinearMap.copy_eq {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : f.copy f' h = f

@[simp]

theorem LinearMap.coe_mk {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : AddHom M M₃) (h : ∀ (m : R) (x : M), f.toFun (m • x) = σ m • f.toFun x) : ⇑{ toAddHom := f, map_smul' := h } = ⇑f

@[simp]

theorem LinearMap.coe_addHom_mk {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : AddHom M M₃) (h : ∀ (m : R) (x : M), f.toFun (m • x) = σ m • f.toFun x) : ↑{ toAddHom := f, map_smul' := h } = f

theorem LinearMap.coe_semilinearMap {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {F : Type u_14} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] (f : F) : ⇑↑f = ⇑f

theorem LinearMap.toLinearMap_injective {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {F : Type u_14} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f : F} {g : F} (h : ↑f = ↑g) : f = g

def LinearMap.id {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] : M →ₗ[R] M

Identity map as a LinearMap

Equations

• LinearMap.id = { toFun := id, map_add' := ⋯, map_smul' := ⋯ }

theorem LinearMap.id_apply {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : LinearMap.id x = x

@[simp]

theorem LinearMap.id_coe {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] : ⇑LinearMap.id = id

def LinearMap.id' {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomId σ] : M →ₛₗ[σ] M

A generalisation of LinearMap.id that constructs the identity function as a σ-semilinear map for any ring homomorphism σ which we know is the identity.

Equations

• LinearMap.id' = { toFun := fun (x : M) => x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.id'_apply {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomId σ] (x : M) : LinearMap.id' x = x

@[simp]

theorem LinearMap.id'_coe {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomId σ] : ⇑LinearMap.id' = id

theorem LinearMap.isLinear {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (fₗ : M →ₗ[R] M₂) : IsLinearMap R ⇑fₗ

theorem LinearMap.coe_injective {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} : Function.Injective DFunLike.coe

theorem LinearMap.congr_arg {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {x : M} {x' : M} : x = x' → f x = f x'

theorem LinearMap.congr_fun {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {g : M →ₛₗ[σ] M₃} (h : f = g) (x : M) : f x = g x

If two linear maps are equal, they are equal at each point.

@[simp]

theorem LinearMap.mk_coe {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : ∀ (m : R) (x : M), (↑f).toFun (m • x) = σ m • (↑f).toFun x) : { toAddHom := ↑f, map_smul' := h } = f

theorem LinearMap.map_add {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (x : M) (y : M) : f (x + y) = f x + f y

theorem LinearMap.map_zero {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) : f 0 = 0

@[simp]

theorem LinearMap.map_smulₛₗ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (c : R) (x : M) : f (c • x) = σ c • f x

theorem LinearMap.map_smul {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (fₗ : M →ₗ[R] M₂) (c : R) (x : M) : fₗ (c • x) = c • fₗ x

theorem LinearMap.map_smul_inv {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) : c • f x = f (σ' c • x)

@[simp]

theorem LinearMap.map_eq_zero_iff {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : Function.Injective ⇑f) {x : M} : f x = 0 ↔ x = 0

class LinearMap.CompatibleSMul (M : Type u_8) (M₂ : Type u_10) [AddCommMonoid M] [AddCommMonoid M₂] (R : Type u_14) (S : Type u_15) [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] : Prop

A typeclass for SMul structures which can be moved through a LinearMap. This typeclass is generated automatically from an IsScalarTower instance, but exists so that we can also add an instance for AddCommGroup.toIntModule, allowing z • to be moved even if S does not support negation.

• map_smul : ∀ (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c • x) = c • fₗ x

  Scalar multiplication by R of M can be moved through linear maps.

theorem LinearMap.CompatibleSMul.map_smul {M : Type u_8} {M₂ : Type u_10} : ∀ {inst : AddCommMonoid M} {inst_1 : AddCommMonoid M₂} {R : Type u_14} {S : Type u_15} {inst_2 : Semiring S} {inst_3 : SMul R M} {inst_4 : Module S M} {inst_5 : SMul R M₂} {inst_6 : Module S M₂} [self : LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c • x) = c • fₗ x

Scalar multiplication by R of M can be moved through linear maps.

@[instance 100]

instance LinearMap.IsScalarTower.compatibleSMul {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] {R : Type u_14} {S : Type u_15} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [SMul R S] [IsScalarTower R S M] [IsScalarTower R S M₂] : LinearMap.CompatibleSMul M M₂ R S

Equations

• ⋯ = ⋯

instance LinearMap.IsScalarTower.compatibleSMul' {M : Type u_8} [AddCommMonoid M] {R : Type u_14} {S : Type u_15} [Semiring S] [SMul R M] [Module S M] [SMul R S] [IsScalarTower R S M] : LinearMap.CompatibleSMul S M R S

Equations

• ⋯ = ⋯

@[simp]

theorem LinearMap.map_smul_of_tower {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] {R : Type u_14} {S : Type u_15} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) : fₗ (c • x) = c • fₗ x

theorem LinearMap.isScalarTower_of_injective {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (R : Type u_14) {S : Type u_15} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [SMul R S] [LinearMap.CompatibleSMul M M₂ R S] [IsScalarTower R S M₂] (f : M →ₗ[S] M₂) (hf : Function.Injective ⇑f) : IsScalarTower R S M

theorem LinearMap.isLinearMap_of_compatibleSMul (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂) : IsLinearMap R ⇑f

def LinearMap.toAddMonoidHom {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) : M →+ M₃

convert a linear map to an additive map

Equations

• f.toAddMonoidHom = { toFun := ⇑f, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem LinearMap.toAddMonoidHom_coe {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) : ⇑f.toAddMonoidHom = ⇑f

def LinearMap.restrictScalars (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) : M →ₗ[R] M₂

If M and M₂ are both R-modules and S-modules and R-module structures are defined by an action of R on S (formally, we have two scalar towers), then any S-linear map from M to M₂ is R-linear.

See also LinearMap.map_smul_of_tower.

Equations

• ↑R fₗ = { toFun := ⇑fₗ, map_add' := ⋯, map_smul' := ⋯ }

instance LinearMap.coeIsScalarTower (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] : CoeHTCT (M →ₗ[S] M₂) (M →ₗ[R] M₂)

Equations

• LinearMap.coeIsScalarTower R = { coe := ↑R }

@[simp]

theorem LinearMap.coe_restrictScalars (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂) : ⇑(↑R f) = ⇑f

theorem LinearMap.restrictScalars_apply (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (x : M) : (↑R fₗ) x = fₗ x

theorem LinearMap.restrictScalars_injective (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] : Function.Injective ↑R

@[simp]

theorem LinearMap.restrictScalars_inj (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (gₗ : M →ₗ[S] M₂) : ↑R fₗ = ↑R gₗ ↔ fₗ = gₗ

theorem LinearMap.toAddMonoidHom_injective {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} : Function.Injective LinearMap.toAddMonoidHom

theorem LinearMap.ext_ring {R : Type u_1} {S : Type u_5} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M₃] [Module S M₃] {σ : R →+* S} {f : R →ₛₗ[σ] M₃} {g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) : f = g

If two σ-linear maps from R are equal on 1, then they are equal.

def RingHom.toSemilinearMap {R : Type u_1} {S : Type u_5} [Semiring R] [Semiring S] (f : R →+* S) : R →ₛₗ[f] S

Interpret a RingHom f as an f-semilinear map.

Equations

• f.toSemilinearMap = { toFun := (↑↑f).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RingHom.toSemilinearMap_apply {R : Type u_1} {S : Type u_5} [Semiring R] [Semiring S] (f : R →+* S) : ∀ (a : R), f.toSemilinearMap a = (↑↑f).toFun a

def LinearMap.comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₃] M₃

Composition of two linear maps is a linear map

Equations

• f.comp g = { toFun := ⇑f ∘ ⇑g, map_add' := ⋯, map_smul' := ⋯ }

def LinearMap.compNotation.delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def LinearMap.compNotation : Lean.TrailingParserDescr

∘ₗ is notation for composition of two linear (not semilinear!) maps into a linear map. This is useful when Lean is struggling to infer the RingHomCompTriple instance.

Equations

• LinearMap.compNotation = Lean.ParserDescr.trailingNode `LinearMap.compNotation 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ₗ ") (Lean.ParserDescr.cat `term 80))

theorem LinearMap.comp_apply {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) (x : M₁) : (f.comp g) x = f (g x)

@[simp]

theorem LinearMap.coe_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem LinearMap.comp_id {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₂] [Semiring R₃] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃) : f.comp LinearMap.id = f

@[simp]

theorem LinearMap.id_comp {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₂] [Semiring R₃] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃) : LinearMap.id.comp f = f

theorem LinearMap.comp_assoc {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {R₄ : Type u_14} {M₄ : Type u_15} [Semiring R₄] [AddCommMonoid M₄] [Module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (f : M₁ →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₃ →ₛₗ[σ₃₄] M₄) : (h.comp g).comp f = h.comp (g.comp f)

theorem Function.Surjective.injective_linearMapComp_right {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {g : M₁ →ₛₗ[σ₁₂] M₂} (hg : Function.Surjective ⇑g) : Function.Injective fun (f : M₂ →ₛₗ[σ₂₃] M₃) => f.comp g

The linear map version of Function.Surjective.injective_comp_right

@[simp]

theorem LinearMap.cancel_right {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} {g : M₁ →ₛₗ[σ₁₂] M₂} {f' : M₂ →ₛₗ[σ₂₃] M₃} (hg : Function.Surjective ⇑g) : f.comp g = f'.comp g ↔ f = f'

theorem Function.Injective.injective_linearMapComp_left {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} (hf : Function.Injective ⇑f) : Function.Injective fun (g : M₁ →ₛₗ[σ₁₂] M₂) => f.comp g

The linear map version of Function.Injective.comp_left

@[simp]

theorem LinearMap.cancel_left {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} {g : M₁ →ₛₗ[σ₁₂] M₂} {g' : M₁ →ₛₗ[σ₁₂] M₂} (hf : Function.Injective ⇑f) : f.comp g = f.comp g' ↔ g = g'

def LinearMap.inverse {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] (f : M →ₛₗ[σ] M₂) (g : M₂ → M) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : M₂ →ₛₗ[σ'] M

If a function g is a left and right inverse of a linear map f, then g is linear itself.

Equations

• f.inverse g h₁ h₂ = { toFun := g, map_add' := ⋯, map_smul' := ⋯ }

theorem LinearMap.injective_of_comp_eq_id {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] (f : M →ₛₗ[σ] M₂) (g : M₂ →ₛₗ[σ'] M) (h : g.comp f = LinearMap.id) : Function.Injective ⇑f

theorem LinearMap.surjective_of_comp_eq_id {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] (f : M →ₛₗ[σ] M₂) (g : M₂ →ₛₗ[σ'] M) (h : g.comp f = LinearMap.id) : Function.Surjective ⇑g

theorem LinearMap.map_neg {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommGroup M] [AddCommGroup M₂] {module_M : Module R M} {module_M₂ : Module S M₂} {σ : R →+* S} (f : M →ₛₗ[σ] M₂) (x : M) : f (-x) = -f x

theorem LinearMap.map_sub {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommGroup M] [AddCommGroup M₂] {module_M : Module R M} {module_M₂ : Module S M₂} {σ : R →+* S} (f : M →ₛₗ[σ] M₂) (x : M) (y : M) : f (x - y) = f x - f y

instance LinearMap.CompatibleSMul.intModule {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] {S : Type u_14} [Semiring S] [Module S M] [Module S M₂] : LinearMap.CompatibleSMul M M₂ ℤ S

Equations

• ⋯ = ⋯

instance LinearMap.CompatibleSMul.units {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] {R : Type u_14} {S : Type u_15} [Monoid R] [MulAction R M] [MulAction R M₂] [Semiring S] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] : LinearMap.CompatibleSMul M M₂ Rˣ S

Equations

• ⋯ = ⋯

def Module.compHom.toLinearMap {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (g : R →+* S) : R →ₗ[R] S

g : R →+* S is R-linear when the module structure on S is Module.compHom S g .

Equations

• Module.compHom.toLinearMap g = { toFun := ⇑g, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Module.compHom.toLinearMap_apply {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (g : R →+* S) (a : R) : (Module.compHom.toLinearMap g) a = g a

@[deprecated]

def DistribMulActionHom.toSemilinearMap {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] [Semiring R] [Module R M] [Semiring S] [Module S M₂] {σ : R →+* S} (fₗ : M →ₑ+[↑σ] M₂) : M →ₛₗ[σ] M₂

A DistribMulActionHom between two modules is a linear map.

Equations

• fₗ.toSemilinearMap = { toFun := fₗ.toFun, map_add' := ⋯, map_smul' := ⋯ }

instance DistribMulActionHom.instSemilinearMapClass {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] [Semiring R] [Module R M] [Semiring S] [Module S M₂] {σ : R →+* S} : SemilinearMapClass (M →ₑ+[↑σ] M₂) σ M M₂

Equations

• ⋯ = ⋯

@[deprecated]

def DistribMulActionHom.toLinearMap {R : Type u_1} {M : Type u_8} {M₃ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₃] [Semiring R] [Module R M] [Module R M₃] (fₗ : M →+[R] M₃) : M →ₗ[R] M₃

A DistribMulActionHom between two modules is a linear map.

Equations

• fₗ.toLinearMap = { toFun := fₗ.toFun, map_add' := ⋯, map_smul' := ⋯ }

instance DistribMulActionHom.instLinearMapClassId {R : Type u_1} {M : Type u_8} {M₃ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₃] [Semiring R] [Module R M] [Module R M₃] : LinearMapClass (M →+[R] M₃) R M M₃

A DistribMulActionHom between two modules is a linear map.

Equations

• ⋯ = ⋯

@[simp]

theorem DistribMulActionHom.coe_toLinearMap {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] [Semiring R] [Module R M] [Semiring S] [Module S M₂] {σ : R →+* S} (f : M →ₑ+[↑σ] M₂) : ⇑↑f = ⇑f

theorem DistribMulActionHom.toLinearMap_injective {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] [Semiring R] [Module R M] [Semiring S] [Module S M₂] {σ : R →+* S} {f : M →ₑ+[↑σ] M₂} {g : M →ₑ+[↑σ] M₂} (h : ↑f = ↑g) : f = g

def IsLinearMap.mk' {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M → M₂) (lin : IsLinearMap R f) : M →ₗ[R] M₂

Convert an IsLinearMap predicate to a LinearMap

Equations

• IsLinearMap.mk' f lin = { toFun := f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem IsLinearMap.mk'_apply {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {f : M → M₂} (lin : IsLinearMap R f) (x : M) : (IsLinearMap.mk' f lin) x = f x

theorem IsLinearMap.isLinearMap_smul {R : Type u_14} {M : Type u_15} [CommSemiring R] [AddCommMonoid M] [Module R M] (c : R) : IsLinearMap R fun (z : M) => c • z

theorem IsLinearMap.isLinearMap_smul' {R : Type u_14} {M : Type u_15} [Semiring R] [AddCommMonoid M] [Module R M] (a : M) : IsLinearMap R fun (c : R) => c • a

theorem IsLinearMap.map_zero {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {f : M → M₂} (lin : IsLinearMap R f) : f 0 = 0

theorem IsLinearMap.isLinearMap_neg {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommGroup M] [Module R M] : IsLinearMap R fun (z : M) => -z

theorem IsLinearMap.map_neg {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] {f : M → M₂} (lin : IsLinearMap R f) (x : M) : f (-x) = -f x

theorem IsLinearMap.map_sub {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] {f : M → M₂} (lin : IsLinearMap R f) (x : M) (y : M) : f (x - y) = f x - f y

def AddMonoidHom.toNatLinearMap {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (f : M →+ M₂) : M →ₗ[ℕ] M₂

Reinterpret an additive homomorphism as an ℕ-linear map.

Equations

• f.toNatLinearMap = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯ }

theorem AddMonoidHom.toNatLinearMap_injective {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] : Function.Injective AddMonoidHom.toNatLinearMap

def AddMonoidHom.toIntLinearMap {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : M →ₗ[ℤ] M₂

Reinterpret an additive homomorphism as a ℤ-linear map.

Equations

• f.toIntLinearMap = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯ }

theorem AddMonoidHom.toIntLinearMap_injective {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] : Function.Injective AddMonoidHom.toIntLinearMap

@[simp]

theorem AddMonoidHom.coe_toIntLinearMap {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : ⇑f.toIntLinearMap = ⇑f

instance LinearMap.instSMul {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] : SMul S (M →ₛₗ[σ₁₂] M₂)

Equations

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

@[simp]

theorem LinearMap.smul_apply {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] (a : S) (f : M →ₛₗ[σ₁₂] M₂) (x : M) : (a • f) x = a • f x

theorem LinearMap.coe_smul {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] (a : S) (f : M →ₛₗ[σ₁₂] M₂) : ⇑(a • f) = a • ⇑f

instance LinearMap.instSMulCommClass {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {T : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [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₂)

Equations

• ⋯ = ⋯

instance LinearMap.instIsScalarTower {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {T : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] [Monoid T] [DistribMulAction T M₂] [SMulCommClass R₂ T M₂] [SMul S T] [IsScalarTower S T M₂] : IsScalarTower S T (M →ₛₗ[σ₁₂] M₂)

Equations

• ⋯ = ⋯

instance LinearMap.instIsCentralScalar {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] [DistribMulAction Sᵐᵒᵖ M₂] [SMulCommClass R₂ Sᵐᵒᵖ M₂] [IsCentralScalar S M₂] : IsCentralScalar S (M →ₛₗ[σ₁₂] M₂)

Equations

• ⋯ = ⋯

Arithmetic on the codomain

instance LinearMap.instZero {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} : Zero (M →ₛₗ[σ₁₂] M₂)

The constant 0 map is linear.

Equations

• LinearMap.instZero = { zero := { toFun := 0, map_add' := ⋯, map_smul' := ⋯ } }

@[simp]

theorem LinearMap.zero_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (x : M) : 0 x = 0

@[simp]

theorem LinearMap.comp_zero {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →ₛₗ[σ₂₃] M₃) : g.comp 0 = 0

@[simp]

theorem LinearMap.zero_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) : LinearMap.comp 0 f = 0

instance LinearMap.instInhabited {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} : Inhabited (M →ₛₗ[σ₁₂] M₂)

Equations

• LinearMap.instInhabited = { default := 0 }

@[simp]

theorem LinearMap.default_def {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} : default = 0

instance LinearMap.uniqueOfLeft {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} [Subsingleton M] : Unique (M →ₛₗ[σ₁₂] M₂)

Equations

• LinearMap.uniqueOfLeft = { toInhabited := inferInstanceAs (Inhabited (M →ₛₗ[σ₁₂] M₂)), uniq := ⋯ }

instance LinearMap.uniqueOfRight {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} [Subsingleton M₂] : Unique (M →ₛₗ[σ₁₂] M₂)

Equations

• LinearMap.uniqueOfRight = ⋯.unique

instance LinearMap.instAdd {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} : Add (M →ₛₗ[σ₁₂] M₂)

The sum of two linear maps is linear.

Equations

• LinearMap.instAdd = { add := fun (f g : M →ₛₗ[σ₁₂] M₂) => { toFun := ⇑f + ⇑g, map_add' := ⋯, map_smul' := ⋯ } }

@[simp]

theorem LinearMap.add_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M →ₛₗ[σ₁₂] M₂) (x : M) : (f + g) x = f x + g x

theorem LinearMap.add_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₂ →ₛₗ[σ₂₃] M₃) : (h + g).comp f = h.comp f + g.comp f

theorem LinearMap.comp_add {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) : h.comp (f + g) = h.comp f + h.comp g

instance LinearMap.addCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} : AddCommMonoid (M →ₛₗ[σ₁₂] M₂)

The type of linear maps is an additive monoid.

Equations

• LinearMap.addCommMonoid = Function.Injective.addCommMonoid (fun (f : M →ₛₗ[σ₁₂] M₂) => ⇑f) ⋯ ⋯ ⋯ ⋯

instance LinearMap.instNeg {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_12} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} : Neg (M →ₛₗ[σ₁₂] N₂)

The negation of a linear map is linear.

Equations

• LinearMap.instNeg = { neg := fun (f : M →ₛₗ[σ₁₂] N₂) => { toFun := -⇑f, map_add' := ⋯, map_smul' := ⋯ } }

@[simp]

theorem LinearMap.neg_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_12} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] N₂) (x : M) : (-f) x = -f x

@[simp]

theorem LinearMap.neg_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {N₃ : Type u_13} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) : (-g).comp f = -g.comp f

@[simp]

theorem LinearMap.comp_neg {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {N₂ : Type u_12} {N₃ : Type u_13} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommGroup N₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ N₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃] N₃) : g.comp (-f) = -g.comp f

instance LinearMap.instSub {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_12} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} : Sub (M →ₛₗ[σ₁₂] N₂)

The subtraction of two linear maps is linear.

Equations

• LinearMap.instSub = { sub := fun (f g : M →ₛₗ[σ₁₂] N₂) => { toFun := ⇑f - ⇑g, map_add' := ⋯, map_smul' := ⋯ } }

@[simp]

theorem LinearMap.sub_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_12} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] N₂) (g : M →ₛₗ[σ₁₂] N₂) (x : M) : (f - g) x = f x - g x

theorem LinearMap.sub_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {N₃ : Type u_13} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) (h : M₂ →ₛₗ[σ₂₃] N₃) : (g - h).comp f = g.comp f - h.comp f

theorem LinearMap.comp_sub {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {N₂ : Type u_12} {N₃ : Type u_13} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommGroup N₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ N₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) : h.comp (g - f) = h.comp g - h.comp f

instance LinearMap.addCommGroup {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_12} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} : AddCommGroup (M →ₛₗ[σ₁₂] N₂)

The type of linear maps is an additive group.

Equations

• LinearMap.addCommGroup = Function.Injective.addCommGroup (fun (f : M →ₛₗ[σ₁₂] N₂) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def LinearMap.evalAddMonoidHom {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (a : M) : (M →ₛₗ[σ₁₂] M₂) →+ M₂

Evaluation of a σ₁₂-linear map at a fixed a, as an AddMonoidHom.

Equations

• LinearMap.evalAddMonoidHom a = { toFun := fun (f : M →ₛₗ[σ₁₂] M₂) => f a, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem LinearMap.evalAddMonoidHom_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (a : M) (f : M →ₛₗ[σ₁₂] M₂) : (LinearMap.evalAddMonoidHom a) f = f a

def LinearMap.toAddMonoidHom' {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} : (M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂

LinearMap.toAddMonoidHom promoted to an AddMonoidHom.

Equations

• LinearMap.toAddMonoidHom' = { toFun := LinearMap.toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem LinearMap.toAddMonoidHom'_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) : LinearMap.toAddMonoidHom' f = f.toAddMonoidHom

@[simp]

theorem LinearMap.identityMapOfZeroModuleIsZero {R₁ : Type u_2} {M : Type u_8} [Semiring R₁] [AddCommMonoid M] [Module R₁ M] [Subsingleton M] : LinearMap.id = 0

If M is the zero module, then the identity map of M is the zero map.

instance LinearMap.instDistribMulAction {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] : DistribMulAction S (M →ₛₗ[σ₁₂] M₂)

Equations

• LinearMap.instDistribMulAction = DistribMulAction.mk ⋯ ⋯

theorem LinearMap.smul_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {S₃ : Type u_6} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [Monoid S₃] [DistribMulAction S₃ M₃] [SMulCommClass R₃ S₃ M₃] (a : S₃) (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂) : (a • g).comp f = a • g.comp f

theorem LinearMap.comp_smul {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Monoid S] [DistribMulAction S M₂] [Module R M₂] [Module R M₃] [SMulCommClass R S M₂] [DistribMulAction S M₃] [SMulCommClass R S M₃] [LinearMap.CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) : g ∘ₗ (a • f) = a • g ∘ₗ f

instance LinearMap.module {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [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.module = Module.mk ⋯ ⋯

@[simp]

theorem LinearMap.restrictScalars_zero (R : Type u_14) (S : Type u_15) (M : Type u_16) (N : Type u_17) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [LinearMap.CompatibleSMul M N R S] : ↑R 0 = 0

@[simp]

theorem LinearMap.restrictScalars_add {R : Type u_14} {S : Type u_15} {M : Type u_16} {N : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [LinearMap.CompatibleSMul M N R S] (f : M →ₗ[S] N) (g : M →ₗ[S] N) : ↑R (f + g) = ↑R f + ↑R g

@[simp]

theorem LinearMap.restrictScalars_neg {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] {M : Type u_19} {N : Type u_20} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module S M] [Module S N] [LinearMap.CompatibleSMul M N R S] (f : M →ₗ[S] N) : ↑R (-f) = -↑R f

@[simp]

theorem LinearMap.restrictScalars_smul {R : Type u_14} {S : Type u_15} {M : Type u_16} {N : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [LinearMap.CompatibleSMul M N R S] {R₁ : Type u_19} [Semiring R₁] [Module R₁ N] [SMulCommClass S R₁ N] [SMulCommClass R R₁ N] (c : R₁) (f : M →ₗ[S] N) : ↑R (c • f) = c • ↑R f

@[simp]

theorem LinearMap.restrictScalars_comp {R : Type u_14} {S : Type u_15} {M : Type u_16} {N : Type u_17} {P : Type u_18} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [LinearMap.CompatibleSMul M N R S] [AddCommMonoid P] [Module S P] [Module R P] [LinearMap.CompatibleSMul N P R S] [LinearMap.CompatibleSMul M P R S] (f : N →ₗ[S] P) (g : M →ₗ[S] N) : ↑R (f ∘ₗ g) = ↑R f ∘ₗ ↑R g

@[simp]

theorem LinearMap.restrictScalars_trans {R : Type u_14} {S : Type u_15} {M : Type u_16} {N : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [LinearMap.CompatibleSMul M N R S] {T : Type u_20} [CommSemiring T] [Module T M] [Module T N] [LinearMap.CompatibleSMul M N S T] [LinearMap.CompatibleSMul M N R T] (f : M →ₗ[T] N) : ↑R (↑S f) = ↑R f

def LinearMap.restrictScalarsₗ (R : Type u_14) (S : Type u_15) (M : Type u_16) (N : Type u_17) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [LinearMap.CompatibleSMul M N R S] (R₁ : Type u_19) [Semiring R₁] [Module R₁ N] [SMulCommClass S R₁ N] [SMulCommClass R R₁ N] : (M →ₗ[S] N) →ₗ[R₁] M →ₗ[R] N

LinearMap.restrictScalars as a LinearMap.

Equations

• LinearMap.restrictScalarsₗ R S M N R₁ = { toFun := ↑R, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.restrictScalarsₗ_apply (R : Type u_14) (S : Type u_15) (M : Type u_16) (N : Type u_17) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [LinearMap.CompatibleSMul M N R S] (R₁ : Type u_19) [Semiring R₁] [Module R₁ N] [SMulCommClass S R₁ N] [SMulCommClass R R₁ N] (fₗ : M →ₗ[S] N) : (LinearMap.restrictScalarsₗ R S M N R₁) fₗ = ↑R fₗ