# 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 (semi)linear maps
• 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.

See `linear_algebra.span` for the span of a set (as a submodule), and `linear_algebra.quotient` for quotients by submodules.

## Main theorems #

See `linear_algebra.isomorphisms` for Noether's three isomorphism theorems for modules.

## Notations #

• We continue to use the notations `M →ₛₗ[σ] M₂` and `M →ₗ[R] M₂` for the type of semilinear (resp. linear) maps from `M` to `M₂` over the ring homomorphism `σ` (resp. over the ring `R`).

## 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.

## TODO #

• Parts of this file have not yet been generalized to semilinear maps

## Tags #

linear algebra, vector space, module

theorem finsupp.smul_sum {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_4} [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_1} {R : Type u_2} {M : Type u_3} {M₂ : Type u_4} [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_1) (M : Type u_9) (α : Type u_20) [fintype α] [semiring R] [ M] (x : α →₀ M) (ᾰ : α) :
x = x ᾰ
noncomputable def finsupp.linear_equiv_fun_on_fintype (R : Type u_1) (M : Type u_9) (α : Type u_20) [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_1) (M : Type u_9) (α : Type u_20) [fintype α] [semiring R] [ M] [decidable_eq α] (x : α) (m : M) :
m) = m
@[simp]
theorem finsupp.linear_equiv_fun_on_fintype_symm_single (R : Type u_1) (M : Type u_9) (α : Type u_20) [fintype α] [semiring R] [ M] [decidable_eq α] (x : α) (m : M) :
.symm) m) =
@[simp]
theorem finsupp.linear_equiv_fun_on_fintype_symm_coe (R : Type u_1) (M : Type u_9) (α : Type u_20) [fintype α] [semiring R] [ M] (f : α →₀ M) :
noncomputable def finsupp.linear_equiv.finsupp_unique (R : Type u_1) (M : Type u_9) [semiring R] [ M] (α : Type u_2) [unique α] :
→₀ M) ≃ₗ[R] M

If `α` has a unique term, then the type of finitely supported functions `α →₀ M` is `R`-linearly equivalent to `M`.

Equations
@[simp]
theorem finsupp.linear_equiv.finsupp_unique_apply {R : Type u_1} {M : Type u_9} [semiring R] [ M] (α : Type u_2) [unique α] (f : α →₀ M) :
@[simp]
theorem finsupp.linear_equiv.finsupp_unique_symm_apply {R : Type u_1} {M : Type u_9} [semiring R] [ M] {α : Type u_2} [unique α] (m : M) :
theorem pi_eq_sum_univ {ι : Type u_1} [fintype ι] [decidable_eq ι] {R : Type u_2} [semiring R] (x : ι → R) :
x = finset.univ.sum (λ (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_1} {R₂ : Type u_3} {R₃ : Type u_4} {R₄ : Type u_5} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} {M₄ : Type u_14} [semiring R] [semiring R₂] [semiring R₃] [semiring R₄] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄] [ M] [module R₂ M₂] [module R₃ M₃] [module R₄ M₄] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₃₄ : R₃ →+* R₄} {σ₁₃ : R →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R →+* R₄} [ σ₂₃ σ₁₃] [ σ₃₄ σ₂₄] [ σ₃₄ σ₁₄] [ σ₂₄ σ₁₄] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₃ →ₛₗ[σ₃₄] M₄) :
(h.comp g).comp f = h.comp (g.comp f)
def linear_map.dom_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : M) :
p →ₛₗ[σ₁₂] 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_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : M) (x : p) :
def linear_map.cod_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (p : M₂) (f : M →ₛₗ[σ₁₂] M₂) (h : ∀ (c : M), f c p) :
M →ₛₗ[σ₁₂] 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_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (p : M₂) (f : M →ₛₗ[σ₁₂] M₂) {h : ∀ (c : M), f c p} (x : M) :
( h) x) = f x
@[simp]
theorem linear_map.comp_cod_restrict {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [semiring R] [semiring R₂] [semiring R₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : M₃) (h : ∀ (b : M₂), g b p) :
h).comp f = (g.comp f) _
@[simp]
theorem linear_map.subtype_comp_cod_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : M₂) (h : ∀ (b : M), f b p) :
p.subtype.comp h) = f
def linear_map.restrict {R : Type u_1} {M : Type u_9} [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_1} {M : Type u_9} [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_1} {M : Type u_9} [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_1} {M : Type u_9} [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_1} {M : Type u_9} [semiring R] [ M] {f : M →ₗ[R] M} {p : M} (hf : ∀ (x : M), f x p) :
@[protected, instance]
def linear_map.unique_of_left {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [subsingleton M] :
unique (M →ₛₗ[σ₁₂] M₂)
Equations
@[protected, instance]
def linear_map.unique_of_right {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [subsingleton M₂] :
unique (M →ₛₗ[σ₁₂] M₂)
Equations
def linear_map.eval_add_monoid_hom {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (a : M) :
(M →ₛₗ[σ₁₂] M₂) →+ M₂

Evaluation of a `σ₁₂`-linear map at a fixed `a`, as an `add_monoid_hom`.

Equations
def linear_map.to_add_monoid_hom' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} :
(M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂

`linear_map.to_add_monoid_hom` promoted to an `add_monoid_hom`

Equations
theorem linear_map.sum_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (t : finset ι) (f : ι → (M →ₛₗ[σ₁₂] M₂)) (b : M) :
(t.sum (λ (d : ι), f d)) b = t.sum (λ (d : ι), (f d) b)
def linear_map.smul_right {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₁ : Type u_11} [semiring R] [add_comm_monoid M₁] [ M] [ M₁] [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_1} {S : Type u_6} {M : Type u_9} {M₁ : Type u_11} [semiring R] [add_comm_monoid M₁] [ M] [ M₁] [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_1} {S : Type u_6} {M : Type u_9} {M₁ : Type u_11} [semiring R] [add_comm_monoid M₁] [ M] [ M₁] [semiring S] [ S] [ M] [ M] (f : M₁ →ₗ[R] S) (x : M) (c : M₁) :
(f.smul_right x) c = f c x
@[protected, instance]
def linear_map.module.End.nontrivial {R : Type u_1} {M : Type u_9} [semiring R] [ M] [nontrivial M] :
@[simp, norm_cast]
theorem linear_map.coe_fn_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {ι : Type u_2} (t : finset ι) (f : ι → (M →ₛₗ[σ₁₂] M₂)) :
(t.sum (λ (i : ι), f i)) = t.sum (λ (i : ι), (f i))
@[simp]
theorem linear_map.pow_apply {R : Type u_1} {M : Type u_9} [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_1} {M : Type u_9} [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_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] 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_1} {M : Type u_9} [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_1} {M : Type u_9} [semiring R] [ M] (f : M →ₗ[R] M) (n : ) :
(f ^ n) = (f^[n])
@[simp]
theorem linear_map.id_pow {R : Type u_1} {M : Type u_9} [semiring R] [ M] (n : ) :
theorem linear_map.iterate_succ {R : Type u_1} {M : Type u_9} [semiring R] [ M] {f' : M →ₗ[R] M} (n : ) :
f' ^ (n + 1) = (f' ^ n).comp f'
theorem linear_map.iterate_surjective {R : Type u_1} {M : Type u_9} [semiring R] [ M] {f' : M →ₗ[R] M} (h : function.surjective f') (n : ) :
theorem linear_map.iterate_injective {R : Type u_1} {M : Type u_9} [semiring R] [ M] {f' : M →ₗ[R] M} (h : function.injective f') (n : ) :
theorem linear_map.iterate_bijective {R : Type u_1} {M : Type u_9} [semiring R] [ M] {f' : M →ₗ[R] M} (h : function.bijective f') (n : ) :
theorem linear_map.injective_of_iterate_injective {R : Type u_1} {M : Type u_9} [semiring R] [ M] {f' : M →ₗ[R] M} {n : } (hn : n 0) (h : function.injective (f' ^ n)) :
theorem linear_map.surjective_of_iterate_surjective {R : Type u_1} {M : Type u_9} [semiring R] [ M] {f' : M →ₗ[R] M} {n : } (hn : n 0) (h : function.surjective (f' ^ n)) :
theorem linear_map.pow_apply_mem_of_forall_mem {R : Type u_1} {M : Type u_9} [semiring R] [ M] {f' : M →ₗ[R] M} {p : M} (n : ) (h : ∀ (x : M), x pf' x p) (x : M) (hx : x p) :
(f' ^ n) x p
theorem linear_map.pow_restrict {R : Type u_1} {M : Type u_9} [semiring R] [ M] {f' : M →ₗ[R] M} {p : M} (n : ) (h : ∀ (x : M), x pf' x p) (h' : (∀ (x : M), x p(f' ^ n) x p) := _) :
f'.restrict h ^ n = (f' ^ n).restrict h'
theorem linear_map.pi_apply_eq_sum_univ {R : Type u_1} {M : Type u_9} {ι : Type u_17} [semiring R] [ M] [fintype ι] [decidable_eq ι] (f : (ι → R) →ₗ[R] M) (x : ι → R) :
f x = finset.univ.sum (λ (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.

@[simp]
theorem linear_map.applyₗ'_apply_apply {R : Type u_1} (S : Type u_6) {M : Type u_9} {M₂ : Type u_12} [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_1} (S : Type u_6) {M : Type u_9} {M₂ : Type u_12} [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_1) (S : Type u_6) (M : Type u_9) [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_1) (S : Type u_6) (M : Type u_9) [semiring R] [semiring S] [ M] [ M] [ M] (x : M) :
M).symm) x = 1.smul_right x
def linear_map.ring_lmap_equiv_self (R : Type u_1) (S : Type u_6) (M : Type u_9) [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
def linear_map.comp_right {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [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.comp_right_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) :
(f.comp_right) g = f.comp g
@[simp]
theorem linear_map.applyₗ_apply_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [add_comm_monoid M₂] [ M] [ M₂] (v : M) (f : M →ₗ[R] M₂) :
f = f v
def linear_map.applyₗ {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [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_1} {M : Type u_9} {M₂ : Type u_12} [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_1} {M : Type u_9} {M₂ : Type u_12} [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (p : M) (x : p) :
f) x = f x
def linear_map.smul_rightₗ {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [add_comm_monoid 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_1} {M : Type u_9} {M₂ : Type u_12} [add_comm_monoid 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} (R : Type u_3) [semiring R] [ B] (f : A →+ B) :
@[simp]
theorem add_monoid_hom_lequiv_nat_symm_apply {A : Type u_1} {B : Type u_2} (R : Type u_3) [semiring R] [ B] (f : A →ₗ[] B) :
def add_monoid_hom_lequiv_nat {A : Type u_1} {B : Type u_2} (R : Type u_3) [semiring R] [ B] :

The `R`-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} (R : Type u_3) [semiring R] [ B] (f : A →ₗ[] B) :
def add_monoid_hom_lequiv_int {A : Type u_1} {B : Type u_2} (R : Type u_3) [semiring R] [ B] :

The `R`-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} (R : Type u_3) [semiring R] [ B] (f : A →+ B) :

### Properties of submodules #

def submodule.of_le {R : Type u_1} {M : Type u_9} [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_1} {M : Type u_9} [semiring R] [ M] {p p' : M} (h : p p') (x : p) :
( x) = x
theorem submodule.of_le_apply {R : Type u_1} {M : Type u_9} [semiring R] [ M] {p p' : M} (h : p p') (x : p) :
x = x, _⟩
theorem submodule.of_le_injective {R : Type u_1} {M : Type u_9} [semiring R] [ M] {p p' : M} (h : p p') :
theorem submodule.subtype_comp_of_le {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p q : M) (h : p q) :
@[simp]
theorem submodule.subsingleton_iff (R : Type u_1) {M : Type u_9} [semiring R] [ M] :
@[simp]
theorem submodule.nontrivial_iff (R : Type u_1) {M : Type u_9} [semiring R] [ M] :
@[protected, instance]
def submodule.unique {R : Type u_1} {M : Type u_9} [semiring R] [ M] [subsingleton M] :
Equations
@[protected, instance]
def submodule.unique' {R : Type u_1} {M : Type u_9} [semiring R] [ M] [subsingleton R] :
Equations
@[protected, instance]
def submodule.nontrivial {R : Type u_1} {M : Type u_9} [semiring R] [ M] [nontrivial M] :
theorem submodule.mem_right_iff_eq_zero_of_disjoint {R : Type u_1} {M : Type u_9} [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_1} {M : Type u_9} [semiring R] [ M] {p p' : M} (h : p') {x : p'} :
x p x = 0
def submodule.map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {F : Type u_20} [sc : σ₁₂ M M₂] (f : F) (p : M) :
M₂

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

Equations
Instances for `↥submodule.map`
@[simp]
theorem submodule.map_coe {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {F : Type u_20} [sc : σ₁₂ M M₂] (f : F) (p : M) :
p) = f '' p
theorem submodule.map_to_add_submonoid {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : M) :
theorem submodule.map_to_add_submonoid' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : M) :
@[simp]
theorem submodule.mem_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} {p : M} {x : M₂} :
x ∃ (y : M), y p f y = x
theorem submodule.mem_map_of_mem {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} {p : M} {r : M} (h : r p) :
f r
theorem submodule.apply_coe_mem_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {F : Type u_20} [sc : σ₁₂ M M₂] (f : F) {p : M} (r : p) :
@[simp]
theorem submodule.map_id {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p : M) :
theorem submodule.map_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [semiring R] [semiring R₂] [semiring R₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ σ₂₃ σ₁₃] [ring_hom_surjective σ₁₂] [ring_hom_surjective σ₂₃] [ring_hom_surjective σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : M) :
submodule.map (g.comp f) p = p)
theorem submodule.map_mono {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} {p p' : M} :
p p' p'
@[simp]
theorem submodule.map_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (p : M) [ring_hom_surjective σ₁₂] :
theorem submodule.map_add_le {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (p : M) [ring_hom_surjective σ₁₂] (f g : M →ₛₗ[σ₁₂] M₂) :
theorem submodule.range_map_nonempty {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (N : M) :
(set.range (λ (ϕ : M →ₛₗ[σ₁₂] M₂), N)).nonempty
noncomputable def submodule.equiv_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ σ₂₁] [ σ₁₂] {F : Type u_20} [sc : σ₁₂ M M₂] (f : F) (i : function.injective f) (p : M) :
p ≃ₛₗ[σ₁₂] p)

The pushforward of a submodule by an injective linear map is linearly equivalent to the original submodule. See also `linear_equiv.submodule_map` for a computable version when `f` has an explicit inverse.

Equations
@[simp]
theorem submodule.coe_equiv_map_of_injective_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ σ₂₁] [ σ₁₂] {F : Type u_20} [sc : σ₁₂ M M₂] (f : F) (i : function.injective f) (p : M) (x : p) :
( x) = f x
def submodule.comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] (f : F) (p : M₂) :
M

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

Equations
@[simp]
theorem submodule.comap_coe {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] (f : F) (p : M₂) :
@[simp]
theorem submodule.mem_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {x : M} {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} {p : M₂} :
x f x p
@[simp]
theorem submodule.comap_id {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p : M) :
theorem submodule.comap_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [semiring R] [semiring R₂] [semiring R₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : M₃) :
theorem submodule.comap_mono {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} {q q' : M₂} :
q q' q'
theorem submodule.le_comap_pow_of_le_comap {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p : M) {f : M →ₗ[R] M} (h : p ) (k : ) :
theorem submodule.map_le_iff_le_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {f : F} {p : M} {q : M₂} :
q p
theorem submodule.gc_map_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] (f : F) :
@[simp]
theorem submodule.map_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] (f : F) :
@[simp]
theorem submodule.map_sup {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (p p' : M) {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] (f : F) :
(p p') = p'
@[simp]
theorem submodule.map_supr {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {ι : Sort u_2} (f : F) (p : ι → M) :
(⨆ (i : ι), p i) = ⨆ (i : ι), (p i)
@[simp]
theorem submodule.comap_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] (f : F) :
@[simp]
theorem submodule.comap_inf {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (q q' : M₂) {F : Type u_20} [sc : σ₁₂ M M₂] (f : F) :
(q q') = q'
@[simp]
theorem submodule.comap_infi {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {ι : Sort u_2} (f : F) (p : ι → M₂) :
(⨅ (i : ι), p i) = ⨅ (i : ι), (p i)
@[simp]
theorem submodule.comap_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (q : M₂) :
theorem submodule.map_comap_le {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] (f : F) (q : M₂) :
q) q
theorem submodule.le_comap_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] (f : F) (p : M) :
p p)
def submodule.gi_map_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} (hf : function.surjective f) [ring_hom_surjective σ₁₂] :

`map f` and `comap f` form a `galois_insertion` when `f` is surjective.

Equations
theorem submodule.map_comap_eq_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} (hf : function.surjective f) [ring_hom_surjective σ₁₂] (p : M₂) :
p) = p
theorem submodule.map_surjective_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} (hf : function.surjective f) [ring_hom_surjective σ₁₂] :
theorem submodule.comap_injective_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} (hf : function.surjective f) [ring_hom_surjective σ₁₂] :
theorem submodule.map_sup_comap_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} (hf : function.surjective f) [ring_hom_surjective σ₁₂] (p q : M₂) :
p q) = p q
theorem submodule.map_supr_comap_of_sujective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} (hf : function.surjective f) [ring_hom_surjective σ₁₂] {ι : Sort u_2} (S : ι → M₂) :
(⨆ (i : ι), (S i)) = supr S
theorem submodule.map_inf_comap_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} (hf : function.surjective f) [ring_hom_surjective σ₁₂] (p q : M₂) :
p q) = p q
theorem submodule.map_infi_comap_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} (hf : function.surjective f) [ring_hom_surjective σ₁₂] {ι : Sort u_2} (S : ι → M₂) :
(⨅ (i : ι), (S i)) = infi S
theorem submodule.comap_le_comap_iff_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} (hf : function.surjective f) [ring_hom_surjective σ₁₂] (p q : M₂) :
p q
theorem submodule.comap_strict_mono_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] {f : F} (hf : function.surjective f) [ring_hom_surjective σ₁₂] :
def submodule.gci_map_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {f : F} (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_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {f : F} (hf : function.injective f) (p : M) :
p) = p
theorem submodule.comap_surjective_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {f : F} (hf : function.injective f) :
theorem submodule.map_injective_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {f : F} (hf : function.injective f) :
theorem submodule.comap_inf_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {f : F} (hf : function.injective f) (p q : M) :
p q) = p q
theorem submodule.comap_infi_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {f : F} (hf : function.injective f) {ι : Sort u_2} (S : ι → M) :
(⨅ (i : ι), (S i)) = infi S
theorem submodule.comap_sup_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {f : F} (hf : function.injective f) (p q : M) :
p q) = p q
theorem submodule.comap_supr_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {f : F} (hf : function.injective f) {ι : Sort u_2} (S : ι → M) :
(⨆ (i : ι), (S i)) = supr S
theorem submodule.map_le_map_iff_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {f : F} (hf : function.injective f) (p q : M) :
p q
theorem submodule.map_strict_mono_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {f : F} (hf : function.injective f) :
theorem submodule.map_inf_eq_map_inf_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : σ₁₂ M M₂] [ring_hom_surjective σ₁₂] {f : F} {p : M} {p' : M₂} :
p' = (p p')
theorem submodule.map_comap_subtype {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p p' : M) :
p') = p p'
theorem submodule.eq_zero_of_bot_submodule {R : Type u_1} {M : Type u_9} [semiring R] [ M] (b : ) :
b = 0
theorem linear_map.infi_invariant {R : Type u_1} {M : Type u_9} [semiring R] [ M] {σ : R →+* R} {ι : Sort u_2} (f : M →ₛₗ[σ] M) {p : ι → M} (hf : ∀ (i : ι) (v : M), v p if v p i) (v : M) (H : v infi p) :
f v infi p

The infimum of a family of invariant submodule of an endomorphism is also an invariant submodule.

@[simp]
theorem submodule.neg_coe {R : Type u_1} {M : Type u_9} [ring R] [ M] (p : M) :
@[protected, simp]
theorem submodule.map_neg {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [ring R] [ M] (p : M) [add_comm_group M₂] [ M₂] (f : M →ₗ[R] M₂) :
p =
theorem submodule.comap_smul {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [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_7} {V : Type u_18} {V₂ : Type u_19} [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_7} {V : Type u_18} {V₂ : Type u_19} [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_7} {V : Type u_18} {V₂ : Type u_19} [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 #

@[simp]
theorem linear_map.map_finsupp_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [ M] [module R₂ M₂] {γ : Type u_20} [has_zero γ] (f : M →ₛₗ[σ₁₂] 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_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [ M] [module R₂ M₂] {γ : Type u_20} [has_zero γ] (t : ι →₀ γ) (g : ι → γ → (M →ₛₗ[σ₁₂] M₂)) :
(t.sum g) = t.sum (λ (i : ι) (d : γ), (g i d))
@[simp]
theorem linear_map.finsupp_sum_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [ M] [module R₂ M₂] {γ : Type u_20} [has_zero γ] (t : ι →₀ γ) (g : ι → γ → (M →ₛₗ[σ₁₂] 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_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [ M] [module R₂ M₂] {γ : ι → Type u_20} [decidable_eq ι] [Π (i : ι), has_zero (γ i)] [Π (i : ι) (x : γ i), decidable (x 0)] (f : M →ₛₗ[σ₁₂] 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_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [ M] [module R₂ M₂] {γ : ι → Type u_20} [decidable_eq ι] [Π (i : ι), has_zero (γ i)] [Π (i : ι) (x : γ i), decidable (x 0)] (t : Π₀ (i : ι), γ i) (g : Π (i : ι), γ i(M →ₛₗ[σ₁₂] M₂)) :
(t.sum g) = t.sum (λ (i : ι) (d : γ i), (g i d))
@[simp]
theorem linear_map.dfinsupp_sum_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [ M] [module R₂ M₂] {γ : ι → Type u_20} [decidable_eq ι] [Π (i : ι), has_zero (γ i)] [Π (i : ι) (x : γ i), decidable (x 0)] (t : Π₀ (i : ι), γ i) (g : Π (i : ι), γ i(M →ₛₗ[σ₁₂] 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_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [ M] [module R₂ M₂] {γ : ι → Type u_20} [decidable_eq ι] [Π (i : ι), add_zero_class (γ i)] (f : M →ₛₗ[σ₁₂] 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_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₂₁ : R₂ →+* R} [ring_hom_surjective σ₂₁] (p : M) (f : M₂ →ₛₗ[σ₂₁] M) (h : ∀ (c : M₂), f c p) (p' : M₂) :
p' = p')
theorem linear_map.comap_cod_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {σ₂₁ : R₂ →+* R} (p : M) (f : M₂ →ₛₗ[σ₂₁] M) (hf : ∀ (c : M₂), f c p) (p' : p) :
p' = p')
def linear_map.range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] (f : F) :
M₂

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

Equations
Instances for `↥linear_map.range`
theorem linear_map.range_coe {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] (f : F) :
theorem linear_map.range_to_add_submonoid {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
@[simp]
theorem linear_map.mem_range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] {f : F} {x : M₂} :
∃ (y : M), f y = x
theorem linear_map.range_eq_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] (f : F) :
theorem linear_map.mem_range_self {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] (f : F) (x : M) :
f x
@[simp]
theorem linear_map.range_id {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
theorem linear_map.range_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [semiring R] [semiring R₂] [semiring R₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ τ₂₃ τ₁₃] [ring_hom_surjective τ₁₂] [ring_hom_surjective τ₂₃] [ring_hom_surjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
theorem linear_map.range_comp_le_range {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [semiring R] [semiring R₂] [semiring R₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ τ₂₃ τ₁₃] [ring_hom_surjective τ₂₃] [ring_hom_surjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
theorem linear_map.range_eq_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] {f : F} :
theorem linear_map.range_le_iff_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] {f : F} {p : M₂} :
theorem linear_map.map_le_range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] {f : F} {p : M} :
@[simp]
theorem linear_map.range_neg {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [semiring R] [ring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
@[simp]
theorem linear_map.iterate_range_coe {R : Type u_1} {M : Type u_9} [semiring R] [ M] (f : M →ₗ[R] M) (n : ) :
def linear_map.iterate_range {R : Type u_1} {M : Type u_9} [semiring R] [ M] (f : M →ₗ[R] M) :

The decreasing sequence of submodules consisting of the ranges of the iterates of a linear map.

Equations
@[reducible]
def linear_map.range_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
M →ₛₗ[τ₁₂]

Restrict the codomain of a linear map `f` to `f.range`.

This is the bundled version of `set.range_factorization`.

Equations
@[protected, instance]
def linear_map.fintype_range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [fintype M] [decidable_eq M₂] [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :

The range of a linear map is finite if the domain is finite. Note: this instance can form a diamond with `subtype.fintype` in the presence of `fintype M₂`.

Equations
def linear_map.ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] (f : F) :
M

The kernel of a linear map `f : M → M₂` is defined to be `comap f ⊥`. This is equivalent to the set of `x : M` such that `f x = 0`. The kernel is a submodule of `M`.

Equations
@[simp]
theorem linear_map.mem_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] {f : F} {y : M} :
f y = 0
@[simp]
theorem linear_map.ker_id {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
@[simp]
theorem linear_map.map_coe_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] (f : F) (x : ) :
f x = 0
theorem linear_map.ker_to_add_submonoid {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
theorem linear_map.comp_ker_subtype {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
f.comp = 0
theorem linear_map.ker_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [semiring R] [semiring R₂] [semiring R₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
theorem linear_map.ker_le_ker_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [semiring R] [semiring R₂] [semiring R₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
theorem linear_map.disjoint_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] {f : F} {p : M} :
∀ (x : M), x pf x = 0x = 0
theorem linear_map.ker_eq_bot' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] {f : F} :
∀ (m : M), f m = 0m = 0
theorem linear_map.ker_eq_bot_of_inverse {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₁] M} (h : g.comp f = linear_map.id) :
theorem linear_map.le_ker_iff_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] {f : F} {p : M} :
theorem linear_map.ker_cod_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₂₁ : R₂ →+* R} (p : M) (f : M₂ →ₛₗ[τ₂₁] M) (hf : ∀ (c : M₂), f c p) :
theorem linear_map.range_cod_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₂₁ : R₂ →+* R} [ring_hom_surjective τ₂₁] (p : M) (f : M₂ →ₛₗ[τ₂₁] M) (hf : ∀ (c : M₂), f c p) :
theorem linear_map.ker_restrict {R : Type u_1} {M : Type u_9} [semiring R] [ M] {p : M} {f : M →ₗ[R] M} (hf : ∀ (x : M), x pf x p) :
theorem submodule.map_comap_eq {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] (f : F) (q : M₂) :
q) =
theorem submodule.map_comap_eq_self {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] {f : F} {q : M₂} (h : q ) :
q) = q
@[simp]
theorem linear_map.ker_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} :
@[simp]
theorem linear_map.range_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] :
theorem linear_map.ker_eq_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} :
f = 0
theorem linear_map.range_le_bot_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
f = 0
theorem linear_map.range_eq_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} :
f = 0
theorem linear_map.range_le_ker_iff {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [semiring R] [semiring R₂] [semiring R₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ τ₂₃ τ₁₃] [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} :
g.comp f = 0
theorem linear_map.comap_le_comap_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] {f : F} (hf : = ) {p p' : M₂} :
p' p p'
theorem linear_map.comap_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] {f : F} (hf : = ) :
theorem linear_map.ker_eq_bot_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] {f : F} (hf : function.injective f) :
@[simp]
theorem linear_map.iterate_ker_coe {R : Type u_1} {M : Type u_9} [semiring R] [ M] (f : M →ₗ[R] M) (n : ) :
def linear_map.iterate_ker {R : Type u_1} {M : Type u_9} [semiring R] [ M] (f : M →ₗ[R] M) :

The increasing sequence of submodules consisting of the kernels of the iterates of a linear map.

Equations
theorem linear_map.range_to_add_subgroup {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [ring R] [ring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
theorem linear_map.ker_to_add_subgroup {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [ring R] [ring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
theorem linear_map.sub_mem_ker_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [ring R] [ring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {x y : M} :
x - y f x = f y
theorem linear_map.disjoint_ker' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [ring R] [ring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {p : M} :
∀ (x : M), x p∀ (y : M), y pf x = f yx = y
theorem linear_map.inj_of_disjoint_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [ring R] [ring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {p : M} {s : set M} (h : s p) (hd : ) (x : M) (H : x s) (y : M) (H_1 : y s) :
f x = f yx = y
theorem linear_map.ker_eq_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [ring R] [ring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} :
theorem linear_map.ker_le_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [ring R] [ring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} [ring_hom_surjective τ₁₂] {p : M} :
∃ (y : M₂) (H : , f ⁻¹' {y} p
theorem linear_map.ker_smul {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [field K] [ V] [add_comm_group V₂] [ V₂] (f : V →ₗ[K] V₂) (a : K) (h : a 0) :
theorem linear_map.ker_smul' {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [field K] [ V] [add_comm_group V₂] [ V₂] (f : V →ₗ[K] V₂) (a : K) :
linear_map.ker (a f) = ⨅ (h : a 0),
theorem linear_map.range_smul {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [field K] [ V] [add_comm_group V₂] [ V₂] (f : V →ₗ[K] V₂) (a : K) (h : a 0) :
theorem linear_map.range_smul' {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [field K] [ V] [add_comm_group V₂] [ V₂] (f : V →ₗ[K] V₂) (a : K) :
linear_map.range (a f) = ⨆ (h : a 0),
theorem is_linear_map.is_linear_map_add {R : Type u_1} {M : Type u_9} [semiring R] [ M] :
(λ (x : M × M), x.fst + x.snd)
theorem is_linear_map.is_linear_map_sub {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
(λ (x : M × M), x.fst - x.snd)
@[simp]
theorem submodule.map_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] [ring_hom_surjective τ₁₂] (f : F) :
@[simp]
theorem submodule.comap_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : τ₁₂ M M₂] (f : F) :
@[simp]
theorem submodule.ker_subtype {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p : M) :
@[simp]
theorem submodule.range_subtype {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p : M) :
theorem submodule.map_subtype_le {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p : M) (p' : p) :
p' p
@[simp]
theorem submodule.map_subtype_top {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p : M) :

Under the canonical linear map from a submodule `p` to the ambient space `M`, the image of the maximal submodule of `p` is just `p`.

@[simp]
theorem submodule.comap_subtype_eq_top {R : Type u_1} {M : Type u_9} [semiring R] [ M] {p p' : M} :
= p p'
@[simp]
theorem submodule.comap_subtype_self {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p : M) :
@[simp]
theorem submodule.ker_of_le {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p p' : M) (h : p p') :
theorem submodule.range_of_le {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p q : M) (h : p q) :
@[simp]
theorem submodule.map_subtype_range_of_le {R : Type u_1} {M : Type u_9} [semiring R] [ M] {p p' : M} (h : p p') :
= p
theorem submodule.disjoint_iff_comap_eq_bot {R : Type u_1} {M : Type u_9} [semiring R] [ M] {p q : M} :
q
def submodule.map_subtype.rel_iso {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p : M) :
p ≃o {p' // p' p}

If `N ⊆ M` then submodules of `N` are the same as submodules of `M` contained in `N`

Equations
def submodule.map_subtype.order_embedding {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p : M) :
p ↪o M

If `p ⊆ M` is a submodule, the ordering of submodules of `p` is embedded in the ordering of submodules of `M`.

Equations
• = (λ (p' : M), p' p))
@[simp]
theorem submodule.map_subtype_embedding_eq {R : Type u_1} {M : Type u_9} [semiring R] [ M] (p : M) (p' : p) :
theorem linear_map.ker_eq_bot_of_cancel {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} (h : ∀ (u v : →ₗ[R] M), f.comp u = f.comp vu = v) :

A monomorphism is injective.

theorem linear_map.range_comp_of_range_eq_top {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [semiring R] [semiring R₂] [semiring R₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ τ₂₃ τ₁₃] [ring_hom_surjective τ₁₂] [ring_hom_surjective τ₂₃] [ring_hom_surjective τ₁₃] {f : M →ₛₗ[τ₁₂] M₂} (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : = ) :
theorem linear_map.ker_comp_of_ker_eq_bot {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [semiring R] [semiring R₂] [semiring R₃] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃} (hg : = ) :
def linear_map.submodule_image {R : Type u_1} {M : Type u_9} [semiring R] [ M] {M' : Type u_2} [add_comm_monoid M'] [ M'] {O : M} (ϕ : O →ₗ[R] M') (N : M) :
M'

If `O` is a submodule of `M`, and `Φ : O →ₗ M'` is a linear map, then `(ϕ : O →ₗ M').submodule_image N` is `ϕ(N)` as a submodule of `M'`

Equations
• = N)
@[simp]
theorem linear_map.mem_submodule_image {R : Type u_1} {M : Type u_9} [semiring R] [ M] {M' : Type u_2} [add_comm_monoid M'] [ M'] {O : M} {ϕ : O →ₗ[R] M'} {N : M} {x : M'} :
x ∃ (y : M) (yO : y O) (yN : y N), ϕ y, yO⟩ = x
theorem linear_map.mem_submodule_image_of_le {R : Type u_1} {M : Type u_9} [semiring R] [ M] {M' : Type u_2} [add_comm_monoid M'] [ M'] {O : M} {ϕ : O →ₗ[R] M'} {N : M} (hNO : N O) {x : M'} :
x ∃ (y : M) (yN : y N), ϕ y, _⟩ = x
theorem linear_map.submodule_image_apply_of_le {R : Type u_1} {M : Type u_9} [semiring R] [ M] {M' : Type u_2} [add_comm_group M'] [ M'] {O : M} (ϕ : O →ₗ[R] M') (N : M) (hNO : N O) :
@[simp]
theorem linear_map.range_range_restrict {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) :

### Linear equivalences #

@[protected, instance]
def linear_equiv.has_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] [subsingleton M] [subsingleton M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ σ₂₁] [ σ₁₂] :
has_zero (M ≃ₛₗ[σ₁₂] M₂)

Between two zero modules, the zero map is an equivalence.

Equations
@[simp]
theorem linear_equiv.zero_symm {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] [subsingleton M] [subsingleton M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ σ₂₁] [ σ₁₂] :
0.symm = 0
@[simp]
theorem linear_equiv.coe_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] [subsingleton M] [subsingleton M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ σ₂₁] [ σ₁₂] :
0 = 0
theorem linear_equiv.zero_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] [subsingleton M] [subsingleton M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ σ₂₁] [ σ₁₂] (x : M) :
0 x = 0
@[protected, instance]
def linear_equiv.unique {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] [subsingleton M] [subsingleton M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ σ₂₁] [ σ₁₂] :
unique (M ≃ₛₗ[σ₁₂] M₂)

Between two zero modules, the zero map is the only equivalence.

Equations
theorem linear_equiv.map_eq_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] {module_M : M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : M} :
= p
def linear_equiv.submodule_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] {module_M : M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : M) :
p ≃ₛₗ[σ₁₂] p)

A linear equivalence of two modules restricts to a linear equivalence from any submodule `p` of the domain onto the image of that submodule.

This is the linear version of `add_equiv.submonoid_map` and `add_equiv.subgroup_map`.

This is `linear_equiv.of_submodule'` but with `map` on the right instead of `comap` on the left.

Equations
@[simp]
theorem linear_equiv.submodule_map_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] {module_M : M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : M) (x : p) :
@[simp]
theorem linear_equiv.submodule_map_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] {module_M : M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : σ₂₁} {re₂₁ : σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : M) (x : p)) :
@[simp]
theorem linear_equiv.map_finsupp_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} {γ : Type u_20} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] [has_zero γ] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [ τ₂₁] [ τ₁₂] (f : M ≃ₛₗ[τ₁₂] M₂) {t : ι →₀ γ} {g : ι → γ → M} :
f (t.sum g) = t.sum (λ (i : ι) (d : γ), f (g i d))
@[simp]
theorem linear_equiv.map_dfinsupp_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [ τ₂₁] [ τ₁₂] {γ : ι → Type u_20} [decidable_eq ι] [Π (i : ι), has_zero (γ i)] [Π (i : ι) (x : γ i), decidable (x 0)] (f : M ≃ₛₗ[τ₁₂] M₂) (t : Π₀ (i : ι), γ i) (g : Π (i : ι), γ i → M) :
f (t.sum g) = t.sum (λ (i : ι) (d : γ i), f (g i d))
@[simp]
theorem linear_equiv.map_dfinsupp_sum_add_hom {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [ τ₂₁] [ τ₁₂] {γ : ι → Type u_20} [decidable_eq ι] [Π (i : ι), add_zero_class (γ i)] (f : M ≃ₛₗ[τ₁₂] M₂) (t : Π₀ (i : ι), γ i) (g : Π (i : ι), γ i →+ M) :
@[protected]
def linear_equiv.curry (R : Type u_1) (V : Type u_18) (V₂ : Type u_19) [semiring R] :
(V × V₂ → R) ≃ₗ[R] V → V₂ → R

Linear equivalence between a curried and uncurried function. Differs from `tensor_product.curry`.

Equations
@[simp]
theorem linear_equiv.coe_curry (R : Type u_1) (V : Type u_18) (V₂ : Type u_19) [semiring R] :
@[simp]
theorem linear_equiv.coe_curry_symm (R : Type u_1) (V : Type u_18) (V₂ : Type u_19) [semiring R] :
def linear_equiv.of_eq {R : Type u_1} {M : Type u_9} [semiring R] {module_M : M} (p q : M) (h : p = q) :

Linear equivalence between two equal submodules.

Equations
@[simp]
theorem linear_equiv.coe_of_eq_apply {R : Type u_1} {M : Type u_9} [semiring R] {module_M : M} {p q : M} (h : p = q) (x : p) :
( h) x) = x
@[simp]
theorem linear_equiv.of_eq_symm {R : Type u_1} {M : Type u_9} [semiring R] {module_M : M} {p q : M} (h : p = q) :
h).symm = _
@[simp]
theorem linear_equiv.of_eq_rfl {R : Type u_1} {M : Type u_9} [semiring R] {module_M : M} {p : M} :
def linear_equiv.of_submodules {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M₂] {module_M : M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ :