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.
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
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)
:
@[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)
:
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.
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₂)
:
@[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))
:
@[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)
:
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.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₂)
:
@[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 σ₁₃]
:
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.
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)
:
@[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))
:
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.
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)
:
@[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 : ↥(LinearMap.range f))
:
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)
:
@[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)
:
@[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₂)
:
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.
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)
:
@[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))
:
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)
:
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✝ : ↥(comap f p))
:
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 ∈ range i)
:
The restriction of a linear map on the target to a submodule of the target given by an inclusion.
Equations
- f.codRestrictOfInjective i hi hf = ↑(LinearEquiv.ofInjective i hi).symm ∘ₗ LinearMap.codRestrict (LinearMap.range i) f hf
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 ∈ range i)
(x : M₁)
:
@[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 ∈ range i)
:
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 ∈ range i)
:
The restriction of a bilinear map to a submodule in which it takes values.
Equations
- f.codRestrict₂ i hi hf = { toFun := fun (x : M₁) => ↑(LinearEquiv.ofInjective i hi).symm ∘ₗ LinearMap.codRestrict (LinearMap.range i) (f x) ⋯, map_add' := ⋯, map_smul' := ⋯ }
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 ∈ range i)
(x : M₁)
(y : M₂)
: