mathlib documentation

algebra.module.linear_map

(Semi)linear maps #

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_16} {S : Type u_17} [semiring R] [semiring S] (σ : R →+* S) (M : Type u_18) (M₂ : Type u_19) [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] :
Type (max u_18 u_19)

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.

def linear_map.to_add_hom {R : Type u_16} {S : Type u_17} [semiring R] [semiring S] {σ : R →+* S} {M : Type u_18} {M₂ : Type u_19} [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.

def linear_map.to_distrib_mul_action_hom {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [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
@[instance]
def linear_map.has_coe_to_fun {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₃ : Type u_11} [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₃)
Equations
@[simp]
theorem linear_map.coe_mk {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₃ : Type u_11} [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_8} [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_8} [semiring R] [add_comm_monoid M] [module R M] (x : M) :
@[simp]
theorem linear_map.id_coe {R : Type u_1} {M : Type u_8} [semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem linear_map.to_fun_eq_coe {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₃ : Type u_11} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₃] [module R M] [module S M₃] (σ : R →+* S) (f : M →ₛₗ[σ] M₃) :
theorem linear_map.is_linear {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [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_8} {M₃ : Type u_11} [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 {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₃ : Type u_11} [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
theorem linear_map.congr_arg {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₃ : Type u_11} [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'
theorem linear_map.congr_fun {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₃ : Type u_11} [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_8} {M₃ : Type u_11} [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_8} {M₃ : Type u_11} [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
@[simp]
theorem linear_map.map_add {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₃ : Type u_11} [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
@[simp]
theorem linear_map.map_smulₛₗ {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₃ : Type u_11} [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
theorem linear_map.map_smul {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [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
theorem linear_map.map_smul_inv {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₃ : Type u_11} [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_zero {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₃ : Type u_11} [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
@[simp]
theorem linear_map.map_eq_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₃ : Type u_11} [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
@[class]
structure linear_map.compatible_smul (M : Type u_8) (M₂ : Type u_10) [add_comm_monoid M] [add_comm_monoid M₂] (R : Type u_16) (S : Type u_17) [semiring S] [has_scalar R M] [module S M] [has_scalar R M₂] [module S M₂] :
Type

A typeclass for has_scalar 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
@[instance]
def linear_map.is_scalar_tower.compatible_smul {M : Type u_8} {M₂ : Type u_10} [add_comm_monoid M] [add_comm_monoid M₂] {R : Type u_1} {S : Type u_2} [semiring S] [has_scalar R S] [has_scalar R M] [module S M] [is_scalar_tower R S M] [has_scalar R M₂] [module S M₂] [is_scalar_tower R S M₂] :
Equations
@[simp]
theorem linear_map.map_smul_of_tower {M : Type u_8} {M₂ : Type u_10} [add_comm_monoid M] [add_comm_monoid M₂] {R : Type u_1} {S : Type u_2} [semiring S] [has_scalar R M] [module S M] [has_scalar 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_8} {M₃ : Type u_11} [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_8} {M₃ : Type u_11} [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_8} {M₂ : Type u_10} [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.restrict_scalars_apply (R : Type u_1) {S : Type u_6} {M : Type u_8} {M₂ : Type u_10} [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) :
(linear_map.restrict_scalars R fₗ) = fₗ ᾰ
theorem linear_map.restrict_scalars_injective (R : Type u_1) {S : Type u_6} {M : Type u_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [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₂) :
@[simp]
theorem linear_map.map_sum {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₃ : Type u_11} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₃] [module R M] [module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) {ι : Type u_2} {t : finset ι} {g : ι → M} :
f (∑ (i : ι) in t, g i) = ∑ (i : ι) in t, f (g i)
theorem linear_map.to_add_monoid_hom_injective {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₃ : Type u_11} [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_11} [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_8} [semiring R] [add_comm_monoid M] [module R M] {σ : R →+* R} {f g : R →ₛₗ[σ] M} :
f = g f 1 = g 1
def linear_map.comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [semiring R₁] [semiring R₂] [semiring R₃] [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_9} {M₂ : Type u_10} {M₃ : Type u_11} [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]
theorem linear_map.coe_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [semiring R₁] [semiring R₂] [semiring R₃] [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_10} {M₃ : Type u_11} [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_10} {M₃ : Type u_11} [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₃) :
def linear_map.inverse {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₂ : Type u_10} [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
@[simp]
theorem linear_map.map_neg {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₂ : Type u_10} [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
@[simp]
theorem linear_map.map_sub {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₂ : Type u_10} [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
@[instance]
def linear_map.compatible_smul.int_module {M : Type u_8} {M₂ : Type u_10} [add_comm_group M] [add_comm_group M₂] {S : Type u_1} [semiring S] [module S M] [module S M₂] :
Equations
@[instance]
def linear_map.compatible_smul.units {M : Type u_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [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
@[instance]
def distrib_mul_action_hom.linear_map.has_coe {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →+[R] M₂) :
@[simp]
theorem distrib_mul_action_hom.coe_to_linear_map {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [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_8} [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_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [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
def module.End (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module 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_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [add_comm_group M] [add_comm_group M₂] (f : M →+ M₂) :
def add_monoid_hom.to_rat_linear_map {M : Type u_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [add_comm_group M] [module M] [add_comm_group M₂] [module M₂] (f : M →+ M₂) :

Arithmetic on the codomain #

@[instance]
def linear_map.has_zero {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} {M₃ : Type u_11} [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_8} {M₂ : Type u_10} {M₃ : Type u_11} [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
@[instance]
def linear_map.inhabited {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [semiring R₁] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R₁ M] [module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
default (M →ₛₗ[σ₁₂] M₂) = 0
@[instance]
def linear_map.has_add {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} {M₃ : Type u_11} [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_8} {M₂ : Type u_10} {M₃ : Type u_11} [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
@[instance]
def linear_map.add_comm_monoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [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
@[instance]
def linear_map.has_neg {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_13} [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_8} {N₂ : Type u_13} [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_8} {M₂ : Type u_10} {N₃ : Type u_14} [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_8} {N₂ : Type u_13} {N₃ : Type u_14} [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
@[instance]
def linear_map.has_sub {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_13} [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 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_8} {N₂ : Type u_13} [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_8} {M₂ : Type u_10} {N₃ : Type u_14} [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_8} {N₂ : Type u_13} {N₃ : Type u_14} [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
@[instance]
def linear_map.add_comm_group {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_13} [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
@[instance]
def linear_map.has_scalar {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₂ : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [monoid S] [distrib_mul_action S M₂] [smul_comm_class R S M₂] :
has_scalar S (M →ₗ[R] M₂)
Equations
@[simp]
theorem linear_map.smul_apply {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₂ : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [monoid S] [distrib_mul_action S M₂] [smul_comm_class R S M₂] (a : S) (f : M →ₗ[R] M₂) (x : M) :
(a f) x = a f x
@[instance]
def linear_map.smul_comm_class {R : Type u_1} {S : Type u_6} {T : Type u_7} {M : Type u_8} {M₂ : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [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₂] :
@[instance]
def linear_map.is_scalar_tower {R : Type u_1} {S : Type u_6} {T : Type u_7} {M : Type u_8} {M₂ : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [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_scalar S T] [is_scalar_tower S T M₂] :
@[instance]
def linear_map.distrib_mul_action {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₂ : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [monoid S] [distrib_mul_action S M₂] [smul_comm_class R S M₂] :
Equations
theorem linear_map.smul_comp {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] [monoid S] [distrib_mul_action S M₂] [smul_comm_class R S M₂] (a : S) (g : M₃ →ₗ[R] M₂) (f : M →ₗ[R] 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_8} {M₂ : Type u_10} {M₃ : Type u_11} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] [monoid S] [distrib_mul_action S 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
@[instance]
def linear_map.module {R : Type u_1} {S : Type u_6} {M : Type u_8} {M₂ : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [semiring S] [module S M₂] [smul_comm_class R S M₂] :
module S (M →ₗ[R] M₂)
Equations

Monoid structure of endomorphisms #

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

@[instance]
def linear_map.module.End.has_one {R : Type u_1} {M : Type u_8} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[instance]
def linear_map.module.End.has_mul {R : Type u_1} {M : Type u_8} [semiring R] [add_comm_monoid M] [module R M] :
Equations
theorem linear_map.one_eq_id {R : Type u_1} {M : Type u_8} [semiring R] [add_comm_monoid M] [module R M] :
theorem linear_map.mul_eq_comp {R : Type u_1} {M : Type u_8} [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_8} [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_8} [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_8} [semiring R] [add_comm_monoid M] [module R M] :
theorem linear_map.coe_mul {R : Type u_1} {M : Type u_8} [semiring R] [add_comm_monoid M] [module R M] (f g : module.End R M) :
f * g = f g
@[instance]
def module.End.monoid {R : Type u_1} {M : Type u_8} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[instance]
def module.End.is_scalar_tower {R : Type u_1} {S : Type u_6} {M : Type u_8} [semiring R] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] :
@[instance]
def module.End.smul_comm_class {R : Type u_1} {S : Type u_6} {M : Type u_8} [semiring R] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [has_scalar S R] [is_scalar_tower S R M] :
@[instance]
def module.End.smul_comm_class' {R : Type u_1} {S : Type u_6} {M : Type u_8} [semiring R] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [has_scalar S R] [is_scalar_tower S R M] :

Action by a module endomorphism. #

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

linear_map.apply_module is faithful.

@[instance]
def linear_map.apply_smul_comm_class {R : Type u_1} {M : Type u_8} [semiring R] [add_comm_monoid M] [module R M] :
@[instance]
def linear_map.apply_smul_comm_class' {R : Type u_1} {M : Type u_8} [semiring R] [add_comm_monoid M] [module R M] :