Linear equivalences involving submodules #
def
LinearEquiv.ofEq
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
(p q : Submodule R M)
(h : p = q)
:
Linear equivalence between two equal submodules.
Instances For
@[simp]
theorem
LinearEquiv.coe_ofEq_apply
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
{p q : Submodule R M}
(h : p = q)
(x : β₯p)
:
β((ofEq p q h) x) = βx
@[simp]
theorem
LinearEquiv.ofEq_symm
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
{p q : Submodule R M}
(h : p = q)
:
@[simp]
theorem
LinearEquiv.ofEq_rfl
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
{p : Submodule R M}
:
def
LinearEquiv.ofSubmodules
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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.
Instances For
@[simp]
theorem
LinearEquiv.ofSubmodules_apply
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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)
:
β((e.ofSubmodules p q h) x) = e βx
@[simp]
theorem
LinearEquiv.ofSubmodules_symm_apply
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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)
:
β((e.ofSubmodules p q h).symm x) = e.symm βx
def
LinearEquiv.ofSubmodule'
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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β)
:
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.
Instances For
theorem
LinearEquiv.ofSubmodule'_toLinearMap
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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β)
:
β(f.ofSubmodule' U) = LinearMap.codRestrict U ((βf).domRestrict (Submodule.comap (βf) U)) β―
@[simp]
theorem
LinearEquiv.ofSubmodule'_apply
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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))
:
β((f.ofSubmodule' U) x) = f βx
@[simp]
theorem
LinearEquiv.ofSubmodule'_symm_apply
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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)
:
β((f.ofSubmodule' U).symm x) = f.symm βx
def
LinearEquiv.ofTop
{R : Type u_1}
{M : Type u_5}
[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.
Instances For
@[simp]
theorem
LinearEquiv.ofTop_apply
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
(p : Submodule R M)
{h : p = β€}
(x : β₯p)
:
(ofTop p h) x = βx
@[simp]
theorem
LinearEquiv.coe_ofTop_symm_apply
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
(p : Submodule R M)
{h : p = β€}
(x : M)
:
theorem
LinearEquiv.ofTop_symm_apply
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
(p : Submodule R M)
{h : p = β€}
(x : M)
:
@[simp]
theorem
LinearEquiv.toLinearMap_ofTop
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
(p : Submodule R M)
{h : p = β€}
:
@[simp]
theorem
LinearEquiv.range
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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β)
:
theorem
LinearEquiv.eq_bot_of_equiv
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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 βββ[Οββ] β₯β₯)
:
p = β₯
@[simp]
theorem
LinearEquiv.range_comp
{R : Type u_1}
{Rβ : Type u_3}
{Rβ : Type u_4}
{M : Type u_5}
{Mβ : Type u_7}
{Mβ : Type u_8}
[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 Οββ]
:
def
LinearEquiv.ofLeftInverse
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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)
:
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.
Instances For
@[simp]
theorem
LinearEquiv.ofLeftInverse_apply
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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)
:
β((ofLeftInverse h) x) = f x
@[simp]
theorem
LinearEquiv.ofLeftInverse_symm_apply
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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 : β₯f.range)
:
(ofLeftInverse h).symm x = g βx
noncomputable def
LinearEquiv.ofInjective
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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)
:
An Injective linear map f : M ββ[R] Mβ defines a linear equivalence
between M and f.range. See also LinearMap.ofLeftInverse.
Instances For
@[simp]
theorem
LinearEquiv.ofInjective_apply
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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)
:
β((ofInjective f h) x) = f x
@[simp]
theorem
LinearEquiv.ofInjective_symm_apply
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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 : β₯f.range)
:
f ((ofInjective f h).symm x) = βx
noncomputable def
LinearEquiv.ofBijective
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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.
Instances For
@[simp]
theorem
LinearEquiv.ofBijective_apply
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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)
:
(ofBijective f hf) x = f x
@[simp]
theorem
LinearEquiv.ofBijective_symm_apply_apply
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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)
:
(ofBijective f h).symm (f x) = x
@[simp]
theorem
LinearEquiv.apply_ofBijective_symm_apply
{R : Type u_1}
{Rβ : Type u_3}
{M : Type u_5}
{Mβ : Type u_7}
[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β)
:
f ((ofBijective f h).symm x) = x
def
Submodule.equivSubtypeMap
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
(q : Submodule R β₯p)
:
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.
Instances For
@[simp]
theorem
Submodule.equivSubtypeMap_apply
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{q : Submodule R β₯p}
(x : β₯q)
:
β((p.equivSubtypeMap q) x) = (p.subtype.domRestrict q) x
@[simp]
theorem
Submodule.equivSubtypeMap_symm_apply
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{q : Submodule R β₯p}
(x : β₯(map p.subtype q))
:
ββ((p.equivSubtypeMap q).symm x) = βx
noncomputable def
Submodule.comap_equiv_self_of_inj_of_le
{R : Type u_1}
{M : Type u_5}
{N : Type u_9}
[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 β€ f.range)
:
A linear injection M βͺ N restricts to an equivalence fβ»ΒΉ p β p for any submodule p
contained in its range.
Instances For
@[simp]
theorem
Submodule.comap_equiv_self_of_inj_of_le_apply
{R : Type u_1}
{M : Type u_5}
{N : Type u_9}
[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 β€ f.range)
(aβ : β₯(comap f p))
:
(comap_equiv_self_of_inj_of_le hf h) aβ = (LinearMap.codRestrict p (f ββ (comap f p).subtype) β―) aβ
noncomputable def
LinearMap.codRestrictOfInjective
{R : Type u_1}
{Mβ : Type u_6}
{Mβ : Type u_7}
{Mβ : Type u_8}
[CommSemiring R]
[AddCommMonoid Mβ]
[AddCommMonoid Mβ]
[AddCommMonoid Mβ]
[Module R Mβ]
[Module R Mβ]
[Module R Mβ]
(f : Mβ ββ[R] Mβ)
(i : Mβ ββ[R] Mβ)
(hi : Function.Injective βi)
(hf : β (x : Mβ), f x β i.range)
:
The restriction of a linear map on the target to a submodule of the target given by an inclusion.
Instances For
@[simp]
theorem
LinearMap.codRestrictOfInjective_comp_apply
{R : Type u_1}
{Mβ : Type u_6}
{Mβ : Type u_7}
{Mβ : Type u_8}
[CommSemiring R]
[AddCommMonoid Mβ]
[AddCommMonoid Mβ]
[AddCommMonoid Mβ]
[Module R Mβ]
[Module R Mβ]
[Module R Mβ]
(f : Mβ ββ[R] Mβ)
(i : Mβ ββ[R] Mβ)
(hi : Function.Injective βi)
(hf : β (x : Mβ), f x β i.range)
(x : Mβ)
:
i ((f.codRestrictOfInjective i hi hf) x) = f x
@[simp]
theorem
LinearMap.codRestrictOfInjective_comp
{R : Type u_1}
{Mβ : Type u_6}
{Mβ : Type u_7}
{Mβ : Type u_8}
[CommSemiring R]
[AddCommMonoid Mβ]
[AddCommMonoid Mβ]
[AddCommMonoid Mβ]
[Module R Mβ]
[Module R Mβ]
[Module R Mβ]
(f : Mβ ββ[R] Mβ)
(i : Mβ ββ[R] Mβ)
(hi : Function.Injective βi)
(hf : β (x : Mβ), f x β i.range)
:
i ββ f.codRestrictOfInjective i hi hf = f
noncomputable def
LinearMap.codRestrictβ
{R : Type u_1}
{M : Type u_5}
{Mβ : Type u_6}
{Mβ : Type u_7}
{Mβ : Type u_8}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid Mβ]
[AddCommMonoid Mβ]
[AddCommMonoid Mβ]
[Module R M]
[Module R Mβ]
[Module R Mβ]
[Module R Mβ]
(f : Mβ ββ[R] Mβ ββ[R] M)
(i : Mβ ββ[R] M)
(hi : Function.Injective βi)
(hf : β (x : Mβ) (y : Mβ), (f x) y β i.range)
:
The restriction of a bilinear map to a submodule in which it takes values.
Instances For
@[simp]
theorem
LinearMap.codRestrictβ_apply
{R : Type u_1}
{M : Type u_5}
{Mβ : Type u_6}
{Mβ : Type u_7}
{Mβ : Type u_8}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid Mβ]
[AddCommMonoid Mβ]
[AddCommMonoid Mβ]
[Module R M]
[Module R Mβ]
[Module R Mβ]
[Module R Mβ]
(f : Mβ ββ[R] Mβ ββ[R] M)
(i : Mβ ββ[R] M)
(hi : Function.Injective βi)
(hf : β (x : Mβ) (y : Mβ), (f x) y β i.range)
(x : Mβ)
(y : Mβ)
:
i (((f.codRestrictβ i hi hf) x) y) = (f x) y