English
If A is symplectic, then its transpose A^T is also symplectic.
Русский
Если A симплектическая, то и A^T симплектическая.
LaTeX
$$A ∈ Sp(l,R) ⇒ A^T ∈ Sp(l,R)$$
Lean4
theorem transpose_mem (hA : A ∈ symplecticGroup l R) : Aᵀ ∈ symplecticGroup l R :=
by
rw [mem_iff] at hA ⊢
rw [transpose_transpose]
have huA := symplectic_det hA
have huAT : IsUnit Aᵀ.det := by
rw [Matrix.det_transpose]
exact huA
calc
Aᵀ * J l R * A = (-Aᵀ) * (J l R)⁻¹ * A := by
rw [J_inv]
simp
_ = (-Aᵀ) * (A * J l R * Aᵀ)⁻¹ * A := by rw [hA]
_ = -(Aᵀ * (Aᵀ⁻¹ * (J l R)⁻¹)) * A⁻¹ * A := by simp only [Matrix.mul_inv_rev, Matrix.mul_assoc, Matrix.neg_mul]
_ = -(J l R)⁻¹ := by rw [mul_nonsing_inv_cancel_left _ _ huAT, nonsing_inv_mul_cancel_right _ _ huA]
_ = J l R := by simp [J_inv]
