Symplectic transvections

Let ω(x, y) = xᵀ J y be the standard alternating form on Fin (m + m) → R, where J is the transported form TauCeti.JFin. For a vector v and a scalar c, the symplectic transvection

τ_{v,c} : x ↦ x + c ω(v, x) v,        τ_{v,c} = 1 + c v (vᵀ J)

preserves ω, because ω(v, v) = 0. This file constructs τ_{v,c} in the standard symplectic group TauCeti.GLSymplecticFin m R over an arbitrary commutative ring and proves its basic laws: τ_{v,a} τ_{v,b} = τ_{v,a+b}, τ_{a v,c} = τ_{v,a²c}, and g τ_{v,c} g⁻¹ = τ_{g v,c} for a symplectic g. Its matrix is the transvection Matrix.unitaryTransvection (JFin m R) (RingHom.id R) v c of the alternating form, so these matrix laws specialize the general ones of Matrix.unitaryTransvection with σ = id and ε = -1.

The standard root elements are products of symplectic transvections. A long-root element is a single transvection along a coordinate vector. For a short root, if u and w span a totally isotropic plane then τ_{u+w,c} τ_{u,-c} τ_{w,-c} = 1 + c (u (wᵀ J) + w (uᵀ J)), and the three short-root families are of this form for suitable coordinate vectors. Since the root subgroups generate the symplectic group over a field (TauCeti.GLSymplecticFin.eq_top_of_root_subgroups), so do the symplectic transvections. Together with the conjugation law, this is what makes the symplectic transvections along the points of projective space an Iwasawa structure, the input of Iwasawa's simplicity criterion for the projective symplectic groups.

Main declarations

• TauCeti.GLSymplecticFin.symplecticTransvection: the transvection τ_{v,c}, with its matrix TauCeti.GLSymplecticFin.coe_symplecticTransvection and its action on vectors TauCeti.GLSymplecticFin.coe_symplecticTransvection_mulVec; as a linear map it is Mathlib's LinearMap.transvection (TauCeti.GLSymplecticFin.toLin'_symplecticTransvection).
• TauCeti.GLSymplecticFin.symplecticTransvectionHom: the one-parameter subgroup c ↦ τ_{v,c}.
• TauCeti.GLSymplecticFin.symplecticTransvection_smul: rescaling the vector.
• TauCeti.GLSymplecticFin.mul_symplecticTransvection_mul_inv: the conjugation law.
• TauCeti.GLSymplecticFin.positiveLongRootTransvectionUnit_eq_symplecticTransvection, TauCeti.GLSymplecticFin.differenceShortRootUnit_eq_symplecticTransvection and their siblings: every root element is a product of at most three symplectic transvections.
• TauCeti.GLSymplecticFin.eq_top_of_symplecticTransvection_mem: over a field, the symplectic transvections generate the symplectic group.

References

• E. Artin, Geometric Algebra (1957), Chapter III, §§4--5.
• D. E. Taylor, The Geometry of the Classical Groups (1992), Chapter 8.

def TauCeti.GLSymplecticFin.symplecticTransvection {R : Type u} [CommRing R] {m : ℕ} (v : Fin (m + m) → R) (c : R) : ↥(GLSymplecticFin m R)

The symplectic transvection τ_{v,c} : x ↦ x + c ω(v, x) v along the vector v, where ω(x, y) = xᵀ J y is the standard alternating form. Its matrix is 1 + c v (vᵀ J) (TauCeti.GLSymplecticFin.coe_symplecticTransvection), built as the rank-one perturbation TauCeti.oneSubVecMulVecGL of the identity by (-c) v (vᵀ J).

@[simp]

theorem TauCeti.GLSymplecticFin.coe_symplecticTransvection {R : Type u} [CommRing R] {m : ℕ} (v : Fin (m + m) → R) (c : R) : ↑↑(symplecticTransvection v c) = 1 + c • Matrix.vecMulVec v (Matrix.vecMul v (JFin m R))

The matrix of the symplectic transvection τ_{v,c} is 1 + c v (vᵀ J).

theorem TauCeti.GLSymplecticFin.coe_symplecticTransvection_mulVec {R : Type u} [CommRing R] {m : ℕ} (v : Fin (m + m) → R) (c : R) (x : Fin (m + m) → R) : (↑↑(symplecticTransvection v c)).mulVec x = x + (c * v ⬝ᵥ (JFin m R).mulVec x) • v

