algebra.module.linear_map

source

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.

source

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)

to_fun : M → M₂
map_add' : ∀ (x y : M), self.to_fun (x + y) = self.to_fun x + self.to_fun y
map_smul' : ∀ (r : R) (x : M), self.to_fun (r • x) = ⇑σ r • self.to_fun x

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

source

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.

source

@[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)

coe : F → Π (a : M), (λ (_x : M), M₂) a
coe_injective' : function.injective semilinear_map_class.coe
map_add : ∀ (f : F) (x y : M), ⇑f (x + y) = ⇑f x + ⇑f y
map_smulₛₗ : ∀ (f : F) (r : R) (x : M), ⇑f (r • x) = ⇑σ r • ⇑f x

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

See also linear_map_class F R M M₂ for the case where σ is the identity map on R.

A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

Instances of this typeclass

Instances of other typeclasses for semilinear_map_class

semilinear_map_class.has_sizeof_inst

source

@[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₂

source

@[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₂.

source

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

add_monoid_hom_class F M M₃

Equations

semilinear_map_class.add_monoid_hom_class F = {coe := λ (f : F), ⇑f, coe_injective' := _, map_add := _, map_zero := _}

source

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

distrib_mul_action_hom_class F R M M₂

Equations

semilinear_map_class.distrib_mul_action_hom_class F = {coe := λ (f : F), ⇑f, coe_injective' := _, map_smul := _, map_add := _, map_zero := _}

source

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)

source

@[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

linear_map.semilinear_map_class = {coe := linear_map.to_fun _inst_12, coe_injective' := _, map_add := _, map_smulₛₗ := _}

source

@[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

linear_map.has_coe_to_fun = {coe := λ (f : M →ₛₗ[σ] M₃), ⇑f}

source

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

f.to_distrib_mul_action_hom = {to_fun := f.to_fun, map_smul' := _, map_zero' := _, map_add' := _}

source

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

f.to_fun = ⇑f

source

@[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

source

@[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

f.copy f' h = {to_fun := f', map_add' := _, map_smul' := _}

source

@[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'

source

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

source

@[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

linear_map.simps.apply σ M M₃ f = ⇑f

source

@[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

source

def linear_map.id {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :

M →ₗ[R] M

Identity map as a linear_map

Equations

linear_map.id = {to_fun := id M, map_add' := _, map_smul' := _}

source

theorem linear_map.id_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (x : M) :

⇑linear_map.id x = x

source

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

⇑linear_map.id = id

source

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

is_linear_map R ⇑fₗ

source

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} :

function.injective coe_fn

source

@[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'

source

@[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.

source

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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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)

source

@[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

source

@[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

source

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

source

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

source

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

source

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

Type

map_smul : ∀ (fₗ : M →ₗ[S] M₂) (c : R) (x : M), ⇑fₗ (c • x) = c • ⇑fₗ x

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

source

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

linear_map.compatible_smul M M₂ R S

Equations

linear_map.is_scalar_tower.compatible_smul = {map_smul := _}

source

@[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

source

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

f.to_add_monoid_hom = {to_fun := ⇑f, map_zero' := _, map_add' := _}

source

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

⇑(f.to_add_monoid_hom) = ⇑f

source

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.

Equations

linear_map.restrict_scalars R fₗ = {to_fun := ⇑fₗ, map_add' := _, map_smul' := _}

source

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

⇑(linear_map.restrict_scalars R fₗ) = ⇑fₗ

source

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) :

⇑(linear_map.restrict_scalars R fₗ) x = ⇑fₗ x

source

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] :

function.injective (linear_map.restrict_scalars R)

source

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

linear_map.restrict_scalars R fₗ = linear_map.restrict_scalars R gₗ ↔ fₗ = gₗ

source

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} :

function.injective linear_map.to_add_monoid_hom

source

@[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.

source

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

source

@[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

source

@[simp]

theorem ring_hom.to_semilinear_map_apply {R : Type u_1} {S : Type u_6} [semiring R] [semiring S] (f : R →+* S) (ᾰ : R) :

⇑(f.to_semilinear_map) ᾰ = ⇑f ᾰ

source

def ring_hom.to_semilinear_map {R : Type u_1} {S : Type u_6} [semiring R] [semiring S] (f : R →+* S) :

R →ₛₗ[f] S

Interpret a ring_hom f as an f-semilinear map.

Equations

f.to_semilinear_map = {to_fun := ⇑f, map_add' := _, map_smul' := _}

source

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

f.comp g = {to_fun := ⇑f ∘ ⇑g, map_add' := _, map_smul' := _}

source

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)

source

@[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

source

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

f.comp linear_map.id = f

source

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

linear_map.id.comp f = f

source

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'

source

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'

source

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

f.inverse g h₁ h₂ = id (λ (h₂ : ∀ (x : M₂), ⇑f (g x) = x), id (λ (h₁ : ∀ (x : M), g (⇑f x) = x), {to_fun := g, map_add' := _, map_smul' := _}) h₁) h₂

source

@[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

source

@[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

source

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

linear_map.compatible_smul M M₂ ℤ S

Equations

linear_map.compatible_smul.int_module = {map_smul := _}

source

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

linear_map.compatible_smul M M₂ Rˣ S

Equations

linear_map.compatible_smul.units = {map_smul := _}

source

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

⇑(module.comp_hom.to_linear_map g) ᾰ = ⇑g ᾰ

source

def module.comp_hom.to_linear_map {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (g : R →+* S) :

R →ₗ[R] S

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

Equations

module.comp_hom.to_linear_map g = {to_fun := ⇑g, map_add' := _, map_smul' := _}

source

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

fₗ.to_linear_map = {to_fun := fₗ.to_fun, map_add' := _, map_smul' := _}

source

@[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

distrib_mul_action_hom.linear_map.has_coe = {coe := distrib_mul_action_hom.to_linear_map _inst_5}

source

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

f.to_linear_map = ↑f

source

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

⇑↑f = ⇑f

source

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

source

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

is_linear_map.mk' f H = {to_fun := f, map_add' := _, map_smul' := _}

source

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

⇑(is_linear_map.mk' f H) x = f x

source

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)

source

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)

source

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

source

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)

source

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

source

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

source

@[reducible]

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.

source

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

M →ₗ[ℕ ] M₂

Reinterpret an additive homomorphism as a ℕ-linear map.

Equations

f.to_nat_linear_map = {to_fun := ⇑f, map_add' := _, map_smul' := _}

source

theorem add_monoid_hom.to_nat_linear_map_injective {M : Type u_9} {M₂ : Type u_11} [add_comm_monoid M] [add_comm_monoid M₂] :

function.injective add_monoid_hom.to_nat_linear_map

source

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

M →ₗ[ℤ ] M₂

Reinterpret an additive homomorphism as a ℤ-linear map.

Equations

f.to_int_linear_map = {to_fun := ⇑f, map_add' := _, map_smul' := _}

source

theorem add_monoid_hom.to_int_linear_map_injective {M : Type u_9} {M₂ : Type u_11} [add_comm_group M] [add_comm_group M₂] :

function.injective add_monoid_hom.to_int_linear_map

source

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

⇑(f.to_int_linear_map) = ⇑f

source

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

M →ₗ[ℚ ] M₂

Reinterpret an additive homomorphism as a ℚ-linear map.

Equations

f.to_rat_linear_map = {to_fun := f.to_fun, map_add' := _, map_smul' := _}

source

theorem add_monoid_hom.to_rat_linear_map_injective {M : Type u_9} {M₂ : Type u_11} [add_comm_group M] [module ℚ M] [add_comm_group M₂] [module ℚ M₂] :

function.injective add_monoid_hom.to_rat_linear_map

source

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

⇑(f.to_rat_linear_map) = ⇑f

source

@[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

linear_map.has_smul = {smul := λ (a : S) (f : M →ₛₗ[σ₁₂] M₂), {to_fun := a • ⇑f, map_add' := _, map_smul' := _}}

source

@[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

source

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

source

@[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₂)

source

@[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₂)

source

@[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₂)

source

@[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

linear_map.has_zero = {zero := {to_fun := 0, map_add' := _, map_smul' := _}}

source

@[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

source

@[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

source

@[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

source

@[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

linear_map.inhabited = {default := 0}

source

@[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₂} :

inhabited.default = 0

source

@[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

linear_map.has_add = {add := λ (f g : M →ₛₗ[σ₁₂] M₂), {to_fun := ⇑f + ⇑g, map_add' := _, map_smul' := _}}

source

@[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

source

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

source

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

source

@[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

linear_map.add_comm_monoid = function.injective.add_comm_monoid coe_fn linear_map.add_comm_monoid._proof_2 linear_map.add_comm_monoid._proof_3 linear_map.add_comm_monoid._proof_4 linear_map.add_comm_monoid._proof_5

source

@[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

linear_map.has_neg = {neg := λ (f : M →ₛₗ[σ₁₂] N₂), {to_fun := -⇑f, map_add' := _, map_smul' := _}}

source

@[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

source

@[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

source

@[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

source

@[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

linear_map.has_sub = {sub := λ (f g : M →ₛₗ[σ₁₂] N₂), {to_fun := ⇑f - ⇑g, map_add' := _, map_smul' := _}}

source

@[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

source

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

source

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

source

@[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

linear_map.add_comm_group = function.injective.add_comm_group coe_fn linear_map.add_comm_group._proof_3 linear_map.add_comm_group._proof_4 linear_map.add_comm_group._proof_5 linear_map.add_comm_group._proof_6 linear_map.add_comm_group._proof_7 linear_map.add_comm_group._proof_8 linear_map.add_comm_group._proof_9

source

@[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

linear_map.distrib_mul_action = {to_mul_action := {to_has_smul := linear_map.has_smul _inst_13, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}

source

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

source

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

source

@[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

linear_map.module = {to_distrib_mul_action := linear_map.distrib_mul_action _inst_13, add_smul := _, zero_smul := _}

source

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

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

source

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

has_one (module.End R M)

Equations

linear_map.module.End.has_one = {one := linear_map.id _inst_4}

source

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

has_mul (module.End R M)

Equations

linear_map.module.End.has_mul = {mul := linear_map.comp linear_map.module.End.has_mul._proof_1}

source

theorem linear_map.one_eq_id {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :

1 = linear_map.id

source

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) :

f * g = linear_map.comp f g

source

@[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

source

@[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)

source

theorem linear_map.coe_one {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :

⇑1 = id

source

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

source

@[protected, instance]

def module.End.monoid {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :

monoid (module.End R M)

Equations

module.End.monoid = {mul := has_mul.mul linear_map.module.End.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (module.End R M)), npow_zero' := _, npow_succ' := _}

source

@[protected, instance]

def module.End.semiring {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :

semiring (module.End R M)

Equations

module.End.semiring = {add := has_add.add linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid_with_one.nsmul add_monoid_with_one.unary, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul linear_map.module.End.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, nat_cast := λ (n : ℕ), n • 1, nat_cast_zero := _, nat_cast_succ := _, npow := monoid.npow module.End.monoid, npow_zero' := _, npow_succ' := _}

source

@[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

mathlib3 documentation

(Semi)linear maps #

Implementation notes #

Notation #

TODO #

Tags #

Arithmetic on the codomain #

Monoid structure of endomorphisms #

Action by a module endomorphism. #

Actions as module endomorphisms #