Documentation

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

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.

Instances For

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

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.

toFun : M → M₂
map_add' : ∀ (x y : M), self.toFun (x + y) = self.toFun x + self.toFun y
map_smul' : ∀ (r : R) (x : M), self.toFun (r • x) = σ r • self.toFun x
A linear map preserves scalar multiplication. We prefer the spelling _root_.map_smul instead.

Instances For

def «term_→ₛₗ[_]_» :

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.

Instances For

def «term_→ₗ[_]_» :

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.

Instances For

def «term_→ₗ⋆[_]_» :

M →ₗ⋆[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.

Instances For

class SemilinearMapClass (F : Type u_17) {R : outParam (Type u_18)} {S : outParam (Type u_19)} [Semiring R] [Semiring S] (σ : outParam (R →+* S)) (M : outParam (Type u_20)) (M₂ : outParam (Type u_21)) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] [FunLike F M M₂] extends AddHomClass :

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.

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.

Instances

@[inline, reducible]

abbrev LinearMapClass (F : Type u_17) (R : outParam (Type u_18)) (M : Type u_19) (M₂ : Type u_20) [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

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

Instances For

instance SemilinearMapClass.instAddMonoidHomClass {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} (F : Type u_17) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] :

AddMonoidHomClass F M M₃

Equations

⋯ = ⋯

instance SemilinearMapClass.distribMulActionHomClass {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} (F : Type u_17) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [FunLike F M M₂] [LinearMapClass F R M M₂] :

DistribMulActionHomClass F R M M₂

Equations

⋯ = ⋯

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} [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_6} {M : Type u_9} {M₃ : Type u_12} {F : Type u_17} [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 = { toAddHom := { toFun := ⇑f, map_add' := ⋯ }, map_smul' := ⋯ }

Instances For

instance SemilinearMapClass.instCoeToSemilinearMap {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} {F : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] :

CoeHead F (M →ₛₗ[σ] M₃)

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

Equations

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

@[inline, reducible]

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

M₁ →ₗ[R] M₂

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

Equations

LinearMapClass.linearMap f = ↑f

Instances For

instance LinearMapClass.instCoeToLinearMap {R : Type u_1} {M₁ : Type u_10} {M₂ : Type u_11} {F : Type u_17} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [FunLike F M₁ M₂] [LinearMapClass F R M₁ M₂] :

CoeHead F (M₁ →ₗ[R] M₂)

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

Equations

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

instance LinearMap.instFunLike {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} :

FunLike (M →ₛₗ[σ] M₃) M M₃

Equations

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

instance LinearMap.semilinearMapClass {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} :

SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃

Equations

⋯ = ⋯

def LinearMap.toDistribMulActionHom {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) :

M →+[R] M₂

The DistribMulActionHom underlying a LinearMap.

Equations

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

Instances For

@[simp]

theorem LinearMap.coe_toAddHom {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [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_6} {M : Type u_9} {M₃ : Type u_12} [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_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {g : M →ₛₗ[σ] M₃} (h : ∀ (x : M), f x = g x) :

f = g

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

M →ₛₗ[σ] M₃

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

Equations

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

Instances For

@[simp]

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

⇑(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} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) :

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} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : AddHom M M₃) (h : ∀ (r : R) (x : M), f.toFun (r • x) = σ r • f.toFun x) :

⇑{ 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} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : AddHom M M₃) (h : ∀ (r : R) (x : M), f.toFun (r • x) = σ r • f.toFun x) :

