Mathlib.Algebra.Module.Submodule.Equiv

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) :

↥p ≃ₗ[R] ↥q

Linear equivalence between two equal submodules.

Equations

LinearEquiv.ofEq p q h = { toFun := (Equiv.setCongr ⋯).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Equiv.setCongr ⋯).invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[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

source

@[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) :

(ofEq p q h).symm = ofEq q p ⋯

source

@[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} :

ofEq p p ⋯ = refl R ↥p

source

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) :

↥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

source

@[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

source

@[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

source

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

source

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)) ⋯

source

@[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

source

@[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

source

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 = ⊤) :

↥p ≃ₗ[R] M

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

source

@[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

source

@[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) :

↑((ofTop p h).symm x) = x

source

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) :

(ofTop p h).symm x = ⟨x, ⋯⟩

source

@[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 = ⊤

source

@[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) :

LinearMap.range e = ⊤

source

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 = ⊥

source

@[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 ∘ₛₗ ↑e) = LinearMap.range h

source

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

source

@[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

source

@[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)) :

(ofLeftInverse h).symm x = g ↑x

source

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

LinearEquiv.ofInjective f h = LinearEquiv.ofLeftInverse ⋯

Instances For

source

@[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

source

@[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)) :

f ((ofInjective f h).symm x) = ↑x

source

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) :

M ≃ₛₗ[σ₁₂] M₂

A bijective linear map is a linear equivalence.

Equations

LinearEquiv.ofBijective f hf = (LinearEquiv.ofInjective f ⋯).trans (LinearEquiv.ofTop (LinearMap.range f) ⋯)

Instances For

source

@[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

source

@[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

source

@[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

source

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] ↥(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

source

@[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

source

@[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

source

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) :

↥(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

source

@[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)) :

(comap_equiv_self_of_inj_of_le hf h) a✝ = (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) a✝

source

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) :

M₁ →ₗ[R] M₃

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

source

@[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₁) :

i ((f.codRestrictOfInjective i hi hf) x) = f x

source

@[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) :

i ∘ₗ f.codRestrictOfInjective i hi hf = f

source

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) :

M₁ →ₗ[R] M₂ →ₗ[R] M₃

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

source

@[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₂) :

i (((f.codRestrict₂ i hi hf) x) y) = (f x) y