# Documentation

Mathlib.Algebra.Module.LinearMap

# (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.
• Module.End.semiring and Module.End.ring: the (semi)ring of endomorphisms formed by taking the additive structure above with composition as multiplication.

## 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} [] [] [] [Module R M] [Module R M₂] (f : MM₂) :
• map_add : ∀ (x y : M), f (x + y) = f x + f y

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

A linear map preserves scalar multiplication.

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.

Instances For
structure LinearMap {R : Type u_17} {S : Type u_18} [] [] (σ : R →+* S) (M : Type u_19) (M₂ : Type u_20) [] [] [Module R M] [Module S M₂] extends :
Type (max u_19 u_20)

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.

Instances For

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

Instances For

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

Instances For

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

Instances For
class SemilinearMapClass (F : Type u_17) {R : outParam (Type u_18)} {S : outParam (Type u_19)} [] [] (σ : outParam (R →+* S)) (M : outParam (Type u_20)) (M₂ : outParam (Type u_21)) [] [] [Module R M] [Module S M₂] extends :
Type (max (max u_17 u_20) u_21)
• coe : FMM₂
• coe_injective' : Function.Injective FunLike.coe
• map_add : ∀ (f : F) (x y : M), f (x + y) = f x + f y
• map_smulₛₗ : ∀ (f : F) (r : R) (x : M), f (r x) = σ r f x

A semilinear map preserves scalar multiplication up to some ring homomorphism σ. See also _root_.map_smul for the case where σ is the identity.

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.

Instances
@[inline, reducible]
abbrev LinearMapClass (F : Type u_17) (R : outParam (Type u_18)) (M : outParam (Type u_19)) (M₂ : outParam (Type u_20)) [] [] [] [Module R M] [Module R M₂] :
Type (max (max u_17 u_19) u_20)

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₂.