↑{ toAddHom := f, map_smul' := h } = f

theorem LinearMap.coe_semilinearMap {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {F : Type u_17} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] (f : F) :

⇑↑f = ⇑f

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

f = g

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

M →ₗ[R] M

Identity map as a LinearMap

Equations

LinearMap.id = let __src := DistribMulActionHom.id R; { toAddHom := { toFun := __src.toFun, map_add' := ⋯ }, map_smul' := ⋯ }

Instances For

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

LinearMap.id x = x

@[simp]

theorem LinearMap.id_coe {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] :

⇑LinearMap.id = id

@[simp]

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

LinearMap.id' x = x

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

M →ₛₗ[σ] M

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

Equations

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

Instances For

@[simp]

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

⇑LinearMap.id' = id

theorem LinearMap.isLinear {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [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_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} :

Function.Injective DFunLike.coe

theorem LinearMap.congr_arg {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {x : M} {x' : M} :

x = x' → f x = f x'

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

f x = g x

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

theorem LinearMap.ext_iff {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [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} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : ∀ (r : R) (x : M), (↑f).toFun (r • x) = σ r • (↑f).toFun 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} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (x : M) (y : M) :

f (x + y) = f x + f y

theorem LinearMap.map_zero {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [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_6} {M : Type u_9} {M₃ : Type u_12} [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_9} {M₂ : Type u_11} [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_6} {M : Type u_9} {M₃ : Type u_12} [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_6} {M : Type u_9} {M₃ : Type u_12} [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_9) (M₂ : Type u_11) [AddCommMonoid M] [AddCommMonoid M₂] (R : Type u_17) (S : Type u_18) [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.intModule, allowing z • to be moved even if R 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 LinearMap.IsScalarTower.compatibleSMul {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] {R : Type u_17} {S : Type u_18} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [SMul R S] [IsScalarTower R S M] [IsScalarTower R S M₂] :

LinearMap.CompatibleSMul M M₂ R S

Equations

⋯ = ⋯

instance LinearMap.IsScalarTower.compatibleSMul' {M : Type u_9} [AddCommMonoid M] {R : Type u_17} {S : Type u_18} [Semiring S] [SMul R M] [Module S M] [SMul R S] [IsScalarTower R S M] :

LinearMap.CompatibleSMul S M R S

Equations

⋯ = ⋯

@[simp]

theorem LinearMap.map_smul_of_tower {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] {R : Type u_17} {S : Type u_18} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) :

fₗ (c • x) = c • fₗ x

theorem LinearMap.isScalarTower_of_injective {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] (R : Type u_17) {S : Type u_18} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [SMul R S] [LinearMap.CompatibleSMul M M₂ R S] [IsScalarTower R S M₂] (f : M →ₗ[S] M₂) (hf : Function.Injective ⇑f) :

IsScalarTower R S M

theorem LinearMap.isLinearMap_of_compatibleSMul (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂) :

IsLinearMap R ⇑f

def LinearMap.toAddMonoidHom {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [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

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

Instances For

@[simp]

theorem LinearMap.toAddMonoidHom_coe {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :

⇑(LinearMap.toAddMonoidHom f) = ⇑f

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

M →ₗ[R] M₂

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

See also LinearMap.map_smul_of_tower.

Equations

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

Instances For

instance LinearMap.coeIsScalarTower (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] :

CoeHTCT (M →ₗ[S] M₂) (M →ₗ[R] M₂)

Equations

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

@[simp]

theorem LinearMap.coe_restrictScalars (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂) :

⇑(↑R f) = ⇑f

theorem LinearMap.restrictScalars_apply (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (x : M) :

(↑R fₗ) x = fₗ x

theorem LinearMap.restrictScalars_injective (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] :

Function.Injective ↑R

@[simp]

theorem LinearMap.restrictScalars_inj (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (gₗ : M →ₗ[S] M₂) :

↑R fₗ = ↑R gₗ ↔ fₗ = gₗ

theorem LinearMap.toAddMonoidHom_injective {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} :

Function.Injective LinearMap.toAddMonoidHom

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

f = g

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

theorem LinearMap.ext_ring_iff {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [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} [Semiring R] [Semiring S] [AddCommMonoid M₃] [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} [Semiring R] [Semiring S] (f : R →+* S) :

∀ (a : R), (RingHom.toSemilinearMap f) a = f.toFun a

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

R →ₛₗ[f] S

Interpret a RingHom f as an f-semilinear map.

Equations

RingHom.toSemilinearMap f = { toAddHom := { toFun := f.toFun, map_add' := ⋯ }, map_smul' := ⋯ }

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₃] [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

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

Instances For

def LinearMap.compNotation :

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

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

Instances For

Lean.PrettyPrinter.Delaborator.Delab

def LinearMap.compNotation.delab :

Pretty printer defined by notation3 command.

Equations

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

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₃] [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₁) :

(LinearMap.comp 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_10} {M₂ : Type u_11} {M₃ : Type u_12} [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₂) :

⇑(LinearMap.comp f g) = ⇑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₃] [AddCommMonoid M₂] [AddCommMonoid M₃] {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₃] [AddCommMonoid M₂] [AddCommMonoid M₃] {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₃] [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_17} {M₄ : Type u_18} [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₄) :

LinearMap.comp (LinearMap.comp h g) f = LinearMap.comp h (LinearMap.comp g f)

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₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {g : M₁ →ₛₗ[σ₁₂] M₂} (hg : Function.Surjective ⇑g) :

Function.Injective fun (f : M₂ →ₛₗ[σ₂₃] M₃) => LinearMap.comp 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_10} {M₂ : Type u_11} {M₃ : Type u_12} [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) :

LinearMap.comp f g = LinearMap.comp 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_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} (hf : Function.Injective ⇑f) :

Function.Injective fun (g : M₁ →ₛₗ[σ₁₂] M₂) => LinearMap.comp f g

The linear map version of Function.Injective.comp_left

@[simp]

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

LinearMap.comp f g = LinearMap.comp f g' ↔ g = g'

def LinearMap.inverse {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [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

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

Instances For

theorem LinearMap.map_neg {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [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_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommGroup M] [AddCommGroup M₂] {module_M : Module R M} {module_M₂ : Module S M₂} {σ : R →+* S} (f : M →ₛₗ[σ] M₂) (x : M) (y : M) :

f (x - y) = f x - f y

instance LinearMap.CompatibleSMul.intModule {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] {S : Type u_17} [Semiring S] [Module S M] [Module S M₂] :

LinearMap.CompatibleSMul M M₂ ℤ S

Equations

⋯ = ⋯

instance LinearMap.CompatibleSMul.units {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] {R : Type u_17} {S : Type u_18} [Monoid R] [MulAction R M] [MulAction R M₂] [Semiring S] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] :

LinearMap.CompatibleSMul M M₂ Rˣ S

Equations

⋯ = ⋯

@[simp]

theorem Module.compHom.toLinearMap_apply {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] (g : R →+* S) (a : R) :

(Module.compHom.toLinearMap g) a = g a

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

R →ₗ[R] S

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

Equations

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

Instances For

instance DistribMulActionHom.instLinearMapClass {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :

LinearMapClass (M →+[R] M₂) R M M₂

A DistribMulActionHom between two modules is a linear map.

Equations

⋯ = ⋯

instance DistribMulActionHom.instCoeTCLinearMap {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :

CoeTC (M →+[R] M₂) (M →ₗ[R] M₂)

Equations

DistribMulActionHom.instCoeTCLinearMap = { coe := fun (f : M →+[R] M₂) => ↑f }

@[simp]

theorem DistribMulActionHom.coe_toLinearMap {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [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} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [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} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M → M₂) (H : IsLinearMap R f) :

M →ₗ[R] M₂

Convert an IsLinearMap predicate to a LinearMap

Equations

IsLinearMap.mk' f H = { toAddHom := { toFun := f, map_add' := ⋯ }, map_smul' := ⋯ }

Instances For

@[simp]

theorem IsLinearMap.mk'_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {f : M → M₂} (H : IsLinearMap R f) (x : M) :

(IsLinearMap.mk' f H) x = f x

theorem IsLinearMap.isLinearMap_smul {R : Type u_17} {M : Type u_18} [CommSemiring R] [AddCommMonoid M] [Module R M] (c : R) :

IsLinearMap R fun (z : M) => c • z

theorem IsLinearMap.isLinearMap_smul' {R : Type u_17} {M : Type u_18} [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_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {f : M → M₂} (lin : IsLinearMap R f) :

f 0 = 0

theorem IsLinearMap.isLinearMap_neg {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommGroup M] [Module R M] :

IsLinearMap R fun (z : M) => -z

theorem IsLinearMap.map_neg {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] {f : M → M₂} (lin : IsLinearMap R f) (x : M) :

f (-x) = -f x

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

f (x - y) = f x - f y

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

M →ₗ[ℕ ] M₂

Reinterpret an additive homomorphism as an ℕ-linear map.

Equations

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

Instances For

theorem AddMonoidHom.toNatLinearMap_injective {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] :

Function.Injective AddMonoidHom.toNatLinearMap

def AddMonoidHom.toIntLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) :

M →ₗ[ℤ ] M₂

Reinterpret an additive homomorphism as a ℤ-linear map.

Equations

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

Instances For

theorem AddMonoidHom.toIntLinearMap_injective {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] :

Function.Injective AddMonoidHom.toIntLinearMap

@[simp]

theorem AddMonoidHom.coe_toIntLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) :

⇑(AddMonoidHom.toIntLinearMap f) = ⇑f

def AddMonoidHom.toRatLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] (f : M →+ M₂) :

M →ₗ[ℚ ] M₂

Reinterpret an additive homomorphism as a ℚ-linear map.

Equations

AddMonoidHom.toRatLinearMap f = { toAddHom := { toFun := f.toFun, map_add' := ⋯ }, map_smul' := ⋯ }

Instances For

theorem AddMonoidHom.toRatLinearMap_injective {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] :

Function.Injective AddMonoidHom.toRatLinearMap

@[simp]

theorem AddMonoidHom.coe_toRatLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] (f : M →+ M₂) :

⇑(AddMonoidHom.toRatLinearMap f) = ⇑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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] :

SMul S (M →ₛₗ[σ₁₂] M₂)

Equations

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

@[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] [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_6} {M : Type u_9} {M₂ : Type u_11} [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.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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] [Monoid T] [DistribMulAction T M₂] [SMulCommClass R₂ T M₂] [SMulCommClass S T M₂] :

SMulCommClass S T (M →ₛₗ[σ₁₂] M₂)

Equations

⋯ = ⋯

instance LinearMap.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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] [Monoid T] [DistribMulAction T M₂] [SMulCommClass R₂ T M₂] [SMul S T] [IsScalarTower S T M₂] :

IsScalarTower S T (M →ₛₗ[σ₁₂] M₂)

Equations

⋯ = ⋯

instance LinearMap.instIsCentralScalarLinearMapInstSMulLinearMapMulOppositeMonoid {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] [DistribMulAction Sᵐᵒᵖ M₂] [SMulCommClass R₂ Sᵐᵒᵖ M₂] [IsCentralScalar S M₂] :

IsCentralScalar S (M →ₛₗ[σ₁₂] M₂)

Equations

⋯ = ⋯

instance LinearMap.instSMulDomMulActLinearMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] :

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

Equations

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

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

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

@[simp]

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

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

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

⇑(a • f) = a • ⇑f

instance LinearMap.instSMulCommClassDomMulActDomMulActLinearMapInstSMulDomMulActLinearMapInstSMulDomMulActLinearMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} {T' : Type u_18} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] [Monoid T'] [DistribMulAction T' M] [SMulCommClass R T' M] [SMulCommClass S' T' M] :

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

Equations

⋯ = ⋯

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₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :

Zero (M →ₛₗ[σ₁₂] M₂)

The constant 0 map is linear.

Equations

LinearMap.instZeroLinearMap = { zero := { toAddHom := { toFun := 0, map_add' := ⋯ }, map_smul' := ⋯ } }

@[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₂] [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_9} {M₂ : Type u_11} {M₃ : Type u_12} [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₃) :

LinearMap.comp g 0 = 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₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) :

LinearMap.comp 0 f = 0

instance LinearMap.instInhabitedLinearMap {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :

Inhabited (M →ₛₗ[σ₁₂] M₂)

Equations

LinearMap.instInhabitedLinearMap = { default := 0 }

@[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₂] [AddCommMonoid M] [AddCommMonoid M₂] [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₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :

Add (M →ₛₗ[σ₁₂] M₂)

The sum of two linear maps is linear.

Equations

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

@[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₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M →ₛₗ[σ₁₂] M₂) (x : M) :

(f + g) x = f x + g x

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

LinearMap.comp (h + g) f = LinearMap.comp h f + LinearMap.comp 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₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) :

LinearMap.comp h (f + g) = LinearMap.comp h f + LinearMap.comp h g

instance LinearMap.addCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :

AddCommMonoid (M →ₛₗ[σ₁₂] M₂)

The type of linear maps is an additive monoid.

Equations

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

instance LinearMap.instNegLinearMapToAddCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :

Neg (M →ₛₗ[σ₁₂] N₂)

The negation of a linear map is linear.

Equations

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

@[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₂] [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_9} {M₂ : Type u_11} {N₃ : Type u_15} [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₃) :

LinearMap.comp (-g) f = -LinearMap.comp g f

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

LinearMap.comp g (-f) = -LinearMap.comp g f

instance LinearMap.instSubLinearMapToAddCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :

Sub (M →ₛₗ[σ₁₂] N₂)

The subtraction of two linear maps is linear.

Equations

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

@[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₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] N₂) (g : M →ₛₗ[σ₁₂] N₂) (x : M) :

(f - g) x = f x - g x

theorem LinearMap.sub_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {N₃ : Type u_15} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) (h : M₂ →ₛₗ[σ₂₃] N₃) :

LinearMap.comp (g - h) f = LinearMap.comp g f - LinearMap.comp 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₃] [AddCommMonoid M] [AddCommGroup N₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ N₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) :

LinearMap.comp h (g - f) = LinearMap.comp h g - LinearMap.comp h f

instance LinearMap.addCommGroup {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :

AddCommGroup (M →ₛₗ[σ₁₂] N₂)

The type of linear maps is an additive group.

Equations

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

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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] :

DistribMulAction S (M →ₛₗ[σ₁₂] M₂)

Equations

LinearMap.instDistribMulActionLinearMapToAddMonoidAddCommMonoid = DistribMulAction.mk ⋯ ⋯

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

LinearMap.comp (a • g) f = a • LinearMap.comp g f

theorem LinearMap.comp_smul {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Monoid S] [DistribMulAction S M₂] [Module R M₂] [Module R M₃] [SMulCommClass R S M₂] [DistribMulAction S M₃] [SMulCommClass R S M₃] [LinearMap.CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) :

g ∘ₗ (a • f) = a • g ∘ₗ f

instance LinearMap.instDistribMulActionDomMulActLinearMapInstMonoidDomMulActMonoidToAddMonoidAddCommMonoid {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] :

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

Equations

LinearMap.instDistribMulActionDomMulActLinearMapInstMonoidDomMulActMonoidToAddMonoidAddCommMonoid = DistribMulAction.mk ⋯ ⋯