English
For bilinear maps f1, f2 and surjective g, g' as above, f1.compl₁₂ g g' = f2.compl₁₂ g g' if and only if f1 = f2.
Русский
Для билинейных отображений f1, f2 и сюръективных g, g' верно: f1.compl₁₂ g g' = f2.compl₁₂ g g' тогда и только тогда, когда f1 = f2.
LaTeX
$$$f_1.compl_1_2\; g\; g' = f_2.compl_1_2\; g\; g' \iff f_1 = f_2$; при условии сюръективности $g$ и $g'$.$$
Lean4
/-- Composing a linear map `P → Q` and a bilinear map `M → N → P` to
form a bilinear map `M → N → Q`.
See `LinearMap.compr₂ₛₗ` for a version of this which does not support towers of scalars but which
does support semi-linear maps. -/
def compr₂ [Module R A] [Module A M] [Module A Qₗ] [SMulCommClass R A Qₗ] [IsScalarTower R A Qₗ] [IsScalarTower R A Pₗ]
(f : M →ₗ[A] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[A] Qₗ) : M →ₗ[A] Nₗ →ₗ[R] Qₗ
where
toFun x := g.restrictScalars R ∘ₗ (f x)
map_add' _ _ := by ext; simp
map_smul' _ _ := by ext; simp
