mathlib documentation

algebra.module.linear_map

Linear maps and linear equivalences #

In this file we define

Tags #

linear map, linear equiv, linear equivalences, linear isomorphism, linear isomorphic

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) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] :
Type (max v w)

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. Elements of linear_map R M M₂ (available under the notation M →ₗ[R] M₂) are bundled versions of such maps. An unbundled version 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} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (self : M →ₗ[R] M₂) :
add_hom M M₂

The add_hom underlying a linear_map.

def linear_map.to_mul_action_hom {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₂] (self : M →ₗ[R] M₂) :
M →[R] M₂

The mul_action_hom underlying a linear_map.

def linear_map.to_distrib_mul_action_hom {R : Type u} {M : Type w} {M₂ : Type x} [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} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] :
Equations
@[simp]
theorem linear_map.coe_mk {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M → M₂) (h₁ : ∀ (x y : M), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : M), f (m x) = m f x) :
{to_fun := f, map_add' := h₁, map_smul' := h₂} = f
def linear_map.id {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] :

Identity map as a linear_map

Equations
theorem linear_map.id_apply {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] (x : M) :
@[simp]
theorem linear_map.id_coe {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem linear_map.to_fun_eq_coe {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) :
theorem linear_map.is_linear {R : Type u} {M : Type w} {M₂ : Type x} [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} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] :
function.injective (λ (f : M →ₗ[R] M₂), show M → M₂, from f)
@[ext]
theorem linear_map.ext {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] {f g : M →ₗ[R] M₂} (H : ∀ (x : M), f x = g x) :
f = g
theorem linear_map.congr_arg {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] {f : M →ₗ[R] M₂} {x x' : M} :
x = x'f x = f x'
theorem linear_map.congr_fun {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] {f g : M →ₗ[R] 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} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] {f g : M →ₗ[R] M₂} :
f = g ∀ (x : M), f x = g x
@[simp]
theorem linear_map.mk_coe {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) (h₁ : ∀ (x y : M), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : M), f (m x) = m f x) :
{to_fun := f, map_add' := h₁, map_smul' := h₂} = f
@[simp]
theorem linear_map.map_add {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) (x y : M) :
f (x + y) = f x + f y
@[simp]
theorem linear_map.map_smul {R : Type u} {M : Type w} {M₂ : Type x} [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
@[simp]
theorem linear_map.map_zero {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) :
f 0 = 0
@[class]
structure linear_map.compatible_smul (M : Type w) (M₂ : Type x) [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₂] :
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 w} {M₂ : Type x} [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 w} {M₂ : Type x} [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
@[instance]
def linear_map.is_add_monoid_hom {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) :
def linear_map.to_add_monoid_hom {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) :
M →+ M₂

convert a linear map to an additive map

Equations
@[simp]
theorem linear_map.to_add_monoid_hom_coe {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) :
def linear_map.restrict_scalars (R : Type u) {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] {S : Type u_1} [semiring S] [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.map_sum {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) {ι : Type u_1} {t : finset ι} {g : ι → M} :
f (∑ (i : ι) in t, g i) = ∑ (i : ι) in t, f (g i)
@[ext]
theorem linear_map.ext_ring {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] {f g : R →ₗ[R] M} (h : f 1 = g 1) :
f = g

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

theorem linear_map.ext_ring_iff {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] {f g : R →ₗ[R] M} :
f = g f 1 = g 1
def linear_map.comp {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [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₃} (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) :
M →ₗ[R] M₃

Composition of two linear maps is a linear map

Equations
theorem linear_map.comp_apply {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [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₃} (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) (x : M) :
(f.comp g) x = f (g x)
@[simp]
theorem linear_map.coe_comp {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [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₃} (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) :
(f.comp g) = f g
@[simp]
theorem linear_map.comp_id {R : Type u} {M₂ : Type x} {M₃ : Type y} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₂ : module R M₂} {module_M₃ : module R M₃} (f : M₂ →ₗ[R] M₃) :
@[simp]
theorem linear_map.id_comp {R : Type u} {M₂ : Type x} {M₃ : Type y} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₂ : module R M₂} {module_M₃ : module R M₃} (f : M₂ →ₗ[R] M₃) :
def linear_map.inverse {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) (g : M₂ → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) :
M₂ →ₗ[R] 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} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_group M] [add_comm_group M₂] {module_M : module R M} {module_M₂ : module R M₂} (f : M →ₗ[R] M₂) (x : M) :
f (-x) = -f x
@[simp]
theorem linear_map.map_sub {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_group M] [add_comm_group M₂] {module_M : module R M} {module_M₂ : module R M₂} (f : M →ₗ[R] M₂) (x y : M) :
f (x - y) = f x - f y
@[instance]
def linear_map.is_add_group_hom {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_group M] [add_comm_group M₂] {module_M : module R M} {module_M₂ : module R M₂} (f : M →ₗ[R] M₂) :
@[instance]
def linear_map.compatible_smul.int_module {M : Type w} {M₂ : Type x} [add_comm_group M] [add_comm_group M₂] {S : Type u_1} [semiring S] [module S M] [module S M₂] :
Equations
def is_linear_map.mk' {R : Type u} {M : Type w} {M₂ : Type x} [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} {M : Type w} {M₂ : Type x} [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} {M : Type w} {M₂ : Type x} [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} {M : Type w} [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} {M : Type w} {M₂ : Type x} [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} {M : Type w} {M₂ : Type x} [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 linear_map.endomorphism_semiring and algebra structure module.endomorphism_algebra.

def add_monoid_hom.to_int_linear_map {M : Type w} {M₂ : Type x} [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 w} {M₂ : Type x} [add_comm_group M] [add_comm_group M₂] (f : M →+ M₂) :
def add_monoid_hom.to_rat_linear_map {M : Type w} {M₂ : Type x} [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 w} {M₂ : Type x} [add_comm_group M] [module M] [add_comm_group M₂] [module M₂] (f : M →+ M₂) :

Linear equivalences #

@[nolint]
structure linear_equiv (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₂] :
Type (max v w)

A linear equivalence is an invertible linear map.

@[nolint]
def linear_equiv.to_add_equiv {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₂] (self : M ≃ₗ[R] M₂) :
M ≃+ M₂
@[nolint]
def linear_equiv.to_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₂] (self : M ≃ₗ[R] M₂) :
M →ₗ[R] M₂
@[instance]
def linear_equiv.linear_map.has_coe {R : Type u} {M : Type w} {M₂ : Type x} [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
@[instance]
def linear_equiv.has_coe_to_fun {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] :
Equations
@[simp]
theorem linear_equiv.coe_mk {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] {to_fun : M → M₂} {inv_fun : M₂ → M} {map_add : ∀ (x y : M), to_fun (x + y) = to_fun x + to_fun y} {map_smul : ∀ (m : R) (x : M), to_fun (m x) = m to_fun x} {left_inv : function.left_inverse inv_fun to_fun} {right_inv : function.right_inverse inv_fun to_fun} :
{to_fun := to_fun, map_add' := map_add, map_smul' := map_smul, inv_fun := inv_fun, left_inv := left_inv, right_inv := right_inv} = to_fun
@[nolint]
def linear_equiv.to_equiv {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] :
(M ≃ₗ[R] M₂)M M₂
Equations
theorem linear_equiv.to_equiv_injective {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] :
@[simp]
theorem linear_equiv.to_equiv_inj {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] {e₁ e₂ : M ≃ₗ[R] M₂} :
e₁.to_equiv = e₂.to_equiv e₁ = e₂
theorem linear_equiv.to_linear_map_injective {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] :
@[simp]
theorem linear_equiv.to_linear_map_inj {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] {e₁ e₂ : M ≃ₗ[R] M₂} :
e₁ = e₂ e₁ = e₂
theorem linear_equiv.to_linear_map_eq_coe {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
@[simp]
theorem linear_equiv.coe_coe {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
@[simp]
theorem linear_equiv.coe_to_equiv {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
@[simp]
theorem linear_equiv.coe_to_linear_map {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
@[simp]
theorem linear_equiv.to_fun_eq_coe {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
@[ext]
theorem linear_equiv.ext {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} {e e' : M ≃ₗ[R] M₂} (h : ∀ (x : M), e x = e' x) :
e = e'
theorem linear_equiv.congr_arg {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} {e : M ≃ₗ[R] M₂} {x x' : M} :
x = x'e x = e x'
theorem linear_equiv.congr_fun {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} {e e' : M ≃ₗ[R] M₂} (h : e = e') (x : M) :
e x = e' x
theorem linear_equiv.ext_iff {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} {e e' : M ≃ₗ[R] M₂} :
e = e' ∀ (x : M), e x = e' x
def linear_equiv.refl (R : Type u) (M : Type w) [semiring R] [add_comm_monoid M] [module R M] :

The identity map is a linear equivalence.

Equations
@[simp]
theorem linear_equiv.refl_apply {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] (x : M) :
def linear_equiv.symm {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
M₂ ≃ₗ[R] M

Linear equivalences are symmetric.

Equations
def linear_equiv.simps.symm_apply {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃ₗ[R] M₂) :
M₂ → M

See Note [custom simps projection]

Equations
@[simp]
theorem linear_equiv.inv_fun_eq_symm {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
def linear_equiv.trans {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [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₃} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) :
M ≃ₗ[R] M₃

Linear equivalences are transitive.

Equations
@[simp]
theorem linear_equiv.coe_to_add_equiv {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
theorem linear_equiv.to_add_monoid_hom_commutes {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :

The two paths coercion can take to an add_monoid_hom are equivalent

@[simp]
theorem linear_equiv.trans_apply {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [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₃} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) (c : M) :
(e₁.trans e₂) c = e₂ (e₁ c)
@[simp]
theorem linear_equiv.apply_symm_apply {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) (c : M₂) :
e ((e.symm) c) = c
@[simp]
theorem linear_equiv.symm_apply_apply {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) (b : M) :
(e.symm) (e b) = b
@[simp]
theorem linear_equiv.symm_trans_apply {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [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₃} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) (c : M₃) :
((e₁.trans e₂).symm) c = (e₁.symm) ((e₂.symm) c)
@[simp]
theorem linear_equiv.trans_refl {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
@[simp]
theorem linear_equiv.refl_trans {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
theorem linear_equiv.symm_apply_eq {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) {x : M₂} {y : M} :
(e.symm) x = y x = e y
theorem linear_equiv.eq_symm_apply {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) {x : M₂} {y : M} :
y = (e.symm) x e y = x
@[simp]
theorem linear_equiv.refl_symm {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem linear_equiv.trans_symm {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M ≃ₗ[R] M₂) :
@[simp]
theorem linear_equiv.symm_trans {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M ≃ₗ[R] M₂) :
@[simp]
theorem linear_equiv.refl_to_linear_map {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem linear_equiv.comp_coe {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f : M ≃ₗ[R] M₂) (f' : M₂ ≃ₗ[R] M₃) :
f'.comp f = (f.trans f')
@[simp]
theorem linear_equiv.mk_coe {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) (h₁ : ∀ (x y : M), e (x + y) = e x + e y) (h₂ : ∀ (m : R) (x : M), e (m x) = m e x) (f : M₂ → M) (h₃ : function.left_inverse f e) (h₄ : function.right_inverse f e) :
{to_fun := e, map_add' := h₁, map_smul' := h₂, inv_fun := f, left_inv := h₃, right_inv := h₄} = e
@[simp]
theorem linear_equiv.map_add {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) (a b : M) :
e (a + b) = e a + e b
@[simp]
theorem linear_equiv.map_zero {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
e 0 = 0
@[simp]
theorem linear_equiv.map_smul {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) (c : R) (x : M) :
e (c x) = c e x
@[simp]
theorem linear_equiv.map_sum {R : Type u} {M : Type w} {M₂ : Type x} {ι : Type z} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) {s : finset ι} (u : ι → M) :
e (∑ (i : ι) in s, u i) = ∑ (i : ι) in s, e (u i)
@[simp]
theorem linear_equiv.map_eq_zero_iff {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) {x : M} :
e x = 0 x = 0
theorem linear_equiv.map_ne_zero_iff {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) {x : M} :
e x 0 x 0
@[simp]
theorem linear_equiv.symm_symm {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
e.symm.symm = e
theorem linear_equiv.symm_bijective {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] :
@[simp]
theorem linear_equiv.mk_coe' {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) (f : M₂ → M) (h₁ : ∀ (x y : M₂), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : M₂), f (m x) = m f x) (h₃ : function.left_inverse e f) (h₄ : function.right_inverse e f) :
{to_fun := f, map_add' := h₁, map_smul' := h₂, inv_fun := e, left_inv := h₃, right_inv := h₄} = e.symm
@[simp]
theorem linear_equiv.symm_mk {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) (f : M₂ → M) (h₁ : ∀ (x y : M), e (x + y) = e x + e y) (h₂ : ∀ (m : R) (x : M), e (m x) = m e x) (h₃ : function.left_inverse f e) (h₄ : function.right_inverse f e) :
{to_fun := e, map_add' := h₁, map_smul' := h₂, inv_fun := f, left_inv := h₃, right_inv := h₄}.symm = {to_fun := f, map_add' := _, map_smul' := _, inv_fun := e, left_inv := _, right_inv := _}
theorem linear_equiv.bijective {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
theorem linear_equiv.injective {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
theorem linear_equiv.surjective {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) :
theorem linear_equiv.image_eq_preimage {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R M₂} (e : M ≃ₗ[R] M₂) (s : set M) :
e '' s = (e.symm) ⁻¹' s
def linear_equiv.of_involutive {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] (f : M →ₗ[R] M) (hf : function.involutive f) :

An involutive linear map is a linear equivalence.

Equations
@[simp]
theorem linear_equiv.coe_of_involutive {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] (f : M →ₗ[R] M) (hf : function.involutive f) :
def linear_equiv.restrict_scalars (R : Type u) {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] {S : Type u_1} [semiring S] [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-semimodules and S-semimodules and R-semimodule structures are defined by an action of R on S (formally, we have two scalar towers), then any S-linear equivalence from M to M₂ is also an R-linear equivalence.

See also linear_map.restrict_scalars.

Equations
@[simp]
theorem linear_equiv.restrict_scalars_apply (R : Type u) {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] {S : Type u_1} [semiring S] [module S M] [module S M₂] [linear_map.compatible_smul M M₂ R S] (f : M ≃ₗ[S] M₂) (ᾰ : M) :
@[simp]
theorem linear_equiv.restrict_scalars_symm_apply (R : Type u) {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] {S : Type u_1} [semiring S] [module S M] [module S M₂] [linear_map.compatible_smul M M₂ R S] (f : M ≃ₗ[S] M₂) (ᾰ : M₂) :