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 : Submodule R M)
(q : Submodule R M)
(h : p = q)
:
Linear equivalence between two equal submodules.
Equations
- LinearEquiv.ofEq p q h = { toFun := (Equiv.Set.ofEq ⋯).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Equiv.Set.ofEq ⋯).invFun, left_inv := ⋯, right_inv := ⋯ }
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 : 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_5}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
{p : Submodule R M}
{q : Submodule R M}
(h : p = q)
:
(LinearEquiv.ofEq p q h).symm = LinearEquiv.ofEq q p ⋯
@[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}
:
LinearEquiv.ofEq p p ⋯ = LinearEquiv.refl R ↥p
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.
Equations
- e.ofSubmodules p q h = (e.submoduleMap p).trans (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_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₂)
:
↥(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
- f.ofSubmodule' U = (f.symm.ofSubmodules U (Submodule.comap (↑f.symm.symm) U) ⋯).symm
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.
Equations
- LinearEquiv.ofTop p h = { toLinearMap := p.subtype, invFun := fun (x : M) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
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)
:
(LinearEquiv.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)
:
↑((LinearEquiv.ofTop p h).symm x) = x
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)
:
(LinearEquiv.ofTop p h).symm x = ⟨x, ⋯⟩
@[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₂)
:
LinearMap.range ↑e = ⊤
@[simp]
theorem
LinearEquivClass.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₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
{re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
[Module R M]
[Module R₂ M₂]
{F : Type u_10}
[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_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 ≃ₛₗ[σ₁₂] ↥⊥)
:
@[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 σ₁₃]
:
LinearMap.range (h.comp ↑e) = LinearMap.range h
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)
:
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
- LinearEquiv.ofLeftInverse h = { toFun := ⇑f.rangeRestrict, map_add' := ⋯, map_smul' := ⋯, invFun := g ∘ ⇑(LinearMap.range f).subtype, left_inv := h, right_inv := ⋯ }
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)
:
↑((LinearEquiv.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 : ↥(LinearMap.range f))
:
(LinearEquiv.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)
:
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_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)
:
↑((LinearEquiv.ofInjective f h) x) = f 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.
Equations
- LinearEquiv.ofBijective f hf = (LinearEquiv.ofInjective f ⋯).trans (LinearEquiv.ofTop (LinearMap.range f) ⋯)
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)
:
(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_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)
:
(LinearEquiv.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 ((LinearEquiv.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)
:
↥q ≃ₗ[R] ↥(Submodule.map p.subtype 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_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 : ↥(Submodule.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 ≤ 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.comap f p).subtype) ⋯) ⋯
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 ≤ LinearMap.range f)
:
∀ (a : ↥(Submodule.comap f p)),
(Submodule.comap_equiv_self_of_inj_of_le hf h) a = (LinearMap.codRestrict p (f ∘ₗ (Submodule.comap f p).subtype) ⋯) a