English
If p is a perfect pairing between M and N, and eM : M' ≃ M, eN : N' ≃ N are linear isomorphisms, then the pulled-back pairing p.compl₁₂ eM eN on M' × N' is a perfect pairing.
Русский
Пусть p — совершенная пара между M и N, и даны линейные эквивалентности eM : M' ≃ M, eN : N' ≃ N. Тогда вытягиваемая по базисам пара p.compl₁₂ eM eN на M' × N' также является совершенной парой.
LaTeX
$$$\big(p.compl_{1 2} eM eN\big)\IsPerfPair$$
Lean4
instance compl₁₂ (eM : M' ≃ₗ[R] M) (eN : N' ≃ₗ[R] N) : (p.compl₁₂ eM eN : M' →ₗ[R] N' →ₗ[R] R).IsPerfPair :=
⟨((LinearEquiv.congrLeft R R eN).symm.bijective.comp (IsPerfPair.bijective_left p)).comp eM.bijective,
((LinearEquiv.congrLeft R R eM).symm.bijective.comp (IsPerfPair.bijective_right p)).comp eN.bijective⟩
