Linear equivalences involving submodules #
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
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
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)
:
@[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
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
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
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
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
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
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₂)
: