English
A standard identity: applying the codRestrict₂-conceived map and then i recovers the original bilinear value.
Русский
Стандартная идентичность: применение карты codRestrict₂ и затем i восстанавливает исходное билинейное значение.
LaTeX
$$$i( codRestrict₂ f i hi hf x y) = f x y$$$
Lean4
/-- The restriction of a bilinear map to a submodule in which it takes values. -/
noncomputable def codRestrict₂ : M₁ →ₗ[R] M₂ →ₗ[R] M₃ :=
let e : LinearMap.range i ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
{ toFun := fun x ↦ e.comp <| (f x).codRestrict (p := LinearMap.range i) (hf x)
map_add' := by intro x₁ x₂; ext y; simp [f.map_add, ← e.map_add, codRestrict]
map_smul' := by intro t x; ext y; simp [f.map_smul, ← e.map_smul, codRestrict] }
