English
If two bilinear maps f1, f2: M → N → P become equal after precomposing with surjective g: Q → M and surjective g': Q' → N, then f1 = f2.
Русский
Пусть две билинейные карты f1, f2: M → N → P приводят к одинаковому результату после композиции слева с сюръективными g: Q → M и g': Q' → N; тогда f1 = f2.
LaTeX
$$$f_1.compl_1_2\; g\; g' = f_2.compl_1_2\; g\; g'\;\Rightarrow\; f_1 = f_2$, при условии, что $g$ и $g'$ сюръективны.$$
Lean4
theorem compl₁₂_inj [SMulCommClass R₂ R₁ Pₗ] {f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ} {g : Qₗ →ₗ[R₁] Mₗ} {g' : Qₗ' →ₗ[R₂] N}
(hₗ : Function.Surjective g) (hᵣ : Function.Surjective g') : f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂ :=
by
constructor <;> intro h
· -- B₁.comp l r = B₂.comp l r → B₁ = B₂
ext x y
obtain ⟨x', hx⟩ := hₗ x
subst hx
obtain ⟨y', hy⟩ := hᵣ y
subst hy
convert LinearMap.congr_fun₂ h x' y' using 0
· -- B₁ = B₂ → B₁.comp l r = B₂.comp l r
subst h; rfl