The symplectic transvection τ_{v,c} sends x to x + c ω(v, x) v.

theorem TauCeti.GLSymplecticFin.toLin'_symplecticTransvection {R : Type u} [CommRing R] {m : ℕ} (v : Fin (m + m) → R) (c : R) : Matrix.toLin' ↑↑(symplecticTransvection v c) = (c • (Matrix.toBilin' (JFin m R)) v).transvection v

As a linear map, the symplectic transvection τ_{v,c} is Mathlib's transvection x ↦ x + f x • v for the linear form f = c ω(v, ·).

@[simp]

theorem TauCeti.GLSymplecticFin.symplecticTransvection_zero_right {R : Type u} [CommRing R] {m : ℕ} (v : Fin (m + m) → R) : symplecticTransvection v 0 = 1

The transvection with parameter zero is the identity.

@[simp]

theorem TauCeti.GLSymplecticFin.symplecticTransvection_zero_left {R : Type u} [CommRing R] {m : ℕ} (c : R) : symplecticTransvection 0 c = 1

The transvection along the zero vector is the identity.

@[simp]

theorem TauCeti.GLSymplecticFin.symplecticTransvection_add {R : Type u} [CommRing R] {m : ℕ} (v : Fin (m + m) → R) (a b : R) : symplecticTransvection v (a + b) = symplecticTransvection v a * symplecticTransvection v b

Adding parameters multiplies transvections along the same vector.

@[simp]

theorem TauCeti.GLSymplecticFin.symplecticTransvection_inv {R : Type u} [CommRing R] {m : ℕ} (v : Fin (m + m) → R) (c : R) : (symplecticTransvection v c)⁻¹ = symplecticTransvection v (-c)

Inverting a transvection negates its parameter.

theorem TauCeti.GLSymplecticFin.symplecticTransvection_smul {R : Type u} [CommRing R] {m : ℕ} (a : R) (v : Fin (m + m) → R) (c : R) : symplecticTransvection (a • v) c = symplecticTransvection v (a ^ 2 * c)

Rescaling the vector of a transvection multiplies the parameter by the square of the scalar: τ_{a v,c} = τ_{v,a²c}.

def TauCeti.GLSymplecticFin.symplecticTransvectionHom {R : Type u} [CommRing R] {m : ℕ} (v : Fin (m + m) → R) : Multiplicative R →* ↥(GLSymplecticFin m R)

The symplectic transvections along a vector form a one-parameter subgroup.

@[simp]

theorem TauCeti.GLSymplecticFin.symplecticTransvectionHom_apply {R : Type u} [CommRing R] {m : ℕ} (v : Fin (m + m) → R) (c : Multiplicative R) : (symplecticTransvectionHom v) c = symplecticTransvection v (Multiplicative.toAdd c)

The one-parameter subgroup of transvections along v sends c to τ_{v,c}.

theorem TauCeti.GLSymplecticFin.range_symplecticTransvectionHom_smul {m : ℕ} {K : Type u} [Field K] {a : K} (ha : a ≠ 0) (v : Fin (m + m) → K) : (symplecticTransvectionHom (a • v)).range = (symplecticTransvectionHom v).range

Rescaling the vector by a nonzero scalar does not change the group of transvections along it.

theorem TauCeti.GLSymplecticFin.mul_symplecticTransvection_mul_inv {R : Type u} [CommRing R] {m : ℕ} (g : ↥(GLSymplecticFin m R)) (v : Fin (m + m) → R) (c : R) : g * symplecticTransvection v c * g⁻¹ = symplecticTransvection ((↑↑g).mulVec v) c

Conjugating a symplectic transvection by a symplectic matrix g moves its vector by g: g τ_{v,c} g⁻¹ = τ_{g v,c}.

Root elements as products of transvections

theorem TauCeti.GLSymplecticFin.positiveLongRootTransvectionUnit_eq_symplecticTransvection {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) (c : R) : positiveLongRootTransvectionUnit i c = symplecticTransvection (Pi.single (finSumFinEquiv (Sum.inl i)) 1) (-c)

The positive long-root element x_{2eᵢ}(c) is the transvection along the i-th upper coordinate vector with parameter -c.

theorem TauCeti.GLSymplecticFin.negativeLongRootTransvectionUnit_eq_symplecticTransvection {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) (c : R) : negativeLongRootTransvectionUnit i c = symplecticTransvection (Pi.single (finSumFinEquiv (Sum.inr i)) 1) c

The negative long-root element x_{-2eᵢ}(c) is the transvection along the i-th lower coordinate vector with parameter c.

theorem TauCeti.GLSymplecticFin.coe_symplecticTransvection_add_mul_mul {R : Type u} [CommRing R] {m : ℕ} {u w : Fin (m + m) → R} (huw : u ⬝ᵥ (JFin m R).mulVec w = 0) (c : R) : ↑↑(symplecticTransvection (u + w) c * symplecticTransvection u (-c) * symplecticTransvection w (-c)) = 1 + c • (Matrix.vecMulVec u (Matrix.vecMul w (JFin m R)) + Matrix.vecMulVec w (Matrix.vecMul u (JFin m R)))

Three transvections along a totally isotropic plane. If ω(u, w) = 0, then τ_{u+w,c} τ_{u,-c} τ_{w,-c} = 1 + c (u (wᵀ J) + w (uᵀ J)).

theorem TauCeti.GLSymplecticFin.differenceShortRootUnit_eq_symplecticTransvection {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (c : R) : differenceShortRootUnit hij c = symplecticTransvection (Pi.single (finSumFinEquiv (Sum.inl i)) 1 + Pi.single (finSumFinEquiv (Sum.inr j)) 1) c * symplecticTransvection (Pi.single (finSumFinEquiv (Sum.inl i)) 1) (-c) * symplecticTransvection (Pi.single (finSumFinEquiv (Sum.inr j)) 1) (-c)

The difference short-root element x_{eᵢ-eⱼ}(c) is a product of three transvections, along the i-th upper and j-th lower coordinate vectors and their sum.

theorem TauCeti.GLSymplecticFin.positiveSumShortRootUnit_eq_symplecticTransvection {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (c : R) : positiveSumShortRootUnit hij c = symplecticTransvection (Pi.single (finSumFinEquiv (Sum.inl i)) 1 + Pi.single (finSumFinEquiv (Sum.inl j)) 1) (-c) * symplecticTransvection (Pi.single (finSumFinEquiv (Sum.inl i)) 1) c * symplecticTransvection (Pi.single (finSumFinEquiv (Sum.inl j)) 1) c

The positive-sum short-root element x_{eᵢ+eⱼ}(c) is a product of three transvections, along the i-th and j-th upper coordinate vectors and their sum.

theorem TauCeti.GLSymplecticFin.negativeSumShortRootUnit_eq_symplecticTransvection {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (c : R) : negativeSumShortRootUnit hij c = symplecticTransvection (Pi.single (finSumFinEquiv (Sum.inr i)) 1 + Pi.single (finSumFinEquiv (Sum.inr j)) 1) c * symplecticTransvection (Pi.single (finSumFinEquiv (Sum.inr i)) 1) (-c) * symplecticTransvection (Pi.single (finSumFinEquiv (Sum.inr j)) 1) (-c)

The negative-sum short-root element x_{-eᵢ-eⱼ}(c) is a product of three transvections, along the i-th and j-th lower coordinate vectors and their sum.

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.hom_apply_mem_of_symplecticTransvection_mem {R : Type u} [CommRing R] {m : ℕ} (H : Subgroup ↥(GLSymplecticFin m R)) (h : ∀ (v : Fin (m + m) → R) (c : R), symplecticTransvection v c ∈ H) (root : RootSubgroupIndex m) (c : Multiplicative R) : root.hom c ∈ H

A subgroup containing every symplectic transvection contains every standard root element.

theorem TauCeti.GLSymplecticFin.eq_top_of_symplecticTransvection_mem {m : ℕ} {K : Type u} [Field K] (H : Subgroup ↥(GLSymplecticFin m K)) (h : ∀ (v : Fin (m + m) → K) (c : K), symplecticTransvection v c ∈ H) : H = ⊤

The symplectic transvections generate the symplectic group over a field. A subgroup of Sp_{2m}(K) containing every symplectic transvection is the whole group.