Documentation

Mathlib.Algebra.Module.LinearMap.Defs

(Semi)linear maps #

In this file we define

We then provide LinearMap with the following instances:

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 #

TODO #

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 : MM₂) :

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.

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 M →ₙ+ M₂, M →ₑ[σ] M₂ :
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.

Instances For

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.

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 F M M₂, MulActionSemiHomClass F (⇑σ) M M₂ :

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
@[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₂] :

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
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₃] :
@[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₃] :
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
@[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
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
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
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₃
@[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
@[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 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' : 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
  • 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' : MM₃) (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' : MM₃) (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 : 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 : 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 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] :

Identity map as a LinearMap

Equations
theorem LinearMap.id_apply {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
id x = x
@[simp]
theorem LinearMap.id_coe {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] :
def LinearMap.id' {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomId σ] :

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) :
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 σ] :
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} :
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 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 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 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₂] :

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.

Instances
@[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₂] :
CompatibleSMul M M₂ R S
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] :
@[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₂] [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] [CompatibleSMul M M₂ R S] [IsScalarTower R S M₂] (f : M →ₗ[S] M₂) (hf : Function.Injective f) :
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₂] [CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂) :
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
@[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₂] [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₂] [CompatibleSMul M M₂ R S] :
CoeHTCT (M →ₗ[S] M₂) (M →ₗ[R] M₂)
Equations
@[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₂] [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₂] [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₂] [CompatibleSMul M M₂ R S] :
@[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₂] [CompatibleSMul M M₂ R S] (fₗ 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} :
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 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) :

Interpret a RingHom f as an f-semilinear map.

Equations
@[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✝
@[simp]
theorem RingHom.coe_toSemilinearMap {R : Type u_1} {S : Type u_5} [Semiring R] [Semiring S] (f : R →+* S) :
f.toSemilinearMap = f
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 ∘ₛₗ g = { toFun := f g, map_add' := , map_smul' := }

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

Pretty printer defined by notation3 command.

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

Composition of two linear maps is a linear map

Equations
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 ∘ₛₗ 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 ∘ₛₗ 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₃) :
@[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₃) :
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₄) :
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 : Surjective g) :
Injective fun (f : M₂ →ₛₗ[σ₂₃] M₃) => f ∘ₛₗ 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 ∘ₛₗ g = f' ∘ₛₗ 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 : Injective f) :
Injective fun (g : M₁ →ₛₗ[σ₁₂] M₂) => f ∘ₛₗ g

The linear map version of Function.Injective.comp_left

theorem LinearMap.surjective_comp_left_of_exists_rightInverse {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₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomCompTriple σ₁₃ σ₃₂ σ₁₂] (hf : ∃ (f' : M₃ →ₛₗ[σ₃₂] M₂), f ∘ₛₗ f' = id) :
Function.Surjective fun (g : M₁ →ₛₗ[σ₁₂] M₂) => f ∘ₛₗ g
@[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 g' : M₁ →ₛₗ[σ₁₂] M₂} (hf : Function.Injective f) :
f ∘ₛₗ g = f ∘ₛₗ 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 ∘ₛₗ f = id) :
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 ∘ₛₗ f = id) :
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 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₂] :
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₂] [CompatibleSMul M M₂ R S] :
CompatibleSMul M M₂ Rˣ S
def Module.compHom.toLinearMap {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (g : R →+* S) :

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

Equations
@[simp]
theorem Module.compHom.toLinearMap_apply {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (g : R →+* S) (a : R) :
(toLinearMap g) a = g a
@[deprecated "No deprecation message was provided." (since := "2024-11-08")]
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
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₂
@[deprecated "No deprecation message was provided." (since := "2024-11-08")]
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
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.

@[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 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 : MM₂) (lin : IsLinearMap R f) :
M →ₗ[R] M₂

Convert an IsLinearMap predicate to a LinearMap

Equations
@[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 : MM₂} (lin : IsLinearMap R f) (x : M) :
(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 : MM₂} (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 : MM₂} (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 : MM₂} (lin : IsLinearMap R f) (x 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₂) :

Reinterpret an additive homomorphism as an -linear map.

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

Reinterpret an additive homomorphism as a -linear map.

Equations
@[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
@[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₂)
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₂)
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₂)

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
@[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 ∘ₛₗ 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₂) :
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
@[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₂} :
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
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
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
@[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 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 h : M₂ →ₛₗ[σ₂₃] M₃) :
(h + g) ∘ₛₗ f = h ∘ₛₗ f + g ∘ₛₗ 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 g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) :
h ∘ₛₗ (f + g) = h ∘ₛₗ f + h ∘ₛₗ 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
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
@[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₃) :
@[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₃) :
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
@[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 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 h : M₂ →ₛₗ[σ₂₃] N₃) :
(g - h) ∘ₛₗ f = g ∘ₛₗ f - h ∘ₛₗ 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 g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) :
h ∘ₛₗ (g - f) = h ∘ₛₗ g - h ∘ₛₗ 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
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
@[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₂) :
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
@[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₂) :
@[simp]
theorem LinearMap.identityMapOfZeroModuleIsZero {R₁ : Type u_2} {M : Type u_8} [Semiring R₁] [AddCommMonoid M] [Module R₁ M] [Subsingleton M] :
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
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) ∘ₛₗ f = a g ∘ₛₗ 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₃] [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
@[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] [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] [CompatibleSMul M N R S] (f 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] [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] [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] [CompatibleSMul M N R S] [AddCommMonoid P] [Module S P] [Module R P] [CompatibleSMul N P R S] [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] [CompatibleSMul M N R S] {T : Type u_20} [CommSemiring T] [Module T M] [Module T N] [CompatibleSMul M N S T] [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] [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
@[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] [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) :
(restrictScalarsₗ R S M N R₁) fₗ = R fₗ