# Documentation

Mathlib.Algebra.Module.LinearMap

# (Semi)linear maps #

In this file we define

• LinearMap σ M M₂, M →ₛₗ[σ] M₂→ₛₗ[σ] M₂ : a semilinear map between two Modules. Here, σ is a RingHom from R to R₂ and an f : M →ₛₗ[σ] 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₂→ₗ[R] M₂. We also add the notation M →ₗ⋆[R] M₂→ₗ⋆[R] M₂⋆[R] M₂ for star-linear maps.

• IsLinearMap R f : predicate saying that f : M → 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} [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] (f : MM₂) :
• A linear map preserves addition.

map_add : ∀ (x y : M), f (x + y) = f x + f y
• A linear map preserves scalar multiplication.

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

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_1} {S : Type u_2} [inst : ] [inst : ] (σ : R →+* S) (M : Type u_3) (M₂ : Type u_4) [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₂] extends :
Type (maxu_3u_4)
• A linear map preserves scalar multiplication. We prefer the spelling _root_.map_smul instead.

A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S→+* 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₂→ₛₗ[σ] M₂) are bundled versions of such maps. For plain linear maps (i.e. for which σ = RingHom.id R), the notation M →ₗ[R] 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→ₛₗ[σ] N is the type of σ-semilinear maps from M to N.

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

M →ₗ[R] N→ₗ[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.

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

Equations
• One or more equations did not get rendered due to their size.
class SemilinearMapClass (F : Type u_1) {R : outParam (Type u_2)} {S : outParam (Type u_3)} [inst : ] [inst : ] (σ : outParam (R →+* S)) (M : outParam (Type u_4)) (M₂ : outParam (Type u_5)) [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₂] extends :
Type (max(maxu_1u_4)u_5)
• A semilinear map preserves scalar multiplication up to some ring homomorphism σ. See also _root_.map_smul for the case where σ is the identity.

map_smulₛₗ : ∀ (f : F) (r : R) (x : M), f (r x) = σ r f x

SemilinearMapClass F σ M M₂ asserts F is a type of bundled σ-semilinear maps M → 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→+* 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]
abbrev LinearMapClass (F : Type u_1) (R : outParam (Type u_2)) (M : outParam (Type u_3)) (M₂ : outParam (Type u_4)) [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] :
Type (max(maxu_1u_3)u_4)

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

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