Instances For
instance SemilinearMapClass.addMonoidHomClass {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} (F : Type u_17) [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} [SemilinearMapClass F σ M M₃] :
instance SemilinearMapClass.distribMulActionHomClass {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} (F : Type u_17) [] [] [] [Module R M] [Module R M₂] [LinearMapClass F R M M₂] :
theorem SemilinearMapClass.map_smul_inv {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} {F : Type u_17} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} (f : F) [i : SemilinearMapClass F σ M M₃] {σ' : S →+* R} [] (c : S) (x : M) :
c f x = f (σ' c x)
instance LinearMap.semilinearMapClass {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} :
SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃
instance LinearMap.instFunLike {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} :
FunLike (M →ₛₗ[σ] M₃) M fun x => M₃
def LinearMap.toDistribMulActionHom {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [] [] [] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) :
M →+[R] M₂

The DistribMulActionHom underlying a LinearMap.

Instances For
@[simp]
theorem LinearMap.coe_toAddHom {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
theorem LinearMap.toFun_eq_coe {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} :
f.toFun = f
theorem LinearMap.ext {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [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_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : MM₃) (h : f' = f) :
M →ₛₗ[σ] M₃

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

Instances For
@[simp]
theorem LinearMap.coe_copy {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : MM₃) (h : f' = f) :
↑(LinearMap.copy f f' h) = f'
theorem LinearMap.copy_eq {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : MM₃) (h : f' = f) :
LinearMap.copy f f' h = f
@[simp]
theorem LinearMap.coe_mk {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} (f : AddHom M M₃) (h : ∀ (r : R) (x : M), AddHom.toFun f (r x) = σ r ) :
{ toAddHom := f, map_smul' := h } = f
@[simp]
theorem LinearMap.coe_addHom_mk {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} (f : AddHom M M₃) (h : ∀ (r : R) (x : M), AddHom.toFun f (r x) = σ r ) :
{ toAddHom := f, map_smul' := h } = f
def LinearMap.id {R : Type u_1} {M : Type u_9} [] [] [Module R M] :

Identity map as a LinearMap

Instances For
theorem LinearMap.id_apply {R : Type u_1} {M : Type u_9} [] [] [Module R M] (x : M) :
LinearMap.id x = x
@[simp]
theorem LinearMap.id_coe {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
LinearMap.id = id
@[simp]
theorem LinearMap.id'_apply {R : Type u_1} {M : Type u_9} [] [] [Module R M] {σ : R →+* R} [] (x : M) :
LinearMap.id' x = x
def LinearMap.id' {R : Type u_1} {M : Type u_9} [] [] [Module R M] {σ : R →+* R} [] :

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

Instances For
@[simp]
theorem LinearMap.id'_coe {R : Type u_1} {M : Type u_9} [] [] [Module R M] {σ : R →+* R} [] :
LinearMap.id' = id
theorem LinearMap.isLinear {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [] [] [] [Module R M] [Module R M₂] (fₗ : M →ₗ[R] M₂) :
IsLinearMap R fₗ
theorem LinearMap.coe_injective {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} :
Function.Injective FunLike.coe
theorem LinearMap.congr_arg {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [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_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [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.

theorem LinearMap.ext_iff {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {g : M →ₛₗ[σ] M₃} :
f = g ∀ (x : M), f x = g x
@[simp]
theorem LinearMap.mk_coe {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : ∀ (r : R) (x : M), AddHom.toFun (f) (r x) = σ r AddHom.toFun (f) x) :
{ toAddHom := f, map_smul' := h } = f
theorem LinearMap.map_add {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [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_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
f 0 = 0
theorem LinearMap.map_smulₛₗ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [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_9} {M₂ : Type u_11} [] [] [] [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_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) {σ' : S →+* R} [] (c : S) (x : M) :
c f x = f (σ' c x)
@[simp]
theorem LinearMap.map_eq_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : ) {x : M} :
f x = 0 x = 0
@[simp]
theorem image_smul_setₛₗ {R : Type u_1} {S : Type u_6} (M : Type u_9) (M₃ : Type u_12) [] [] [] [] [Module R M] [Module S M₃] (σ : R →+* S) {F : Type u_17} (h : F) [SemilinearMapClass F σ M M₃] (c : R) (s : Set M) :
h '' (c s) = σ c h '' s
theorem preimage_smul_setₛₗ {R : Type u_1} {S : Type u_6} (M : Type u_9) (M₃ : Type u_12) [] [] [] [] [Module R M] [Module S M₃] (σ : R →+* S) {F : Type u_17} (h : F) [SemilinearMapClass F σ M M₃] {c : R} (hc : ) (s : Set M₃) :
h ⁻¹' (σ c s) = c h ⁻¹' s
theorem image_smul_set (R : Type u_1) (M : Type u_9) (M₂ : Type u_11) [] [] [] [Module R M] [Module R M₂] {F : Type u_17} (h : F) [LinearMapClass F R M M₂] (c : R) (s : Set M) :
h '' (c s) = c h '' s
theorem preimage_smul_set (R : Type u_1) (M : Type u_9) (M₂ : Type u_11) [] [] [] [Module R M] [Module R M₂] {F : Type u_17} (h : F) [LinearMapClass F R M M₂] {c : R} (hc : ) (s : Set M₂) :
h ⁻¹' (c s) = c h ⁻¹' s
class LinearMap.CompatibleSMul (M : Type u_9) (M₂ : Type u_11) [] [] (R : Type u_17) (S : Type u_18) [] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] :
• 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.

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.intModule, allowing z • to be moved even if R does not support negation.

Instances
instance LinearMap.IsScalarTower.compatibleSMul {M : Type u_9} {M₂ : Type u_11} [] [] {R : Type u_17} {S : Type u_18} [] [SMul R S] [SMul R M] [Module S M] [] [SMul R M₂] [Module S M₂] [IsScalarTower R S M₂] :
@[simp]
theorem LinearMap.map_smul_of_tower {M : Type u_9} {M₂ : Type u_11} [] [] {R : Type u_17} {S : Type u_18} [] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) :
fₗ (c x) = c fₗ x
def LinearMap.toAddMonoidHom {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
M →+ M₃

convert a linear map to an additive map

Instances For
@[simp]
theorem LinearMap.toAddMonoidHom_coe {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
= f
def LinearMap.restrictScalars (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [] [] [] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [] (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.

Instances For
instance LinearMap.coeIsScalarTower (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [] [] [] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [] :
CoeHTCT (M →ₗ[S] M₂) (M →ₗ[R] M₂)
@[simp]
theorem LinearMap.coe_restrictScalars (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [] [] [] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [] (f : M →ₗ[S] M₂) :
↑(R f) = f
theorem LinearMap.restrictScalars_apply (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [] [] [] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [] (fₗ : M →ₗ[S] M₂) (x : M) :
↑(R fₗ) x = fₗ x
theorem LinearMap.restrictScalars_injective (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [] [] [] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [] :
@[simp]
theorem LinearMap.restrictScalars_inj (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [] [] [] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [] (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_6} {M : Type u_9} {M₃ : Type u_12} [] [] [] [] [Module R M] [Module S M₃] {σ : R →+* S} :
theorem LinearMap.ext_ring {R : Type u_1} {S : Type u_6} {M₃ : Type u_12} [] [] [] [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.

theorem LinearMap.ext_ring_iff {R : Type u_1} {M : Type u_9} [] [] [Module R M] {σ : R →+* R} {f : R →ₛₗ[σ] M} {g : R →ₛₗ[σ] M} :
f = g f 1 = g 1
theorem LinearMap.ext_ring_op {R : Type u_1} {S : Type u_6} {M₃ : Type u_12} [] [] [] [Module S M₃] {σ : Rᵐᵒᵖ →+* S} {f : R →ₛₗ[σ] M₃} {g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) :
f = g
@[simp]
theorem RingHom.toSemilinearMap_apply {R : Type u_1} {S : Type u_6} [] [] (f : R →+* S) :
∀ (a : R), ↑() a = OneHom.toFun (f) a
def RingHom.toSemilinearMap {R : Type u_1} {S : Type u_6} [] [] (f : R →+* S) :

Interpret a RingHom f as an f-semilinear map.

Instances For
def LinearMap.comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {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

Instances For

∘ₗ 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.

Instances For
theorem LinearMap.comp_apply {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {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₁) :
↑() x = f (g x)
@[simp]
theorem LinearMap.coe_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {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 g
@[simp]
theorem LinearMap.comp_id {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₂] [Semiring R₃] [] [] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃) :
LinearMap.comp f LinearMap.id = f
@[simp]
theorem LinearMap.id_comp {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₂] [Semiring R₃] [] [] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃) :
LinearMap.comp LinearMap.id f = f
theorem LinearMap.comp_assoc {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {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_17} {M₄ : Type u_18} [Semiring R₄] [] [Module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (f : M₁ →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₃ →ₛₗ[σ₃₄] M₄) :
theorem Function.Surjective.injective_linearMapComp_right {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {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 : ) :

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_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {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 : ) :
= f = f'
theorem Function.Injective.injective_linearMapComp_left {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {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 : ) :

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_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {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 : ) :
= g = g'
def LinearMap.inverse {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] (f : M →ₛₗ[σ] M₂) (g : M₂M) (h₁ : ) (h₂ : ) :
M₂ →ₛₗ[σ'] M

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

Instances For
theorem LinearMap.map_neg {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [] [] [] {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_6} {M : Type u_9} {M₂ : Type u_11} [] [] [] [] {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_9} {M₂ : Type u_11} [] [] {S : Type u_17} [] [Module S M] [Module S M₂] :
instance LinearMap.CompatibleSMul.units {M : Type u_9} {M₂ : Type u_11} [] [] {R : Type u_17} {S : Type u_18} [] [] [MulAction R M₂] [] [Module S M] [Module S M₂] [] :
@[simp]
theorem Module.compHom.toLinearMap_apply {R : Type u_17} {S : Type u_18} [] [] (g : R →+* S) (a : R) :
= g a
def Module.compHom.toLinearMap {R : Type u_17} {S : Type u_18} [] [] (g : R →+* S) :

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

Instances For
def DistribMulActionHom.toLinearMap {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [] [] [] [Module R M] [Module R M₂] (fₗ : M →+[R] M₂) :
M →ₗ[R] M₂

A DistribMulActionHom between two modules is a linear map.

Instances For
@[simp]
theorem DistribMulActionHom.coe_toLinearMap {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [] [] [] [Module R M] [Module R M₂] (f : M →+[R] M₂) :
f = f
theorem DistribMulActionHom.toLinearMap_injective {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [] [] [] [Module R M] [Module R M₂] {f : M →+[R] M₂} {g : M →+[R] M₂} (h : f = g) :
f = g
def IsLinearMap.mk' {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [] [] [] [Module R M] [Module R M₂] (f : MM₂) (H : ) :
M →ₗ[R] M₂

Convert an IsLinearMap predicate to a LinearMap

Instances For
@[simp]
theorem IsLinearMap.mk'_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [] [] [] [Module R M] [Module R M₂] {f : MM₂} (H : ) (x : M) :
↑() x = f x
theorem IsLinearMap.isLinearMap_smul {R : Type u_17} {M : Type u_18} [] [] [Module R M] (c : R) :
IsLinearMap R fun z => c z
theorem IsLinearMap.isLinearMap_smul' {R : Type u_17} {M : Type u_18} [] [] [Module R M] (a : M) :
IsLinearMap R fun c => c a
theorem IsLinearMap.map_zero {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [] [] [] [Module R M] [Module R M₂] {f : MM₂} (lin : ) :
f 0 = 0
theorem IsLinearMap.isLinearMap_neg {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
IsLinearMap R fun z => -z
theorem IsLinearMap.map_neg {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [] [] [] [Module R M] [Module R M₂] {f : MM₂} (lin : ) (x : M) :
f (-x) = -f x
theorem IsLinearMap.map_sub {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [] [] [] [Module R M] [Module R M₂] {f : MM₂} (lin : ) (x : M) (y : M) :
f (x - y) = f x - f y
@[inline, reducible]
abbrev Module.End (R : Type u) (M : Type v) [] [] [Module R M] :

Linear endomorphisms of a module, with associated ring structure Module.End.semiring and algebra structure Module.End.algebra.

Instances For
def AddMonoidHom.toNatLinearMap {M : Type u_9} {M₂ : Type u_11} [] [] (f : M →+ M₂) :

Reinterpret an additive homomorphism as an ℕ-linear map.

Instances For
theorem AddMonoidHom.toNatLinearMap_injective {M : Type u_9} {M₂ : Type u_11} [] [] :
def AddMonoidHom.toIntLinearMap {M : Type u_9} {M₂ : Type u_11} [] [] (f : M →+ M₂) :

Reinterpret an additive homomorphism as a ℤ-linear map.

Instances For
theorem AddMonoidHom.toIntLinearMap_injective {M : Type u_9} {M₂ : Type u_11} [] [] :
@[simp]
theorem AddMonoidHom.coe_toIntLinearMap {M : Type u_9} {M₂ : Type u_11} [] [] (f : M →+ M₂) :
= f
def AddMonoidHom.toRatLinearMap {M : Type u_9} {M₂ : Type u_11} [] [] [] [Module M₂] (f : M →+ M₂) :

Reinterpret an additive homomorphism as a ℚ-linear map.

Instances For
theorem AddMonoidHom.toRatLinearMap_injective {M : Type u_9} {M₂ : Type u_11} [] [] [] [Module M₂] :
@[simp]
theorem AddMonoidHom.coe_toRatLinearMap {M : Type u_9} {M₂ : Type u_11} [] [] [] [Module M₂] (f : M →+ M₂) :
= f
instance LinearMap.instSMulLinearMap {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] [] [SMulCommClass R₂ S M₂] :
SMul S (M →ₛₗ[σ₁₂] M₂)
@[simp]
theorem LinearMap.smul_apply {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] [] [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_6} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] [] [SMulCommClass R₂ S M₂] (a : S) (f : M →ₛₗ[σ₁₂] M₂) :
↑(a f) = a f
instance LinearMap.instSMulCommClassLinearMapInstSMulLinearMapInstSMulLinearMap {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {T : Type u_8} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] [] [SMulCommClass R₂ S M₂] [] [] [SMulCommClass R₂ T M₂] [SMulCommClass S T M₂] :
SMulCommClass S T (M →ₛₗ[σ₁₂] M₂)
instance LinearMap.instIsScalarTowerLinearMapInstSMulLinearMapInstSMulLinearMap {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {T : Type u_8} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] [] [SMulCommClass R₂ S M₂] [] [] [SMulCommClass R₂ T M₂] [SMul S T] [IsScalarTower S T M₂] :
IsScalarTower S T (M →ₛₗ[σ₁₂] M₂)
instance LinearMap.instIsCentralScalarLinearMapInstSMulLinearMapMulOppositeMonoid {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] [] [SMulCommClass R₂ S M₂] [] [SMulCommClass R₂ Sᵐᵒᵖ M₂] [] :
IsCentralScalar S (M →ₛₗ[σ₁₂] M₂)

### Arithmetic on the codomain #

instance LinearMap.instZeroLinearMap {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [] [] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
Zero (M →ₛₗ[σ₁₂] M₂)

The constant 0 map is linear.

@[simp]
theorem LinearMap.zero_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [] [] [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_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →ₛₗ[σ₂₃] M₃) :
= 0
@[simp]
theorem LinearMap.zero_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) :
= 0
instance LinearMap.instInhabitedLinearMap {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [] [] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
Inhabited (M →ₛₗ[σ₁₂] M₂)
@[simp]
theorem LinearMap.default_def {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [] [] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
default = 0
instance LinearMap.instAddLinearMap {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [] [] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :

The sum of two linear maps is linear.

@[simp]
theorem LinearMap.add_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [] [] [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_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] [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₃) :
LinearMap.comp (h + g) f = +
theorem LinearMap.comp_add {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] [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₃) :
LinearMap.comp h (f + g) = +
instance LinearMap.addCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [] [] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :

The type of linear maps is an additive monoid.

instance LinearMap.instNegLinearMapToAddCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [] [] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
Neg (M →ₛₗ[σ₁₂] N₂)

The negation of a linear map is linear.

@[simp]
theorem LinearMap.neg_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [] [] [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_9} {M₂ : Type u_11} {N₃ : Type u_15} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] [Module R₁ M] [Module R₂ M₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) :
@[simp]
theorem LinearMap.comp_neg {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {N₂ : Type u_14} {N₃ : Type u_15} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] [Module R₁ M] [Module R₂ N₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃] N₃) :
instance LinearMap.instSubLinearMapToAddCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [] [] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
Sub (M →ₛₗ[σ₁₂] N₂)

The subtraction of two linear maps is linear.

@[simp]
theorem LinearMap.sub_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [] [] [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_9} {M₂ : Type u_11} {N₃ : Type u_15} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] [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₃) :
LinearMap.comp (g - h) f = -
theorem LinearMap.comp_sub {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {N₂ : Type u_14} {N₃ : Type u_15} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] [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₃) :
LinearMap.comp h (g - f) = -
instance LinearMap.addCommGroup {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [] [] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :

The type of linear maps is an additive group.

instance LinearMap.instDistribMulActionLinearMapToAddMonoidAddCommMonoid {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] [] [SMulCommClass R₂ S M₂] :
DistribMulAction S (M →ₛₗ[σ₁₂] M₂)
theorem LinearMap.smul_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {S₃ : Type u_7} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [] [Semiring R₂] [Semiring R₃] [] [] [] [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₂) :
LinearMap.comp (a g) f = a
theorem LinearMap.comp_smul {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [] [] [] [] [Module R M] [] [] [Module R M₂] [Module R M₃] [SMulCommClass R S M₂] [] [SMulCommClass R S M₃] [LinearMap.CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) :
LinearMap.comp g (a f) = a
instance LinearMap.module {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] [Module S M₂] [SMulCommClass R₂ S M₂] :
Module S (M →ₛₗ[σ₁₂] M₂)
instance LinearMap.instNoZeroSMulDivisorsLinearMapToZeroToMonoidWithZeroInstZeroLinearMapInstSMulLinearMapToMonoidToDistribMulAction {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] [Module S M₂] [SMulCommClass R₂ S M₂] [] :
NoZeroSMulDivisors S (M →ₛₗ[σ₁₂] M₂)

### Monoid structure of endomorphisms #

instance LinearMap.instOneEnd {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
One ()
instance LinearMap.instMulEnd {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
Mul ()
theorem LinearMap.one_eq_id {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
1 = LinearMap.id
theorem LinearMap.mul_eq_comp {R : Type u_1} {M : Type u_9} [] [] [Module R M] (f : ) (g : ) :
f * g =
@[simp]
theorem LinearMap.one_apply {R : Type u_1} {M : Type u_9} [] [] [Module R M] (x : M) :
1 x = x
@[simp]
theorem LinearMap.mul_apply {R : Type u_1} {M : Type u_9} [] [] [Module R M] (f : ) (g : ) (x : M) :
↑(f * g) x = f (g x)
theorem LinearMap.coe_one {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
1 = id
theorem LinearMap.coe_mul {R : Type u_1} {M : Type u_9} [] [] [Module R M] (f : ) (g : ) :
↑(f * g) = f g
instance Module.End.monoid {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
instance Module.End.semiring {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
@[simp]
theorem Module.End.natCast_apply {R : Type u_1} {M : Type u_9} [] [] [Module R M] (n : ) (m : M) :
n m = n m

See also Module.End.natCast_def.

instance Module.End.ring {R : Type u_1} {N₁ : Type u_13} [] [] [Module R N₁] :
Ring (Module.End R N₁)
@[simp]
theorem Module.End.intCast_apply {R : Type u_1} {N₁ : Type u_13} [] [] [Module R N₁] (z : ) (m : N₁) :
z m = z m

See also Module.End.intCast_def.

instance Module.End.isScalarTower {R : Type u_1} {S : Type u_6} {M : Type u_9} [] [] [Module R M] [] [] [] :
instance Module.End.smulCommClass {R : Type u_1} {S : Type u_6} {M : Type u_9} [] [] [Module R M] [] [] [] [SMul S R] [] :
instance Module.End.smulCommClass' {R : Type u_1} {S : Type u_6} {M : Type u_9} [] [] [Module R M] [] [] [] [SMul S R] [] :
theorem Module.End_isUnit_apply_inv_apply_of_isUnit {R : Type u_1} {M : Type u_9} [] [] [Module R M] {f : } (h : ) (x : M) :
f (().inv x) = x
theorem Module.End_isUnit_inv_apply_apply_of_isUnit {R : Type u_1} {M : Type u_9} [] [] [Module R M] {f : } (h : ) (x : M) :
().inv (f x) = x
theorem LinearMap.coe_pow {R : Type u_1} {M : Type u_9} [] [] [Module R M] (f : M →ₗ[R] M) (n : ) :
↑(f ^ n) = (f)^[n]
theorem LinearMap.pow_apply {R : Type u_1} {M : Type u_9} [] [] [Module R M] (f : M →ₗ[R] M) (n : ) (m : M) :
↑(f ^ n) m = (f)^[n] m
theorem LinearMap.pow_map_zero_of_le {R : Type u_1} {M : Type u_9} [] [] [Module R M] {f : } {m : M} {k : } {l : } (hk : k l) (hm : ↑(f ^ k) m = 0) :
↑(f ^ l) m = 0
theorem LinearMap.commute_pow_left_of_commute {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [] [] [Module R M] [Semiring R₂] [] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} {g : } {g₂ : Module.End R₂ M₂} (h : = ) (k : ) :
LinearMap.comp (g₂ ^ k) f = LinearMap.comp f (g ^ k)
@[simp]
theorem LinearMap.id_pow {R : Type u_1} {M : Type u_9} [] [] [Module R M] (n : ) :
LinearMap.id ^ n = LinearMap.id
theorem LinearMap.iterate_succ {R : Type u_1} {M : Type u_9} [] [] [Module R M] {f' : M →ₗ[R] M} (n : ) :
f' ^ (n + 1) = LinearMap.comp (f' ^ n) f'
theorem LinearMap.iterate_surjective {R : Type u_1} {M : Type u_9} [] [] [Module R M] {f' : M →ₗ[R] M} (h : ) (n : ) :
theorem LinearMap.iterate_injective {R : Type u_1} {M : Type u_9} [] [] [Module R M] {f' : M →ₗ[R] M} (h : ) (n : ) :
theorem LinearMap.iterate_bijective {R : Type u_1} {M : Type u_9} [] [] [Module R M] {f' : M →ₗ[R] M} (h : ) (n : ) :
theorem LinearMap.injective_of_iterate_injective {R : Type u_1} {M : Type u_9} [] [] [Module R M] {f' : M →ₗ[R] M} {n : } (hn : n 0) (h : Function.Injective ↑(f' ^ n)) :
theorem LinearMap.surjective_of_iterate_surjective {R : Type u_1} {M : Type u_9} [] [] [Module R M] {f' : M →ₗ[R] M} {n : } (hn : n 0) (h : Function.Surjective ↑(f' ^ n)) :

### Action by a module endomorphism. #

instance LinearMap.applyModule {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
Module () M

The tautological action by Module.End R M (aka M →ₗ[R] M) on M.

This generalizes Function.End.applyMulAction.

@[simp]
theorem LinearMap.smul_def {R : Type u_1} {M : Type u_9} [] [] [Module R M] (f : ) (a : M) :
f a = f a
instance LinearMap.apply_faithfulSMul {R : Type u_1} {M : Type u_9} [] [] [Module R M] :

LinearMap.applyModule is faithful.

instance LinearMap.apply_smulCommClass {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
instance LinearMap.apply_smulCommClass' {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
instance LinearMap.apply_isScalarTower {R : Type u_17} {M : Type u_18} [] [] [Module R M] :

### Actions as module endomorphisms #

@[simp]
theorem DistribMulAction.toLinearMap_apply (R : Type u_1) {S : Type u_6} (M : Type u_9) [] [] [Module R M] [] [] [] (s : S) :
∀ (a : M), ↑() a = s a
def DistribMulAction.toLinearMap (R : Type u_1) {S : Type u_6} (M : Type u_9) [] [] [Module R M] [] [] [] (s : S) :

Each element of the monoid defines a linear map.

This is a stronger version of DistribMulAction.toAddMonoidHom.

Instances For
@[simp]
theorem DistribMulAction.toModuleEnd_apply (R : Type u_1) {S : Type u_6} (M : Type u_9) [] [] [Module R M] [] [] [] (s : S) :
↑() s =
def DistribMulAction.toModuleEnd (R : Type u_1) {S : Type u_6} (M : Type u_9) [] [] [Module R M] [] [] [] :
S →*

Each element of the monoid defines a module endomorphism.

This is a stronger version of DistribMulAction.toAddMonoidEnd.

Instances For
@[simp]
theorem Module.toModuleEnd_apply (R : Type u_1) {S : Type u_6} (M : Type u_9) [] [] [Module R M] [] [Module S M] [] (s : S) :
↑() s =
def Module.toModuleEnd (R : Type u_1) {S : Type u_6} (M : Type u_9) [] [] [Module R M] [] [Module S M] [] :

Each element of the semiring defines a module endomorphism.

This is a stronger version of DistribMulAction.toModuleEnd.

Instances For
@[simp]
theorem Module.moduleEndSelf_symm_apply (R : Type u_1) [] (f : ) :
↑() f = MulOpposite.op (f 1)
@[simp]
theorem Module.moduleEndSelf_apply (R : Type u_1) [] (s : Rᵐᵒᵖ) :
↑() s =

The canonical (semi)ring isomorphism from Rᵐᵒᵖ to Module.End R R induced by the right multiplication.

Instances For
@[simp]
theorem Module.moduleEndSelfOp_symm_apply (R : Type u_1) [] (f : ) :
↑() f = f 1
@[simp]
theorem Module.moduleEndSelfOp_apply (R : Type u_1) [] (s : R) :
def Module.moduleEndSelfOp (R : Type u_1) [] :

The canonical (semi)ring isomorphism from R to Module.End Rᵐᵒᵖ R induced by the left multiplication.

Instances For
theorem Module.End.natCast_def (R : Type u_1) {N₁ : Type u_13} [] (n : ) [] [Module R N₁] :
n = ↑() n
theorem Module.End.intCast_def (R : Type u_1) {N₁ : Type u_13} [] (z : ) [] [Module R N₁] :
z = ↑() z