mathlibdocumentation

algebra.module.linear_map

(Semi)linear maps #

In this file we define

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

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

We then provide linear_map with the following instances:

Implementation notes #

To ensure that composition works smoothly for semilinear maps, we use the typeclasses ring_hom_comp_triple, ring_hom_inv_pair and ring_hom_surjective from algebra/ring/comp_typeclasses.

Notation #

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

TODO #

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

Tags #

linear map

structure is_linear_map (R : Type u) {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M → M₂) :
Prop
• map_add : ∀ (x y : M), f (x + y) = f x + f y
• map_smul : ∀ (c : R) (x : M), f (c x) = c f x

A 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 is_linear_map R f asserts this property. A bundled version is available with linear_map, and should be favored over is_linear_map most of the time.

structure linear_map {R : Type u_17} {S : Type u_18} [semiring R] [semiring S] (σ : R →+* S) (M : Type u_19) (M₂ : Type u_20) [add_comm_monoid M₂] [ M] [ M₂] :
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 linear_map σ M M₂ (available under the notation M →ₛₗ[σ] M₂) are bundled versions of such maps. For plain linear maps (i.e. for which σ = ring_hom.id R), the notation M →ₗ[R] M₂ is available. An unbundled version of plain linear maps is available with the predicate is_linear_map, but it should be avoided most of the time.

Instances for linear_map
def linear_map.to_add_hom {R : Type u_17} {S : Type u_18} [semiring R] [semiring S] {σ : R →+* S} {M : Type u_19} {M₂ : Type u_20} [add_comm_monoid M₂] [ M] [ M₂] (self : M →ₛₗ[σ] M₂) :
M₂

@[class]
structure semilinear_map_class (F : Type u_17) {R : out_param (Type u_18)} {S : out_param (Type u_19)} [semiring R] [semiring S] (σ : out_param (R →+* S)) (M : out_param (Type u_20)) (M₂ : out_param (Type u_21)) [add_comm_monoid M₂] [ M] [ M₂] :
Type (max u_17 u_20 u_21)
• coe : F → Π (a : M), (λ (_x : M), M₂) a
• coe_injective' :
• 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

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

See also linear_map_class 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 of this typeclass
Instances of other typeclasses for semilinear_map_class
• semilinear_map_class.has_sizeof_inst
@[nolint, instance]
def semilinear_map_class.to_add_hom_class (F : Type u_17) {R : out_param (Type u_18)} {S : out_param (Type u_19)} [semiring R] [semiring S] (σ : out_param (R →+* S)) (M : out_param (Type u_20)) (M₂ : out_param (Type u_21)) [add_comm_monoid M₂] [ M] [ M₂] [self : M M₂] :
M₂
def linear_map_class (F : Type u_1) (R : out_param (Type u_2)) (M : out_param (Type u_3)) (M₂ : out_param (Type u_4)) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
Type (max u_1 u_3 u_4)

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

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

