def CompatibleTriple.Sp2n (l : Type u_1) [DecidableEq l] [Fintype l] : Set (Matrix (l ⊕ l) (l ⊕ l) ℝ)

The symplectic group $\mathrm{Sp}(2n) = \{A : A^T J A = J\}$, realized as a set of real $(l \sqcup l) \times (l \sqcup l)$ matrices using the standard symplectic form $J$.

def CompatibleTriple.O2n (l : Type u_1) [DecidableEq l] [Fintype l] : Set (Matrix (l ⊕ l) (l ⊕ l) ℝ)

The orthogonal group $O(2n) = \{A : A^T A = I\}$.

def CompatibleTriple.GLnC (l : Type u_1) [DecidableEq l] [Fintype l] : Set (Matrix (l ⊕ l) (l ⊕ l) ℝ)

The subgroup of $\mathrm{GL}(2n, \mathbb{R})$ that commutes with $J$, identified with $\mathrm{GL}(n, \mathbb{C}) = \{A : AJ = JA\}$ via the standard complex structure $J$.

def CompatibleTriple.Un (l : Type u_1) [DecidableEq l] [Fintype l] : Set (Matrix (l ⊕ l) (l ⊕ l) ℝ)

The unitary group $U(n) = \mathrm{GL}(n, \mathbb{C}) \cap O(2n)$.

theorem CompatibleTriple.J_mul_left_cancel {l : Type u_1} [DecidableEq l] [Fintype l] {M N : Matrix (l ⊕ l) (l ⊕ l) ℝ} (h : Matrix.J l ℝ * M = Matrix.J l ℝ * N) : M = N

Left-cancellation by the invertible matrix $J$: if $J M = J N$ then $M = N$.

theorem CompatibleTriple.comm_J_transpose {l : Type u_1} [DecidableEq l] [Fintype l] {A : Matrix (l ⊕ l) (l ⊕ l) ℝ} (h : A * Matrix.J l ℝ = Matrix.J l ℝ * A) : A.transpose * Matrix.J l ℝ = Matrix.J l ℝ * A.transpose

If $A$ commutes with $J$ (i.e. $A \in \mathrm{GL}(n, \mathbb{C})$), so does $A^T$, using that $J^T = -J$.

theorem CompatibleTriple.sp_cap_gl_sub_O {l : Type u_1} [DecidableEq l] [Fintype l] {A : Matrix (l ⊕ l) (l ⊕ l) ℝ} (hSp : A ∈ Sp2n l) (hGL : A ∈ GLnC l) : A ∈ O2n l

$\mathrm{Sp}(2n) \cap \mathrm{GL}(n, \mathbb{C}) \subseteq O(2n)$: a symplectic matrix which is also complex-linear is orthogonal.

theorem CompatibleTriple.O_cap_gl_sub_Sp {l : Type u_1} [DecidableEq l] [Fintype l] {A : Matrix (l ⊕ l) (l ⊕ l) ℝ} (hO : A ∈ O2n l) (hGL : A ∈ GLnC l) : A ∈ Sp2n l

$O(2n) \cap \mathrm{GL}(n, \mathbb{C}) \subseteq \mathrm{Sp}(2n)$: an orthogonal matrix which is also complex-linear is symplectic.

theorem CompatibleTriple.sp_cap_O_sub_GL {l : Type u_1} [DecidableEq l] [Fintype l] {A : Matrix (l ⊕ l) (l ⊕ l) ℝ} (hSp : A ∈ Sp2n l) (hO : A ∈ O2n l) : A ∈ GLnC l

$\mathrm{Sp}(2n) \cap O(2n) \subseteq \mathrm{GL}(n, \mathbb{C})$: a symplectic and orthogonal matrix is automatically complex-linear.

theorem CompatibleTriple.sp_cap_O_eq_U {l : Type u_1} [DecidableEq l] [Fintype l] : Sp2n l ∩ O2n l = Un l

The "two out of three" theorem for compatible triples. $$\mathrm{Sp}(2n) \cap O(2n) = \mathrm{Sp}(2n) \cap \mathrm{GL}(n, \mathbb{C}) = O(2n) \cap \mathrm{GL}(n, \mathbb{C}) = U(n).$$ This file proves the first equality; the others follow by the same argument.