Equations
instance SemilinearMapClass.addMonoidHomClass {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} (F : Type u_5) :
{x : } → {x_1 : } → {x_2 : } → {x_3 : } → {x_4 : Module R M} → {x_5 : Module S M₃} → {σ : R →+* S} → [inst : SemilinearMapClass F σ M M₃] →
Equations
instance SemilinearMapClass.distribMulActionHomClass {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} (F : Type u_4) :
{x : } → {x_1 : } → {x_2 : } → {x_3 : Module R M} → {x_4 : Module R M₂} → [inst : LinearMapClass F R M M₂] →
Equations
• One or more equations did not get rendered due to their size.
theorem SemilinearMapClass.map_smul_inv {R : Type u_2} {S : Type u_1} {M : Type u_5} {M₃ : Type u_3} {F : Type u_4} :
∀ {x : } {x_1 : } {x_2 : } {x_3 : } {x_4 : Module R M} {x_5 : Module S M₃} {σ : R →+* S} (f : F) [i : SemilinearMapClass F σ M M₃] {σ' : S →+* R} [inst : ] (c : S) (x_6 : M), c f x_6 = f (σ' c x_6)
instance LinearMap.instSemilinearMapClassLinearMap {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} :
SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃
Equations
instance LinearMap.instFunLikeLinearMap {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} :
FunLike (M →ₛₗ[σ] M₃) M fun x => M₃
Equations
• LinearMap.instFunLikeLinearMap = let src := AddHomClass.toFunLike; { coe := FunLike.coe, coe_injective' := (_ : Function.Injective FunLike.coe) }
def LinearMap.toDistribMulActionHom {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] (f : M →ₗ[R] M₂) :
M →+[R] M₂

The DistribMulActionHom underlying a LinearMap.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem LinearMap.coe_toAddHom {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
theorem LinearMap.toFun_eq_coe {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} :
theorem LinearMap.ext {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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_2} {M : Type u_3} {M₃ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem LinearMap.coe_copy {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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_2} {M : Type u_3} {M₃ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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_2} {M : Type u_3} {M₃ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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_2} {M : Type u_3} {M₃ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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_2} [inst : ] [inst : ] [inst : Module R M] :

Identity map as a LinearMap

Equations
• One or more equations did not get rendered due to their size.
theorem LinearMap.id_apply {R : Type u_2} {M : Type u_1} [inst : ] [inst : ] [inst : Module R M] (x : M) :
LinearMap.id x = x
@[simp]
theorem LinearMap.id_coe {R : Type u_2} {M : Type u_1} [inst : ] [inst : ] [inst : Module R M] :
LinearMap.id = id
theorem LinearMap.isLinear {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] (fₗ : M →ₗ[R] M₂) :
IsLinearMap R fₗ
theorem LinearMap.coe_injective {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} :
Function.Injective FunLike.coe
theorem LinearMap.congr_arg {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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_2} {M : Type u_3} {M₃ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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_3} {S : Type u_4} {M : Type u_2} {M₃ : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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_3} {S : Type u_4} {M : Type u_2} {M₃ : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
f 0 = 0
theorem LinearMap.map_smulₛₗ {R : Type u_2} {S : Type u_4} {M : Type u_3} {M₃ : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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_2} {M : Type u_3} {M₂ : Type u_1} [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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_2} {S : Type u_1} {M : Type u_4} {M₃ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) {σ' : S →+* R} [inst : ] (c : S) (x : M) :
c f x = f (σ' c x)
@[simp]
theorem LinearMap.map_eq_zero_iff {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : ) {x : M} :
f x = 0 x = 0
@[simp]
theorem image_smul_setₛₗ {R : Type u_2} {S : Type u_3} (M : Type u_4) (M₃ : Type u_5) [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₃] (σ : R →+* S) {F : Type u_1} (h : F) [inst : SemilinearMapClass F σ M M₃] (c : R) (s : Set M) :
h '' (c s) = σ c h '' s
theorem preimage_smul_setₛₗ {R : Type u_2} {S : Type u_3} (M : Type u_4) (M₃ : Type u_5) [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₃] (σ : R →+* S) {F : Type u_1} (h : F) [inst : SemilinearMapClass F σ M M₃] {c : R} (hc : ) (s : Set M₃) :
h ⁻¹' (σ c s) = c h ⁻¹' s
theorem image_smul_set (R : Type u_2) (M : Type u_3) (M₂ : Type u_4) [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] {F : Type u_1} (h : F) [inst : LinearMapClass F R M M₂] (c : R) (s : Set M) :
h '' (c s) = c h '' s
theorem preimage_smul_set (R : Type u_2) (M : Type u_3) (M₂ : Type u_4) [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] {F : Type u_1} (h : F) [inst : LinearMapClass F R M M₂] {c : R} (hc : ) (s : Set M₂) :
h ⁻¹' (c s) = c h ⁻¹' s
class LinearMap.CompatibleSMul (M : Type u_1) (M₂ : Type u_2) [inst : ] [inst : ] (R : Type u_3) (S : Type u_4) [inst : ] [inst : SMul R M] [inst : Module S M] [inst : SMul R M₂] [inst : Module S M₂] :
• Scalar multiplication by R of M can be moved through linear maps.

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

A typeclass for has_smul structures which can be moved through a LinearMap. This typeclass is generated automatically from a 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_1} {M₂ : Type u_2} [inst : ] [inst : ] {R : Type u_3} {S : Type u_4} [inst : ] [inst : SMul R S] [inst : SMul R M] [inst : Module S M] [inst : ] [inst : SMul R M₂] [inst : Module S M₂] [inst : IsScalarTower R S M₂] :
Equations
• LinearMap.IsScalarTower.compatibleSMul = { map_smul := (_ : ∀ (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c x) = c fₗ x) }
@[simp]
theorem LinearMap.map_smul_of_tower {M : Type u_3} {M₂ : Type u_4} [inst : ] [inst : ] {R : Type u_1} {S : Type u_2} [inst : ] [inst : SMul R M] [inst : Module S M] [inst : SMul R M₂] [inst : Module S M₂] [inst : ] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) :
fₗ (c x) = c fₗ x
def LinearMap.toAddMonoidHom {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
M →+ M₃

convert a linear map to an additive map

Equations
• = { toZeroHom := { toFun := f, map_zero' := (_ : f 0 = 0) }, map_add' := (_ : ∀ (x y : M), f (x + y) = f x + f y) }
@[simp]
theorem LinearMap.toAddMonoidHom_coe {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
= f
def LinearMap.restrictScalars (R : Type u_1) {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : ] (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ₗ = { toAddHom := { toFun := fₗ, map_add' := (_ : ∀ (x y : M), fₗ (x + y) = fₗ x + fₗ y) }, map_smul' := (_ : ∀ (c : R) (x : M), fₗ (c x) = c fₗ x) }
instance LinearMap.coeIsScalarTower (R : Type u_1) {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : ] :
CoeHTCT (M →ₗ[S] M₂) (M →ₗ[R] M₂)
Equations
• = { coe := R }
@[simp]
theorem LinearMap.coe_restrictScalars (R : Type u_4) {S : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : ] (f : M →ₗ[S] M₂) :
↑(R f) = f
theorem LinearMap.restrictScalars_apply (R : Type u_4) {S : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : ] (fₗ : M →ₗ[S] M₂) (x : M) :
↑(R fₗ) x = fₗ x
theorem LinearMap.restrictScalars_injective (R : Type u_4) {S : Type u_3} {M : Type u_1} {M₂ : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : ] :
@[simp]
theorem LinearMap.restrictScalars_inj (R : Type u_4) {S : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : ] (fₗ : M →ₗ[S] M₂) (gₗ : M →ₗ[S] M₂) :
R fₗ = R gₗ fₗ = gₗ
theorem LinearMap.toAddMonoidHom_injective {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} :
theorem LinearMap.ext_ring {R : Type u_1} {S : Type u_2} {M₃ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : 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_2} [inst : ] [inst : ] [inst : 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_2} {M₃ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : 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_2} [inst : ] [inst : ] (f : R →+* S) (a : R) :
↑() a = f a
def RingHom.toSemilinearMap {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] (f : R →+* S) :

Interpret a RingHom f as an f-semilinear map.

Equations
• One or more equations did not get rendered due to their size.
def LinearMap.comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) :
M₁ →ₛₗ[σ₁₃] M₃

Composition of two linear maps is a linear map

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

∘ₗ∘ₗ 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
theorem LinearMap.comp_apply {R₁ : Type u_3} {R₂ : Type u_5} {R₃ : Type u_4} {M₁ : Type u_2} {M₂ : Type u_6} {M₃ : Type u_1} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) (x : M₁) :
↑() x = f (g x)
@[simp]
theorem LinearMap.coe_comp {R₁ : Type u_3} {R₂ : Type u_5} {R₃ : Type u_4} {M₁ : Type u_1} {M₂ : Type u_6} {M₃ : Type u_2} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : 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_1} {M₃ : Type u_2} [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] {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_1} {M₃ : Type u_2} [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃) :
LinearMap.comp LinearMap.id f = f
theorem LinearMap.cancel_right {R₁ : Type u_3} {R₂ : Type u_4} {R₃ : Type u_6} {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_5} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} {g : M₁ →ₛₗ[σ₁₂] M₂} {f' : M₂ →ₛₗ[σ₂₃] M₃} (hg : ) :
= f = f'
theorem LinearMap.cancel_left {R₁ : Type u_6} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_5} {M₂ : Type u_1} {M₃ : Type u_2} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} {g : M₁ →ₛₗ[σ₁₂] M₂} {g' : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) :
= g = g'
def LinearMap.inverse {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module S M₂] {σ : R →+* S} {σ' : S →+* R} [inst : ] (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.

Equations
• One or more equations did not get rendered due to their size.
theorem LinearMap.map_neg {R : Type u_3} {S : Type u_4} {M : Type u_2} {M₂ : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] {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_3} {S : Type u_4} {M : Type u_2} {M₂ : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] {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_1} {M₂ : Type u_2} [inst : ] [inst : ] {S : Type u_3} [inst : ] [inst : Module S M] [inst : Module S M₂] :
Equations
• LinearMap.CompatibleSMul.intModule = { map_smul := (_ : ∀ (fₗ : M →ₗ[S] M₂) (c : ) (x : M), fₗ (c x) = c fₗ x) }
instance LinearMap.CompatibleSMul.units {M : Type u_1} {M₂ : Type u_2} [inst : ] [inst : ] {R : Type u_3} {S : Type u_4} [inst : ] [inst : ] [inst : MulAction R M₂] [inst : ] [inst : Module S M] [inst : Module S M₂] [inst : ] :
Equations
• LinearMap.CompatibleSMul.units = { map_smul := (_ : ∀ (fₗ : M →ₗ[S] M₂) (c : Rˣ) (x : M), fₗ (c x) = c fₗ x) }
@[simp]
theorem Module.compHom.toLinearMap_apply {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] (g : R →+* S) (a : R) :
= g a
def Module.compHom.toLinearMap {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] (g : R →+* S) :

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

Equations
• = { toAddHom := { toFun := g, map_add' := (_ : ∀ (a b : R), g (a + b) = g a + g b) }, map_smul' := (_ : ∀ (a b : R), g (a * b) = g a * g b) }
def DistribMulActionHom.toLinearMap {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] (fₗ : M →+[R] M₂) :
M →ₗ[R] M₂

A DistribMulActionHom between two modules is a linear map.

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem DistribMulActionHom.coe_toLinearMap {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] (f : M →+[R] M₂) :
f = f
theorem DistribMulActionHom.toLinearMap_injective {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : 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_2} {M₂ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] (f : MM₂) (H : ) :
M →ₗ[R] M₂

Convert an IsLinearMap predicate to a LinearMap

Equations
• = { toAddHom := { toFun := f, map_add' := (_ : ∀ (x y : M), f (x + y) = f x + f y) }, map_smul' := (_ : ∀ (c : R) (x : M), f (c x) = c f x) }
@[simp]
theorem IsLinearMap.mk'_apply {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] {f : MM₂} (H : ) (x : M) :
↑() x = f x
theorem IsLinearMap.isLinearMap_smul {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] (c : R) :
IsLinearMap R fun z => c z
theorem IsLinearMap.isLinearMap_smul' {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] (a : M) :
IsLinearMap R fun c => c a
theorem IsLinearMap.map_zero {R : Type u_3} {M : Type u_2} {M₂ : Type u_1} [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] {f : MM₂} (lin : ) :
f 0 = 0
theorem IsLinearMap.isLinearMap_neg {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] :
IsLinearMap R fun z => -z
theorem IsLinearMap.map_neg {R : Type u_3} {M : Type u_2} {M₂ : Type u_1} [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] {f : MM₂} (lin : ) (x : M) :
f (-x) = -f x
theorem IsLinearMap.map_sub {R : Type u_3} {M : Type u_2} {M₂ : Type u_1} [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R M₂] {f : MM₂} (lin : ) (x : M) (y : M) :
f (x - y) = f x - f y
@[inline]
abbrev Module.End (R : Type u) (M : Type v) [inst : ] [inst : ] [inst : Module R M] :

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

Equations
def AddMonoidHom.toNatLinearMap {M : Type u_1} {M₂ : Type u_2} [inst : ] [inst : ] (f : M →+ M₂) :

Reinterpret an additive homomorphism as a ℕ-linear map.

Equations
• = { toAddHom := { toFun := f, map_add' := (_ : ∀ (a b : M), f (a + b) = f a + f b) }, map_smul' := (_ : ∀ (n : ) (a : M), f (n a) = n f a) }
theorem AddMonoidHom.toNatLinearMap_injective {M : Type u_1} {M₂ : Type u_2} [inst : ] [inst : ] :
def AddMonoidHom.toIntLinearMap {M : Type u_1} {M₂ : Type u_2} [inst : ] [inst : ] (f : M →+ M₂) :

Reinterpret an additive homomorphism as a ℤ-linear map.

Equations
• = { toAddHom := { toFun := f, map_add' := (_ : ∀ (a b : M), f (a + b) = f a + f b) }, map_smul' := (_ : ∀ (n : ) (g : M), f (n g) = n f g) }
theorem AddMonoidHom.toIntLinearMap_injective {M : Type u_1} {M₂ : Type u_2} [inst : ] [inst : ] :
@[simp]
theorem AddMonoidHom.coe_toIntLinearMap {M : Type u_1} {M₂ : Type u_2} [inst : ] [inst : ] (f : M →+ M₂) :
= f
def AddMonoidHom.toRatLinearMap {M : Type u_1} {M₂ : Type u_2} [inst : ] [inst : ] [inst : ] [inst : Module M₂] (f : M →+ M₂) :

Reinterpret an additive homomorphism as a ℚ-linear map.

Equations
• One or more equations did not get rendered due to their size.
theorem AddMonoidHom.toRatLinearMap_injective {M : Type u_1} {M₂ : Type u_2} [inst : ] [inst : ] [inst : ] [inst : Module M₂] :
@[simp]
theorem AddMonoidHom.coe_toRatLinearMap {M : Type u_1} {M₂ : Type u_2} [inst : ] [inst : ] [inst : ] [inst : Module M₂] (f : M →+ M₂) :
= f
instance LinearMap.instSMulLinearMap {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : ] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : ] [inst : ] [inst : SMulCommClass R₂ S M₂] :
SMul S (M →ₛₗ[σ₁₂] M₂)
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem LinearMap.smul_apply {R : Type u_1} {R₂ : Type u_2} {S : Type u_5} {M : Type u_3} {M₂ : Type u_4} [inst : ] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : ] [inst : ] [inst : 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_2} {S : Type u_5} {M : Type u_3} {M₂ : Type u_4} [inst : ] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : ] [inst : ] [inst : SMulCommClass R₂ S M₂] (a : S) (f : M →ₛₗ[σ₁₂] M₂) :
↑(a f) = a f
instance LinearMap.instSMulCommClassLinearMapInstSMulLinearMapInstSMulLinearMap {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {T : Type u_4} {M : Type u_5} {M₂ : Type u_6} [inst : ] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : ] [inst : ] [inst : SMulCommClass R₂ S M₂] [inst : ] [inst : ] [inst : SMulCommClass R₂ T M₂] [inst : SMulCommClass S T M₂] :
SMulCommClass S T (M →ₛₗ[σ₁₂] M₂)
Equations
instance LinearMap.instIsScalarTowerLinearMapInstSMulLinearMapInstSMulLinearMap {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {T : Type u_4} {M : Type u_5} {M₂ : Type u_6} [inst : ] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : ] [inst : ] [inst : SMulCommClass R₂ S M₂] [inst : ] [inst : ] [inst : SMulCommClass R₂ T M₂] [inst : SMul S T] [inst : IsScalarTower S T M₂] :
IsScalarTower S T (M →ₛₗ[σ₁₂] M₂)
Equations
instance LinearMap.instIsCentralScalarLinearMapInstSMulLinearMapMulOppositeMonoid {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : ] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : ] [inst : ] [inst : SMulCommClass R₂ S M₂] [inst : ] [inst : SMulCommClass R₂ Sᵐᵒᵖ M₂] [inst : ] :
IsCentralScalar S (M →ₛₗ[σ₁₂] M₂)
Equations

### Arithmetic on the codomain #

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

The constant 0 map is linear.

Equations
• LinearMap.instZeroLinearMap = { zero := { toAddHom := { toFun := 0, map_add' := (_ : MM0 = 0 + 0) }, map_smul' := (_ : ∀ (a : R₁), M0 = σ₁₂ a 0) } }
@[simp]
theorem LinearMap.zero_apply {R₁ : Type u_3} {R₂ : Type u_4} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R₁] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (x : M) :
0 x = 0
@[simp]
theorem LinearMap.comp_zero {R₁ : Type u_6} {R₂ : Type u_1} {R₃ : Type u_2} {M : Type u_5} {M₂ : Type u_3} {M₃ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ M₂] [inst : Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →ₛₗ[σ₂₃] M₃) :
= 0
@[simp]
theorem LinearMap.zero_comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_6} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ M₂] [inst : Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) :
= 0
instance LinearMap.instInhabitedLinearMap {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
Inhabited (M →ₛₗ[σ₁₂] M₂)
Equations
• LinearMap.instInhabitedLinearMap = { default := 0 }
@[simp]
theorem LinearMap.default_def {R₁ : Type u_3} {R₂ : Type u_4} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R₁] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
default = 0
instance LinearMap.instAddLinearMap {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :

The sum of two linear maps is linear.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem LinearMap.add_apply {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R₁ M] [inst : 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_1} {R₂ : Type u_2} {R₃ : Type u_5} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ M₂] [inst : Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₂ →ₛₗ[σ₂₃] M₃) :
LinearMap.comp (h + g) f = +
theorem LinearMap.comp_add {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_5} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ M₂] [inst : Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) :
LinearMap.comp h (f + g) = +
instance LinearMap.addCommMonoid {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :

The type of linear maps is an additive monoid.

Equations
• One or more equations did not get rendered due to their size.
instance LinearMap.instNegLinearMapToAddCommMonoid {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {N₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
Neg (M →ₛₗ[σ₁₂] N₂)

The negation of a linear map is linear.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem LinearMap.neg_apply {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {N₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] N₂) (x : M) :
↑(-f) x = -f x
@[simp]
theorem LinearMap.neg_comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_5} {M : Type u_3} {M₂ : Type u_4} {N₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ M₂] [inst : Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) :
@[simp]
theorem LinearMap.comp_neg {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_5} {M : Type u_3} {N₂ : Type u_4} {N₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ N₂] [inst : Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃] N₃) :
instance LinearMap.instSubLinearMapToAddCommMonoid {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {N₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
Sub (M →ₛₗ[σ₁₂] N₂)

The subtraction of two linear maps is linear.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem LinearMap.sub_apply {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {N₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R₁ M] [inst : 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_1} {R₂ : Type u_2} {R₃ : Type u_5} {M : Type u_3} {M₂ : Type u_4} {N₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ M₂] [inst : Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) (h : M₂ →ₛₗ[σ₂₃] N₃) :
LinearMap.comp (g - h) f = -
theorem LinearMap.comp_sub {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_5} {M : Type u_3} {N₂ : Type u_4} {N₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ N₂] [inst : Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) :
LinearMap.comp h (g - f) = -
instance LinearMap.addCommGroup {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {N₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R₁ M] [inst : Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :

The type of linear maps is an additive group.

Equations
• One or more equations did not get rendered due to their size.
instance LinearMap.instDistribMulActionLinearMapToAddMonoidAddCommMonoid {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : ] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : ] [inst : ] [inst : SMulCommClass R₂ S M₂] :
DistribMulAction S (M →ₛₗ[σ₁₂] M₂)
Equations
theorem LinearMap.smul_comp {R : Type u_5} {R₂ : Type u_1} {R₃ : Type u_2} {S₃ : Type u_7} {M : Type u_6} {M₂ : Type u_3} {M₃ : Type u_4} [inst : ] [inst : Semiring R₂] [inst : Semiring R₃] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : Module R₂ M₂] [inst : Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst : Monoid S₃] [inst : DistribMulAction S₃ M₃] [inst : 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_4} {M : Type u_5} {M₂ : Type u_2} {M₃ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : ] [inst : Module R M] [inst : ] [inst : ] [inst : Module R M₂] [inst : Module R M₃] [inst : SMulCommClass R S M₂] [inst : ] [inst : SMulCommClass R S M₃] [inst : LinearMap.CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) :
LinearMap.comp g (a f) = a
instance LinearMap.instModuleLinearMapAddCommMonoid {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : ] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : ] [inst : Module S M₂] [inst : SMulCommClass R₂ S M₂] :
Module S (M →ₛₗ[σ₁₂] M₂)
Equations
instance LinearMap.instNoZeroSMulDivisorsLinearMapToZeroToMonoidWithZeroInstZeroLinearMapInstSMulLinearMapToMonoidToDistribMulAction {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : ] [inst : Semiring R₂] [inst : ] [inst : ] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : ] [inst : Module S M₂] [inst : SMulCommClass R₂ S M₂] [inst : ] :
NoZeroSMulDivisors S (M →ₛₗ[σ₁₂] M₂)
Equations
• One or more equations did not get rendered due to their size.

### Monoid structure of endomorphisms #

Lemmas about pow such as LinearMap.pow_apply appear in later files.

instance LinearMap.instOneEnd {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] :
One ()
Equations
• LinearMap.instOneEnd = { one := LinearMap.id }
instance LinearMap.instMulEnd {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] :
Mul ()
Equations
• LinearMap.instMulEnd = { mul := LinearMap.comp }
theorem LinearMap.one_eq_id {R : Type u_2} {M : Type u_1} [inst : ] [inst : ] [inst : Module R M] :
1 = LinearMap.id
theorem LinearMap.mul_eq_comp {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] (f : ) (g : ) :
f * g =
@[simp]
theorem LinearMap.one_apply {R : Type u_2} {M : Type u_1} [inst : ] [inst : ] [inst : Module R M] (x : M) :
1 x = x
@[simp]
theorem LinearMap.mul_apply {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] (f : ) (g : ) (x : M) :
↑(f * g) x = f (g x)
theorem LinearMap.coe_one {R : Type u_2} {M : Type u_1} [inst : ] [inst : ] [inst : Module R M] :
1 = id
theorem LinearMap.coe_mul {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] (f : ) (g : ) :
↑(f * g) = f g
instance Module.End.monoid {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] :
Equations
instance Module.End.semiring {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Module.End.natCast_apply {R : Type u_2} {M : Type u_1} [inst : ] [inst : ] [inst : 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_2} [inst : ] [inst : ] [inst : Module R N₁] :
Ring (Module.End R N₁)
Equations
• Module.End.ring = let src := Module.End.semiring; let src_1 := LinearMap.addCommGroup; Ring.mk SubNegMonoid.zsmul (_ : ∀ (a : N₁ →ₗ[R] N₁), -a + a = 0)
@[simp]
theorem Module.End.intCast_apply {R : Type u_2} {N₁ : Type u_1} [inst : ] [inst : ] [inst : 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_2} {M : Type u_3} [inst : ] [inst : ] [inst : Module R M] [inst : ] [inst : ] [inst : ] :
Equations
instance Module.End.smulCommClass {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : ] [inst : ] [inst : Module R M] [inst : ] [inst : ] [inst : ] [inst : SMul S R] [inst : ] :
Equations
instance Module.End.smulCommClass' {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : ] [inst : ] [inst : Module R M] [inst : ] [inst : ] [inst : ] [inst : SMul S R] [inst : ] :
Equations

### Action by a module endomorphism. #

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

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

This generalizes Function.End.applyMulAction.

Equations
• LinearMap.applyModule = Module.mk (_ : ∀ (f g : M →ₗ[R] M) (x : M), ↑(f + g) x = f x + g x) (_ : ∀ (x : M), 0 x = 0)
@[simp]
theorem LinearMap.smul_def {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] (f : ) (a : M) :
f a = f a
instance LinearMap.apply_faithfulSMul {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] :

LinearMap.applyModule is faithful.

Equations
instance LinearMap.apply_smulCommClass {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] :
Equations
instance LinearMap.apply_smulCommClass' {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] :
Equations
instance LinearMap.apply_isScalarTower {R : Type u_1} {M : Type u_2} [inst : ] [inst : ] [inst : Module R M] :
Equations

### Actions as module endomorphisms #

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

Each element of the monoid defines a linear map.

This is a stronger version of DistribMulAction.toAddMonoidHom.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem DistribMulAction.toModuleEnd_apply (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : ] [inst : ] [inst : Module R M] [inst : ] [inst : ] [inst : ] (s : S) :
↑() s =
def DistribMulAction.toModuleEnd (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : ] [inst : ] [inst : Module R M] [inst : ] [inst : ] [inst : ] :
S →*

Each element of the monoid defines a module endomorphism.

This is a stronger version of DistribMulAction.toAddMonoidEnd.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Module.toModuleEnd_apply (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : ] [inst : ] [inst : Module R M] [inst : ] [inst : Module S M] [inst : ] (s : S) :
↑() s =
def Module.toModuleEnd (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : ] [inst : ] [inst : Module R M] [inst : ] [inst : Module S M] [inst : ] :

Each element of the semiring defines a module endomorphism.

This is a stronger version of DistribMulAction.toModuleEnd.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Module.moduleEndSelf_symm_apply_unop (R : Type u_1) [inst : ] (f : ) :
(↑() f).unop = f 1
@[simp]
theorem Module.moduleEndSelf_apply (R : Type u_1) [inst : ] (s : Rᵐᵒᵖ) :
↑() s =
def Module.moduleEndSelf (R : Type u_1) [inst : ] :

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Module.moduleEndSelfOp_symm_apply (R : Type u_1) [inst : ] (f : ) :
↑() f = f 1
@[simp]
theorem Module.moduleEndSelfOp_apply (R : Type u_1) [inst : ] (s : R) :
def Module.moduleEndSelfOp (R : Type u_1) [inst : ] :

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

Equations
• One or more equations did not get rendered due to their size.
theorem Module.End.natCast_def (R : Type u_2) {N₁ : Type u_1} [inst : ] (n : ) [inst : ] [inst : Module R N₁] :
n = ↑() n
theorem Module.End.intCast_def (R : Type u_2) {N₁ : Type u_1} [inst : ] (z : ) [inst : ] [inst : Module R N₁] :
z = ↑() z