3. Symplectic form
Throughout this section we assume that \mathsf{R} is a commutative Ring.
Lean code
variable {R : Type} [CommRing R]
Below we define the symplectic inner product or symplectic form on \mathsf{R}.
The symplectic inner product of \p = (p_1, p_2) and \q = (q_1, q_2) in ℤ_d^2 is
\braket{\p,\q} := p_2 q_1 - p_1 q_2.
The symplectic inner product is antisymmetric.
For all \p,\q ∈ ℤ_d^2,
\braket{\p,\q} = -\braket{\q,\p}.
\braket{\p,\q} = p_2 q_1 - p_1 q_2 = - (q_2 p_1 - q_1 p_2) = -\braket{\q,\p}.
Lean code for Lemma3.2
Associated Lean declarations
-
symp_antisymmetric[complete]
-
symp_antisymmetric[complete]
lemma symp_antisymmetric (p q : R × R) :
⟨p, q⟩ = -⟨q, p⟩ := R:Typeinst✝:CommRing Rp:R × Rq:R × R⊢ ⟨p,q⟩ = -⟨q,p⟩ R:Typeinst✝:CommRing Rp:R × Rq:R × R⊢ p.2 * q.1 - p.1 * q.2 = -(q.2 * p.1 - q.1 * p.2); All goals completed! 🐙
Every vector is isotropic under the symplectic inner product.
For any \p ∈ ℤ_d^2,
\braket{\p,\p} = 0.
\braket{\p,\p} = p_2 p_1 - p_1 p_2 = 0.
Lean code for Lemma3.3
Associated Lean declarations
-
self_eq_zero[complete]
-
self_eq_zero[complete]
@[simp]
lemma self_eq_zero (p : R × R) : ⟨p, p⟩ = 0 :=
R:Typeinst✝:CommRing Rp:R × R⊢ ⟨p,p⟩ = 0 R:Typeinst✝:CommRing Rp:R × R⊢ p.2 * p.1 - p.1 * p.2 = 0; All goals completed! 🐙
The symplectic inner product is additive in the first and second argument.
For all \p, \p', \q ∈ ℤ_d^2,
\braket{\p + \p', \q} = \braket{\p,\q} + \braket{\p',\q}.
Lean code for Lemma3.4
Associated Lean declarations
-
symp_add_left[complete]
-
symp_add_left[complete]
@[simp]
lemma symp_add_left (p p' q : R × R) :
⟨p + p', q⟩ = ⟨p, q⟩ + ⟨p', q⟩ := R:Typeinst✝:CommRing Rp:R × Rp':R × Rq:R × R⊢ ⟨p + p',q⟩ = ⟨p,q⟩ + ⟨p',q⟩ R:Typeinst✝:CommRing Rp:R × Rp':R × Rq:R × R⊢ (p + p').2 * q.1 - (p + p').1 * q.2 = p.2 * q.1 - p.1 * q.2 + (p'.2 * q.1 - p'.1 * q.2); R:Typeinst✝:CommRing Rp:R × Rp':R × Rq:R × R⊢ (p.2 + p'.2) * q.1 - (p.1 + p'.1) * q.2 = p.2 * q.1 - p.1 * q.2 + (p'.2 * q.1 - p'.1 * q.2); All goals completed! 🐙
For all \p, \q, \q' ∈ ℤ_d^2,
\braket{\p, \q + \q'} = \braket{\p,\q} + \braket{\p,\q'}.
Lean code for Lemma3.5
Associated Lean declarations
-
symp_add_right[complete]
-
symp_add_right[complete]
@[simp]
lemma symp_add_right (p q q' : R × R) :
⟨p, (q + q')⟩ = ⟨p, q ⟩ + ⟨p, q'⟩ := R:Typeinst✝:CommRing Rp:R × Rq:R × Rq':R × R⊢ ⟨p,q + q'⟩ = ⟨p,q⟩ + ⟨p,q'⟩ R:Typeinst✝:CommRing Rp:R × Rq:R × Rq':R × R⊢ p.2 * (q + q').1 - p.1 * (q + q').2 = p.2 * q.1 - p.1 * q.2 + (p.2 * q'.1 - p.1 * q'.2); R:Typeinst✝:CommRing Rp:R × Rq:R × Rq':R × R⊢ p.2 * (q.1 + q'.1) - p.1 * (q.2 + q'.2) = p.2 * q.1 - p.1 * q.2 + (p.2 * q'.1 - p.1 * q'.2); All goals completed! 🐙
Constants can be pulled out of the first and second argument.
For all c ∈ ℤ_d and \p, \q ∈ ℤ_d^2,
\braket{c\p, \q} = c\braket{\p,\q}.
Lean code for Lemma3.6
Associated Lean declarations
-
symp_smul_left[complete]
-
symp_smul_left[complete]
@[simp]
lemma symp_smul_left (c : R) (p q : R × R) :
⟨(c • p), q⟩ = c * ⟨p, q⟩ := R:Typeinst✝:CommRing Rc:Rp:R × Rq:R × R⊢ ⟨c • p,q⟩ = c * ⟨p,q⟩ R:Typeinst✝:CommRing Rc:Rp:R × Rq:R × R⊢ (c • p).2 * q.1 - (c • p).1 * q.2 = c * (p.2 * q.1 - p.1 * q.2); R:Typeinst✝:CommRing Rc:Rp:R × Rq:R × R⊢ c * p.2 * q.1 - c * p.1 * q.2 = c * (p.2 * q.1 - p.1 * q.2); All goals completed! 🐙
For all c ∈ ℤ_d and \p, \q ∈ ℤ_d^2,
\braket{\p, c\q} = c\braket{\p,\q}.
Lean code for Lemma3.7
Associated Lean declarations
-
symp_smul_right[complete]
-
symp_smul_right[complete]
@[simp]
lemma symp_smul_right (c : R) (p q : R × R) :
⟨p, (c • q)⟩ = c * ⟨p, q⟩ := R:Typeinst✝:CommRing Rc:Rp:R × Rq:R × R⊢ ⟨p,c • q⟩ = c * ⟨p,q⟩ R:Typeinst✝:CommRing Rc:Rp:R × Rq:R × R⊢ p.2 * (c • q).1 - p.1 * (c • q).2 = c * (p.2 * q.1 - p.1 * q.2); R:Typeinst✝:CommRing Rc:Rp:R × Rq:R × R⊢ p.2 * (c * q.1) - p.1 * (c * q.2) = c * (p.2 * q.1 - p.1 * q.2); All goals completed! 🐙
If both arguments of the symplectic inner product are transformed by a linear map F, the value gets multiplied by \det F.
We first rely on the usual coercion between tuples and two-dimensional vectors to define Matrix multiplication over \mathsf{R}^2
Lean code
Associated Lean declarations
-
pair_apply_mat[complete]
-
pair_apply_mat_alg[complete]
-
pair_apply_mat[complete] -
pair_apply_mat_alg[complete]
@[simp]
def pair_apply_mat (F : Matrix (Fin 2) (Fin 2) R) (p : R × R) : R × R
:= F.mulVec p
@[simp]
lemma pair_apply_mat_alg
(F : Matrix (Fin 2) (Fin 2) R)
(p : R × R) :
pair_apply_mat F p = ((F 0 0) * p.1 + (F 0 1) * p.2,
(F 1 0) * p.1 + (F 1 1) * p.2)
:= R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × R⊢ pair_apply_mat F p = (F 0 0 * p.1 + F 0 1 * p.2, F 1 0 * p.1 + F 1 1 * p.2) R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × R⊢ F.mulVec ![p.1, p.2] 0 = F 0 0 * p.1 + F 0 1 * p.2 ∧ F.mulVec ![p.1, p.2] 1 = F 1 0 * p.1 + F 1 1 * p.2; R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × R⊢ ∑ j, F 0 j * ![p.1, p.2] j = F 0 0 * p.1 + F 0 1 * p.2 ∧ F.mulVec ![p.1, p.2] 1 = F 1 0 * p.1 + F 1 1 * p.2;
R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × R⊢ F.mulVec ![p.1, p.2] 1 = F 1 0 * p.1 + F 1 1 * p.2; R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × R⊢ ∑ j, F 1 j * ![p.1, p.2] j = F 1 0 * p.1 + F 1 1 * p.2; All goals completed! 🐙
For any matrix F \in \mathrm{M}_2(ℤ_d) and vectors \p, \q \in ℤ_d^2,
\langle F\p, F\q \rangle = (\det F) \langle \p, \q \rangle.
If F = \bigl(\begin{smallmatrix} \alpha & \beta \\ \gamma & \delta \end{smallmatrix}\bigr) and \p = (p_1, \, p_2)^T then
F\p = (\alpha p_1 + \beta p_2, \, \gamma p_1 + \delta p_2)^T.
After applying F the symplectic inner product evaluates to
\begin{aligned}
\langle F\p, F\q\rangle
&= (\gamma p_1 + \delta p_2)(\alpha q_1 + \beta q_2) - (\alpha p_1 + \beta p_2)(\gamma q_1 + \delta q_2) \\
&= (\alpha\delta - \beta\gamma)(p_2 q_1 - p_1 q_2) \\
&= (\det F)\langle \p, \q\rangle.
\end{aligned}
Lean code for Lemma3.8
Associated Lean declarations
-
symp_det[complete]
-
symp_det[complete]
lemma symp_det (F : Matrix (Fin 2) (Fin 2) R)
(p q : R × R) :
⟨(pair_apply_mat F p), (pair_apply_mat F q)⟩ =
Matrix.det F * ⟨p, q⟩ :=
R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × Rq:R × R⊢ ⟨pair_apply_mat F p,pair_apply_mat F q⟩ = F.det * ⟨p,q⟩ calc
symp (pair_apply_mat F p) (pair_apply_mat F q) =
symp ((F 0 0) * p.1 + (F 0 1) * p.2,
(F 1 0) * p.1 + (F 1 1) * p.2)
((F 0 0) * q.1 + (F 0 1) * q.2,
(F 1 0) * q.1 + (F 1 1) * q.2)
:= R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × Rq:R × R⊢ ⟨pair_apply_mat F p,pair_apply_mat F q⟩ =
⟨(F 0 0 * p.1 + F 0 1 * p.2, F 1 0 * p.1 + F 1 1 * p.2),(F 0 0 * q.1 + F 0 1 * q.2, F 1 0 * q.1 + F 1 1 * q.2)⟩ All goals completed! 🐙;
_ = (((F 1 0) * p.1 + (F 1 1) * p.2) *
((F 0 0) * q.1 + (F 0 1) * q.2)) -
(((F 1 0) * q.1 + (F 1 1) * q.2) *
((F 0 0) * p.1 + (F 0 1) * p.2))
:= R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × Rq:R × R⊢ ⟨(F 0 0 * p.1 + F 0 1 * p.2, F 1 0 * p.1 + F 1 1 * p.2),(F 0 0 * q.1 + F 0 1 * q.2, F 1 0 * q.1 + F 1 1 * q.2)⟩ =
(F 1 0 * p.1 + F 1 1 * p.2) * (F 0 0 * q.1 + F 0 1 * q.2) - (F 1 0 * q.1 + F 1 1 * q.2) * (F 0 0 * p.1 + F 0 1 * p.2) R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × Rq:R × R⊢ (F 0 0 * p.1 + F 0 1 * p.2, F 1 0 * p.1 + F 1 1 * p.2).2 * (F 0 0 * q.1 + F 0 1 * q.2, F 1 0 * q.1 + F 1 1 * q.2).1 -
(F 0 0 * p.1 + F 0 1 * p.2, F 1 0 * p.1 + F 1 1 * p.2).1 *
(F 0 0 * q.1 + F 0 1 * q.2, F 1 0 * q.1 + F 1 1 * q.2).2 =
(F 1 0 * p.1 + F 1 1 * p.2) * (F 0 0 * q.1 + F 0 1 * q.2) - (F 1 0 * q.1 + F 1 1 * q.2) * (F 0 0 * p.1 + F 0 1 * p.2); R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × Rq:R × R⊢ (F 0 0 * p.1 + F 0 1 * p.2) * (F 1 0 * q.1 + F 1 1 * q.2) = (F 1 0 * q.1 + F 1 1 * q.2) * (F 0 0 * p.1 + F 0 1 * p.2); All goals completed! 🐙
_ = ((F 0 0) * (F 1 1) - (F 1 0) * (F 0 1)) *
(p.2 * q.1 - p.1 * q.2 )
:= R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × Rq:R × R⊢ (F 1 0 * p.1 + F 1 1 * p.2) * (F 0 0 * q.1 + F 0 1 * q.2) - (F 1 0 * q.1 + F 1 1 * q.2) * (F 0 0 * p.1 + F 0 1 * p.2) =
(F 0 0 * F 1 1 - F 1 0 * F 0 1) * (p.2 * q.1 - p.1 * q.2) All goals completed! 🐙
_ = (Matrix.det F) * (symp p q)
:= R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × Rq:R × R⊢ (F 0 0 * F 1 1 - F 1 0 * F 0 1) * (p.2 * q.1 - p.1 * q.2) = F.det * ⟨p,q⟩ R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × Rq:R × R⊢ F.det * ⟨p,q⟩ = (F 0 0 * F 1 1 - F 1 0 * F 0 1) * (p.2 * q.1 - p.1 * q.2); R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × Rq:R × R⊢ F.det * (p.2 * q.1 - p.1 * q.2) = (F 0 0 * F 1 1 - F 1 0 * F 0 1) * (p.2 * q.1 - p.1 * q.2); R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) Rp:R × Rq:R × R⊢ (F 0 0 * F 1 1 - F 0 1 * F 1 0) * (p.2 * q.1 - p.1 * q.2) = (F 0 0 * F 1 1 - F 1 0 * F 0 1) * (p.2 * q.1 - p.1 * q.2); All goals completed! 🐙
Adjoint property of the symplectic inner product. Properties on matrices of the Special Linear Group
Lean code
Associated Lean declarations
-
SpecialLinearInverse[complete]
-
MatrixMulToDoubleApply[complete]
-
SpecialLinearDet[complete]
-
FactorByInverse[complete]
-
SpecialLinearInverse[complete] -
MatrixMulToDoubleApply[complete] -
SpecialLinearDet[complete] -
FactorByInverse[complete]
def SpecialLinearInverse (F : Matrix.SpecialLinearGroup (Fin 2) R)
: Matrix.SpecialLinearGroup (Fin 2) R := Matrix.SpecialLinearGroup.hasInv.inv F
lemma MatrixMulToDoubleApply
(F G : Matrix (Fin 2) (Fin 2) R)
(p : R × R) : pair_apply_mat F (pair_apply_mat G p) = pair_apply_mat (F * G) p
:= R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) RG:Matrix (Fin 2) (Fin 2) Rp:R × R⊢ pair_apply_mat F (pair_apply_mat G p) = pair_apply_mat (F * G) p R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) RG:Matrix (Fin 2) (Fin 2) Rp:R × R⊢ (F.mulVec ![(G.mulVec ![p.1, p.2] 0, G.mulVec ![p.1, p.2] 1).1, (G.mulVec ![p.1, p.2] 0, G.mulVec ![p.1, p.2] 1).2] 0,
F.mulVec ![(G.mulVec ![p.1, p.2] 0, G.mulVec ![p.1, p.2] 1).1, (G.mulVec ![p.1, p.2] 0, G.mulVec ![p.1, p.2] 1).2]
1) =
((F * G).mulVec ![p.1, p.2] 0, (F * G).mulVec ![p.1, p.2] 1); R:Typeinst✝:CommRing RF:Matrix (Fin 2) (Fin 2) RG:Matrix (Fin 2) (Fin 2) Rp:R × R⊢ (F.mulVec ![(G.mulVec ![p.1, p.2] 0, G.mulVec ![p.1, p.2] 1).1, (G.mulVec ![p.1, p.2] 0, G.mulVec ![p.1, p.2] 1).2] 0,
F.mulVec ![(G.mulVec ![p.1, p.2] 0, G.mulVec ![p.1, p.2] 1).1, (G.mulVec ![p.1, p.2] 0, G.mulVec ![p.1, p.2] 1).2]
1) =
(F.mulVec (G.mulVec ![p.1, p.2]) 0, F.mulVec (G.mulVec ![p.1, p.2]) 1); All goals completed! 🐙
@[simp]
lemma SpecialLinearDet
(F : Matrix.SpecialLinearGroup (Fin 2) R):
Matrix.det (CoeFun.coe F) = 1 := R:Typeinst✝:CommRing RF:Matrix.SpecialLinearGroup (Fin 2) R⊢ Matrix.det (CoeFun.coe F) = 1 All goals completed! 🐙
lemma FactorByInverse (F : Matrix.SpecialLinearGroup (Fin 2) R)
(p : R × R) : pair_apply_mat ↑((F * F⁻¹) :
Matrix.SpecialLinearGroup (Fin 2) R) p = p :=
R:Typeinst✝:CommRing RF:Matrix.SpecialLinearGroup (Fin 2) Rp:R × R⊢ pair_apply_mat (↑(F * F⁻¹)) p = p R:Typeinst✝:CommRing RF:Matrix.SpecialLinearGroup (Fin 2) Rp:R × R⊢ pair_apply_mat (↑1) p = p; All goals completed! 🐙
If F ∈ \SL(2,ℤ_d) then
\braket{\p,F\q} \equiv \braket{F^{-1}\p,\q} \pmod{d}
for all \p,\q ∈ ℤ.
Since F is invertible, one can write p = FF^{-1}p. Hence,
\begin{align*}
\langle p, F q \rangle &= \langle FF^{-1}p , F q \rangle \\
&= (\det F) \langle F^{-1}p, q \rangle\\
&=\langle F^{-1}p, q \rangle
\end{align*}
Lean code for Lemma3.9
Associated Lean declarations
-
symp_adjoint[complete]
-
symp_adjoint[complete]
lemma symp_adjoint
(F : Matrix.SpecialLinearGroup (Fin 2) R)
(p q : R × R) :
(⟨p, (pair_apply_mat F q)⟩) =
(⟨(pair_apply_mat (SpecialLinearInverse F) p), q⟩)
:= R:Typeinst✝:CommRing RF:Matrix.SpecialLinearGroup (Fin 2) Rp:R × Rq:R × R⊢ ⟨p,pair_apply_mat (↑F) q⟩ = ⟨pair_apply_mat (↑(SpecialLinearInverse F)) p,q⟩ calc
⟨p, (pair_apply_mat F q)⟩ =
⟨ (pair_apply_mat ((F * (SpecialLinearInverse F))
: Matrix.SpecialLinearGroup (Fin 2) R) p)
, (pair_apply_mat F q)⟩
:= R:Typeinst✝:CommRing RF:Matrix.SpecialLinearGroup (Fin 2) Rp:R × Rq:R × R⊢ ⟨p,pair_apply_mat (↑F) q⟩ = ⟨pair_apply_mat (↑(F * SpecialLinearInverse F)) p,pair_apply_mat (↑F) q⟩ R:Typeinst✝:CommRing RF:Matrix.SpecialLinearGroup (Fin 2) Rp:R × Rq:R × R⊢ ⟨pair_apply_mat (↑(F * SpecialLinearInverse F)) p,pair_apply_mat (↑F) q⟩ = ⟨p,pair_apply_mat (↑F) q⟩; R:Typeinst✝:CommRing RF:Matrix.SpecialLinearGroup (Fin 2) Rp:R × Rq:R × R⊢ ⟨pair_apply_mat (↑(F * F⁻¹)) p,pair_apply_mat (↑F) q⟩ = ⟨p,pair_apply_mat (↑F) q⟩; All goals completed! 🐙
_ = (Matrix.det
(Matrix.SpecialLinearGroup.instCoeFun.coe F)) *
symp (pair_apply_mat (SpecialLinearInverse F) p) q
:= R:Typeinst✝:CommRing RF:Matrix.SpecialLinearGroup (Fin 2) Rp:R × Rq:R × R⊢ ⟨pair_apply_mat (↑(F * SpecialLinearInverse F)) p,pair_apply_mat (↑F) q⟩ =
Matrix.det (CoeFun.coe F) * ⟨pair_apply_mat (↑(SpecialLinearInverse F)) p,q⟩ R:Typeinst✝:CommRing RF:Matrix.SpecialLinearGroup (Fin 2) Rp:R × Rq:R × R⊢ ⟨pair_apply_mat (↑F * ↑(SpecialLinearInverse F)) p,pair_apply_mat (↑F) q⟩ =
Matrix.det (CoeFun.coe F) * ⟨pair_apply_mat (↑(SpecialLinearInverse F)) p,q⟩; R:Typeinst✝:CommRing RF:Matrix.SpecialLinearGroup (Fin 2) Rp:R × Rq:R × R⊢ ⟨pair_apply_mat (↑F) (pair_apply_mat (↑(SpecialLinearInverse F)) p),pair_apply_mat (↑F) q⟩ =
Matrix.det (CoeFun.coe F) * ⟨pair_apply_mat (↑(SpecialLinearInverse F)) p,q⟩; All goals completed! 🐙
_ = symp (pair_apply_mat (SpecialLinearInverse F) p) q
:= R:Typeinst✝:CommRing RF:Matrix.SpecialLinearGroup (Fin 2) Rp:R × Rq:R × R⊢ Matrix.det (CoeFun.coe F) * ⟨pair_apply_mat (↑(SpecialLinearInverse F)) p,q⟩ =
⟨pair_apply_mat (↑(SpecialLinearInverse F)) p,q⟩ R:Typeinst✝:CommRing RF:Matrix.SpecialLinearGroup (Fin 2) Rp:R × Rq:R × R⊢ 1 * ⟨pair_apply_mat (↑(SpecialLinearInverse F)) p,q⟩ = ⟨pair_apply_mat (↑(SpecialLinearInverse F)) p,q⟩; All goals completed! 🐙