# mathlibdocumentation

linear_algebra.basic

# Linear algebra #

This file defines the basics of linear algebra. It sets up the "categorical/lattice structure" of modules over a ring, submodules, and linear maps.

Many of the relevant definitions, including `module`, `submodule`, and `linear_map`, are found in `src/algebra/module`.

## Main definitions #

• Many constructors for linear maps
• `submodule.span s` is defined to be the smallest submodule containing the set `s`.
• If `p` is a submodule of `M`, `submodule.quotient p` is the quotient of `M` with respect to `p`: that is, elements of `M` are identified if their difference is in `p`. This is itself a module.
• The kernel `ker` and range `range` of a linear map are submodules of the domain and codomain respectively.
• The general linear group is defined to be the group of invertible linear maps from `M` to itself.

## Main statements #

• The first, second and third isomorphism laws for modules are proved as `linear_map.quot_ker_equiv_range`, `linear_map.quotient_inf_equiv_sup_quotient` and `submodule.quotient_quotient_equiv_quotient`.

## Notations #

• We continue to use the notation `M →ₗ[R] M₂` for the type of linear maps from `M` to `M₂` over the ring `R`.
• We introduce the notations `M ≃ₗ M₂` and `M ≃ₗ[R] M₂` for `linear_equiv M M₂`. In the first, the ring `R` is implicit.
• We introduce the notation `R ∙ v` for the span of a singleton, `submodule.span R {v}`. This is `\.`, not the same as the scalar multiplication `•`/`\bub`.

## Implementation notes #

We note that, when constructing linear maps, it is convenient to use operations defined on bundled maps (`linear_map.prod`, `linear_map.coprod`, arithmetic operations like `+`) instead of defining a function and proving it is linear.

## Tags #

linear algebra, vector space, module

theorem finsupp.smul_sum {α : Type u} {β : Type v} {R : Type w} {M : Type y} [has_zero β] [monoid R] [ M] {v : α →₀ β} {c : R} {h : α → β → M} :
c v.sum h = v.sum (λ (a : α) (b : β), c h a b)
@[simp]
theorem finsupp.sum_smul_index_linear_map' {α : Type u} {R : Type v} {M : Type w} {M₂ : Type x} [semiring R] [ M] [add_comm_monoid M₂] [ M₂] {v : α →₀ M} {c : R} {h : α → (M →ₗ[R] M₂)} :
(c v).sum (λ (a : α), (h a)) = c v.sum (λ (a : α), (h a))
@[simp]
theorem finsupp.linear_equiv_fun_on_fintype_apply (R : Type u) {M : Type v} {α : Type u_1} [fintype α] [semiring R] [ M] (x : α →₀ M) (ᾰ : α) :
= x ᾰ
def finsupp.linear_equiv_fun_on_fintype (R : Type u) {M : Type v} {α : Type u_1} [fintype α] [semiring R] [ M] :
→₀ M) ≃ₗ[R] α → M

Given `fintype α`, `linear_equiv_fun_on_fintype R` is the natural `R`-linear equivalence between `α →₀ β` and `α → β`.

Equations
@[simp]
theorem finsupp.linear_equiv_fun_on_fintype_single (R : Type u) {M : Type v} {α : Type u_1} [decidable_eq α] [fintype α] [semiring R] [ M] (x : α) (m : M) :
= m
@[simp]
theorem finsupp.linear_equiv_fun_on_fintype_symm_single (R : Type u) {M : Type v} {α : Type u_1} [decidable_eq α] [fintype α] [semiring R] [ M] (x : α) (m : M) :
m) =
theorem pi_eq_sum_univ {ι : Type u} [fintype ι] {R : Type v} [semiring R] (x : ι → R) :
x = ∑ (i : ι), x i λ (j : ι), ite (i = j) 1 0

decomposing `x : ι → R` as a sum along the canonical basis

### Properties of linear maps #

theorem linear_map.comp_assoc {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ M₄] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (h : M₃ →ₗ[R] M₄) :
(h.comp g).comp f = h.comp (g.comp f)
def linear_map.dom_restrict {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (p : M) :
p →ₗ[R] M₂

The restriction of a linear map `f : M → M₂` to a submodule `p ⊆ M` gives a linear map `p → M₂`.

Equations
@[simp]
theorem linear_map.dom_restrict_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (p : M) (x : p) :
def linear_map.cod_restrict {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (p : M) (f : M₂ →ₗ[R] M) (h : ∀ (c : M₂), f c p) :
M₂ →ₗ[R] p

A linear map `f : M₂ → M` whose values lie in a submodule `p ⊆ M` can be restricted to a linear map M₂ → p.

Equations
@[simp]
theorem linear_map.cod_restrict_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (p : M) (f : M₂ →ₗ[R] M) {h : ∀ (c : M₂), f c p} (x : M₂) :
( h) x) = f x
@[simp]
theorem linear_map.comp_cod_restrict {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) (p : M₂) (h : ∀ (b : M), f b p) (g : M₃ →ₗ[R] M) :
h).comp g = (f.comp g) _
@[simp]
theorem linear_map.subtype_comp_cod_restrict {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (p : M₂) (h : ∀ (b : M), f b p) :
p.subtype.comp h) = f
def linear_map.restrict {R : Type u} {M : Type v} [semiring R] [ M] (f : M →ₗ[R] M) {p : M} (hf : ∀ (x : M), x pf x p) :

Restrict domain and codomain of an endomorphism.

