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 LinearMap, are found in
Algebra/Module.
Main definitions #
- Many constructors for (semi)linear maps
See LinearAlgebra.Span for the span of a set (as a submodule),
and LinearAlgebra.Quotient for quotients by submodules.
Main theorems #
See LinearAlgebra.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 (LinearMap.prod, LinearMap.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
Properties of linear maps #
@[simp]
theorem
addMonoidHomLequivNat_apply
{A : Type u_20}
{B : Type u_21}
(R : Type u_22)
[Semiring R]
[AddCommMonoid A]
[AddCommMonoid B]
[Module R B]
(f : A →+ B)
:
@[simp]
theorem
addMonoidHomLequivNat_symm_apply
{A : Type u_20}
{B : Type u_21}
(R : Type u_22)
[Semiring R]
[AddCommMonoid A]
[AddCommMonoid B]
[Module R B]
(f : A →ₗ[ℕ] B)
:
def
addMonoidHomLequivNat
{A : Type u_20}
{B : Type u_21}
(R : Type u_22)
[Semiring R]
[AddCommMonoid A]
[AddCommMonoid B]
[Module R B]
:
The R-linear equivalence between additive morphisms A →+ B and ℕ-linear morphisms A →ₗ[ℕ] B.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
addMonoidHomLequivInt_symm_apply
{A : Type u_20}
{B : Type u_21}
(R : Type u_22)
[Semiring R]
[AddCommGroup A]
[AddCommGroup B]
[Module R B]
(f : A →ₗ[ℤ] B)
:
@[simp]
theorem
addMonoidHomLequivInt_apply
{A : Type u_20}
{B : Type u_21}
(R : Type u_22)
[Semiring R]
[AddCommGroup A]
[AddCommGroup B]
[Module R B]
(f : A →+ B)
:
def
addMonoidHomLequivInt
{A : Type u_20}
{B : Type u_21}
(R : Type u_22)
[Semiring R]
[AddCommGroup A]
[AddCommGroup B]
[Module R B]
:
The R-linear equivalence between additive morphisms A →+ B and ℤ-linear morphisms A →ₗ[ℤ] B.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
addMonoidEndRingEquivInt_apply
(A : Type u_20)
[AddCommGroup A]
:
∀ (a : A →+ A), (addMonoidEndRingEquivInt A) a = (addMonoidHomLequivInt ℤ).toFun a
@[simp]
theorem
addMonoidEndRingEquivInt_symm_apply
(A : Type u_20)
[AddCommGroup A]
:
∀ (a : A →ₗ[ℤ] A), (RingEquiv.symm (addMonoidEndRingEquivInt A)) a = (addMonoidHomLequivInt ℤ).invFun a
Ring equivalence between additive group endomorphisms of an AddCommGroup A and
ℤ-module endomorphisms of A.
Equations
- addMonoidEndRingEquivInt A = let __src := addMonoidHomLequivInt ℤ; { toEquiv := { toFun := __src.toFun, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯, map_add' := ⋯ }
Instances For
Properties of linear maps #
def
LinearMap.eqLocus
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
(f : F)
(g : F)
:
Submodule R M
A linear map version of AddMonoidHom.eqLocusM
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LinearMap.mem_eqLocus
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{x : M}
{f : F}
{g : F}
:
x ∈ LinearMap.eqLocus f g ↔ f x = g x
theorem
LinearMap.eqLocus_toAddSubmonoid
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
(f : F)
(g : F)
:
(LinearMap.eqLocus f g).toAddSubmonoid = AddMonoidHom.eqLocusM ↑f ↑g
@[simp]
theorem
LinearMap.eqLocus_eq_top
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
{g : F}
:
LinearMap.eqLocus f g = ⊤ ↔ f = g
@[simp]
theorem
LinearMap.eqLocus_same
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
(f : F)
:
LinearMap.eqLocus f f = ⊤
theorem
LinearMap.le_eqLocus
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
{g : F}
{S : Submodule R M}
:
S ≤ LinearMap.eqLocus f g ↔ Set.EqOn ⇑f ⇑g ↑S
theorem
LinearMap.eqOn_sup
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
{g : F}
{S : Submodule R M}
{T : Submodule R M}
(hS : Set.EqOn ⇑f ⇑g ↑S)
(hT : Set.EqOn ⇑f ⇑g ↑T)
:
theorem
LinearMap.ext_on_codisjoint
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_20}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
{g : F}
{S : Submodule R M}
{T : Submodule R M}
(hST : Codisjoint S T)
(hS : Set.EqOn ⇑f ⇑g ↑S)
(hT : Set.EqOn ⇑f ⇑g ↑T)
:
f = g
theorem
LinearMap.eqLocus_eq_ker_sub
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Ring R]
[Ring R₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
(f : M →ₛₗ[τ₁₂] M₂)
(g : M →ₛₗ[τ₁₂] M₂)
:
LinearMap.eqLocus f g = LinearMap.ker (f - g)
theorem
IsLinearMap.isLinearMap_add
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
IsLinearMap R fun (x : M × M) => x.1 + x.2
theorem
IsLinearMap.isLinearMap_sub
{R : Type u_20}
{M : Type u_21}
[Semiring R]
[AddCommGroup M]
[Module R M]
:
IsLinearMap R fun (x : M × M) => x.1 - x.2
Linear equivalences #
instance
LinearEquiv.instZeroLinearEquiv
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[Subsingleton M]
[Subsingleton M₂]
:
Between two zero modules, the zero map is an equivalence.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LinearEquiv.zero_symm
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[Subsingleton M]
[Subsingleton M₂]
:
LinearEquiv.symm 0 = 0
@[simp]
theorem
LinearEquiv.coe_zero
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[Subsingleton M]
[Subsingleton M₂]
:
⇑0 = 0
theorem
LinearEquiv.zero_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[Subsingleton M]
[Subsingleton M₂]
(x : M)
:
0 x = 0
instance
LinearEquiv.instUniqueLinearEquiv
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[Subsingleton M]
[Subsingleton M₂]
:
Between two zero modules, the zero map is the only equivalence.
Equations
- LinearEquiv.instUniqueLinearEquiv = { toInhabited := { default := 0 }, uniq := ⋯ }
instance
LinearEquiv.uniqueOfSubsingleton
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[Subsingleton R]
[Subsingleton R₂]
:
Equations
- LinearEquiv.uniqueOfSubsingleton = inferInstance
@[simp]
theorem
LinearEquiv.coe_curry
(R : Type u_1)
(V : Type u_18)
(V₂ : Type u_19)
[Semiring R]
:
⇑(LinearEquiv.curry R V V₂) = Function.curry
@[simp]
theorem
LinearEquiv.coe_curry_symm
(R : Type u_1)
(V : Type u_18)
(V₂ : Type u_19)
[Semiring R]
:
⇑(LinearEquiv.symm (LinearEquiv.curry R V V₂)) = Function.uncurry
def
LinearEquiv.ofEq
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
(p : Submodule R M)
(q : Submodule R M)
(h : p = q)
:
Linear equivalence between two equal submodules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LinearEquiv.coe_ofEq_apply
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
{p : Submodule R M}
{q : Submodule R M}
(h : p = q)
(x : ↥p)
:
↑((LinearEquiv.ofEq p q h) x) = ↑x
@[simp]
theorem
LinearEquiv.ofEq_symm
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
{p : Submodule R M}
{q : Submodule R M}
(h : p = q)
:
LinearEquiv.symm (LinearEquiv.ofEq p q h) = LinearEquiv.ofEq q p ⋯
@[simp]
theorem
LinearEquiv.ofEq_rfl
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
{p : Submodule R M}
:
LinearEquiv.ofEq p p ⋯ = LinearEquiv.refl R ↥p
def
LinearEquiv.ofSubmodules
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(e : M ≃ₛₗ[σ₁₂] M₂)
(p : Submodule R M)
(q : Submodule R₂ M₂)
(h : Submodule.map (↑e) p = q)
:
A linear equivalence which maps a submodule of one module onto another, restricts to a linear equivalence of the two submodules.
Equations
- LinearEquiv.ofSubmodules e p q h = LinearEquiv.trans (LinearEquiv.submoduleMap e p) (LinearEquiv.ofEq (Submodule.map (↑e) p) q h)
Instances For
@[simp]
theorem
LinearEquiv.ofSubmodules_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(e : M ≃ₛₗ[σ₁₂] M₂)
{p : Submodule R M}
{q : Submodule R₂ M₂}
(h : Submodule.map e p = q)
(x : ↥p)
:
↑((LinearEquiv.ofSubmodules e p q h) x) = e ↑x
@[simp]
theorem
LinearEquiv.ofSubmodules_symm_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(e : M ≃ₛₗ[σ₁₂] M₂)
{p : Submodule R M}
{q : Submodule R₂ M₂}
(h : Submodule.map e p = q)
(x : ↥q)
:
↑((LinearEquiv.symm (LinearEquiv.ofSubmodules e p q h)) x) = (LinearEquiv.symm e) ↑x
def
LinearEquiv.ofSubmodule'
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
[Module R M]
[Module R₂ M₂]
(f : M ≃ₛₗ[σ₁₂] M₂)
(U : Submodule R₂ M₂)
:
↥(Submodule.comap (↑f) U) ≃ₛₗ[σ₁₂] ↥U
A linear equivalence of two modules restricts to a linear equivalence from the preimage of any submodule to that submodule.
This is LinearEquiv.ofSubmodule but with comap on the left instead of map on the right.
Equations
- LinearEquiv.ofSubmodule' f U = LinearEquiv.symm (LinearEquiv.ofSubmodules (LinearEquiv.symm f) U (Submodule.comap (↑(LinearEquiv.symm (LinearEquiv.symm f))) U) ⋯)
Instances For
theorem
LinearEquiv.ofSubmodule'_toLinearMap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
[Module R M]
[Module R₂ M₂]
(f : M ≃ₛₗ[σ₁₂] M₂)
(U : Submodule R₂ M₂)
:
↑(LinearEquiv.ofSubmodule' f U) = LinearMap.codRestrict U (LinearMap.domRestrict (↑f) (Submodule.comap (↑f) U)) ⋯
@[simp]
theorem
LinearEquiv.ofSubmodule'_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
[Module R M]
[Module R₂ M₂]
(f : M ≃ₛₗ[σ₁₂] M₂)
(U : Submodule R₂ M₂)
(x : ↥(Submodule.comap (↑f) U))
:
↑((LinearEquiv.ofSubmodule' f U) x) = f ↑x
@[simp]
theorem
LinearEquiv.ofSubmodule'_symm_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
[Module R M]
[Module R₂ M₂]
(f : M ≃ₛₗ[σ₁₂] M₂)
(U : Submodule R₂ M₂)
(x : ↥U)
:
↑((LinearEquiv.symm (LinearEquiv.ofSubmodule' f U)) x) = (LinearEquiv.symm f) ↑x
def
LinearEquiv.ofTop
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
(p : Submodule R M)
(h : p = ⊤)
:
The top submodule of M is linearly equivalent to M.
Equations
- LinearEquiv.ofTop p h = let __src := Submodule.subtype p; { toLinearMap := __src, invFun := fun (x : M) => { val := x, property := ⋯ }, left_inv := ⋯, right_inv := ⋯ }
Instances For
@[simp]
theorem
LinearEquiv.ofTop_apply
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
(p : Submodule R M)
{h : p = ⊤}
(x : ↥p)
:
(LinearEquiv.ofTop p h) x = ↑x
@[simp]
theorem
LinearEquiv.coe_ofTop_symm_apply
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
(p : Submodule R M)
{h : p = ⊤}
(x : M)
:
↑((LinearEquiv.symm (LinearEquiv.ofTop p h)) x) = x
theorem
LinearEquiv.ofTop_symm_apply
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
(p : Submodule R M)
{h : p = ⊤}
(x : M)
:
(LinearEquiv.symm (LinearEquiv.ofTop p h)) x = { val := x, property := ⋯ }
def
LinearEquiv.ofLinear
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(f : M →ₛₗ[σ₁₂] M₂)
(g : M₂ →ₛₗ[σ₂₁] M)
(h₁ : LinearMap.comp f g = LinearMap.id)
(h₂ : LinearMap.comp g f = LinearMap.id)
:
If a linear map has an inverse, it is a linear equivalence.
Equations
- LinearEquiv.ofLinear f g h₁ h₂ = { toLinearMap := f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }
Instances For
@[simp]
theorem
LinearEquiv.ofLinear_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(f : M →ₛₗ[σ₁₂] M₂)
(g : M₂ →ₛₗ[σ₂₁] M)
{h₁ : LinearMap.comp f g = LinearMap.id}
{h₂ : LinearMap.comp g f = LinearMap.id}
(x : M)
:
(LinearEquiv.ofLinear f g h₁ h₂) x = f x
@[simp]
theorem
LinearEquiv.ofLinear_symm_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(f : M →ₛₗ[σ₁₂] M₂)
(g : M₂ →ₛₗ[σ₂₁] M)
{h₁ : LinearMap.comp f g = LinearMap.id}
{h₂ : LinearMap.comp g f = LinearMap.id}
(x : M₂)
:
(LinearEquiv.symm (LinearEquiv.ofLinear f g h₁ h₂)) x = g x
@[simp]
theorem
LinearEquiv.range
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(e : M ≃ₛₗ[σ₁₂] M₂)
:
LinearMap.range ↑e = ⊤
@[simp]
theorem
LinearEquivClass.range
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
[Module R M]
[Module R₂ M₂]
{F : Type u_20}
[EquivLike F M M₂]
[SemilinearEquivClass F σ₁₂ M M₂]
(e : F)
:
theorem
LinearEquiv.eq_bot_of_equiv
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(p : Submodule R M)
[Module R₂ M₂]
(e : ↥p ≃ₛₗ[σ₁₂] ↥⊥)
:
@[simp]
theorem
LinearEquiv.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₃]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{module_M₃ : Module R₃ M₃}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(e : M ≃ₛₗ[σ₁₂] M₂)
(h : M₂ →ₛₗ[σ₂₃] M₃)
[RingHomSurjective σ₂₃]
[RingHomSurjective σ₁₃]
:
LinearMap.range (LinearMap.comp h ↑e) = LinearMap.range h
def
LinearEquiv.ofLeftInverse
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{f : M →ₛₗ[σ₁₂] M₂}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{g : M₂ → M}
(h : Function.LeftInverse g ⇑f)
:
M ≃ₛₗ[σ₁₂] ↥(LinearMap.range f)
A linear map f : M →ₗ[R] M₂ with a left-inverse g : M₂ →ₗ[R] M defines a linear
equivalence between M and f.range.
This is a computable alternative to LinearEquiv.ofInjective, and a bidirectional version of
LinearMap.rangeRestrict.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LinearEquiv.ofLeftInverse_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{f : M →ₛₗ[σ₁₂] M₂}
{g : M₂ →ₛₗ[σ₂₁] M}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(h : Function.LeftInverse ⇑g ⇑f)
(x : M)
:
↑((LinearEquiv.ofLeftInverse h) x) = f x
@[simp]
theorem
LinearEquiv.ofLeftInverse_symm_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{f : M →ₛₗ[σ₁₂] M₂}
{g : M₂ →ₛₗ[σ₂₁] M}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(h : Function.LeftInverse ⇑g ⇑f)
(x : ↥(LinearMap.range f))
:
(LinearEquiv.symm (LinearEquiv.ofLeftInverse h)) x = g ↑x
noncomputable def
LinearEquiv.ofInjective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
(f : M →ₛₗ[σ₁₂] M₂)
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(h : Function.Injective ⇑f)
:
M ≃ₛₗ[σ₁₂] ↥(LinearMap.range f)
An Injective linear map f : M →ₗ[R] M₂ defines a linear equivalence
between M and f.range. See also LinearMap.ofLeftInverse.
Equations
Instances For
@[simp]
theorem
LinearEquiv.ofInjective_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
(f : M →ₛₗ[σ₁₂] M₂)
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{h : Function.Injective ⇑f}
(x : M)
:
↑((LinearEquiv.ofInjective f h) x) = f x
noncomputable def
LinearEquiv.ofBijective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
(f : M →ₛₗ[σ₁₂] M₂)
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(hf : Function.Bijective ⇑f)
:
A bijective linear map is a linear equivalence.
Equations
- LinearEquiv.ofBijective f hf = LinearEquiv.trans (LinearEquiv.ofInjective f ⋯) (LinearEquiv.ofTop (LinearMap.range f) ⋯)
Instances For
@[simp]
theorem
LinearEquiv.ofBijective_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
(f : M →ₛₗ[σ₁₂] M₂)
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{hf : Function.Bijective ⇑f}
(x : M)
:
(LinearEquiv.ofBijective f hf) x = f x
@[simp]
theorem
LinearEquiv.ofBijective_symm_apply_apply
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
{module_M : Module R M}
{module_M₂ : Module R₂ M₂}
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
(f : M →ₛₗ[σ₁₂] M₂)
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{h : Function.Bijective ⇑f}
(x : M)
:
(LinearEquiv.symm (LinearEquiv.ofBijective f h)) (f x) = x
x ↦ -x as a LinearEquiv
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LinearEquiv.coe_neg
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommGroup M]
[Module R M]
:
⇑(LinearEquiv.neg R) = -id
theorem
LinearEquiv.neg_apply
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommGroup M]
[Module R M]
(x : M)
:
(LinearEquiv.neg R) x = -x
@[simp]
theorem
LinearEquiv.symm_neg
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommGroup M]
[Module R M]
:
def
LinearEquiv.smulOfUnit
{R : Type u_1}
{M : Type u_9}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(a : Rˣ)
:
Multiplying by a unit a of the ring R is a linear equivalence.
Equations
Instances For
def
LinearEquiv.arrowCongr
{R : Type u_20}
{M₁ : Type u_21}
{M₂ : Type u_22}
{M₂₁ : Type u_23}
{M₂₂ : Type u_24}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₂₁]
[AddCommMonoid M₂₂]
[Module R M₁]
[Module R M₂]
[Module R M₂₁]
[Module R M₂₂]
(e₁ : M₁ ≃ₗ[R] M₂)
(e₂ : M₂₁ ≃ₗ[R] M₂₂)
:
A linear isomorphism between the domains and codomains of two spaces of linear maps gives a linear isomorphism between the two function spaces.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LinearEquiv.arrowCongr_apply
{R : Type u_20}
{M₁ : Type u_21}
{M₂ : Type u_22}
{M₂₁ : Type u_23}
{M₂₂ : Type u_24}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₂₁]
[AddCommMonoid M₂₂]
[Module R M₁]
[Module R M₂]
[Module R M₂₁]
[Module R M₂₂]
(e₁ : M₁ ≃ₗ[R] M₂)
(e₂ : M₂₁ ≃ₗ[R] M₂₂)
(f : M₁ →ₗ[R] M₂₁)
(x : M₂)
:
((LinearEquiv.arrowCongr e₁ e₂) f) x = e₂ (f ((LinearEquiv.symm e₁) x))
@[simp]
theorem
LinearEquiv.arrowCongr_symm_apply
{R : Type u_20}
{M₁ : Type u_21}
{M₂ : Type u_22}
{M₂₁ : Type u_23}
{M₂₂ : Type u_24}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₂₁]
[AddCommMonoid M₂₂]
[Module R M₁]
[Module R M₂]
[Module R M₂₁]
[Module R M₂₂]
(e₁ : M₁ ≃ₗ[R] M₂)
(e₂ : M₂₁ ≃ₗ[R] M₂₂)
(f : M₂ →ₗ[R] M₂₂)
(x : M₁)
:
((LinearEquiv.symm (LinearEquiv.arrowCongr e₁ e₂)) f) x = (LinearEquiv.symm e₂) (f (e₁ x))
theorem
LinearEquiv.arrowCongr_comp
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
{M₃ : Type u_13}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
{N : Type u_20}
{N₂ : Type u_21}
{N₃ : Type u_22}
[AddCommMonoid N]
[AddCommMonoid N₂]
[AddCommMonoid N₃]
[Module R N]
[Module R N₂]
[Module R N₃]
(e₁ : M ≃ₗ[R] N)
(e₂ : M₂ ≃ₗ[R] N₂)
(e₃ : M₃ ≃ₗ[R] N₃)
(f : M →ₗ[R] M₂)
(g : M₂ →ₗ[R] M₃)
:
(LinearEquiv.arrowCongr e₁ e₃) (g ∘ₗ f) = (LinearEquiv.arrowCongr e₂ e₃) g ∘ₗ (LinearEquiv.arrowCongr e₁ e₂) f
theorem
LinearEquiv.arrowCongr_trans
{R : Type u_1}
[CommSemiring R]
{M₁ : Type u_20}
{M₂ : Type u_21}
{M₃ : Type u_22}
{N₁ : Type u_23}
{N₂ : Type u_24}
{N₃ : Type u_25}
[AddCommMonoid M₁]
[Module R M₁]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
[AddCommMonoid N₁]
[Module R N₁]
[AddCommMonoid N₂]
[Module R N₂]
[AddCommMonoid N₃]
[Module R N₃]
(e₁ : M₁ ≃ₗ[R] M₂)
(e₂ : N₁ ≃ₗ[R] N₂)
(e₃ : M₂ ≃ₗ[R] M₃)
(e₄ : N₂ ≃ₗ[R] N₃)
:
LinearEquiv.arrowCongr e₁ e₂ ≪≫ₗ LinearEquiv.arrowCongr e₃ e₄ = LinearEquiv.arrowCongr (e₁ ≪≫ₗ e₃) (e₂ ≪≫ₗ e₄)
def
LinearEquiv.congrRight
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
{M₃ : Type u_13}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
(f : M₂ ≃ₗ[R] M₃)
:
If M₂ and M₃ are linearly isomorphic then the two spaces of linear maps from M into M₂
and M into M₃ are linearly isomorphic.
Equations
Instances For
def
LinearEquiv.conj
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(e : M ≃ₗ[R] M₂)
:
Module.End R M ≃ₗ[R] Module.End R M₂
If M and M₂ are linearly isomorphic then the two spaces of linear maps from M and M₂ to
themselves are linearly isomorphic.
Equations
Instances For
theorem
LinearEquiv.conj_apply
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(e : M ≃ₗ[R] M₂)
(f : Module.End R M)
:
(LinearEquiv.conj e) f = (↑e ∘ₗ f) ∘ₗ ↑(LinearEquiv.symm e)
theorem
LinearEquiv.conj_apply_apply
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(e : M ≃ₗ[R] M₂)
(f : Module.End R M)
(x : M₂)
:
((LinearEquiv.conj e) f) x = e (f ((LinearEquiv.symm e) x))
theorem
LinearEquiv.symm_conj_apply
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(e : M ≃ₗ[R] M₂)
(f : Module.End R M₂)
:
(LinearEquiv.conj (LinearEquiv.symm e)) f = (↑(LinearEquiv.symm e) ∘ₗ f) ∘ₗ ↑e
theorem
LinearEquiv.conj_comp
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(e : M ≃ₗ[R] M₂)
(f : Module.End R M)
(g : Module.End R M)
:
(LinearEquiv.conj e) (g ∘ₗ f) = (LinearEquiv.conj e) g ∘ₗ (LinearEquiv.conj e) f
theorem
LinearEquiv.conj_trans
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
{M₃ : Type u_13}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₂ ≃ₗ[R] M₃)
:
LinearEquiv.conj e₁ ≪≫ₗ LinearEquiv.conj e₂ = LinearEquiv.conj (e₁ ≪≫ₗ e₂)
@[simp]
theorem
LinearEquiv.conj_id
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(e : M ≃ₗ[R] M₂)
:
(LinearEquiv.conj e) LinearMap.id = LinearMap.id
def
LinearEquiv.congrLeft
(M : Type u_9)
{M₂ : Type u_12}
{M₃ : Type u_13}
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
{R : Type u_20}
(S : Type u_21)
[Semiring R]
[Semiring S]
[Module R M₂]
[Module R M₃]
[Module R M]
[Module S M]
[SMulCommClass R S M]
(e : M₂ ≃ₗ[R] M₃)
:
An R-linear isomorphism between two R-modules M₂ and M₃ induces an S-linear
isomorphism between M₂ →ₗ[R] M and M₃ →ₗ[R] M, if M is both an R-module and an
S-module and their actions commute.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LinearEquiv.smulOfNeZero_symm_apply
(K : Type u_7)
(M : Type u_9)
[Field K]
[AddCommGroup M]
[Module K M]
(a : K)
(ha : a ≠ 0)
:
∀ (a_1 : M), (LinearEquiv.symm (LinearEquiv.smulOfNeZero K M a ha)) a_1 = (Units.mk0 a ha)⁻¹ • a_1
@[simp]
theorem
LinearEquiv.smulOfNeZero_apply
(K : Type u_7)
(M : Type u_9)
[Field K]
[AddCommGroup M]
[Module K M]
(a : K)
(ha : a ≠ 0)
:
∀ (a_1 : M), (LinearEquiv.smulOfNeZero K M a ha) a_1 = a • a_1
def
LinearEquiv.smulOfNeZero
(K : Type u_7)
(M : Type u_9)
[Field K]
[AddCommGroup M]
[Module K M]
(a : K)
(ha : a ≠ 0)
:
Multiplying by a nonzero element a of the field K is a linear equivalence.
Equations
- LinearEquiv.smulOfNeZero K M a ha = LinearEquiv.smulOfUnit (Units.mk0 a ha)
Instances For
def
Submodule.equivSubtypeMap
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
(q : Submodule R ↥p)
:
↥q ≃ₗ[R] ↥(Submodule.map (Submodule.subtype p) q)
Given p a submodule of the module M and q a submodule of p, p.equivSubtypeMap q
is the natural LinearEquiv between q and q.map p.subtype.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Submodule.equivSubtypeMap_apply
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{q : Submodule R ↥p}
(x : ↥q)
:
↑((Submodule.equivSubtypeMap p q) x) = (LinearMap.domRestrict (Submodule.subtype p) q) x
@[simp]
theorem
Submodule.equivSubtypeMap_symm_apply
{R : Type u_1}
{M : Type u_9}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{q : Submodule R ↥p}
(x : ↥(Submodule.map (Submodule.subtype p) q))
:
↑↑((LinearEquiv.symm (Submodule.equivSubtypeMap p q)) x) = ↑x
@[simp]
theorem
Submodule.comap_equiv_self_of_inj_of_le_apply
{R : Type u_1}
{M : Type u_9}
{N : Type u_15}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
{f : M →ₗ[R] N}
{p : Submodule R N}
(hf : Function.Injective ⇑f)
(h : p ≤ LinearMap.range f)
:
∀ (a : ↥(Submodule.comap f p)),
(Submodule.comap_equiv_self_of_inj_of_le hf h) a = (LinearMap.codRestrict p (f ∘ₗ Submodule.subtype (Submodule.comap f p)) ⋯) a
noncomputable def
Submodule.comap_equiv_self_of_inj_of_le
{R : Type u_1}
{M : Type u_9}
{N : Type u_15}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
{f : M →ₗ[R] N}
{p : Submodule R N}
(hf : Function.Injective ⇑f)
(h : p ≤ LinearMap.range f)
:
↥(Submodule.comap f p) ≃ₗ[R] ↥p
A linear injection M ↪ N restricts to an equivalence f⁻¹ p ≃ p for any submodule p
contained in its range.
Equations
- Submodule.comap_equiv_self_of_inj_of_le hf h = LinearEquiv.ofBijective (LinearMap.codRestrict p (f ∘ₗ Submodule.subtype (Submodule.comap f p)) ⋯) ⋯
Instances For
def
Equiv.toLinearEquiv
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_12}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
(e : M ≃ M₂)
(h : IsLinearMap R ⇑e)
:
An equivalence whose underlying function is linear is a linear equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LinearMap.funLeft
(R : Type u_1)
(M : Type u_9)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{m : Type u_20}
{n : Type u_21}
(f : m → n)
:
Given an R-module M and a function m → n between arbitrary types,
construct a linear map (n → M) →ₗ[R] (m → M)
Equations
- LinearMap.funLeft R M f = { toAddHom := { toFun := fun (x : n → M) => x ∘ f, map_add' := ⋯ }, map_smul' := ⋯ }
Instances For
@[simp]
theorem
LinearMap.funLeft_apply
(R : Type u_1)
(M : Type u_9)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{m : Type u_20}
{n : Type u_21}
(f : m → n)
(g : n → M)
(i : m)
:
(LinearMap.funLeft R M f) g i = g (f i)
@[simp]
theorem
LinearMap.funLeft_id
(R : Type u_1)
(M : Type u_9)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{n : Type u_21}
(g : n → M)
:
(LinearMap.funLeft R M id) g = g
theorem
LinearMap.funLeft_comp
(R : Type u_1)
(M : Type u_9)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{m : Type u_20}
{n : Type u_21}
{p : Type u_22}
(f₁ : n → p)
(f₂ : m → n)
:
LinearMap.funLeft R M (f₁ ∘ f₂) = LinearMap.funLeft R M f₂ ∘ₗ LinearMap.funLeft R M f₁
theorem
LinearMap.funLeft_surjective_of_injective
(R : Type u_1)
(M : Type u_9)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{m : Type u_20}
{n : Type u_21}
(f : m → n)
(hf : Function.Injective f)
:
Function.Surjective ⇑(LinearMap.funLeft R M f)
theorem
LinearMap.funLeft_injective_of_surjective
(R : Type u_1)
(M : Type u_9)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{m : Type u_20}
{n : Type u_21}
(f : m → n)
(hf : Function.Surjective f)
:
Function.Injective ⇑(LinearMap.funLeft R M f)
def
LinearEquiv.funCongrLeft
(R : Type u_1)
(M : Type u_9)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{m : Type u_20}
{n : Type u_21}
(e : m ≃ n)
:
Given an R-module M and an equivalence m ≃ n between arbitrary types,
construct a linear equivalence (n → M) ≃ₗ[R] (m → M)
Equations
- LinearEquiv.funCongrLeft R M e = LinearEquiv.ofLinear (LinearMap.funLeft R M ⇑e) (LinearMap.funLeft R M ⇑e.symm) ⋯ ⋯
Instances For
@[simp]
theorem
LinearEquiv.funCongrLeft_apply
(R : Type u_1)
(M : Type u_9)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{m : Type u_20}
{n : Type u_21}
(e : m ≃ n)
(x : n → M)
:
(LinearEquiv.funCongrLeft R M e) x = (LinearMap.funLeft R M ⇑e) x
@[simp]
theorem
LinearEquiv.funCongrLeft_id
(R : Type u_1)
(M : Type u_9)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{n : Type u_21}
:
LinearEquiv.funCongrLeft R M (Equiv.refl n) = LinearEquiv.refl R (n → M)
@[simp]
theorem
LinearEquiv.funCongrLeft_comp
(R : Type u_1)
(M : Type u_9)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{m : Type u_20}
{n : Type u_21}
{p : Type u_22}
(e₁ : m ≃ n)
(e₂ : n ≃ p)
:
LinearEquiv.funCongrLeft R M (e₁.trans e₂) = LinearEquiv.funCongrLeft R M e₂ ≪≫ₗ LinearEquiv.funCongrLeft R M e₁
@[simp]
theorem
LinearEquiv.funCongrLeft_symm
(R : Type u_1)
(M : Type u_9)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{m : Type u_20}
{n : Type u_21}
(e : m ≃ n)
:
LinearEquiv.symm (LinearEquiv.funCongrLeft R M e) = LinearEquiv.funCongrLeft R M e.symm