isAdjointPair_iff_eq_of_nondegenerate

English

Equivalence between IsAdjointPair and equality to the left adjoint holds for nondegenerate B.

Русский

Эквивалентность между IsAdjointPair и равенством левому сопряженному сохраняется для невырожденной B.

LaTeX

$$$IsAdjointPair B B \\psi \\phi \\iff \\psi = B.leftAdjointOfNondegenerate b \\phi$$$

Lean4

/-- Given the nondegenerate bilinear form `B`, the linear map `φ` has a unique left adjoint given by
`BilinForm.leftAdjointOfNondegenerate`. -/
theorem isAdjointPair_iff_eq_of_nondegenerate (B : BilinForm K V) (b : B.Nondegenerate) (ψ φ : V →ₗ[K] V) :
    IsAdjointPair B B ψ φ ↔ ψ = B.leftAdjointOfNondegenerate b φ :=
  ⟨fun h => B.isAdjointPair_unique_of_nondegenerate b φ ψ _ h (isAdjointPairLeftAdjointOfNondegenerate _ _ _), fun h =>
    h.symm ▸ isAdjointPairLeftAdjointOfNondegenerate _ _ _⟩

Похожие утверждения