English
Let K be a field and M,N finite-dimensional vector spaces over K. If a bilinear form p: M × N → K is injective in each argument (p and p.flip), then p is a perfect pairing.
Русский
Пусть K — поле, M,N — конечномерные векторные пространства над K. Если билинейная форма p: M × N → K инъективна по каждому аргументу (p и p.flip), то p — совершенная пара.
LaTeX
$$$p.IsPerfPair$$$
Lean4
/-- If the coefficients are a field, and one of the spaces is finite-dimensional, it is sufficient
to check only injectivity instead of bijectivity of the bilinear pairing. -/
theorem of_injective [FiniteDimensional K M] (h : Injective p) (h' : Injective p.flip) : p.IsPerfPair
where
bijective_left := ⟨h, by rwa [← p.flip_injective_iff₁]⟩
bijective_right :=
⟨h', by
have : FiniteDimensional K N := FiniteDimensional.of_injective p.flip h'
rwa [← p.flip.flip_injective_iff₁, LinearMap.flip_flip]⟩
