mathlib3 documentation

algebra.module.linear_map

(Semi)linear maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define

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 #

TODO #

Tags #

linear map

structure is_linear_map (R : Type u) {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R 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] [add_comm_monoid M₂] [module R M] [module S 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] [add_comm_monoid M₂] [module R M] [module S M₂] (self : M →ₛₗ[σ] M₂) :
add_hom M M₂

The add_hom underlying a linear_map.

@[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] [add_comm_monoid M₂] [module R M] [module S M₂] :
Type (max u_17 u_20 u_21)

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] [add_comm_monoid M₂] [module R M] [module S M₂] [self : semilinear_map_class F σ M M₂] :
add_hom_class F M M₂
@[reducible]
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] [add_comm_monoid M₂] [module R M] [module R 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] [add_comm_monoid M₃] [module R M] [module S M₃] {σ : R →+* S} [semilinear_map_class F σ 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] [add_comm_monoid M₂] [module R M] [module R M₂] [linear_map_class F R 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] [add_comm_monoid M₃] [module R M] [module S M₃] {σ : R →+* S} (f : F) [i : semilinear_map_class F σ M M₃] {σ' : S →+* R} [ring_hom_inv_pair σ σ'] (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] [add_comm_monoid M₃] [module R M] [module S 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] [add_comm_monoid M₃] [module R M] [module S 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] [add_comm_monoid M₂] [module R M] [module R 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] [add_comm_monoid M₃] [module R M] [module S 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] [add_comm_monoid M₃] [module R M] [module S 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] [add_comm_monoid M₃] [module R M] [module S 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
@[simp]
theorem linear_map.coe_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] [add_comm_monoid M₃] [module R M] [module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : M M₃) (h : f' = f) :
(f.copy f' h) = f'
theorem linear_map.copy_eq {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₃] [module R M] [module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : M M₃) (h : f' = f) :
f.copy f' h = f
@[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] [add_comm_monoid M₃] [module R M] [module S M₃] (f : M →ₛₗ[σ] M₃) :
M M₃

See Note [custom simps projection].

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] [add_comm_monoid M₃] [module R M] [module S 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] [add_comm_monoid M] [module R M] :

Identity map as a linear_map

Equations
theorem linear_map.id_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (x : M) :
@[simp, norm_cast]
theorem linear_map.id_coe {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module 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] [add_comm_monoid M₂] [module R M] [module R M₂] (fₗ : M →ₗ[R] M₂) :
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] [add_comm_monoid M₃] [module R M] [module S 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] [add_comm_monoid M₃] [module R M] [module S 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] [add_comm_monoid 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.

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] [add_comm_monoid M₃] [module R M] [module S 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] [add_comm_monoid M₃] [module R M] [module S 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] [add_comm_monoid M₃] [module R M] [module S 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] [add_comm_monoid M₃] [module R M] [module S 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] [add_comm_monoid M₃] [module R M] [module S 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] [add_comm_monoid M₂] [module R M] [module R 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] [add_comm_monoid M₃] [module R M] [module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) {σ' : S →+* R} [ring_hom_inv_pair σ σ'] (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] [add_comm_monoid M₃] [module R M] [module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : function.injective f) {x : M} :
f x = 0 x = 0
@[simp]
theorem image_smul_setₛₗ {R : Type u_1} {S : Type u_6} (M : Type u_9) (M₃ : Type u_12) [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₃] [module R M] [module S M₃] (σ : R →+* S) {F : Type u_17} (h : F) [semilinear_map_class F σ M M₃] (c : R) (s : set M) :
h '' (c s) = σ c h '' s
theorem preimage_smul_setₛₗ {R : Type u_1} {S : Type u_6} (M : Type u_9) (M₃ : Type u_12) [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₃] [module R M] [module S M₃] (σ : R →+* S) {F : Type u_17} (h : F) [semilinear_map_class F σ M M₃] {c : R} (hc : is_unit c) (s : set M₃) :
h ⁻¹' (σ c s) = c h ⁻¹' s
theorem image_smul_set (R : Type u_1) (M : Type u_9) (M₂ : Type u_11) [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] {F : Type u_17} (h : F) [linear_map_class F R M M₂] (c : R) (s : set M) :
h '' (c s) = c h '' s
theorem preimage_smul_set (R : Type u_1) (M : Type u_9) (M₂ : Type u_11) [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] {F : Type u_17} (h : F) [linear_map_class F R M M₂] {c : R} (hc : is_unit c) (s : set M₂) :
h ⁻¹' (c s) = c h ⁻¹' s
@[class]
structure linear_map.compatible_smul (M : Type u_9) (M₂ : Type u_11) [add_comm_monoid M] [add_comm_monoid M₂] (R : Type u_17) (S : Type u_18) [semiring S] [has_smul R M] [module S M] [has_smul R M₂] [module S M₂] :

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] [add_comm_monoid M₂] {R : Type u_1} {S : Type u_2} [semiring S] [has_smul R S] [has_smul R M] [module S M] [is_scalar_tower R S M] [has_smul R M₂] [module S M₂] [is_scalar_tower R S M₂] :
Equations
@[simp]
theorem linear_map.map_smul_of_tower {M : Type u_9} {M₂ : Type u_11} [add_comm_monoid M] [add_comm_monoid M₂] {R : Type u_1} {S : Type u_2} [semiring S] [has_smul R M] [module S M] [has_smul R M₂] [module S M₂] [linear_map.compatible_smul M M₂ R 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] [add_comm_monoid 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 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] [add_comm_monoid M₃] [module R M] [module S 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] [add_comm_monoid M₂] [module R M] [module R M₂] [module S M] [module S M₂] [linear_map.compatible_smul 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 linear_map.map_smul_of_tower.

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] [add_comm_monoid M₂] [module R M] [module R M₂] [module S M] [module S M₂] [linear_map.compatible_smul M M₂ R S] (fₗ : M →ₗ[S] M₂) :
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] [add_comm_monoid M₂] [module R M] [module R M₂] [module S M] [module S M₂] [linear_map.compatible_smul M M₂ R S] (fₗ : M →ₗ[S] M₂) (x : M) :
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] [add_comm_monoid M₂] [module R M] [module R M₂] [module S M] [module S M₂] [linear_map.compatible_smul M M₂ R 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] [add_comm_monoid M₂] [module R M] [module R M₂] [module S M] [module S M₂] [linear_map.compatible_smul M M₂ R S] (fₗ gₗ : M →ₗ[S] M₂) :
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] [add_comm_monoid M₃] [module R M] [module S 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₃] [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.

theorem linear_map.ext_ring_iff {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module 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₃] [module S 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₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (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₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (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₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (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₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] {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₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] {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] [add_comm_monoid M₂] [module R M] [module S M₂] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] (f : M →ₛₗ[σ] M₂) (g : M₂ M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse 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
@[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] [add_comm_group M₂] {module_M : module R M} {module_M₂ : module S 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] [add_comm_group 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
@[protected, instance]
def linear_map.compatible_smul.int_module {M : Type u_9} {M₂ : Type u_11} [add_comm_group M] [add_comm_group M₂] {S : Type u_1} [semiring S] [module S M] [module S M₂] :
Equations
@[protected, instance]
def linear_map.compatible_smul.units {M : Type u_9} {M₂ : Type u_11} [add_comm_group M] [add_comm_group M₂] {R : Type u_1} {S : Type u_2} [monoid R] [mul_action R M] [mul_action R M₂] [semiring S] [module S M] [module S M₂] [linear_map.compatible_smul M M₂ R 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) :
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] [add_comm_monoid M₂] [module R M] [module R 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] [add_comm_monoid M₂] [module R M] [module R 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] [add_comm_monoid M₂] [module R M] [module R 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] [add_comm_monoid M₂] [module R M] [module R 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] [add_comm_monoid M₂] [module R M] [module R 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] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M M₂) (H : is_linear_map R 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] [add_comm_monoid M₂] [module R M] [module R M₂] {f : M M₂} (H : is_linear_map R f) (x : M) :
theorem is_linear_map.is_linear_map_smul {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (c : R) :
is_linear_map R (λ (z : M), c z)
theorem is_linear_map.is_linear_map_smul' {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (a : M) :
is_linear_map R (λ (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] [add_comm_monoid M₂] [module R M] [module R M₂] {f : M M₂} (lin : is_linear_map R f) :
f 0 = 0
theorem is_linear_map.is_linear_map_neg {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_group M] [module R M] :
is_linear_map R (λ (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] [add_comm_group M₂] [module R M] [module R M₂] {f : M M₂} (lin : is_linear_map R 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] [add_comm_group M₂] [module R M] [module R M₂] {f : M M₂} (lin : is_linear_map R f) (x y : M) :
f (x - y) = f x - f y
@[reducible]
def module.End (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] :

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] [add_comm_monoid M₂] (f : M →+ M₂) :

Reinterpret an additive homomorphism as a -linear map.

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

Reinterpret an additive homomorphism as a -linear map.

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

Reinterpret an additive homomorphism as a -linear map.

Equations
@[simp]
theorem add_monoid_hom.coe_to_rat_linear_map {M : Type u_9} {M₂ : Type u_11} [add_comm_group M] [module M] [add_comm_group M₂] [module 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] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [distrib_mul_action S M₂] [smul_comm_class R₂ S M₂] :
has_smul S (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] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [distrib_mul_action S M₂] [smul_comm_class R₂ 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] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [distrib_mul_action S M₂] [smul_comm_class R₂ 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] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [distrib_mul_action S M₂] [smul_comm_class R₂ S M₂] [monoid T] [distrib_mul_action T M₂] [smul_comm_class R₂ T M₂] [smul_comm_class S T M₂] :
smul_comm_class S T (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] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [distrib_mul_action S M₂] [smul_comm_class R₂ S M₂] [monoid T] [distrib_mul_action T M₂] [smul_comm_class R₂ T M₂] [has_smul S T] [is_scalar_tower S T M₂] :
is_scalar_tower S T (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] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [distrib_mul_action S M₂] [smul_comm_class R₂ S M₂] [distrib_mul_action Sᵐᵒᵖ M₂] [smul_comm_class R₂ Sᵐᵒᵖ M₂] [is_central_scalar S M₂] :
is_central_scalar S (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] [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] [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₂] [add_comm_monoid M₃] [module R₁ M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (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₂] [add_comm_monoid M₃] [module R₁ M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (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] [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] [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] [add_comm_monoid M₂] [module R₁ M] [module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
has_add (M →ₛₗ[σ₁₂] M₂)

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] [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₂] [add_comm_monoid M₃] [module R₁ M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (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₂] [add_comm_monoid M₃] [module R₁ M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (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] [add_comm_monoid M₂] [module R₁ M] [module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
add_comm_monoid (M →ₛₗ[σ₁₂] M₂)

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_monoid M] [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_monoid M] [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_monoid M₂] [add_comm_group N₃] [module R₁ M] [module R₂ M₂] [module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (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_monoid M] [add_comm_group N₂] [add_comm_group N₃] [module R₁ M] [module R₂ N₂] [module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (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_monoid M] [add_comm_group N₂] [module R₁ M] [module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
has_sub (M →ₛₗ[σ₁₂] N₂)

The subtraction of two linear maps 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_monoid M] [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_monoid M₂] [add_comm_group N₃] [module R₁ M] [module R₂ M₂] [module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (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_monoid M] [add_comm_group N₂] [add_comm_group N₃] [module R₁ M] [module R₂ N₂] [module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (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_monoid M] [add_comm_group N₂] [module R₁ M] [module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
add_comm_group (M →ₛₗ[σ₁₂] N₂)

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] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [monoid S] [distrib_mul_action S M₂] [smul_comm_class R₂ S M₂] :
distrib_mul_action S (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₂] [add_comm_monoid M₃] [module R M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [monoid S₃] [distrib_mul_action S₃ M₃] [smul_comm_class R₃ 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₂] [add_comm_monoid M₃] [module R M] [monoid S] [distrib_mul_action S M₂] [module R M₂] [module R M₃] [smul_comm_class R S M₂] [distrib_mul_action S M₃] [smul_comm_class R S M₃] [linear_map.compatible_smul 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] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [semiring S] [module S M₂] [smul_comm_class R₂ S M₂] :
module S (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] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [semiring S] [module S M₂] [smul_comm_class R₂ S M₂] [no_zero_smul_divisors S 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] [add_comm_monoid M] [module R M] :
Equations
@[protected, instance]
def linear_map.module.End.has_mul {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
Equations
theorem linear_map.one_eq_id {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
theorem linear_map.mul_eq_comp {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (f g : module.End R M) :
@[simp]
theorem linear_map.one_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (x : M) :
1 x = x
@[simp]
theorem linear_map.mul_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (f g : module.End R M) (x : M) :
(f * g) x = f (g x)
theorem linear_map.coe_one {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
theorem linear_map.coe_mul {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (f g : module.End R M) :
(f * g) = f g
@[protected, instance]
def module.End.monoid {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[simp]
theorem module.End.nat_cast_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (n : ) (m : M) :
n m = n m

See also module.End.nat_cast_def.

@[simp]
theorem module.End.int_cast_apply {R : Type u_1} {N₁ : Type u_13} [semiring R] [add_comm_group N₁] [module R N₁] (z : ) (m : N₁) :
z m = z m

See also module.End.int_cast_def.

@[protected, instance]
def module.End.is_scalar_tower {R : Type u_1} {S : Type u_6} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] :
@[protected, instance]
def module.End.smul_comm_class {R : Type u_1} {S : Type u_6} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [has_smul S R] [is_scalar_tower S R M] :
@[protected, instance]
def module.End.smul_comm_class' {R : Type u_1} {S : Type u_6} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [has_smul S R] [is_scalar_tower S R M] :

Action by a module endomorphism. #

@[protected, instance]
def linear_map.apply_module {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R 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] [add_comm_monoid M] [module R M] (f : module.End R M) (a : M) :
f a = f a
@[protected, instance]

linear_map.apply_module is faithful.

@[protected, instance]
@[protected, instance]
@[protected, instance]

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] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S M] [smul_comm_class S R M] (s : S) (ᾰ : M) :
def distrib_mul_action.to_linear_map (R : Type u_1) {S : Type u_6} (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S M] [smul_comm_class S R 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] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S M] [smul_comm_class S R M] :

Each element of the monoid defines a module endomorphism.

This is a stronger version of distrib_mul_action.to_add_monoid_End.

Equations
def module.to_module_End (R : Type u_1) {S : Type u_6} (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] [semiring S] [module S M] [smul_comm_class S R M] :

Each element of the semiring 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] [add_comm_monoid M] [module R M] [semiring S] [module S M] [smul_comm_class S R M] (s : S) :

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

Equations

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

Equations
theorem module.End.nat_cast_def (R : Type u_1) {N₁ : Type u_13} [semiring R] (n : ) [add_comm_monoid N₁] [module R N₁] :
theorem module.End.int_cast_def (R : Type u_1) {N₁ : Type u_13} [semiring R] (z : ) [add_comm_group N₁] [module R N₁] :