English
If the coefficient ring is a field and one side is finite-dimensional, then a bilinear form B with injective B and injective B.flip yields a perfect pairing; mkOfInjective constructs such a PerfectPairing.
Русский
Если коэффициентное кольцо является полем, и одна из сторон конечномерна, то билинейная форма B с инъективными B и B.flip задаёт совершенную пару; mkOfInjective строит такую PerfectPairing.
LaTeX
$$$\text{PerfectPairing}(K,V,W)$$$
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 form. -/
@[deprecated LinearMap.IsPerfPair.of_injective (since := "2025-05-27")]
def mkOfInjective {K V W : Type*} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
[FiniteDimensional K V] (B : V →ₗ[K] W →ₗ[K] K) (h : Injective B) (h' : Injective B.flip) : PerfectPairing K V W
where
toLinearMap := B
bijective_left := ⟨h, by rwa [← B.flip_injective_iff₁]⟩
bijective_right :=
⟨h', by
have : FiniteDimensional K W := FiniteDimensional.of_injective B.flip h'
rwa [← B.flip.flip_injective_iff₁, LinearMap.flip_flip]⟩