Equations
theorem linear_map.restrict_apply {R : Type u} {M : Type v} [semiring R] [ M] {f : M →ₗ[R] M} {p : M} (hf : ∀ (x : M), x pf x p) (x : p) :
(f.restrict hf) x = f x, _⟩
theorem linear_map.subtype_comp_restrict {R : Type u} {M : Type v} [semiring R] [ M] {f : M →ₗ[R] M} {p : M} (hf : ∀ (x : M), x pf x p) :
theorem linear_map.restrict_eq_cod_restrict_dom_restrict {R : Type u} {M : Type v} [semiring R] [ M] {f : M →ₗ[R] M} {p : M} (hf : ∀ (x : M), x pf x p) :
f.restrict hf = _
theorem linear_map.restrict_eq_dom_restrict_cod_restrict {R : Type u} {M : Type v} [semiring R] [ M] {f : M →ₗ[R] M} {p : M} (hf : ∀ (x : M), f x p) :
@[instance]
def linear_map.has_zero {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
has_zero (M →ₗ[R] M₂)

The constant 0 map is linear.

Equations
@[instance]
def linear_map.inhabited {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
Equations
@[simp]
theorem linear_map.zero_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (x : M) :
0 x = 0
@[simp]
theorem linear_map.default_def {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
default (M →ₗ[R] M₂) = 0
@[instance]
def linear_map.unique_of_left {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] [subsingleton M] :
unique (M →ₗ[R] M₂)
Equations
@[instance]
def linear_map.unique_of_right {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] [subsingleton M₂] :
unique (M →ₗ[R] M₂)
Equations
@[instance]
def linear_map.has_add {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
has_add (M →ₗ[R] M₂)

The sum of two linear maps is linear.

Equations
@[simp]
theorem linear_map.add_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f g : M →ₗ[R] M₂) (x : M) :
(f + g) x = f x + g x
@[instance]
def linear_map.add_comm_monoid {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :

The type of linear maps is an additive monoid.

Equations
def linear_map.eval_add_monoid_hom {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (a : M) :
(M →ₗ[R] M₂) →+ M₂

Evaluation of an `R`-linear map at a fixed `a`, as an `add_monoid_hom`.

Equations
theorem linear_map.add_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) (g h : M₂ →ₗ[R] M₃) :
(h + g).comp f = h.comp f + g.comp f
theorem linear_map.comp_add {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f g : M →ₗ[R] M₂) (h : M₂ →ₗ[R] M₃) :
h.comp (f + g) = h.comp f + h.comp g
def linear_map.to_add_monoid_hom' {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
(M →ₗ[R] M₂) →+ M →+ M₂

`linear_map.to_add_monoid_hom` promoted to an `add_monoid_hom`

Equations
theorem linear_map.sum_apply {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (t : finset ι) (f : ι → (M →ₗ[R] M₂)) (b : M) :
(∑ (d : ι) in t, f d) b = ∑ (d : ι) in t, (f d) b
def linear_map.smul_right {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {S : Type u_1} [semiring S] [ S] [ M] [ M] (f : M₂ →ₗ[R] S) (x : M) :
M₂ →ₗ[R] M

When `f` is an `R`-linear map taking values in `S`, then `λb, f b • x` is an `R`-linear map.

Equations
@[simp]
theorem linear_map.coe_smul_right {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {S : Type u_1} [semiring S] [ S] [ M] [ M] (f : M₂ →ₗ[R] S) (x : M) :
(f.smul_right x) = λ (c : M₂), f c x
theorem linear_map.smul_right_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {S : Type u_1} [semiring S] [ S] [ M] [ M] (f : M₂ →ₗ[R] S) (x : M) (c : M₂) :
(f.smul_right x) c = f c x
@[instance]
def linear_map.has_one {R : Type u} {M : Type v} [semiring R] [ M] :
Equations
@[instance]
def linear_map.has_mul {R : Type u} {M : Type v} [semiring R] [ M] :
Equations
theorem linear_map.one_eq_id {R : Type u} {M : Type v} [semiring R] [ M] :
theorem linear_map.mul_eq_comp {R : Type u} {M : Type v} [semiring R] [ M] (f g : M →ₗ[R] M) :
f * g = f.comp g
@[simp]
theorem linear_map.one_apply {R : Type u} {M : Type v} [semiring R] [ M] (x : M) :
1 x = x
@[simp]
theorem linear_map.mul_apply {R : Type u} {M : Type v} [semiring R] [ M] (f g : M →ₗ[R] M) (x : M) :
(f * g) x = f (g x)
theorem linear_map.coe_one {R : Type u} {M : Type v} [semiring R] [ M] :
theorem linear_map.coe_mul {R : Type u} {M : Type v} [semiring R] [ M] (f g : M →ₗ[R] M) :
f * g = f g
@[instance]
def linear_map.module.End.nontrivial {R : Type u} {M : Type v} [semiring R] [ M] [nontrivial M] :
@[simp]
theorem linear_map.comp_zero {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) :
f.comp 0 = 0
@[simp]
theorem linear_map.zero_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) :
0.comp f = 0
@[simp]
theorem linear_map.coe_fn_sum {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {ι : Type u_1} (t : finset ι) (f : ι → (M →ₗ[R] M₂)) :
∑ (i : ι) in t, f i = ∑ (i : ι) in t, (f i)
@[instance]
def linear_map.monoid {R : Type u} {M : Type v} [semiring R] [ M] :
Equations
@[simp]
theorem linear_map.pow_apply {R : Type u} {M : Type v} [semiring R] [ M] (f : M →ₗ[R] M) (n : ) (m : M) :
(f ^ n) m = f^[n] m
theorem linear_map.pow_map_zero_of_le {R : Type u} {M : Type v} [semiring R] [ M] {f : M} {m : M} {k l : } (hk : k l) (hm : (f ^ k) m = 0) :
(f ^ l) m = 0
theorem linear_map.commute_pow_left_of_commute {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} {g : M} {g₂ : M₂} (h : f = f.comp g) (k : ) :
linear_map.comp (g₂ ^ k) f = f.comp (g ^ k)
theorem linear_map.submodule_pow_eq_zero_of_pow_eq_zero {R : Type u} {M : Type v} [semiring R] [ M] {N : M} {g : N} {G : M} (h : = N.subtype.comp g) {k : } (hG : G ^ k = 0) :
g ^ k = 0
theorem linear_map.coe_pow {R : Type u} {M : Type v} [semiring R] [ M] (f : M →ₗ[R] M) (n : ) :
(f ^ n) = (f^[n])
@[simp]
theorem linear_map.id_pow {R : Type u} {M : Type v} [semiring R] [ M] (n : ) :
theorem linear_map.iterate_succ {R : Type u} {M : Type v} [semiring R] [ M] {f' : M →ₗ[R] M} (n : ) :
f' ^ (n + 1) = (f' ^ n).comp f'
theorem linear_map.iterate_surjective {R : Type u} {M : Type v} [semiring R] [ M] {f' : M →ₗ[R] M} (h : function.surjective f') (n : ) :
theorem linear_map.iterate_injective {R : Type u} {M : Type v} [semiring R] [ M] {f' : M →ₗ[R] M} (h : function.injective f') (n : ) :
theorem linear_map.iterate_bijective {R : Type u} {M : Type v} [semiring R] [ M] {f' : M →ₗ[R] M} (h : function.bijective f') (n : ) :
theorem linear_map.injective_of_iterate_injective {R : Type u} {M : Type v} [semiring R] [ M] {f' : M →ₗ[R] M} {n : } (hn : n 0) (h : function.injective (f' ^ n)) :
theorem linear_map.pi_apply_eq_sum_univ {R : Type u} {M : Type v} {ι : Type x} [semiring R] [ M] [fintype ι] (f : (ι → R) →ₗ[R] M) (x : ι → R) :
f x = ∑ (i : ι), x i f (λ (j : ι), ite (i = j) 1 0)

A linear map `f` applied to `x : ι → R` can be computed using the image under `f` of elements of the canonical basis.

@[instance]
def linear_map.has_neg {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_group M₂] [ M] [ M₂] :
has_neg (M →ₗ[R] M₂)

The negation of a linear map is linear.

Equations
@[simp]
theorem linear_map.neg_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_group M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (x : M) :
(-f) x = -f x
@[simp]
theorem linear_map.comp_neg {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_group M₂] [add_comm_group M₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
g.comp (-f) = -g.comp f
@[instance]
def linear_map.has_sub {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_group M₂] [ M] [ M₂] :
has_sub (M →ₗ[R] M₂)

The negation of a linear map is linear.

Equations
@[simp]
theorem linear_map.sub_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_group M₂] [ M] [ M₂] (f g : M →ₗ[R] M₂) (x : M) :
(f - g) x = f x - g x
theorem linear_map.sub_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_group M₂] [add_comm_group M₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) (g h : M₂ →ₗ[R] M₃) :
(g - h).comp f = g.comp f - h.comp f
theorem linear_map.comp_sub {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_group M₂] [add_comm_group M₃] [ M] [ M₂] [ M₃] (f g : M →ₗ[R] M₂) (h : M₂ →ₗ[R] M₃) :
h.comp (g - f) = h.comp g - h.comp f
@[instance]
def linear_map.add_comm_group {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_group M₂] [ M] [ M₂] :

The type of linear maps is an additive group.

Equations
@[instance]
def linear_map.has_scalar {R : Type u} {M : Type v} {M₂ : Type w} {S : Type u_1} [semiring R] [monoid S] [add_comm_monoid M₂] [ M] [ M₂] [ M₂] [ M₂] :
(M →ₗ[R] M₂)
Equations
@[simp]
theorem linear_map.smul_apply {R : Type u} {M : Type v} {M₂ : Type w} {S : Type u_1} [semiring R] [monoid S] [add_comm_monoid M₂] [ M] [ M₂] [ M₂] [ M₂] (f : M →ₗ[R] M₂) (a : S) (x : M) :
(a f) x = a f x
@[instance]
def linear_map.smul_comm_class {R : Type u} {M : Type v} {M₂ : Type w} {S : Type u_1} [semiring R] [monoid S] [add_comm_monoid M₂] [ M] [ M₂] [ M₂] [ M₂] {T : Type u_2} [monoid T] [ M₂] [ M₂] [ M₂] :
(M →ₗ[R] M₂)
@[instance]
def linear_map.is_scalar_tower {R : Type u} {M : Type v} {M₂ : Type w} {S : Type u_1} [semiring R] [monoid S] [add_comm_monoid M₂] [ M] [ M₂] [ M₂] [ M₂] {T : Type u_2} [monoid T] [ T] [ M₂] [ M₂] [ M₂] :
(M →ₗ[R] M₂)
@[instance]
def linear_map.distrib_mul_action {R : Type u} {M : Type v} {M₂ : Type w} {S : Type u_1} [semiring R] [monoid S] [add_comm_monoid M₂] [ M] [ M₂] [ M₂] [ M₂] :
(M →ₗ[R] M₂)
Equations
theorem linear_map.smul_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {S : Type u_1} [semiring R] [monoid S] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] [ M₂] [ M₂] (a : S) (g : M₃ →ₗ[R] M₂) (f : M →ₗ[R] M₃) :
(a g).comp f = a g.comp f
@[instance]
def linear_map.module {R : Type u} {M : Type v} {M₂ : Type w} {S : Type u_1} [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] [ M₂] [ M₂] :
(M →ₗ[R] M₂)
Equations
@[simp]
theorem linear_map.applyₗ'_apply_apply {R : Type u} {M : Type v} {M₂ : Type w} (S : Type u_1) [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] [ M₂] [ M₂] (v : M) (f : M →ₗ[R] M₂) :
( v) f = f v
def linear_map.applyₗ' {R : Type u} {M : Type v} {M₂ : Type w} (S : Type u_1) [semiring R] [semiring S] [add_comm_monoid M₂] [ M] [ M₂] [ M₂] [ M₂] :
M →+ (M →ₗ[R] M₂) →ₗ[S] M₂

Applying a linear map at `v : M`, seen as `S`-linear map from `M →ₗ[R] M₂` to `M₂`.

See `linear_map.applyₗ` for a version where `S = R`.

Equations
@[simp]
theorem linear_map.ring_lmap_equiv_self_apply (R : Type u) (M : Type v) (S : Type u_1) [semiring R] [semiring S] [ M] [ M] [ M] (f : R →ₗ[R] M) :
f = f 1
@[simp]
theorem linear_map.ring_lmap_equiv_self_symm_apply (R : Type u) (M : Type v) (S : Type u_1) [semiring R] [semiring S] [ M] [ M] [ M] (x : M) :
S).symm) x = 1.smul_right x
def linear_map.ring_lmap_equiv_self (R : Type u) (M : Type v) (S : Type u_1) [semiring R] [semiring S] [ M] [ M] [ M] :
(R →ₗ[R] M) ≃ₗ[S] M

The equivalence between R-linear maps from `R` to `M`, and points of `M` itself. This says that the forgetful functor from `R`-modules to types is representable, by `R`.

This as an `S`-linear equivalence, under the assumption that `S` acts on `M` commuting with `R`. When `R` is commutative, we can take this to be the usual action with `S = R`. Otherwise, `S = ℕ` shows that the equivalence is additive. See note [bundled maps over different rings].

Equations
theorem linear_map.comp_smul {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (a : R) :
g.comp (a f) = a g.comp f
def linear_map.comp_right {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M₂ →ₗ[R] M₃) :
(M →ₗ[R] M₂) →ₗ[R] M →ₗ[R] M₃

Composition by `f : M₂ → M₃` is a linear map from the space of linear maps `M → M₂` to the space of linear maps `M₂ → M₃`.

Equations
@[simp]
theorem linear_map.applyₗ_apply_apply {R : Type u} {M : Type v} {M₂ : Type w} [add_comm_monoid M₂] [ M] [ M₂] (v : M) (f : M →ₗ[R] M₂) :
f = f v
def linear_map.applyₗ {R : Type u} {M : Type v} {M₂ : Type w} [add_comm_monoid M₂] [ M] [ M₂] :
M →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] M₂

Applying a linear map at `v : M`, seen as a linear map from `M →ₗ[R] M₂` to `M₂`. See also `linear_map.applyₗ'` for a version that works with two different semirings.

This is the `linear_map` version of `add_monoid_hom.eval`.

Equations
def linear_map.dom_restrict' {R : Type u} {M : Type v} {M₂ : Type w} [add_comm_monoid M₂] [ M] [ M₂] (p : M) :
(M →ₗ[R] M₂) →ₗ[R] p →ₗ[R] M₂

Alternative version of `dom_restrict` as a linear map.

Equations
@[simp]
theorem linear_map.dom_restrict'_apply {R : Type u} {M : Type v} {M₂ : Type w} [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (p : M) (x : p) :
f) x = f x
@[instance]
def linear_map.endomorphism_semiring {R : Type u} {M : Type v} [semiring R] [ M] :
Equations
@[instance]
def linear_map.endomorphism_ring {R : Type u} {M : Type v} [ring R] [ M] :
ring (M →ₗ[R] M)
Equations
def linear_map.smul_rightₗ {R : Type u} {M : Type v} {M₂ : Type w} [comm_ring R] [add_comm_group M₂] [ M] [ M₂] :
(M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M

The family of linear maps `M₂ → M` parameterised by `f ∈ M₂ → R`, `x ∈ M`, is linear in `f`, `x`.

Equations
@[simp]
theorem linear_map.smul_rightₗ_apply {R : Type u} {M : Type v} {M₂ : Type w} [comm_ring R] [add_comm_group M₂] [ M] [ M₂] (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :
x) c = f c x
@[simp]
theorem add_monoid_hom_lequiv_nat_apply {A : Type u_1} {B : Type u_2} (f : A →+ B) :
@[simp]
theorem add_monoid_hom_lequiv_nat_symm_apply {A : Type u_1} {B : Type u_2} (f : A →ₗ[] B) :
def add_monoid_hom_lequiv_nat {A : Type u_1} {B : Type u_2}  :

The `ℕ`-linear equivalence between additive morphisms `A →+ B` and `ℕ`-linear morphisms `A →ₗ[ℕ] B`.

Equations
@[simp]
theorem add_monoid_hom_lequiv_int_symm_apply {A : Type u_1} {B : Type u_2} (f : A →ₗ[] B) :
def add_monoid_hom_lequiv_int {A : Type u_1} {B : Type u_2}  :

The `ℤ`-linear equivalence between additive morphisms `A →+ B` and `ℤ`-linear morphisms `A →ₗ[ℤ] B`.

Equations
@[simp]
theorem add_monoid_hom_lequiv_int_apply {A : Type u_1} {B : Type u_2} (f : A →+ B) :

### Properties of submodules #

def submodule.of_le {R : Type u} {M : Type v} [semiring R] [ M] {p p' : M} (h : p p') :

If two submodules `p` and `p'` satisfy `p ⊆ p'`, then `of_le p p'` is the linear map version of this inclusion.

Equations
@[simp]
theorem submodule.coe_of_le {R : Type u} {M : Type v} [semiring R] [ M] {p p' : M} (h : p p') (x : p) :
( x) = x
theorem submodule.of_le_apply {R : Type u} {M : Type v} [semiring R] [ M] {p p' : M} (h : p p') (x : p) :
x = x, _⟩
theorem submodule.subtype_comp_of_le {R : Type u} {M : Type v} [semiring R] [ M] (p q : M) (h : p q) :
@[instance]
def submodule.add_comm_monoid_submodule {R : Type u} {M : Type v} [semiring R] [ M] :
Equations
@[simp]
theorem submodule.add_eq_sup {R : Type u} {M : Type v} [semiring R] [ M] (p q : M) :
p + q = p q
@[simp]
theorem submodule.zero_eq_bot {R : Type u} {M : Type v} [semiring R] [ M] :
0 =
theorem submodule.subsingleton_iff (R : Type u) {M : Type v} [semiring R] [ M] :
theorem submodule.nontrivial_iff (R : Type u) {M : Type v} [semiring R] [ M] :
@[instance]
def submodule.unique {R : Type u} {M : Type v} [semiring R] [ M] [subsingleton M] :
Equations
@[instance]
def submodule.unique' {R : Type u} {M : Type v} [semiring R] [ M] [subsingleton R] :
Equations
@[instance]
def submodule.nontrivial {R : Type u} {M : Type v} [semiring R] [ M] [nontrivial M] :
theorem submodule.disjoint_def {R : Type u} {M : Type v} [semiring R] [ M] {p p' : M} :
p' ∀ (x : M), x px p'x = 0
theorem submodule.disjoint_def' {R : Type u} {M : Type v} [semiring R] [ M] {p p' : M} :
p' ∀ (x : M), x p∀ (y : M), y p'x = yx = 0
theorem submodule.mem_right_iff_eq_zero_of_disjoint {R : Type u} {M : Type v} [semiring R] [ M] {p p' : M} (h : p') {x : p} :
x p' x = 0
theorem submodule.mem_left_iff_eq_zero_of_disjoint {R : Type u} {M : Type v} [semiring R] [ M] {p p' : M} (h : p') {x : p'} :
x p x = 0
def submodule.map {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (p : M) :
M₂

The pushforward of a submodule `p ⊆ M` by `f : M → M₂`

Equations
@[simp]
theorem submodule.map_coe {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (p : M) :
p) = f '' p
@[simp]
theorem submodule.mem_map {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} {p : M} {x : M₂} :
x ∃ (y : M), y p f y = x
theorem submodule.mem_map_of_mem {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} {p : M} {r : M} (h : r p) :
f r
theorem submodule.apply_coe_mem_map {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) {p : M} (r : p) :
@[simp]
theorem submodule.map_id {R : Type u} {M : Type v} [semiring R] [ M] (p : M) :
theorem submodule.map_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (p : M) :
submodule.map (g.comp f) p = p)
theorem submodule.map_mono {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} {p p' : M} :
p p' p'
@[simp]
theorem submodule.map_zero {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (p : M) :
theorem submodule.range_map_nonempty {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (N : M) :
(set.range (λ (ϕ : M →ₗ[R] M₂), N)).nonempty
def submodule.equiv_map_of_injective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (i : function.injective f) (p : M) :

The pushforward of a submodule by an injective linear map is linearly equivalent to the original submodule.

Equations
@[simp]
theorem submodule.coe_equiv_map_of_injective_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (i : function.injective f) (p : M) (x : p) :
( x) = f x
def submodule.comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (p : M₂) :
M

The pullback of a submodule `p ⊆ M₂` along `f : M → M₂`

Equations
@[simp]
theorem submodule.comap_coe {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (p : M₂) :
@[simp]
theorem submodule.mem_comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {x : M} {f : M →ₗ[R] M₂} {p : M₂} :
x f x p
theorem submodule.comap_id {R : Type u} {M : Type v} [semiring R] [ M] (p : M) :
theorem submodule.comap_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (p : M₃) :
theorem submodule.comap_mono {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} {q q' : M₂} :
q q' q'
theorem submodule.map_le_iff_le_comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} {p : M} {q : M₂} :
q p
theorem submodule.gc_map_comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) :
@[simp]
theorem submodule.map_bot {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) :
@[simp]
theorem submodule.map_sup {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (p p' : M) (f : M →ₗ[R] M₂) :
(p p') = p'
@[simp]
theorem submodule.map_supr {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {ι : Sort u_1} (f : M →ₗ[R] M₂) (p : ι → M) :
(⨆ (i : ι), p i) = ⨆ (i : ι), (p i)
@[simp]
theorem submodule.comap_top {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) :
@[simp]
theorem submodule.comap_inf {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (q q' : M₂) (f : M →ₗ[R] M₂) :
(q q') = q'
@[simp]
theorem submodule.comap_infi {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {ι : Sort u_1} (f : M →ₗ[R] M₂) (p : ι → M₂) :
(⨅ (i : ι), p i) = ⨅ (i : ι), (p i)
@[simp]
theorem submodule.comap_zero {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (q : M₂) :
theorem submodule.map_comap_le {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (q : M₂) :
q) q
theorem submodule.le_comap_map {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (p : M) :
p p)
def submodule.gci_map_comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} (hf : function.injective f) :

`map f` and `comap f` form a `galois_coinsertion` when `f` is injective.

Equations
theorem submodule.comap_map_eq_of_injective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} (hf : function.injective f) (p : M) :
p) = p
theorem submodule.comap_surjective_of_injective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} (hf : function.injective f) :
theorem submodule.map_injective_of_injective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} (hf : function.injective f) :
theorem submodule.comap_inf_map_of_injective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} (hf : function.injective f) (p q : M) :
p q) = p q
theorem submodule.comap_infi_map_of_injective {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} (hf : function.injective f) (S : ι → M) :
(⨅ (i : ι), (S i)) = infi S
theorem submodule.comap_sup_map_of_injective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} (hf : function.injective f) (p q : M) :
p q) = p q
theorem submodule.comap_supr_map_of_injective {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} (hf : function.injective f) (S : ι → M) :
(⨆ (i : ι), (S i)) = supr S
theorem submodule.map_le_map_iff_of_injective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} (hf : function.injective f) (p q : M) :
p q
theorem submodule.map_strict_mono_of_injective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} (hf : function.injective f) :
theorem submodule.map_inf_eq_map_inf_comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} {p : M} {p' : M₂} :
p' = (p p')
theorem submodule.map_comap_subtype {R : Type u} {M : Type v} [semiring R] [ M] (p p' : M) :
p') = p p'
theorem submodule.eq_zero_of_bot_submodule {R : Type u} {M : Type v} [semiring R] [ M] (b : ) :
b = 0
def submodule.span (R : Type u) {M : Type v} [semiring R] [ M] (s : set M) :
M

The span of a set `s ⊆ M` is the smallest submodule of M that contains `s`.

Equations
theorem submodule.mem_span {R : Type u} {M : Type v} [semiring R] [ M] {x : M} {s : set M} :
x ∀ (p : M), s px p
theorem submodule.subset_span {R : Type u} {M : Type v} [semiring R] [ M] {s : set M} :
s s)
theorem submodule.span_le {R : Type u} {M : Type v} [semiring R] [ M] {s : set M} {p : M} :
p s p
theorem submodule.span_mono {R : Type u} {M : Type v} [semiring R] [ M] {s t : set M} (h : s t) :
theorem submodule.span_eq_of_le {R : Type u} {M : Type v} [semiring R] [ M] (p : M) {s : set M} (h₁ : s p) (h₂ : p ) :
= p
@[simp]
theorem submodule.span_eq {R : Type u} {M : Type v} [semiring R] [ M] (p : M) :
= p
theorem submodule.map_span {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (s : set M) :
s) = (f '' s)
theorem linear_map.map_span {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (s : set M) :
s) = (f '' s)

Alias of `submodule.map_span`.

theorem submodule.map_span_le {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (s : set M) (N : M₂) :
s) N ∀ (m : M), m sf m N
theorem linear_map.map_span_le {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (s : set M) (N : M₂) :
s) N ∀ (m : M), m sf m N

Alias of `submodule.map_span_le`.

theorem submodule.span_preimage_le {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (s : set M₂) :
(f ⁻¹' s) s)
theorem linear_map.span_preimage_le {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (s : set M₂) :
(f ⁻¹' s) s)

Alias of `submodule.span_preimage_le`.

theorem submodule.span_induction {R : Type u} {M : Type v} [semiring R] [ M] {x : M} {s : set M} {p : M → Prop} (h : x ) (Hs : ∀ (x : M), x sp x) (H0 : p 0) (H1 : ∀ (x y : M), p xp yp (x + y)) (H2 : ∀ (a : R) (x : M), p xp (a x)) :
p x

An induction principle for span membership. If `p` holds for 0 and all elements of `s`, and is preserved under addition and scalar multiplication, then `p` holds for all elements of the span of `s`.

theorem submodule.span_nat_eq_add_submonoid_closure {M : Type v} (s : set M) :
@[simp]
theorem submodule.span_nat_eq {M : Type v} (s : add_submonoid M) :
theorem submodule.span_int_eq_add_subgroup_closure {M : Type u_1} (s : set M) :
@[simp]
theorem submodule.span_int_eq {M : Type u_1} (s : add_subgroup M) :
def submodule.gi (R : Type u) (M : Type v) [semiring R] [ M] :

`span` forms a Galois insertion with the coercion from submodule to set.

Equations
@[simp]
theorem submodule.span_empty {R : Type u} {M : Type v} [semiring R] [ M] :
@[simp]
theorem submodule.span_univ {R : Type u} {M : Type v} [semiring R] [ M] :
theorem submodule.span_union {R : Type u} {M : Type v} [semiring R] [ M] (s t : set M) :
(s t) =
theorem submodule.span_Union {R : Type u} {M : Type v} [semiring R] [ M] {ι : Sort u_1} (s : ι → set M) :
(⋃ (i : ι), s i) = ⨆ (i : ι), (s i)
theorem submodule.span_eq_supr_of_singleton_spans {R : Type u} {M : Type v} [semiring R] [ M] (s : set M) :
= ⨆ (x : M) (H : x s), {x}
@[simp]
theorem submodule.coe_supr_of_directed {R : Type u} {M : Type v} [semiring R] [ M] {ι : Sort u_1} [hι : nonempty ι] (S : ι → M) (H : S) :
(supr S) = ⋃ (i : ι), (S i)
theorem submodule.sum_mem_bsupr {R : Type u} {M : Type v} [semiring R] [ M] {ι : Type u_1} {s : finset ι} {f : ι → M} {p : ι → M} (h : ∀ (i : ι), i sf i p i) :
∑ (i : ι) in s, f i ⨆ (i : ι) (H : i s), p i
theorem submodule.sum_mem_supr {R : Type u} {M : Type v} [semiring R] [ M] {ι : Type u_1} [fintype ι] {f : ι → M} {p : ι → M} (h : ∀ (i : ι), f i p i) :
∑ (i : ι), f i ⨆ (i : ι), p i
@[simp]
theorem submodule.mem_supr_of_directed {R : Type u} {M : Type v} [semiring R] [ M] {ι : Sort u_1} [nonempty ι] (S : ι → M) (H : S) {x : M} :
x supr S ∃ (i : ι), x S i
theorem submodule.mem_Sup_of_directed {R : Type u} {M : Type v} [semiring R] [ M] {s : set M)} {z : M} (hs : s.nonempty) (hdir : s) :
z Sup s ∃ (y : M) (H : y s), z y
@[simp]
theorem submodule.coe_supr_of_chain {R : Type u} {M : Type v} [semiring R] [ M] (a : →ₘ M) :
(⨆ (k : ), a k) = ⋃ (k : ), (a k)
theorem submodule.coe_scott_continuous {R : Type u} {M : Type v} [semiring R] [ M] :

We can regard `coe_supr_of_chain` as the statement that `coe : (submodule R M) → set M` is Scott continuous for the ω-complete partial order induced by the complete lattice structures.

@[simp]
theorem submodule.mem_supr_of_chain {R : Type u} {M : Type v} [semiring R] [ M] (a : →ₘ M) (m : M) :
(m ⨆ (k : ), a k) ∃ (k : ), m a k
theorem submodule.mem_sup {R : Type u} {M : Type v} [semiring R] [ M] {p p' : M} {x : M} :
x p p' ∃ (y : M) (H : y p) (z : M) (H : z p'), y + z = x
theorem submodule.mem_sup' {R : Type u} {M : Type v} [semiring R] [ M] {p p' : M} {x : M} :
x p p' ∃ (y : p) (z : p'), y + z = x
theorem submodule.coe_sup {R : Type u} {M : Type v} [semiring R] [ M] {p p' : M} :
(p p') = p + p'
theorem submodule.mem_span_singleton_self {R : Type u} {M : Type v} [semiring R] [ M] (x : M) :
x {x}
theorem submodule.nontrivial_span_singleton {R : Type u} {M : Type v} [semiring R] [ M] {x : M} (h : x 0) :
theorem submodule.mem_span_singleton {R : Type u} {M : Type v} [semiring R] [ M] {x y : M} :
x {y} ∃ (a : R), a y = x
theorem submodule.le_span_singleton_iff {R : Type u} {M : Type v} [semiring R] [ M] {s : M} {v₀ : M} :
s {v₀} ∀ (v : M), v s(∃ (r : R), r v₀ = v)
theorem submodule.span_singleton_eq_top_iff {R : Type u} {M : Type v} [semiring R] [ M] (x : M) :
{x} = ∀ (v : M), ∃ (r : R), r x = v
@[simp]
theorem submodule.span_zero_singleton {R : Type u} {M : Type v} [semiring R] [ M] :
{0} =
theorem submodule.span_singleton_eq_range {R : Type u} {M : Type v} [semiring R] [ M] (y : M) :
{y}) = set.range (λ (_x : R), _x y)
theorem submodule.span_singleton_smul_le {R : Type u} {M : Type v} [semiring R] [ M] (r : R) (x : M) :
{r x} {x}
theorem submodule.span_singleton_smul_eq {K : Type u_1} {E : Type u_2} [ E] {r : K} (x : E) (hr : r 0) :
{r x} = {x}
theorem submodule.disjoint_span_singleton {K : Type u_1} {E : Type u_2} [ E] {s : E} {x : E} :
{x}) x sx = 0
theorem submodule.disjoint_span_singleton' {K : Type u_1} {E : Type u_2} [ E] {p : E} {x : E} (x0 : x 0) :
{x}) x p
theorem submodule.mem_span_insert {R : Type u} {M : Type v} [semiring R] [ M] {x : M} {s : set M} {y : M} :
x (insert y s) ∃ (a : R) (z : M) (H : z s), x = a y + z
theorem submodule.span_insert_eq_span {R : Type u} {M : Type v} [semiring R] [ M] {x : M} {s : set M} (h : x ) :
(insert x s) =
theorem submodule.span_span {R : Type u} {M : Type v} [semiring R] [ M] {s : set M} :
s) =
theorem submodule.span_eq_bot {R : Type u} {M : Type v} [semiring R] [ M] {s : set M} :
= ∀ (x : M), x sx = 0
@[simp]
theorem submodule.span_singleton_eq_bot {R : Type u} {M : Type v} [semiring R] [ M] {x : M} :
{x} = x = 0
@[simp]
theorem submodule.span_zero {R : Type u} {M : Type v} [semiring R] [ M] :
@[simp]
theorem submodule.span_image {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {s : set M} (f : M →ₗ[R] M₂) :
(f '' s) = s)
theorem submodule.apply_mem_span_image_of_mem_span {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) {x : M} {s : set M} (h : x ) :
f x (f '' s)
theorem submodule.not_mem_span_of_apply_not_mem_span_image {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) {x : M} {s : set M} (h : f x (f '' s)) :
x

`f` is an explicit argument so we can `apply` this theorem and obtain `h` as a new goal.

theorem submodule.supr_eq_span {R : Type u} {M : Type v} [semiring R] [ M] {ι : Sort w} (p : ι → M) :
(⨆ (i : ι), p i) = (⋃ (i : ι), (p i))
theorem submodule.span_singleton_le_iff_mem {R : Type u} {M : Type v} [semiring R] [ M] (m : M) (p : M) :
{m} p m p
theorem submodule.singleton_span_is_compact_element {R : Type u} {M : Type v} [semiring R] [ M] (x : M) :
@[instance]
def submodule.is_compactly_generated {R : Type u} {M : Type v} [semiring R] [ M] :
theorem submodule.lt_add_iff_not_mem {R : Type u} {M : Type v} [semiring R] [ M] {I : M} {a : M} :
I < I + {a} a I
theorem submodule.mem_supr {R : Type u} {M : Type v} [semiring R] [ M] {ι : Sort w} (p : ι → M) {m : M} :
(m ⨆ (i : ι), p i) ∀ (N : M), (∀ (i : ι), p i N)m N
theorem submodule.mem_span_finite_of_mem_span {R : Type u} {M : Type v} [semiring R] [ M] {S : set M} {x : M} (hx : x ) :
∃ (T : finset M), T S x

For every element in the span of a set, there exists a finite subset of the set such that the element is contained in the span of the subset.

def submodule.prod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (p : M) (q : M₂) :
(M × M₂)

The product of two submodules is a submodule.

Equations
@[simp]
theorem submodule.prod_coe {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (p : M) (q : M₂) :
(p.prod q) = p.prod q
@[simp]
theorem submodule.mem_prod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {p : M} {q : M₂} {x : M × M₂} :
x p.prod q x.fst p x.snd q
theorem submodule.span_prod_le {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (s : set M) (t : set M₂) :
(s.prod t) s).prod t)
@[simp]
theorem submodule.prod_top {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
@[simp]
theorem submodule.prod_bot {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
theorem submodule.prod_mono {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {p p' : M} {q q' : M₂} :
p p'q q'p.prod q p'.prod q'
@[simp]
theorem submodule.prod_inf_prod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (p p' : M) (q q' : M₂) :
p.prod q p'.prod q' = (p p').prod (q q')
@[simp]
theorem submodule.prod_sup_prod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (p p' : M) (q q' : M₂) :
p.prod q p'.prod q' = (p p').prod (q q')
@[simp]
theorem submodule.neg_coe {R : Type u} {M : Type v} [ring R] [ M] (p : M) :
@[simp]
theorem submodule.map_neg {R : Type u} {M : Type v} {M₂ : Type w} [ring R] [add_comm_group M₂] [ M] [ M₂] (p : M) (f : M →ₗ[R] M₂) :
p =
@[simp]
theorem submodule.span_neg {R : Type u} {M : Type v} [ring R] [ M] (s : set M) :
(-s) =
theorem submodule.mem_span_insert' {R : Type u} {M : Type v} [ring R] [ M] {x y : M} {s : set M} :
x (insert y s) ∃ (a : R), x + a y
def submodule.quotient_rel {R : Type u} {M : Type v} [ring R] [ M] (p : M) :

The equivalence relation associated to a submodule `p`, defined by `x ≈ y` iff `y - x ∈ p`.

Equations
def submodule.quotient {R : Type u} {M : Type v} [ring R] [ M] (p : M) :
Type v

The quotient of a module `M` by a submodule `p ⊆ M`.

Equations
def submodule.quotient.mk {R : Type u} {M : Type v} [ring R] [ M] {p : M} :
M → p.quotient

Map associating to an element of `M` the corresponding element of `M/p`, when `p` is a submodule of `M`.

Equations
@[simp]
theorem submodule.quotient.mk_eq_mk {R : Type u} {M : Type v} [ring R] [ M] {p : M} (x : M) :
@[simp]
theorem submodule.quotient.mk'_eq_mk {R : Type u} {M : Type v} [ring R] [ M] {p : M} (x : M) :
@[simp]
theorem submodule.quotient.quot_mk_eq_mk {R : Type u} {M : Type v} [ring R] [ M] {p : M} (x : M) :
quot.mk setoid.r x =
theorem submodule.quotient.eq {R : Type u} {M : Type v} [ring R] [ M] (p : M) {x y : M} :
x - y p
@[instance]
def submodule.quotient.has_zero {R : Type u} {M : Type v} [ring R] [ M] (p : M) :
Equations
@[instance]
def submodule.quotient.inhabited {R : Type u} {M : Type v} [ring R] [ M] (p : M) :
Equations
@[simp]
theorem submodule.quotient.mk_zero {R : Type u} {M : Type v} [ring R] [ M] (p : M) :
@[simp]
theorem submodule.quotient.mk_eq_zero {R : Type u} {M : Type v} [ring R] [ M] (p : M) {x : M} :
x p
@[instance]
def submodule.quotient.has_add {R : Type u} {M : Type v} [ring R] [ M] (p : M) :
Equations
@[simp]
theorem submodule.quotient.mk_add {R : Type u} {M : Type v} [ring R] [ M] (p : M) {x y : M} :
@[instance]
def submodule.quotient.has_neg {R : Type u} {M : Type v} [ring R] [ M] (p : M) :
Equations
@[simp]
theorem submodule.quotient.mk_neg {R : Type u} {M : Type v} [ring R] [ M] (p : M) {x : M} :
@[instance]
def submodule.quotient.has_sub {R : Type u} {M : Type v} [ring R] [ M] (p : M) :
Equations
@[simp]
theorem submodule.quotient.mk_sub {R : Type u} {M : Type v} [ring R] [ M] (p : M) {x y : M} :
@[instance]
def submodule.quotient.add_comm_group {R : Type u} {M : Type v} [ring R] [ M] (p : M) :
Equations
@[instance]
def submodule.quotient.has_scalar {R : Type u} {M : Type v} [ring R] [ M] (p : M) :
Equations
@[simp]
theorem submodule.quotient.mk_smul {R : Type u} {M : Type v} [ring R] [ M] (p : M) {r : R} {x : M} :
@[simp]
theorem submodule.quotient.mk_nsmul {R : Type u} {M : Type v} [ring R] [ M] (p : M) {x : M} (n : ) :
@[instance]
def submodule.quotient.module {R : Type u} {M : Type v} [ring R] [ M] (p : M) :
Equations
theorem submodule.quotient.mk_surjective {R : Type u} {M : Type v} [ring R] [ M] (p : M) :
theorem submodule.quotient.nontrivial_of_lt_top {R : Type u} {M : Type v} [ring R] [ M] (p : M) (h : p < ) :
theorem submodule.quot_hom_ext {R : Type u} {M : Type v} {M₂ : Type w} [ring R] [add_comm_group M₂] [ M] [ M₂] (p : M) ⦃f g : p.quotient →ₗ[R] M₂⦄ (h : ∀ (x : M), = ) :
f = g
theorem submodule.comap_smul {K : Type u'} {V : Type v'} {V₂ : Type w'} [field K] [ V] [add_comm_group V₂] [ V₂] (f : V →ₗ[K] V₂) (p : V₂) (a : K) (h : a 0) :
theorem submodule.map_smul {K : Type u'} {V : Type v'} {V₂ : Type w'} [field K] [ V] [add_comm_group V₂] [ V₂] (f : V →ₗ[K] V₂) (p : V) (a : K) (h : a 0) :
theorem submodule.comap_smul' {K : Type u'} {V : Type v'} {V₂ : Type w'} [field K] [ V] [add_comm_group V₂] [ V₂] (f : V →ₗ[K] V₂) (p : V₂) (a : K) :
submodule.comap (a f) p = ⨅ (h : a 0),
theorem submodule.map_smul' {K : Type u'} {V : Type v'} {V₂ : Type w'} [field K] [ V] [add_comm_group V₂] [ V₂] (f : V →ₗ[K] V₂) (p : V) (a : K) :
submodule.map (a f) p = ⨆ (h : a 0),

### Properties of linear maps #

theorem linear_map.eq_on_span {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {s : set M} {f g : M →ₗ[R] M₂} (H : g s) ⦃x : M⦄ (h : x ) :
f x = g x

If two linear maps are equal on a set `s`, then they are equal on `submodule.span s`.

See also `linear_map.eq_on_span'` for a version using `set.eq_on`.

theorem linear_map.eq_on_span' {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {s : set M} {f g : M →ₗ[R] M₂} (H : g s) :
g s)

If two linear maps are equal on a set `s`, then they are equal on `submodule.span s`.

This version uses `set.eq_on`, and the hidden argument will expand to `h : x ∈ (span R s : set M)`. See `linear_map.eq_on_span` for a version that takes `h : x ∈ span R s` as an argument.

theorem linear_map.ext_on {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {s : set M} {f g : M →ₗ[R] M₂} (hv : = ) (h : g s) :
f = g

If `s` generates the whole module and linear maps `f`, `g` are equal on `s`, then they are equal.

theorem linear_map.ext_on_range {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {v : ι → M} {f g : M →ₗ[R] M₂} (hv : (set.range v) = ) (h : ∀ (i : ι), f (v i) = g (v i)) :
f = g

If the range of `v : ι → M` generates the whole module and linear maps `f`, `g` are equal at each `v i`, then they are equal.

@[simp]
theorem linear_map.map_finsupp_sum {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {γ : Type u_1} [has_zero γ] (f : M →ₗ[R] M₂) {t : ι →₀ γ} {g : ι → γ → M} :
f (t.sum g) = t.sum (λ (i : ι) (d : γ), f (g i d))
theorem linear_map.coe_finsupp_sum {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {γ : Type u_1} [has_zero γ] (t : ι →₀ γ) (g : ι → γ → (M →ₗ[R] M₂)) :
(t.sum g) = t.sum (λ (i : ι) (d : γ), (g i d))
@[simp]
theorem linear_map.finsupp_sum_apply {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {γ : Type u_1} [has_zero γ] (t : ι →₀ γ) (g : ι → γ → (M →ₗ[R] M₂)) (b : M) :
(t.sum g) b = t.sum (λ (i : ι) (d : γ), (g i d) b)
@[simp]
theorem linear_map.map_dfinsupp_sum {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {γ : ι → Type u_1} [decidable_eq ι] [Π (i : ι), has_zero (γ i)] [Π (i : ι) (x : γ i), decidable (x 0)] (f : M →ₗ[R] M₂) {t : Π₀ (i : ι), γ i} {g : Π (i : ι), γ i → M} :
f (t.sum g) = t.sum (λ (i : ι) (d : γ i), f (g i d))
theorem linear_map.coe_dfinsupp_sum {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {γ : ι → Type u_1} [decidable_eq ι] [Π (i : ι), has_zero (γ i)] [Π (i : ι) (x : γ i), decidable (x 0)] (t : Π₀ (i : ι), γ i) (g : Π (i : ι), γ i(M →ₗ[R] M₂)) :
(t.sum g) = t.sum (λ (i : ι) (d : γ i), (g i d))
@[simp]
theorem linear_map.dfinsupp_sum_apply {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {γ : ι → Type u_1} [decidable_eq ι] [Π (i : ι), has_zero (γ i)] [Π (i : ι) (x : γ i), decidable (x 0)] (t : Π₀ (i : ι), γ i) (g : Π (i : ι), γ i(M →ₗ[R] M₂)) (b : M) :
(t.sum g) b = t.sum (λ (i : ι) (d : γ i), (g i d) b)
@[simp]
theorem linear_map.map_dfinsupp_sum_add_hom {R : Type u} {M : Type v} {M₂ : Type w} {ι : Type x} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {γ : ι → Type u_1} [decidable_eq ι] [Π (i : ι), add_zero_class (γ i)] (f : M →ₗ[R] M₂) {t : Π₀ (i : ι), γ i} {g : Π (i : ι), γ i →+ M} :
f t) = (dfinsupp.sum_add_hom (λ (i : ι), f.to_add_monoid_hom.comp (g i))) t
theorem linear_map.map_cod_restrict {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (p : M) (f : M₂ →ₗ[R] M) (h : ∀ (c : M₂), f c p) (p' : M₂) :
p' = p')
theorem linear_map.comap_cod_restrict {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (p : M) (f : M₂ →ₗ[R] M) (hf : ∀ (c : M₂), f c p) (p' : p) :
p' = p')
def linear_map.range {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) :
M₂

The range of a linear map `f : M → M₂` is a submodule of `M₂`. See Note [range copy pattern].

Equations
theorem linear_map.range_coe {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) :
(f.range) =
@[simp]
theorem linear_map.mem_range {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {f : M →ₗ[R] M₂} {x : M₂} :
x f.range ∃ (y : M), f y = x
theorem linear_map.range_eq_map {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) :
f.range =
theorem linear_map.mem_range_self {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (x : M) :
@[simp]
theorem linear_map.range_id {R : Type u} {M : Type v} [semiring R] [ M] :
theorem linear_map.range_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
(g.comp f).range =
theorem linear_map.range_comp_le_range {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [