Linear algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
kerand rangerangeof a linear map are submodules of the domain and codomain respectively.
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₂andM →ₗ[R] M₂for the type of semilinear (resp. linear) maps fromMtoM₂over the ring homomorphismσ(resp. over the ringR).
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
@[simp]
noncomputable
def
finsupp.linear_equiv_fun_on_finite
(R : Type u_1)
(M : Type u_9)
(α : Type u_20)
[finite α]
[add_comm_monoid M]
[semiring R]
[module R M] :
Given finite α, linear_equiv_fun_on_finite R is the natural R-linear equivalence between
α →₀ β and α → β.
Equations
- finsupp.linear_equiv_fun_on_finite R M α = {to_fun := coe_fn finsupp.has_coe_to_fun, map_add' := _, map_smul' := _, inv_fun := finsupp.equiv_fun_on_finite.inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
finsupp.linear_equiv_fun_on_finite_apply
(R : Type u_1)
(M : Type u_9)
(α : Type u_20)
[finite α]
[add_comm_monoid M]
[semiring R]
[module R M]
(x : α →₀ M)
(ᾰ : α) :
⇑(finsupp.linear_equiv_fun_on_finite R M α) x ᾰ = ⇑x ᾰ
@[simp]
theorem
finsupp.linear_equiv_fun_on_finite_single
(R : Type u_1)
(M : Type u_9)
(α : Type u_20)
[finite α]
[add_comm_monoid M]
[semiring R]
[module R M]
[decidable_eq α]
(x : α)
(m : M) :
⇑(finsupp.linear_equiv_fun_on_finite R M α) (finsupp.single x m) = pi.single x m
@[simp]
theorem
finsupp.linear_equiv_fun_on_finite_symm_single
(R : Type u_1)
(M : Type u_9)
(α : Type u_20)
[finite α]
[add_comm_monoid M]
[semiring R]
[module R M]
[decidable_eq α]
(x : α)
(m : M) :
⇑((finsupp.linear_equiv_fun_on_finite R M α).symm) (pi.single x m) = finsupp.single x m
@[simp]
theorem
finsupp.linear_equiv_fun_on_finite_symm_coe
(R : Type u_1)
(M : Type u_9)
(α : Type u_20)
[finite α]
[add_comm_monoid M]
[semiring R]
[module R M]
(f : α →₀ M) :
⇑((finsupp.linear_equiv_fun_on_finite R M α).symm) ⇑f = f
noncomputable
def
finsupp.linear_equiv.finsupp_unique
(R : Type u_1)
(M : Type u_9)
[add_comm_monoid M]
[semiring R]
[module R M]
(α : Type u_2)
[unique α] :
If α has a unique term, then the type of finitely supported functions α →₀ M is
R-linearly equivalent to M.
Equations
- finsupp.linear_equiv.finsupp_unique R M α = {to_fun := (finsupp.equiv_fun_on_finite.trans (equiv.fun_unique α M)).to_fun, map_add' := _, map_smul' := _, inv_fun := (finsupp.equiv_fun_on_finite.trans (equiv.fun_unique α M)).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
finsupp.linear_equiv.finsupp_unique_apply
{R : Type u_1}
{M : Type u_9}
[add_comm_monoid M]
[semiring R]
[module R M]
(α : Type u_2)
[unique α]
(f : α →₀ M) :
⇑(finsupp.linear_equiv.finsupp_unique R M α) f = ⇑f inhabited.default
@[simp]
theorem
finsupp.linear_equiv.finsupp_unique_symm_apply
{R : Type u_1}
{M : Type u_9}
[add_comm_monoid M]
[semiring R]
[module R M]
{α : Type u_2}
[unique α]
(m : M) :
⇑((finsupp.linear_equiv.finsupp_unique R M α).symm) m = finsupp.single inhabited.default m
theorem
pi_eq_sum_univ
{ι : Type u_1}
[fintype ι]
[decidable_eq ι]
{R : Type u_2}
[semiring R]
(x : ι → R) :
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₃]
[add_comm_monoid M₄]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
[module R₄ M₄]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₃₄ : R₃ →+* R₄}
{σ₁₃ : R →+* R₃}
{σ₂₄ : R₂ →+* R₄}
{σ₁₄ : R →+* R₄}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄]
[ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
[ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄]
(f : M →ₛₗ[σ₁₂] M₂)
(g : M₂ →ₛₗ[σ₂₃] M₃)
(h : M₃ →ₛₗ[σ₃₄] M₄) :
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(f : M →ₛₗ[σ₁₂] M₂)
(p : submodule R M) :
The restriction of a linear map f : M → M₂ to a submodule p ⊆ M gives a linear map
p → M₂.
Equations
- f.dom_restrict p = f.comp p.subtype
@[simp]
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(p : submodule R₂ M₂)
(f : M →ₛₗ[σ₁₂] M₂)
(h : ∀ (c : M), ⇑f c ∈ p) :
A linear map f : M₂ → M whose values lie in a submodule p ⊆ M can be restricted to a
linear map M₂ → p.
@[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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(p : submodule R₂ M₂)
(f : M →ₛₗ[σ₁₂] M₂)
{h : ∀ (c : M), ⇑f c ∈ p}
(x : M) :
↑(⇑(linear_map.cod_restrict p f 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₂]
[add_comm_monoid M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M →ₛₗ[σ₁₂] M₂)
(g : M₂ →ₛₗ[σ₂₃] M₃)
(p : submodule R₃ M₃)
(h : ∀ (b : M₂), ⇑g b ∈ p) :
(linear_map.cod_restrict p g h).comp f = linear_map.cod_restrict p (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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(f : M →ₛₗ[σ₁₂] M₂)
(p : submodule R₂ M₂)
(h : ∀ (b : M), ⇑f b ∈ p) :
p.subtype.comp (linear_map.cod_restrict p f h) = f
def
linear_map.restrict
{R : Type u_1}
{M : Type u_9}
{M₁ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₁]
[module R M]
[module R M₁]
(f : M →ₗ[R] M₁)
{p : submodule R M}
{q : submodule R M₁}
(hf : ∀ (x : M), x ∈ p → ⇑f x ∈ q) :
Restrict domain and codomain of a linear map.
Equations
- f.restrict hf = linear_map.cod_restrict q (f.dom_restrict p) _
@[simp]
theorem
linear_map.subtype_comp_restrict
{R : Type u_1}
{M : Type u_9}
{M₁ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₁]
[module R M]
[module R M₁]
{f : M →ₗ[R] M₁}
{p : submodule R M}
{q : submodule R M₁}
(hf : ∀ (x : M), x ∈ p → ⇑f x ∈ q) :
q.subtype.comp (f.restrict hf) = f.dom_restrict p
theorem
linear_map.restrict_eq_cod_restrict_dom_restrict
{R : Type u_1}
{M : Type u_9}
{M₁ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₁]
[module R M]
[module R M₁]
{f : M →ₗ[R] M₁}
{p : submodule R M}
{q : submodule R M₁}
(hf : ∀ (x : M), x ∈ p → ⇑f x ∈ q) :
f.restrict hf = linear_map.cod_restrict q (f.dom_restrict p) _
theorem
linear_map.restrict_eq_dom_restrict_cod_restrict
{R : Type u_1}
{M : Type u_9}
{M₁ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₁]
[module R M]
[module R M₁]
{f : M →ₗ[R] M₁}
{p : submodule R M}
{q : submodule R M₁}
(hf : ∀ (x : M), ⇑f x ∈ q) :
f.restrict _ = (linear_map.cod_restrict q f hf).dom_restrict 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[subsingleton 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[subsingleton M₂] :
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(a : M) :
Evaluation of a σ₁₂-linear map at a fixed a, as an add_monoid_hom.
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂} :
linear_map.to_add_monoid_hom promoted to an add_monoid_hom
Equations
- linear_map.to_add_monoid_hom' = {to_fun := linear_map.to_add_monoid_hom σ₁₂, map_zero' := _, map_add' := _}
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]
[add_comm_monoid M₁]
[module R M]
[module R M₁]
[semiring S]
[module R S]
[module S M]
[is_scalar_tower R S M]
(f : M₁ →ₗ[R] S)
(x : M) :
When f is an R-linear map taking values in S, then λb, f b • x is an R-linear map.
@[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]
[add_comm_monoid M₁]
[module R M]
[module R M₁]
[semiring S]
[module R S]
[module S M]
[is_scalar_tower R S 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]
[add_comm_monoid M₁]
[module R M]
[module R M₁]
[semiring S]
[module R S]
[module S M]
[is_scalar_tower R S 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]
[add_comm_monoid M]
[module R M]
[nontrivial M] :
nontrivial (module.End R M)
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{f : M →ₛₗ[σ₁₂] M₂}
{g : module.End R M}
{g₂ : module.End R₂ M₂}
(h : linear_map.comp g₂ 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]
[add_comm_monoid M]
[module R M]
{N : submodule R M}
{g : module.End R ↥N}
{G : module.End R M}
(h : linear_map.comp G N.subtype = N.subtype.comp g)
{k : ℕ}
(hG : G ^ k = 0) :
@[simp]
theorem
linear_map.id_pow
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(n : ℕ) :
theorem
linear_map.iterate_surjective
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
{f' : M →ₗ[R] M}
(h : function.surjective ⇑f')
(n : ℕ) :
function.surjective ⇑(f' ^ n)
theorem
linear_map.iterate_injective
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
{f' : M →ₗ[R] M}
(h : function.injective ⇑f')
(n : ℕ) :
function.injective ⇑(f' ^ n)
theorem
linear_map.iterate_bijective
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
{f' : M →ₗ[R] M}
(h : function.bijective ⇑f')
(n : ℕ) :
function.bijective ⇑(f' ^ n)
theorem
linear_map.injective_of_iterate_injective
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module 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]
[add_comm_monoid M]
[module R M]
{f' : M →ₗ[R] M}
{n : ℕ}
(hn : n ≠ 0)
(h : function.surjective ⇑(f' ^ n)) :
theorem
linear_map.pi_apply_eq_sum_univ
{R : Type u_1}
{M : Type u_9}
{ι : Type u_17}
[semiring R]
[add_comm_monoid M]
[module R M]
[fintype ι]
[decidable_eq ι]
(f : (ι → R) →ₗ[R] M)
(x : ι → R) :
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]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
[module S M₂]
[smul_comm_class R S M₂]
(v : M)
(f : M →ₗ[R] M₂) :
⇑(⇑(linear_map.applyₗ' S) 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]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
[module S M₂]
[smul_comm_class R 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.
@[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]
[add_comm_monoid M]
[module R M]
[module S M]
[smul_comm_class R S M]
(f : R →ₗ[R] M) :
⇑(linear_map.ring_lmap_equiv_self R S 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]
[add_comm_monoid M]
[module R M]
[module S M]
[smul_comm_class R S M]
(x : M) :
⇑((linear_map.ring_lmap_equiv_self R S 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]
[add_comm_monoid M]
[module R M]
[module S M]
[smul_comm_class R 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].
def
linear_map.comp_right
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
{M₃ : Type u_13}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M₂ →ₗ[R] M₃) :
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₃.
@[simp]
theorem
linear_map.comp_right_apply
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
{M₃ : Type u_13}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M₂ →ₗ[R] M₃)
(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}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(v : M)
(f : M →ₗ[R] M₂) :
⇑(⇑linear_map.applyₗ v) f = ⇑f v
def
linear_map.applyₗ
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module 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.
def
linear_map.dom_restrict'
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(p : submodule R M) :
Alternative version of dom_restrict as a linear map.
Equations
- linear_map.dom_restrict' p = {to_fun := λ (φ : M →ₗ[R] M₂), φ.dom_restrict p, map_add' := _, map_smul' := _}
@[simp]
theorem
linear_map.dom_restrict'_apply
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →ₗ[R] M₂)
(p : submodule R M)
(x : ↥p) :
def
linear_map.smul_rightₗ
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
The family of linear maps M₂ → M parameterised by f ∈ M₂ → R, x ∈ M, is linear in f, x.
@[simp]
theorem
linear_map.smul_rightₗ_apply
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M₂ →ₗ[R] R)
(x : M)
(c : M₂) :
@[simp]
theorem
add_monoid_hom_lequiv_nat_apply
{A : Type u_1}
{B : Type u_2}
(R : Type u_3)
[semiring R]
[add_comm_monoid A]
[add_comm_monoid B]
[module 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]
[add_comm_monoid A]
[add_comm_monoid B]
[module R B]
(f : A →ₗ[ℕ] B) :
⇑((add_monoid_hom_lequiv_nat R).symm) f = f.to_add_monoid_hom
def
add_monoid_hom_lequiv_nat
{A : Type u_1}
{B : Type u_2}
(R : Type u_3)
[semiring R]
[add_comm_monoid A]
[add_comm_monoid B]
[module R B] :
The R-linear equivalence between additive morphisms A →+ B and ℕ-linear morphisms A →ₗ[ℕ] B.
Equations
- add_monoid_hom_lequiv_nat R = {to_fun := add_monoid_hom.to_nat_linear_map _inst_3, map_add' := _, map_smul' := _, inv_fun := linear_map.to_add_monoid_hom (ring_hom.id ℕ), left_inv := _, right_inv := _}
@[simp]
theorem
add_monoid_hom_lequiv_int_symm_apply
{A : Type u_1}
{B : Type u_2}
(R : Type u_3)
[semiring R]
[add_comm_group A]
[add_comm_group B]
[module R B]
(f : A →ₗ[ℤ] B) :
⇑((add_monoid_hom_lequiv_int R).symm) f = f.to_add_monoid_hom
def
add_monoid_hom_lequiv_int
{A : Type u_1}
{B : Type u_2}
(R : Type u_3)
[semiring R]
[add_comm_group A]
[add_comm_group B]
[module R B] :
The R-linear equivalence between additive morphisms A →+ B and ℤ-linear morphisms A →ₗ[ℤ] B.
Equations
- add_monoid_hom_lequiv_int R = {to_fun := add_monoid_hom.to_int_linear_map _inst_3, map_add' := _, map_smul' := _, inv_fun := linear_map.to_add_monoid_hom (ring_hom.id ℤ), left_inv := _, right_inv := _}
@[simp]
theorem
add_monoid_hom_lequiv_int_apply
{A : Type u_1}
{B : Type u_2}
(R : Type u_3)
[semiring R]
[add_comm_group A]
[add_comm_group B]
[module R B]
(f : A →+ B) :
Properties of submodules #
def
submodule.of_le
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
{p p' : submodule R 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
- submodule.of_le h = linear_map.cod_restrict p' p.subtype _
@[simp]
theorem
submodule.coe_of_le
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
{p p' : submodule R M}
(h : p ≤ p')
(x : ↥p) :
↑(⇑(submodule.of_le h) x) = ↑x
theorem
submodule.of_le_apply
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
{p p' : submodule R M}
(h : p ≤ p')
(x : ↥p) :
⇑(submodule.of_le h) x = ⟨↑x, _⟩
theorem
submodule.of_le_injective
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
{p p' : submodule R M}
(h : p ≤ p') :
theorem
submodule.subtype_comp_of_le
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(p q : submodule R M)
(h : p ≤ q) :
q.subtype.comp (submodule.of_le h) = p.subtype
@[simp]
theorem
submodule.subsingleton_iff
(R : Type u_1)
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
subsingleton (submodule R M) ↔ subsingleton M
@[simp]
theorem
submodule.nontrivial_iff
(R : Type u_1)
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
nontrivial (submodule R M) ↔ nontrivial M
@[protected, instance]
def
submodule.unique
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
[subsingleton M] :
Equations
- submodule.unique = {to_inhabited := {default := ⊥}, uniq := _}
@[protected, instance]
def
submodule.unique'
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
[subsingleton R] :
Equations
@[protected, instance]
def
submodule.nontrivial
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
[nontrivial M] :
nontrivial (submodule R M)
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[ring_hom_surjective σ₁₂]
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
(f : F)
(p : submodule R M) :
submodule R₂ M₂
The pushforward of a submodule p ⊆ M by f : M → M₂
@[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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[ring_hom_surjective σ₁₂]
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
(f : F)
(p : submodule R 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[ring_hom_surjective σ₁₂]
(f : M →ₛₗ[σ₁₂] M₂)
(p : submodule R 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[ring_hom_surjective σ₁₂]
(f : M →ₛₗ[σ₁₂] M₂)
(p : submodule R 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[ring_hom_surjective σ₁₂]
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
{f : F}
{p : submodule R M}
{x : M₂} :
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[ring_hom_surjective σ₁₂]
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
{f : F}
{p : submodule R M}
{r : M}
(h : r ∈ p) :
⇑f r ∈ submodule.map f p
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[ring_hom_surjective σ₁₂]
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
(f : F)
{p : submodule R M}
(r : ↥p) :
⇑f ↑r ∈ submodule.map f p
@[simp]
theorem
submodule.map_id
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(p : submodule R 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₂]
[add_comm_monoid M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_surjective σ₁₂]
[ring_hom_surjective σ₂₃]
[ring_hom_surjective σ₁₃]
(f : M →ₛₗ[σ₁₂] M₂)
(g : M₂ →ₛₗ[σ₂₃] M₃)
(p : submodule R M) :
submodule.map (g.comp f) p = submodule.map g (submodule.map f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[ring_hom_surjective σ₁₂]
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
{f : F}
{p p' : submodule R M} :
p ≤ p' → submodule.map f p ≤ submodule.map f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(p : submodule R M)
[ring_hom_surjective σ₁₂] :
submodule.map 0 p = ⊥
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(p : submodule R M)
[ring_hom_surjective σ₁₂]
(f g : M →ₛₗ[σ₁₂] M₂) :
submodule.map (f + g) p ≤ submodule.map f p ⊔ submodule.map g p
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[ring_hom_surjective σ₁₂]
(N : submodule R M) :
(set.range (λ (ϕ : M →ₛₗ[σ₁₂] M₂), submodule.map ϕ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
(f : F)
(i : function.injective ⇑f)
(p : submodule R M) :
↥p ≃ₛₗ[σ₁₂] ↥(submodule.map f 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.
@[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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
(f : F)
(i : function.injective ⇑f)
(p : submodule R M)
(x : ↥p) :
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
(f : F)
(p : submodule R₂ M₂) :
submodule R M
The pullback of a submodule p ⊆ M₂ along f : M → M₂
@[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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
(f : F)
(p : submodule R₂ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{x : M}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
{f : F}
{p : submodule R₂ M₂} :
x ∈ submodule.comap f p ↔ ⇑f x ∈ p
@[simp]
theorem
submodule.comap_id
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(p : submodule R 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₂]
[add_comm_monoid M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M →ₛₗ[σ₁₂] M₂)
(g : M₂ →ₛₗ[σ₂₃] M₃)
(p : submodule R₃ M₃) :
submodule.comap (g.comp f) p = submodule.comap f (submodule.comap g p)
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
{f : F}
{q q' : submodule R₂ M₂} :
q ≤ q' → submodule.comap f q ≤ submodule.comap f q'
theorem
submodule.le_comap_pow_of_le_comap
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(p : submodule R M)
{f : M →ₗ[R] M}
(h : p ≤ submodule.comap f p)
(k : ℕ) :
p ≤ submodule.comap (f ^ k) p
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
{f : F}
{p : submodule R M}
{q : submodule R₂ M₂} :
submodule.map f p ≤ q ↔ p ≤ submodule.comap f q
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
(f : F) :
submodule.map 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(p p' : submodule R M)
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
(f : F) :
submodule.map f (p ⊔ p') = submodule.map f p ⊔ submodule.map f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
{ι : Sort u_2}
(f : F)
(p : ι → submodule R M) :
submodule.map f (⨆ (i : ι), p i) = ⨆ (i : ι), submodule.map f (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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
(f : F) :
submodule.comap 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(q q' : submodule R₂ M₂)
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
(f : F) :
submodule.comap f (q ⊓ q') = submodule.comap f q ⊓ submodule.comap f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
{ι : Sort u_2}
(f : F)
(p : ι → submodule R₂ M₂) :
submodule.comap f (⨅ (i : ι), p i) = ⨅ (i : ι), submodule.comap f (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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(q : submodule R₂ M₂) :
submodule.comap 0 q = ⊤
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
(f : F)
(q : submodule R₂ M₂) :
submodule.map f (submodule.comap f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
(f : F)
(p : submodule R M) :
p ≤ submodule.comap f (submodule.map f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
{f : F}
(hf : function.surjective ⇑f)
[ring_hom_surjective σ₁₂]
(p : submodule R₂ M₂) :
submodule.map f (submodule.comap f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
{f : F}
(hf : function.surjective ⇑f)
[ring_hom_surjective σ₁₂]
(p q : submodule R₂ M₂) :
submodule.map f (submodule.comap f p ⊔ submodule.comap f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
{f : F}
(hf : function.surjective ⇑f)
[ring_hom_surjective σ₁₂]
{ι : Sort u_2}
(S : ι → submodule R₂ M₂) :
submodule.map f (⨆ (i : ι), submodule.comap f (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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
{f : F}
(hf : function.surjective ⇑f)
[ring_hom_surjective σ₁₂]
(p q : submodule R₂ M₂) :
submodule.map f (submodule.comap f p ⊓ submodule.comap f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
{f : F}
(hf : function.surjective ⇑f)
[ring_hom_surjective σ₁₂]
{ι : Sort u_2}
(S : ι → submodule R₂ M₂) :
submodule.map f (⨅ (i : ι), submodule.comap f (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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
{f : F}
(hf : function.surjective ⇑f)
[ring_hom_surjective σ₁₂]
(p q : submodule R₂ M₂) :
submodule.comap f p ≤ submodule.comap f q ↔ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
{f : F}
(hf : function.injective ⇑f)
(p : submodule R M) :
submodule.comap f (submodule.map f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
{f : F}
(hf : function.injective ⇑f)
(p q : submodule R M) :
submodule.comap f (submodule.map f p ⊓ submodule.map f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
{f : F}
(hf : function.injective ⇑f)
{ι : Sort u_2}
(S : ι → submodule R M) :
submodule.comap f (⨅ (i : ι), submodule.map f (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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
{f : F}
(hf : function.injective ⇑f)
(p q : submodule R M) :
submodule.comap f (submodule.map f p ⊔ submodule.map f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
{f : F}
(hf : function.injective ⇑f)
{ι : Sort u_2}
(S : ι → submodule R M) :
submodule.comap f (⨆ (i : ι), submodule.map f (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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
{f : F}
(hf : function.injective ⇑f)
(p q : submodule R M) :
submodule.map f p ≤ submodule.map f q ↔ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
{f : F}
(hf : function.injective ⇑f) :
@[simp]
theorem
submodule.order_iso_map_comap_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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{F : Type u_20}
[semilinear_equiv_class F σ₁₂ M M₂]
(f : F)
(p : submodule R₂ M₂) :
⇑(rel_iso.symm (submodule.order_iso_map_comap f)) p = submodule.comap f p
def
submodule.order_iso_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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{F : Type u_20}
[semilinear_equiv_class F σ₁₂ M M₂]
(f : F) :
A linear isomorphism induces an order isomorphism of submodules.
Equations
- submodule.order_iso_map_comap f = {to_equiv := {to_fun := submodule.map f, inv_fun := submodule.comap f, left_inv := _, right_inv := _}, map_rel_iff' := _}
@[simp]
theorem
submodule.order_iso_map_comap_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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{F : Type u_20}
[semilinear_equiv_class F σ₁₂ M M₂]
(f : F)
(p : submodule R M) :
⇑(submodule.order_iso_map_comap f) p = submodule.map f p
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F σ₁₂ M M₂]
[ring_hom_surjective σ₁₂]
{f : F}
{p : submodule R M}
{p' : submodule R₂ M₂} :
submodule.map f p ⊓ p' = submodule.map f (p ⊓ submodule.comap f p')
theorem
submodule.map_comap_subtype
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(p p' : submodule R M) :
submodule.map p.subtype (submodule.comap p.subtype p') = p ⊓ p'
theorem
submodule.eq_zero_of_bot_submodule
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(b : ↥⊥) :
b = 0
theorem
linear_map.infi_invariant
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
{σ : R →+* R}
[ring_hom_surjective σ]
{ι : Sort u_2}
(f : M →ₛₗ[σ] M)
{p : ι → submodule R M}
(hf : ∀ (i : ι) (v : M), v ∈ p i → ⇑f v ∈ p i)
(v : M)
(H : v ∈ infi p) :
The infimum of a family of invariant submodule of an endomorphism is also an invariant submodule.
@[protected, simp]
theorem
submodule.map_neg
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
[add_comm_group M₂]
[module R M₂]
(f : M →ₗ[R] M₂) :
submodule.map (-f) p = submodule.map f p
theorem
submodule.comap_smul
{K : Type u_7}
{V : Type u_18}
{V₂ : Type u_19}
[field K]
[add_comm_group V]
[module K V]
[add_comm_group V₂]
[module K V₂]
(f : V →ₗ[K] V₂)
(p : submodule K V₂)
(a : K)
(h : a ≠ 0) :
submodule.comap (a • f) p = submodule.comap f p
theorem
submodule.map_smul
{K : Type u_7}
{V : Type u_18}
{V₂ : Type u_19}
[field K]
[add_comm_group V]
[module K V]
[add_comm_group V₂]
[module K V₂]
(f : V →ₗ[K] V₂)
(p : submodule K V)
(a : K)
(h : a ≠ 0) :
submodule.map (a • f) p = submodule.map f p
theorem
submodule.comap_smul'
{K : Type u_7}
{V : Type u_18}
{V₂ : Type u_19}
[field K]
[add_comm_group V]
[module K V]
[add_comm_group V₂]
[module K V₂]
(f : V →ₗ[K] V₂)
(p : submodule K V₂)
(a : K) :
submodule.comap (a • f) p = ⨅ (h : a ≠ 0), submodule.comap f p
theorem
submodule.map_smul'
{K : Type u_7}
{V : Type u_18}
{V₂ : Type u_19}
[field K]
[add_comm_group V]
[module K V]
[add_comm_group V₂]
[module K V₂]
(f : V →ₗ[K] V₂)
(p : submodule K V)
(a : K) :
submodule.map (a • f) p = ⨆ (h : a ≠ 0), submodule.map f p
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]
[add_comm_monoid M₂]
{σ₁₂ : R →+* R₂}
[module R M]
[module R₂ M₂]
{γ : Type u_20}
[has_zero γ]
(f : M →ₛₗ[σ₁₂] M₂)
{t : ι →₀ γ}
{g : ι → γ → M} :
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]
[add_comm_monoid M₂]
{σ₁₂ : R →+* R₂}
[module R M]
[module R₂ M₂]
{γ : Type u_20}
[has_zero γ]
(t : ι →₀ γ)
(g : ι → γ → (M →ₛₗ[σ₁₂] M₂)) :
@[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]
[add_comm_monoid M₂]
{σ₁₂ : R →+* R₂}
[module R M]
[module R₂ M₂]
{γ : Type u_20}
[has_zero γ]
(t : ι →₀ γ)
(g : ι → γ → (M →ₛₗ[σ₁₂] M₂))
(b : M) :
@[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]
[add_comm_monoid M₂]
{σ₁₂ : R →+* R₂}
[module 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} :
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]
[add_comm_monoid M₂]
{σ₁₂ : R →+* R₂}
[module 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₂)) :
@[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]
[add_comm_monoid M₂]
{σ₁₂ : R →+* R₂}
[module 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) :
@[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]
[add_comm_monoid M₂]
{σ₁₂ : R →+* R₂}
[module 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 (⇑(dfinsupp.sum_add_hom g) 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₂₁ : R₂ →+* R}
[ring_hom_surjective σ₂₁]
(p : submodule R M)
(f : M₂ →ₛₗ[σ₂₁] M)
(h : ∀ (c : M₂), ⇑f c ∈ p)
(p' : submodule R₂ M₂) :
submodule.map (linear_map.cod_restrict p f h) p' = submodule.comap p.subtype (submodule.map f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₂₁ : R₂ →+* R}
(p : submodule R M)
(f : M₂ →ₛₗ[σ₂₁] M)
(hf : ∀ (c : M₂), ⇑f c ∈ p)
(p' : submodule R ↥p) :
submodule.comap (linear_map.cod_restrict p f hf) p' = submodule.comap f (submodule.map p.subtype 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
[ring_hom_surjective τ₁₂]
(f : F) :
submodule R₂ M₂
The range of a linear map f : M → M₂ is a submodule of M₂.
See Note [range copy pattern].
Equations
- linear_map.range f = (submodule.map f ⊤).copy (set.range ⇑f) _
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
[ring_hom_surjective τ₁₂]
(f : F) :
↑(linear_map.range f) = set.range ⇑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]
[add_comm_monoid M₂]
[module R 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
[ring_hom_surjective τ₁₂]
{f : F}
{x : M₂} :
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
[ring_hom_surjective τ₁₂]
(f : F)
(x : M) :
⇑f x ∈ linear_map.range f
@[simp]
theorem
linear_map.range_id
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module 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₂]
[add_comm_monoid M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{τ₁₂ : R →+* R₂}
{τ₂₃ : R₂ →+* R₃}
{τ₁₃ : R →+* R₃}
[ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃]
[ring_hom_surjective τ₁₂]
[ring_hom_surjective τ₂₃]
[ring_hom_surjective τ₁₃]
(f : M →ₛₗ[τ₁₂] M₂)
(g : M₂ →ₛₗ[τ₂₃] M₃) :
linear_map.range (g.comp f) = submodule.map g (linear_map.range f)
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₂]
[add_comm_monoid M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{τ₁₂ : R →+* R₂}
{τ₂₃ : R₂ →+* R₃}
{τ₁₃ : R →+* R₃}
[ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃]
[ring_hom_surjective τ₂₃]
[ring_hom_surjective τ₁₃]
(f : M →ₛₗ[τ₁₂] M₂)
(g : M₂ →ₛₗ[τ₂₃] M₃) :
linear_map.range (g.comp f) ≤ linear_map.range g
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
[ring_hom_surjective τ₁₂]
{f : F}
{p : submodule R₂ M₂} :
linear_map.range f ≤ p ↔ submodule.comap f p = ⊤
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
[ring_hom_surjective τ₁₂]
{f : F}
{p : submodule R M} :
submodule.map f p ≤ linear_map.range f
@[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_monoid M]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂) :
def
linear_map.eq_locus
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(f g : M →ₛₗ[τ₁₂] M₂) :
submodule R M
A linear map version of add_monoid_hom.eq_locus
theorem
linear_map.eq_locus_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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(f g : M →ₛₗ[τ₁₂] M₂) :
@[simp]
theorem
linear_map.iterate_range_coe
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(f : M →ₗ[R] M)
(n : ℕ) :
⇑(f.iterate_range) n = linear_map.range (f ^ n)
def
linear_map.iterate_range
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(f : M →ₗ[R] M) :
The decreasing sequence of submodules consisting of the ranges of the iterates of a linear map.
Equations
- f.iterate_range = {to_fun := λ (n : ℕ), linear_map.range (f ^ n), monotone' := _}
@[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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂) :
M →ₛₗ[τ₁₂] ↥(linear_map.range f)
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]
[add_comm_monoid M₂]
[module R 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
(f : F) :
submodule R 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
Instances for ↥linear_map.ker
@[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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
{f : F}
{y : M} :
y ∈ linear_map.ker f ↔ ⇑f y = 0
@[simp]
theorem
linear_map.ker_id
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
(f : F)
(x : ↥(linear_map.ker f)) :
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]
[add_comm_monoid M₂]
[module R 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(f : M →ₛₗ[τ₁₂] M₂) :
f.comp (linear_map.ker f).subtype = 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₂]
[add_comm_monoid M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{τ₁₂ : R →+* R₂}
{τ₂₃ : R₂ →+* R₃}
{τ₁₃ : R →+* R₃}
[ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃]
(f : M →ₛₗ[τ₁₂] M₂)
(g : M₂ →ₛₗ[τ₂₃] M₃) :
linear_map.ker (g.comp f) = submodule.comap f (linear_map.ker g)
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₂]
[add_comm_monoid M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{τ₁₂ : R →+* R₂}
{τ₂₃ : R₂ →+* R₃}
{τ₁₃ : R →+* R₃}
[ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃]
(f : M →ₛₗ[τ₁₂] M₂)
(g : M₂ →ₛₗ[τ₂₃] M₃) :
linear_map.ker f ≤ linear_map.ker (g.comp f)
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
{f : F}
{p : submodule R M} :
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
{f : F} :
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{τ₂₁ : R₂ →+* R}
[ring_hom_inv_pair τ₁₂ τ₂₁]
{f : M →ₛₗ[τ₁₂] M₂}
{g : M₂ →ₛₗ[τ₂₁] M}
(h : g.comp f = linear_map.id) :
linear_map.ker f = ⊥
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
[ring_hom_surjective τ₁₂]
{f : F}
{p : submodule R M} :
p ≤ linear_map.ker f ↔ submodule.map f p = ⊥
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₂₁ : R₂ →+* R}
(p : submodule R M)
(f : M₂ →ₛₗ[τ₂₁] M)
(hf : ∀ (c : M₂), ⇑f c ∈ p) :
linear_map.ker (linear_map.cod_restrict p f hf) = linear_map.ker f
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₂₁ : R₂ →+* R}
[ring_hom_surjective τ₂₁]
(p : submodule R M)
(f : M₂ →ₛₗ[τ₂₁] M)
(hf : ∀ (c : M₂), ⇑f c ∈ p) :
linear_map.range (linear_map.cod_restrict p f hf) = submodule.comap p.subtype (linear_map.range f)
theorem
linear_map.ker_restrict
{R : Type u_1}
{M : Type u_9}
{M₁ : Type u_11}
[semiring R]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₁]
[module R M₁]
{p : submodule R M}
{q : submodule R M₁}
{f : M →ₗ[R] M₁}
(hf : ∀ (x : M), x ∈ p → ⇑f x ∈ q) :
linear_map.ker (f.restrict hf) = linear_map.ker (f.dom_restrict 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
[ring_hom_surjective τ₁₂]
(f : F)
(q : submodule R₂ M₂) :
submodule.map f (submodule.comap f q) = linear_map.range f ⊓ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
[ring_hom_surjective τ₁₂]
{f : F}
{q : submodule R₂ M₂}
(h : q ≤ linear_map.range f) :
submodule.map f (submodule.comap f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂} :
linear_map.ker 0 = ⊤
@[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]
[add_comm_monoid M₂]
[module R 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{f : M →ₛₗ[τ₁₂] M₂} :
linear_map.ker f = ⊤ ↔ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂) :
linear_map.range f ≤ ⊥ ↔ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
{f : M →ₛₗ[τ₁₂] M₂} :
linear_map.range f = ⊥ ↔ 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₂]
[add_comm_monoid M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{τ₁₂ : R →+* R₂}
{τ₂₃ : R₂ →+* R₃}
{τ₁₃ : R →+* R₃}
[ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃]
[ring_hom_surjective τ₁₂]
{f : M →ₛₗ[τ₁₂] M₂}
{g : M₂ →ₛₗ[τ₂₃] M₃} :
linear_map.range f ≤ linear_map.ker g ↔ 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
[ring_hom_surjective τ₁₂]
{f : F}
(hf : linear_map.range f = ⊤)
{p p' : submodule R₂ M₂} :
submodule.comap f p ≤ submodule.comap f 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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
[ring_hom_surjective τ₁₂]
{f : F}
(hf : linear_map.range f = ⊤) :
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]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
{f : F}
(hf : function.injective ⇑f) :
linear_map.ker f = ⊥
@[simp]
theorem
linear_map.iterate_ker_coe
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(f : M →ₗ[R] M)
(n : ℕ) :
⇑(f.iterate_ker) n = linear_map.ker (f ^ n)
def
linear_map.iterate_ker
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(f : M →ₗ[R] M) :
The increasing sequence of submodules consisting of the kernels of the iterates of a linear map.
Equations
- f.iterate_ker = {to_fun := λ (n : ℕ), linear_map.ker (f ^ n), monotone' := _}
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]
[add_comm_group M₂]
[module R 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]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(f : M →ₛₗ[τ₁₂] M₂) :
theorem
linear_map.eq_locus_eq_ker_sub
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[ring R]
[ring R₂]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(f g : M →ₛₗ[τ₁₂] M₂) :
f.eq_locus g = linear_map.ker (f - g)
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]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
{f : F}
{x y : M} :
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]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
{f : F}
{p : submodule R M} :
theorem
linear_map.inj_on_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]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[sc : semilinear_map_class F τ₁₂ M M₂]
{f : F}
{p : submodule R M}
{s : set M}
(h : s ⊆ ↑p)
(hd : disjoint p (linear_map.ker f)) :
set.inj_on ⇑f s
theorem
linear_map_class.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]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(F : Type u_20)
[sc : semilinear_map_class F τ₁₂ M M₂]
{f : F} :
linear_map.ker f = ⊥ ↔</