3. Symplectic form
Throughout this section we assume that d ≥ 1.
Lean code
variable (d : ℕ) [NeZero d]
Below we define the symplectic inner product or symplectic form on ℤ_d^2.
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.
Lean code for Definition3.2
Associated Lean declarations
-
symp[complete]
Associated Lean declarations
-
symp[complete]
def symp {R : Type*} [CommRing R] (p q : R × R) : R :=
p.2 * q.1 - p.1 * q.2
The symplectic inner product is antisymmetric.
Lemma3.3
Group: Basic properties of the symplectic inner product. (8)
Preview
Definition 3.2
Associated Lean declarations
-
symp_antisymmetric[complete]
Used by 3
Preview
Theorem 7.1
For all \p,\q ∈ ℤ_d^2,
\braket{\p,\q} = -\braket{\q,\p}.
Proof
\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.3
Associated Lean declarations
-
symp_antisymmetric[complete]
Associated Lean declarations
-
symp_antisymmetric[complete]
omit [NeZero d] in
lemma symp_antisymmetric (p q : ZMod d × ZMod d) :
symp p q = - symp q p := d:ℕp:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp p q = -symp q p
d:ℕp:ZMod d × ZMod dq:ZMod d × ZMod d⊢ 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.
Lemma3.4
Group: Basic properties of the symplectic inner product. (8)
Preview
Definition 3.2
Associated Lean declarations
-
self_eq_zero[complete]
Used by 2
Preview
Lemma 5.49
For any \p ∈ ℤ_d^2,
\braket{\p,\p} = 0.
Proof
\braket{\p,\p} = p_2 p_1 - p_1 p_2 = 0.
Lean code for Lemma3.4
Associated Lean declarations
-
self_eq_zero[complete]
Associated Lean declarations
-
self_eq_zero[complete]
lemma self_eq_zero (p : ZMod d × ZMod d) : symp p p = 0 :=
d:ℕinst✝:NeZero dp:ZMod d × ZMod d⊢ symp p p = 0 d:ℕinst✝:NeZero dp:ZMod d × ZMod d⊢ p.2 * p.1 - p.1 * p.2 = 0; All goals completed! 🐙
The symplectic inner product is additive in the first argument.
Lemma3.5
Group: Basic properties of the symplectic inner product. (8)
Preview
Definition 3.2
Associated Lean declarations
-
symp_add_left[complete]
For all \p, \p', \q ∈ ℤ_d^2,
\braket{\p + \p', \q} = \braket{\p,\q} + \braket{\p',\q}.
Lean code for Lemma3.5
Associated Lean declarations
-
symp_add_left[complete]
Associated Lean declarations
-
symp_add_left[complete]
omit [NeZero d] in
lemma symp_add_left
(p p' q : ZMod d × ZMod d) :
symp (p + p') q =
symp p q + symp p' q := d:ℕp:ZMod d × ZMod dp':ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp (p + p') q = symp p q + symp p' q
d:ℕp:ZMod d × ZMod dp':ZMod d × ZMod dq:ZMod d × ZMod d⊢ (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)
d:ℕp:ZMod d × ZMod dp':ZMod d × ZMod dq:ZMod d × ZMod d⊢ (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! 🐙
The symplectic inner product is additive in the second argument.
Lemma3.6
Group: Basic properties of the symplectic inner product. (8)
Preview
Definition 3.2
Associated Lean declarations
-
symp_add_right[complete]
For all \p, \q, \q' ∈ ℤ_d^2,
\braket{\p, \q + \q'} = \braket{\p,\q} + \braket{\p,\q'}.
Lean code for Lemma3.6
Associated Lean declarations
-
symp_add_right[complete]
Associated Lean declarations
-
symp_add_right[complete]
omit [NeZero d] in
lemma symp_add_right
(p q q' : ZMod d × ZMod d) :
symp p (q + q') =
symp p q + symp p q' :=
d:ℕp:ZMod d × ZMod dq:ZMod d × ZMod dq':ZMod d × ZMod d⊢ symp p (q + q') = symp p q + symp p q' d:ℕp:ZMod d × ZMod dq:ZMod d × ZMod dq':ZMod d × ZMod d⊢ 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); d:ℕp:ZMod d × ZMod dq:ZMod d × ZMod dq':ZMod d × ZMod d⊢ 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 argument.
Lemma3.7
Group: Basic properties of the symplectic inner product. (8)
Preview
Definition 3.2
Associated Lean declarations
-
symp_smul_left[complete]
For all c ∈ ℤ_d and \p, \q ∈ ℤ_d^2,
\braket{c\p, \q} = c\braket{\p,\q}.
Lean code for Lemma3.7
Associated Lean declarations
-
symp_smul_left[complete]
Associated Lean declarations
-
symp_smul_left[complete]
omit [NeZero d] in
lemma symp_smul_left
(c : ZMod d) (p q : ZMod d × ZMod d) :
symp (c • p) q = c * symp p q :=
d:ℕc:ZMod dp:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp (c • p) q = c * symp p q d:ℕc:ZMod dp:ZMod d × ZMod dq:ZMod d × ZMod d⊢ (c • p).2 * q.1 - (c • p).1 * q.2 = c * (p.2 * q.1 - p.1 * q.2); d:ℕc:ZMod dp:ZMod d × ZMod dq:ZMod d × ZMod d⊢ c * p.2 * q.1 - c * p.1 * q.2 = c * (p.2 * q.1 - p.1 * q.2); All goals completed! 🐙
Constants can be pulled out of the second argument.
Lemma3.8
Group: Basic properties of the symplectic inner product. (8)
Preview
Definition 3.2
Associated Lean declarations
-
symp_smul_right[complete]
For all c ∈ ℤ_d and \p, \q ∈ ℤ_d^2,
\braket{\p, c\q} = c\braket{\p,\q}.
Lean code for Lemma3.8
Associated Lean declarations
-
symp_smul_right[complete]
Associated Lean declarations
-
symp_smul_right[complete]
omit [NeZero d] in
lemma symp_smul_right
(c : ZMod d) (p q : ZMod d × ZMod d) :
symp p (c • q) = c * symp p q :=
d:ℕc:ZMod dp:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp p (c • q) = c * symp p q d:ℕc:ZMod dp:ZMod d × ZMod dq:ZMod d × ZMod d⊢ p.2 * (c • q).1 - p.1 * (c • q).2 = c * (p.2 * q.1 - p.1 * q.2); d:ℕc:ZMod dp:ZMod d × ZMod dq:ZMod d × ZMod d⊢ 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.
Lemma3.9
Group: Basic properties of the symplectic inner product. (8)
Preview
Definition 3.2
Associated Lean declarations
-
pair_apply_mat[complete] -
pair_apply_mat.vecForm[complete] -
pair_apply_mat_alg[complete] -
symp_det[complete]
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.
Proof
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.9
Associated Lean declarations
-
pair_apply_mat[complete]
-
pair_apply_mat.vecForm[complete]
-
pair_apply_mat_alg[complete]
-
symp_det[complete]
Associated Lean declarations
-
pair_apply_mat[complete] -
pair_apply_mat.vecForm[complete] -
pair_apply_mat_alg[complete] -
symp_det[complete]
def pair_apply_mat (F : Matrix (Fin 2) (Fin 2) (ZMod d))
(p : ZMod d × ZMod d) : ZMod d × ZMod d :=
(vecForm 0, vecForm 1) where
vecForm := (Matrix.vecMul (fun i :
Fin 2 => if i.val = 0 then p.fst else p.snd) F)
lemma pair_apply_mat_alg
(F : Matrix (Fin 2) (Fin 2) (ZMod d))
(p : ZMod d × ZMod d) :
pair_apply_mat d F p = ((F 0 0) * p.1 + (F 1 0) * p.2,
(F 0 1) * p.1 + (F 1 1) * p.2)
:= d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ pair_apply_mat d F p = (F 0 0 * p.1 + F 1 0 * p.2, F 0 1 * p.1 + F 1 1 * p.2) d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ (pair_apply_mat.vecForm d F p 0, pair_apply_mat.vecForm d F p 1) =
(F 0 0 * p.1 + F 1 0 * p.2, F 0 1 * p.1 + F 1 1 * p.2); d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ (Matrix.vecMul (fun i => if ↑i = 0 then p.1 else p.2) F 0, Matrix.vecMul (fun i => if ↑i = 0 then p.1 else p.2) F 1) =
(F 0 0 * p.1 + F 1 0 * p.2, F 0 1 * p.1 + F 1 1 * p.2); d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ (have j := 0;
(fun i => if ↑i = 0 then p.1 else p.2) ⬝ᵥ fun i => F i j,
have j := 1;
(fun i => if ↑i = 0 then p.1 else p.2) ⬝ᵥ fun i => F i j) =
(F 0 0 * p.1 + F 1 0 * p.2, F 0 1 * p.1 + F 1 1 * p.2); d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ p.1 * F 0 0 + p.2 * F 1 0 = F 0 0 * p.1 + F 1 0 * p.2 ∧ p.1 * F 0 1 + p.2 * F 1 1 = F 0 1 * p.1 + F 1 1 * p.2; d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ p.1 * F 0 0 + p.2 * F 1 0 = F 0 0 * p.1 + F 1 0 * p.2d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ p.1 * F 0 1 + p.2 * F 1 1 = F 0 1 * p.1 + F 1 1 * p.2; d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ p.1 * F 0 1 + p.2 * F 1 1 = F 0 1 * p.1 + F 1 1 * p.2; All goals completed! 🐙
lemma symp_det (F : Matrix (Fin 2) (Fin 2) (ZMod d))
(p q : ZMod d × ZMod d) :
symp (pair_apply_mat d F p) (pair_apply_mat d F q) =
Matrix.det F * (symp p q) :=
d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp (pair_apply_mat d F p) (pair_apply_mat d F q) = F.det * symp p q calc
symp (pair_apply_mat d F p) (pair_apply_mat d F q) =
symp ((F 0 0) * p.1 + (F 1 0) * p.2,
(F 0 1) * p.1 + (F 1 1) * p.2)
((F 0 0) * q.1 + (F 1 0) * q.2,
(F 0 1) * q.1 + (F 1 1) * q.2)
:= d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp (pair_apply_mat d F p) (pair_apply_mat d F q) =
symp (F 0 0 * p.1 + F 1 0 * p.2, F 0 1 * p.1 + F 1 1 * p.2) (F 0 0 * q.1 + F 1 0 * q.2, F 0 1 * q.1 + F 1 1 * q.2) d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp (pair_apply_mat.vecForm d F p 0, pair_apply_mat.vecForm d F p 1)
(pair_apply_mat.vecForm d F q 0, pair_apply_mat.vecForm d F q 1) =
symp (F 0 0 * p.1 + F 1 0 * p.2, F 0 1 * p.1 + F 1 1 * p.2) (F 0 0 * q.1 + F 1 0 * q.2, F 0 1 * q.1 + F 1 1 * q.2); d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp
(Matrix.vecMul (fun i => if ↑i = 0 then p.1 else p.2) F 0, Matrix.vecMul (fun i => if ↑i = 0 then p.1 else p.2) F 1)
(Matrix.vecMul (fun i => if ↑i = 0 then q.1 else q.2) F 0,
Matrix.vecMul (fun i => if ↑i = 0 then q.1 else q.2) F 1) =
symp (F 0 0 * p.1 + F 1 0 * p.2, F 0 1 * p.1 + F 1 1 * p.2) (F 0 0 * q.1 + F 1 0 * q.2, F 0 1 * q.1 + F 1 1 * q.2); d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp
(have j := 0;
(fun i => if ↑i = 0 then p.1 else p.2) ⬝ᵥ fun i => F i j,
have j := 1;
(fun i => if ↑i = 0 then p.1 else p.2) ⬝ᵥ fun i => F i j)
(have j := 0;
(fun i => if ↑i = 0 then q.1 else q.2) ⬝ᵥ fun i => F i j,
have j := 1;
(fun i => if ↑i = 0 then q.1 else q.2) ⬝ᵥ fun i => F i j) =
symp (F 0 0 * p.1 + F 1 0 * p.2, F 0 1 * p.1 + F 1 1 * p.2) (F 0 0 * q.1 + F 1 0 * q.2, F 0 1 * q.1 + F 1 1 * q.2); d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp (p.1 * F 0 0 + p.2 * F 1 0, p.1 * F 0 1 + p.2 * F 1 1) (q.1 * F 0 0 + q.2 * F 1 0, q.1 * F 0 1 + q.2 * F 1 1) =
symp (F 0 0 * p.1 + F 1 0 * p.2, F 0 1 * p.1 + F 1 1 * p.2) (F 0 0 * q.1 + F 1 0 * q.2, F 0 1 * q.1 + F 1 1 * q.2); All goals completed! 🐙
_ = (((F 0 1) * p.1 + (F 1 1) * p.2) *
((F 0 0) * q.1 + (F 1 0) * q.2)) -
(((F 0 1) * q.1 + (F 1 1) * q.2) *
((F 0 0) * p.1 + (F 1 0) * p.2))
:= d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp (F 0 0 * p.1 + F 1 0 * p.2, F 0 1 * p.1 + F 1 1 * p.2) (F 0 0 * q.1 + F 1 0 * q.2, F 0 1 * q.1 + F 1 1 * q.2) =
(F 0 1 * p.1 + F 1 1 * p.2) * (F 0 0 * q.1 + F 1 0 * q.2) - (F 0 1 * q.1 + F 1 1 * q.2) * (F 0 0 * p.1 + F 1 0 * p.2) d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ (F 0 0 * p.1 + F 1 0 * p.2, F 0 1 * p.1 + F 1 1 * p.2).2 * (F 0 0 * q.1 + F 1 0 * q.2, F 0 1 * q.1 + F 1 1 * q.2).1 -
(F 0 0 * p.1 + F 1 0 * p.2, F 0 1 * p.1 + F 1 1 * p.2).1 *
(F 0 0 * q.1 + F 1 0 * q.2, F 0 1 * q.1 + F 1 1 * q.2).2 =
(F 0 1 * p.1 + F 1 1 * p.2) * (F 0 0 * q.1 + F 1 0 * q.2) - (F 0 1 * q.1 + F 1 1 * q.2) * (F 0 0 * p.1 + F 1 0 * p.2); d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ (F 0 0 * p.1 + F 1 0 * p.2) * (F 0 1 * q.1 + F 1 1 * q.2) = (F 0 1 * q.1 + F 1 1 * q.2) * (F 0 0 * p.1 + F 1 0 * 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 )
:= d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ (F 0 1 * p.1 + F 1 1 * p.2) * (F 0 0 * q.1 + F 1 0 * q.2) - (F 0 1 * q.1 + F 1 1 * q.2) * (F 0 0 * p.1 + F 1 0 * 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)
:= d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ (F 0 0 * F 1 1 - F 1 0 * F 0 1) * (p.2 * q.1 - p.1 * q.2) = F.det * symp p q d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ F.det * symp p q = (F 0 0 * F 1 1 - F 1 0 * F 0 1) * (p.2 * q.1 - p.1 * q.2); d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ 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); d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ (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.
Lemma3.10
⚠L∃∀N
used by 1
Associated Lean declarations
-
SpecialLinearInverse[complete] -
MatrixMulToDoubleApply[sorry in proof] -
SpecialLinearDet[complete] -
FactorByInverse[complete] -
symp_adjoint[complete]
If F ∈ \SL(2,ℤ_d) then
\braket{\p,F\q} \equiv \braket{F^{-1}\p,\q} \pmod{d}
for all \p,\q ∈ ℤ.
Proof
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.10
Associated Lean declarations
-
SpecialLinearInverse[complete]
-
MatrixMulToDoubleApply[sorry in proof]
-
SpecialLinearDet[complete]
-
FactorByInverse[complete]
-
symp_adjoint[complete]
Associated Lean declarations
-
SpecialLinearInverse[complete] -
MatrixMulToDoubleApply[sorry in proof] -
SpecialLinearDet[complete] -
FactorByInverse[complete] -
symp_adjoint[complete]
def SpecialLinearInverse
(F : Matrix.SpecialLinearGroup (Fin 2) (ZMod d))
: Matrix.SpecialLinearGroup (Fin 2) (ZMod d) :=
Matrix.SpecialLinearGroup.hasInv.inv F
lemma MatrixMulToDoubleApply
(F G : Matrix (Fin 2) (Fin 2) (ZMod d))
(p : ZMod d × ZMod d) :
pair_apply_mat d F (pair_apply_mat d G p)
= pair_apply_mat d (F * G) p
:= d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)G:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ pair_apply_mat d F (pair_apply_mat d G p) = pair_apply_mat d (F * G) p d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)G:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ (F 0 0 * (pair_apply_mat d G p).1 + F 1 0 * (pair_apply_mat d G p).2,
F 0 1 * (pair_apply_mat d G p).1 + F 1 1 * (pair_apply_mat d G p).2) =
pair_apply_mat d (F * G) p; d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)G:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ (F 0 0 * (G 0 0 * p.1 + G 1 0 * p.2, G 0 1 * p.1 + G 1 1 * p.2).1 +
F 1 0 * (G 0 0 * p.1 + G 1 0 * p.2, G 0 1 * p.1 + G 1 1 * p.2).2,
F 0 1 * (G 0 0 * p.1 + G 1 0 * p.2, G 0 1 * p.1 + G 1 1 * p.2).1 +
F 1 1 * (G 0 0 * p.1 + G 1 0 * p.2, G 0 1 * p.1 + G 1 1 * p.2).2) =
pair_apply_mat d (F * G) p; d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)G:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ (F 0 0 * (G 0 0 * p.1 + G 1 0 * p.2, G 0 1 * p.1 + G 1 1 * p.2).1 +
F 1 0 * (G 0 0 * p.1 + G 1 0 * p.2, G 0 1 * p.1 + G 1 1 * p.2).2,
F 0 1 * (G 0 0 * p.1 + G 1 0 * p.2, G 0 1 * p.1 + G 1 1 * p.2).1 +
F 1 1 * (G 0 0 * p.1 + G 1 0 * p.2, G 0 1 * p.1 + G 1 1 * p.2).2) =
((F * G) 0 0 * p.1 + (F * G) 1 0 * p.2, (F * G) 0 1 * p.1 + (F * G) 1 1 * p.2); d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)G:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ F 0 0 * (G 0 0 * p.1 + G 1 0 * p.2) + F 1 0 * (G 0 1 * p.1 + G 1 1 * p.2) = (F * G) 0 0 * p.1 + (F * G) 1 0 * p.2 ∧
F 0 1 * (G 0 0 * p.1 + G 1 0 * p.2) + F 1 1 * (G 0 1 * p.1 + G 1 1 * p.2) = (F * G) 0 1 * p.1 + (F * G) 1 1 * p.2; d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)G:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ F 0 0 * (G 0 0 * p.1 + G 1 0 * p.2) + F 1 0 * (G 0 1 * p.1 + G 1 1 * p.2) = (F * G) 0 0 * p.1 + (F * G) 1 0 * p.2d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)G:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ F 0 1 * (G 0 0 * p.1 + G 1 0 * p.2) + F 1 1 * (G 0 1 * p.1 + G 1 1 * p.2) = (F * G) 0 1 * p.1 + (F * G) 1 1 * p.2; d:ℕinst✝:NeZero dF:Matrix (Fin 2) (Fin 2) (ZMod d)G:Matrix (Fin 2) (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ F 0 1 * (G 0 0 * p.1 + G 1 0 * p.2) + F 1 1 * (G 0 1 * p.1 + G 1 1 * p.2) = (F * G) 0 1 * p.1 + (F * G) 1 1 * p.2; All goals completed! 🐙
-- Find a way to unfold matrix product
lemma SpecialLinearDet
(F : Matrix.SpecialLinearGroup (Fin 2) (ZMod d)):
Matrix.det (CoeFun.coe F) = 1
:= d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)⊢ Matrix.det (CoeFun.coe F) = 1 All goals completed! 🐙
lemma FactorByInverse
(F : Matrix.SpecialLinearGroup (Fin 2) (ZMod d))
(p : ZMod d × ZMod d) :
pair_apply_mat d ↑((F * F⁻¹) :
Matrix.SpecialLinearGroup (Fin 2) (ZMod d)) p = p :=
d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ pair_apply_mat d (↑(F * F⁻¹)) p = p d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ pair_apply_mat d (↑1) p = p; d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ pair_apply_mat d 1 p = p; d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ (pair_apply_mat.vecForm d 1 p 0, pair_apply_mat.vecForm d 1 p 1) = p;
d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod d⊢ (Matrix.vecMul (fun i => if ↑i = 0 then p.1 else p.2) 1 0, Matrix.vecMul (fun i => if ↑i = 0 then p.1 else p.2) 1 1) = p; All goals completed! 🐙
lemma symp_adjoint
(F : Matrix.SpecialLinearGroup (Fin 2) (ZMod d))
(p q : ZMod d × ZMod d) :
(symp p (pair_apply_mat d F q)) =
(symp (pair_apply_mat d (SpecialLinearInverse d F) p) q)
:= d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp p (pair_apply_mat d (↑F) q) = symp (pair_apply_mat d (↑(SpecialLinearInverse d F)) p) q calc
symp p (pair_apply_mat d F q) =
symp
(pair_apply_mat d ((F * (SpecialLinearInverse d F))
: Matrix.SpecialLinearGroup (Fin 2) (ZMod d)) p)
(pair_apply_mat d F q)
:= d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp p (pair_apply_mat d (↑F) q) = symp (pair_apply_mat d (↑(F * SpecialLinearInverse d F)) p) (pair_apply_mat d (↑F) q) d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp (pair_apply_mat d (↑(F * SpecialLinearInverse d F)) p) (pair_apply_mat d (↑F) q) = symp p (pair_apply_mat d (↑F) q); d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp (pair_apply_mat d (↑(F * F⁻¹)) p) (pair_apply_mat d (↑F) q) = symp p (pair_apply_mat d (↑F) q); All goals completed! 🐙
_ = (Matrix.det
(Matrix.SpecialLinearGroup.instCoeFun.coe F)) *
symp (pair_apply_mat d (SpecialLinearInverse d F) p) q
:= d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp (pair_apply_mat d (↑(F * SpecialLinearInverse d F)) p) (pair_apply_mat d (↑F) q) =
Matrix.det (CoeFun.coe F) * symp (pair_apply_mat d (↑(SpecialLinearInverse d F)) p) q d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp (pair_apply_mat d (↑F * ↑(SpecialLinearInverse d F)) p) (pair_apply_mat d (↑F) q) =
Matrix.det (CoeFun.coe F) * symp (pair_apply_mat d (↑(SpecialLinearInverse d F)) p) q; d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ symp (pair_apply_mat d (↑F) (pair_apply_mat d (↑(SpecialLinearInverse d F)) p)) (pair_apply_mat d (↑F) q) =
Matrix.det (CoeFun.coe F) * symp (pair_apply_mat d (↑(SpecialLinearInverse d F)) p) q; All goals completed! 🐙
_ = symp (pair_apply_mat d (SpecialLinearInverse d F) p) q
:= d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ Matrix.det (CoeFun.coe F) * symp (pair_apply_mat d (↑(SpecialLinearInverse d F)) p) q =
symp (pair_apply_mat d (↑(SpecialLinearInverse d F)) p) q d:ℕinst✝:NeZero dF:Matrix.SpecialLinearGroup (Fin 2) (ZMod d)p:ZMod d × ZMod dq:ZMod d × ZMod d⊢ 1 * symp (pair_apply_mat d (↑(SpecialLinearInverse d F)) p) q =
symp (pair_apply_mat d (↑(SpecialLinearInverse d F)) p) q; All goals completed! 🐙