@[protected, nolint, instance]
def semilinear_map_class.add_monoid_hom_class {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} (F : Type u_17) [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} [ M M₃] :
M₃
Equations
@[protected, nolint, instance]
def semilinear_map_class.distrib_mul_action_hom_class {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} (F : Type u_17) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] [ M M₂] :
M₂
Equations
theorem semilinear_map_class.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] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : F) [i : M M₃] {σ' : S →+* R} [ σ'] (c : S) (x : M) :
c f x = f (σ' c x)
@[protected, instance]
def linear_map.semilinear_map_class {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} :
semilinear_map_class (M →ₛₗ[σ] M₃) σ M M₃
Equations
@[protected, instance]
def linear_map.has_coe_to_fun {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} :
has_coe_to_fun (M →ₛₗ[σ] M₃) (λ (_x : M →ₛₗ[σ] M₃), M → M₃)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
def linear_map.to_distrib_mul_action_hom {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) :
M →+[R] M₂

The distrib_mul_action_hom underlying a linear_map.

Equations
@[simp]
theorem linear_map.to_fun_eq_coe {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} :
@[ext]
theorem linear_map.ext {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} {f g : M →ₛₗ[σ] M₃} (h : ∀ (x : M), f x = g x) :
f = g
@[protected]
def linear_map.copy {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = f) :
M →ₛₗ[σ] M₃

Copy of a linear_map with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[protected]
def linear_map.simps.apply {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (σ : R →+* S) (M : Type u_3) (M₃ : Type u_4) [add_comm_monoid M₃] [ M] [ M₃] (f : M →ₛₗ[σ] M₃) :
M → M₃
Equations
@[simp]
theorem linear_map.coe_mk {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : M → M₃) (h₁ : ∀ (x y : M), f (x + y) = f x + f y) (h₂ : ∀ (r : R) (x : M), f (r x) = σ r f x) :
{to_fun := f, map_add' := h₁, map_smul' := h₂} = f
def linear_map.id {R : Type u_1} {M : Type u_9} [semiring R] [ M] :

Identity map as a linear_map

Equations
theorem linear_map.id_apply {R : Type u_1} {M : Type u_9} [semiring R] [ M] (x : M) :
@[simp, norm_cast]
theorem linear_map.id_coe {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
theorem linear_map.is_linear {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (fₗ : M →ₗ[R] M₂) :
fₗ
theorem linear_map.coe_injective {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} :
@[protected]
theorem linear_map.congr_arg {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {x x' : M} :
x = x'f x = f x'
@[protected]
theorem linear_map.congr_fun {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ 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.

theorem linear_map.ext_iff {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} {f g : M →ₛₗ[σ] M₃} :
f = g ∀ (x : M), f x = g x
@[simp]
theorem linear_map.mk_coe {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h₁ : ∀ (x y : M), f (x + y) = f x + f y) (h₂ : ∀ (r : R) (x : M), f (r x) = σ r f x) :
{to_fun := f, map_add' := h₁, map_smul' := h₂} = f
@[protected]
theorem linear_map.map_add {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (x y : M) :
f (x + y) = f x + f y
@[protected]
theorem linear_map.map_zero {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
f 0 = 0
@[protected, simp]
theorem linear_map.map_smulₛₗ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (c : R) (x : M) :
f (c x) = σ c f x
@[protected]
theorem linear_map.map_smul {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (fₗ : M →ₗ[R] M₂) (c : R) (x : M) :
fₗ (c x) = c fₗ x
@[protected]
theorem linear_map.map_smul_inv {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) {σ' : S →+* R} [ σ'] (c : S) (x : M) :
c f x = f (σ' c x)
@[simp]
theorem linear_map.map_eq_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : function.injective f) {x : M} :
f x = 0 x = 0
@[simp]
theorem linear_map.image_smul_setₛₗ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (c : R) (s : set M) :
f '' (c s) = σ c f '' s
theorem linear_map.image_smul_set {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (fₗ : M →ₗ[R] M₂) (c : R) (s : set M) :
fₗ '' (c s) = c fₗ '' s
theorem linear_map.preimage_smul_setₛₗ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) {c : R} (hc : is_unit c) (s : set M₃) :
f ⁻¹' (σ c s) = c f ⁻¹' s
theorem linear_map.preimage_smul_set {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (fₗ : M →ₗ[R] M₂) {c : R} (hc : is_unit c) (s : set M₂) :
fₗ ⁻¹' (c s) = c fₗ ⁻¹' s
@[class]
structure linear_map.compatible_smul (M : Type u_9) (M₂ : Type u_11) [add_comm_monoid M₂] (R : Type u_17) (S : Type u_18) [semiring S] [ M] [ M] [ M₂] [ M₂] :
Type

A typeclass for has_smul structures which can be moved through a linear_map. This typeclass is generated automatically from a is_scalar_tower instance, but exists so that we can also add an instance for add_comm_group.int_module, allowing z • to be moved even if R does not support negation.

Instances of this typeclass
Instances of other typeclasses for linear_map.compatible_smul
• linear_map.compatible_smul.has_sizeof_inst
@[protected, instance]
def linear_map.is_scalar_tower.compatible_smul {M : Type u_9} {M₂ : Type u_11} [add_comm_monoid M₂] {R : Type u_1} {S : Type u_2} [semiring S] [ S] [ M] [ M] [ M] [ M₂] [ M₂] [ M₂] :
S
Equations
@[simp]
theorem linear_map.map_smul_of_tower {M : Type u_9} {M₂ : Type u_11} [add_comm_monoid M₂] {R : Type u_1} {S : Type u_2} [semiring S] [ M] [ M] [ M₂] [ M₂] [ S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) :
fₗ (c x) = c fₗ x
def linear_map.to_add_monoid_hom {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
M →+ M₃

convert a linear map to an additive map

Equations
@[simp]
theorem linear_map.to_add_monoid_hom_coe {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
def linear_map.restrict_scalars (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] [ M] [ M₂] [ 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.

Equations
@[simp]
theorem linear_map.coe_restrict_scalars (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] [ M] [ M₂] [ S] (fₗ : M →ₗ[S] M₂) :
= fₗ
theorem linear_map.restrict_scalars_apply (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] [ M] [ M₂] [ S] (fₗ : M →ₗ[S] M₂) (x : M) :
x = fₗ x
theorem linear_map.restrict_scalars_injective (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] [ M] [ M₂] [ S] :
@[simp]
theorem linear_map.restrict_scalars_inj (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] [ M] [ M₂] [ S] (fₗ gₗ : M →ₗ[S] M₂) :
fₗ = gₗ
@[simp]
theorem linear_map.map_sum {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) {ι : Type u_2} {t : finset ι} {g : ι → M} :
f (t.sum (λ (i : ι), g i)) = t.sum (λ (i : ι), f (g i))
theorem linear_map.to_add_monoid_hom_injective {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M] [ M₃] {σ : R →+* S} :
@[ext]
theorem linear_map.ext_ring {R : Type u_1} {S : Type u_6} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ 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.

theorem linear_map.ext_ring_iff {R : Type u_1} {M : Type u_9} [semiring R] [ M] {σ : R →+* R} {f g : R →ₛₗ[σ] M} :
f = g f 1 = g 1
@[ext]
theorem linear_map.ext_ring_op {R : Type u_1} {S : Type u_6} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M₃] [ M₃] {σ : Rᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) :
f = g
@[simp]
theorem ring_hom.to_semilinear_map_apply {R : Type u_1} {S : Type u_6} [semiring R] [semiring S] (f : R →+* S) (ᾰ : R) :
def ring_hom.to_semilinear_map {R : Type u_1} {S : Type u_6} [semiring R] [semiring S] (f : R →+* S) :

Interpret a ring_hom f as an f-semilinear map.

Equations
def linear_map.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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) :
M₁ →ₛₗ[σ₁₃] M₃

Composition of two linear maps is a linear map

Equations
theorem linear_map.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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) (x : M₁) :
(f.comp g) x = f (g x)
@[simp, norm_cast]
theorem linear_map.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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) :
(f.comp g) = f g
@[simp]
theorem linear_map.comp_id {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_11} {M₃ : Type u_12} [semiring R₂] [semiring R₃] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃) :
@[simp]
theorem linear_map.id_comp {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_11} {M₃ : Type u_12} [semiring R₂] [semiring R₃] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃) :
theorem linear_map.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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} {g : M₁ →ₛₗ[σ₁₂] M₂} {f' : M₂ →ₛₗ[σ₂₃] M₃} (hg : function.surjective g) :
f.comp g = f'.comp g f = f'
theorem linear_map.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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} {g g' : M₁ →ₛₗ[σ₁₂] M₂} (hf : function.injective f) :
f.comp g = f.comp g' g = g'
def linear_map.inverse {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] {σ : R →+* S} {σ' : S →+* R} [ σ'] (f : M →ₛₗ[σ] M₂) (g : M₂ → M) (h₁ : f) (h₂ : f) :
M₂ →ₛₗ[σ'] M

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

Equations
@[protected]
theorem linear_map.map_neg {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [semiring R] [semiring S] [add_comm_group M₂] {module_M : M} {module_M₂ : M₂} {σ : R →+* S} (f : M →ₛₗ[σ] M₂) (x : M) :
f (-x) = -f x
@[protected]
theorem linear_map.map_sub {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [semiring R] [semiring S] [add_comm_group M₂] {module_M : M} {module_M₂ : M₂} {σ : R →+* S} (f : M →ₛₗ[σ] M₂) (x y : M) :
f (x - y) = f x - f y
@[protected, instance]
def linear_map.compatible_smul.int_module {M : Type u_9} {M₂ : Type u_11} [add_comm_group M₂] {S : Type u_1} [semiring S] [ M] [ M₂] :
S
Equations
@[protected, instance]
def linear_map.compatible_smul.units {M : Type u_9} {M₂ : Type u_11} [add_comm_group M₂] {R : Type u_1} {S : Type u_2} [monoid R] [ M] [ M₂] [semiring S] [ M] [ M₂] [ S] :
S
Equations
@[simp]
theorem module.comp_hom.to_linear_map_apply {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (g : R →+* S) (ᾰ : R) :
= g ᾰ
def module.comp_hom.to_linear_map {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (g : R →+* S) :

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

Equations
def distrib_mul_action_hom.to_linear_map {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (fₗ : M →+[R] M₂) :
M →ₗ[R] M₂

A distrib_mul_action_hom between two modules is a linear map.

Equations
@[protected, instance]
def distrib_mul_action_hom.linear_map.has_coe {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
has_coe (M →+[R] M₂) (M →ₗ[R] M₂)
Equations
@[simp]
theorem distrib_mul_action_hom.to_linear_map_eq_coe {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →+[R] M₂) :
@[simp, norm_cast]
theorem distrib_mul_action_hom.coe_to_linear_map {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →+[R] M₂) :
theorem distrib_mul_action_hom.to_linear_map_injective {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f g : M →+[R] M₂} (h : f = g) :
f = g
def is_linear_map.mk' {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M → M₂) (H : f) :
M →ₗ[R] M₂

Convert an is_linear_map predicate to a linear_map

Equations
@[simp]
theorem is_linear_map.mk'_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M → M₂} (H : f) (x : M) :
H) x = f x
theorem is_linear_map.is_linear_map_smul {R : Type u_1} {M : Type u_2} [ M] (c : R) :
(λ (z : M), c z)
theorem is_linear_map.is_linear_map_smul' {R : Type u_1} {M : Type u_2} [semiring R] [ M] (a : M) :
(λ (c : R), c a)
theorem is_linear_map.map_zero {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M → M₂} (lin : f) :
f 0 = 0
theorem is_linear_map.is_linear_map_neg {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
(λ (z : M), -z)
theorem is_linear_map.map_neg {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_group M₂] [ M] [ M₂] {f : M → M₂} (lin : f) (x : M) :
f (-x) = -f x
theorem is_linear_map.map_sub {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [semiring R] [add_comm_group M₂] [ M] [ M₂] {f : M → M₂} (lin : f) (x y : M) :
f (x - y) = f x - f y
def module.End (R : Type u) (M : Type v) [semiring R] [ M] :
Type v

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

def add_monoid_hom.to_nat_linear_map {M : Type u_9} {M₂ : Type u_11} [add_comm_monoid M₂] (f : M →+ M₂) :

Reinterpret an additive homomorphism as a -linear map.

Equations
theorem add_monoid_hom.to_nat_linear_map_injective {M : Type u_9} {M₂ : Type u_11} [add_comm_monoid M₂] :
def add_monoid_hom.to_int_linear_map {M : Type u_9} {M₂ : Type u_11} [add_comm_group M₂] (f : M →+ M₂) :

Reinterpret an additive homomorphism as a -linear map.

Equations
theorem add_monoid_hom.to_int_linear_map_injective {M : Type u_9} {M₂ : Type u_11} [add_comm_group M₂] :
@[simp]
theorem add_monoid_hom.coe_to_int_linear_map {M : Type u_9} {M₂ : Type u_11} [add_comm_group M₂] (f : M →+ M₂) :
def add_monoid_hom.to_rat_linear_map {M : Type u_9} {M₂ : Type u_11} [ M] [add_comm_group M₂] [ M₂] (f : M →+ M₂) :

Reinterpret an additive homomorphism as a -linear map.

Equations
theorem add_monoid_hom.to_rat_linear_map_injective {M : Type u_9} {M₂ : Type u_11} [ M] [add_comm_group M₂] [ M₂] :
@[simp]
theorem add_monoid_hom.coe_to_rat_linear_map {M : Type u_9} {M₂ : Type u_11} [ M] [add_comm_group M₂] [ M₂] (f : M →+ M₂) :
@[protected, instance]
def linear_map.has_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₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [ M₂] [ S M₂] :
(M →ₛₗ[σ₁₂] M₂)
Equations
@[simp]
theorem linear_map.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₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [ M₂] [ S M₂] (a : S) (f : M →ₛₗ[σ₁₂] M₂) (x : M) :
(a f) x = a f x
theorem linear_map.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₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [ M₂] [ S M₂] (a : S) (f : M →ₛₗ[σ₁₂] M₂) :
(a f) = a f
@[protected, instance]
def linear_map.smul_comm_class {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₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [ M₂] [ S M₂] [monoid T] [ M₂] [ T M₂] [ M₂] :
(M →ₛₗ[σ₁₂] M₂)
@[protected, instance]
def linear_map.is_scalar_tower {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₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [ M₂] [ S M₂] [monoid T] [ M₂] [ T M₂] [ T] [ M₂] :
(M →ₛₗ[σ₁₂] M₂)
@[protected, instance]
def linear_map.is_central_scalar {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [ M₂] [ S M₂] [ M₂] [ M₂] [ M₂] :
(M →ₛₗ[σ₁₂] M₂)

Arithmetic on the codomain #

@[protected, instance]
def linear_map.has_zero {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [semiring R₁] [semiring R₂] [add_comm_monoid M₂] [module R₁ M] [module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
has_zero (M →ₛₗ[σ₁₂] M₂)

The constant 0 map is linear.

Equations
@[simp]
theorem linear_map.zero_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [semiring R₁] [semiring R₂] [add_comm_monoid M₂] [module R₁ M] [module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (x : M) :
0 x = 0
@[simp]
theorem linear_map.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₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R₁ M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ σ₂₃ σ₁₃] (g : M₂ →ₛₗ[σ₂₃] M₃) :
g.comp 0 = 0
@[simp]
theorem linear_map.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₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R₁ M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) :
0.comp f = 0
@[protected, instance]
def linear_map.inhabited {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [semiring R₁] [semiring R₂] [add_comm_monoid M₂] [module R₁ M] [module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
inhabited (M →ₛₗ[σ₁₂] M₂)
Equations
@[simp]
theorem linear_map.default_def {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [semiring R₁] [semiring R₂] [add_comm_monoid M₂] [module R₁ M] [module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
@[protected, instance]
def linear_map.has_add {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [semiring R₁] [semiring R₂] [add_comm_monoid M₂] [module R₁ M] [module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :

The sum of two linear maps is linear.

Equations
@[simp]
theorem linear_map.add_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [semiring R₁] [semiring R₂] [add_comm_monoid M₂] [module R₁ M] [module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (f g : M →ₛₗ[σ₁₂] M₂) (x : M) :
(f + g) x = f x + g x
theorem linear_map.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₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R₁ M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃] M₃) :
(h + g).comp f = h.comp f + g.comp f
theorem linear_map.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₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R₁ M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ σ₂₃ σ₁₃] (f g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) :
h.comp (f + g) = h.comp f + h.comp g
@[protected, instance]
def linear_map.add_comm_monoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [semiring R₁] [semiring R₂] [add_comm_monoid M₂] [module R₁ M] [module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :

The type of linear maps is an additive monoid.

Equations
@[protected, instance]
def linear_map.has_neg {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [semiring R₁] [semiring R₂] [add_comm_group N₂] [module R₁ M] [module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
has_neg (M →ₛₗ[σ₁₂] N₂)

The negation of a linear map is linear.

Equations
@[simp]
theorem linear_map.neg_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [semiring R₁] [semiring R₂] [add_comm_group N₂] [module R₁ M] [module R₂ N₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] N₂) (x : M) :
(-f) x = -f x
@[simp]
theorem linear_map.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₃] [add_comm_monoid M₂] [add_comm_group N₃] [module R₁ M] [module R₂ M₂] [module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) :
(-g).comp f = -g.comp f
@[simp]
theorem linear_map.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₃] [add_comm_group N₂] [add_comm_group N₃] [module R₁ M] [module R₂ N₂] [module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃] N₃) :
g.comp (-f) = -g.comp f
@[protected, instance]
def linear_map.has_sub {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [semiring R₁] [semiring R₂] [add_comm_group N₂] [module R₁ M] [module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
has_sub (M →ₛₗ[σ₁₂] N₂)

The negation of a linear map is linear.

Equations
@[simp]
theorem linear_map.sub_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [semiring R₁] [semiring R₂] [add_comm_group N₂] [module R₁ M] [module R₂ N₂] {σ₁₂ : R₁ →+* R₂} (f g : M →ₛₗ[σ₁₂] N₂) (x : M) :
(f - g) x = f x - g x
theorem linear_map.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₃] [add_comm_monoid M₂] [add_comm_group N₃] [module R₁ M] [module R₂ M₂] [module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃] N₃) :
(g - h).comp f = g.comp f - h.comp f
theorem linear_map.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₃] [add_comm_group N₂] [add_comm_group N₃] [module R₁ M] [module R₂ N₂] [module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ σ₂₃ σ₁₃] (f g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) :
h.comp (g - f) = h.comp g - h.comp f
@[protected, instance]
def linear_map.add_comm_group {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [semiring R₁] [semiring R₂] [add_comm_group N₂] [module R₁ M] [module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :

The type of linear maps is an additive group.

Equations
@[protected, instance]
def linear_map.distrib_mul_action {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [ M₂] [ S M₂] :
(M →ₛₗ[σ₁₂] M₂)
Equations
theorem linear_map.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₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ σ₂₃ σ₁₃] [monoid S₃] [ M₃] [ S₃ M₃] (a : S₃) (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂) :
(a g).comp f = a g.comp f
theorem linear_map.comp_smul {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [monoid S] [ M₂] [ M₂] [ M₃] [ M₂] [ M₃] [ M₃] [ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) :
g.comp (a f) = a g.comp f
@[protected, instance]
def linear_map.module {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [semiring S] [ M₂] [ S M₂] :
(M →ₛₗ[σ₁₂] M₂)
Equations
@[protected, instance]
def linear_map.no_zero_smul_divisors {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [semiring S] [ M₂] [ S M₂] [ M₂] :
(M →ₛₗ[σ₁₂] M₂)

Monoid structure of endomorphisms #

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

@[protected, instance]
def linear_map.module.End.has_one {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
Equations
@[protected, instance]
def linear_map.module.End.has_mul {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
Equations
theorem linear_map.one_eq_id {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
theorem linear_map.mul_eq_comp {R : Type u_1} {M : Type u_9} [semiring R] [ M] (f g : M) :
f * g =
@[simp]
theorem linear_map.one_apply {R : Type u_1} {M : Type u_9} [semiring R] [ M] (x : M) :
1 x = x
@[simp]
theorem linear_map.mul_apply {R : Type u_1} {M : Type u_9} [semiring R] [ M] (f g : M) (x : M) :
(f * g) x = f (g x)
theorem linear_map.coe_one {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
theorem linear_map.coe_mul {R : Type u_1} {M : Type u_9} [semiring R] [ M] (f g : M) :
(f * g) = f g
@[protected, instance]
def module.End.monoid {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
Equations
@[protected, instance]
def module.End.semiring {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
Equations
@[protected, instance]
def module.End.ring {R : Type u_1} {N₁ : Type u_13} [semiring R] [add_comm_group N₁] [ N₁] :
ring N₁)
Equations
@[protected, instance]
def module.End.is_scalar_tower {R : Type u_1} {S : Type u_6} {M : Type u_9} [semiring R] [ M] [monoid S] [ M] [ M] :
M) M)
@[protected, instance]
def module.End.smul_comm_class {R : Type u_1} {S : Type u_6} {M : Type u_9} [semiring R] [ M] [monoid S] [ M] [ M] [ R] [ M] :
M) M)
@[protected, instance]
def module.End.smul_comm_class' {R : Type u_1} {S : Type u_6} {M : Type u_9} [semiring R] [ M] [monoid S] [ M] [ M] [ R] [ M] :
S M)

Action by a module endomorphism. #

@[protected, instance]
def linear_map.apply_module {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
module M) M

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

This generalizes function.End.apply_mul_action.

Equations
@[protected, simp]
theorem linear_map.smul_def {R : Type u_1} {M : Type u_9} [semiring R] [ M] (f : M) (a : M) :
f a = f a
@[protected, instance]
def linear_map.apply_has_faithful_smul {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
M

linear_map.apply_module is faithful.

@[protected, instance]
def linear_map.apply_smul_comm_class {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
M) M
@[protected, instance]
def linear_map.apply_smul_comm_class' {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
R M
@[protected, instance]
def linear_map.apply_is_scalar_tower {R : Type u_1} {M : Type u_2} [ M] :
M) M

Actions as module endomorphisms #

@[simp]
theorem distrib_mul_action.to_linear_map_apply (R : Type u_1) {S : Type u_6} (M : Type u_9) [semiring R] [ M] [monoid S] [ M] [ M] (s : S) (ᾰ : M) :
= s
def distrib_mul_action.to_linear_map (R : Type u_1) {S : Type u_6} (M : Type u_9) [semiring R] [ M] [monoid S] [ M] [ M] (s : S) :

Each element of the monoid defines a linear map.

This is a stronger version of distrib_mul_action.to_add_monoid_hom.

Equations
def distrib_mul_action.to_module_End (R : Type u_1) {S : Type u_6} (M : Type u_9) [semiring R] [ M] [monoid S] [ M] [ M] :
S →* M

Each element of the monoid defines a module endomorphism.

This is a stronger version of distrib_mul_action.to_add_monoid_End.

Equations
@[simp]
theorem distrib_mul_action.to_module_End_apply (R : Type u_1) {S : Type u_6} (M : Type u_9) [semiring R] [ M] [monoid S] [ M] [ M] (s : S) :
def module.to_module_End (R : Type u_1) {S : Type u_6} (M : Type u_9) [semiring R] [ M] [semiring S] [ M] [ M] :
S →+* M

Each element of the monoid defines a module endomorphism.

This is a stronger version of distrib_mul_action.to_module_End.

Equations
@[simp]
theorem module.to_module_End_apply (R : Type u_1) {S : Type u_6} (M : Type u_9) [semiring R] [ M] [semiring S] [ M] [ M] (s : S) :
M) s =
@[simp]
theorem module.module_End_self_apply (R : Type u_1) [semiring R] (s : Rᵐᵒᵖ) :
@[simp]
theorem module.module_End_self_symm_apply (R : Type u_1) [semiring R] (f : R) :
def module.module_End_self (R : Type u_1) [semiring R] :

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

Equations
@[simp]
theorem module.module_End_self_op_apply (R : Type u_1) [semiring R] (s : R) :
def module.module_End_self_op (R : Type u_1) [semiring R] :

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

Equations
@[simp]
theorem module.module_End_self_op_symm_apply (R : Type u_1) [semiring R] (f : R) :
f = f 1