The symplectic group as a subgroup of the general linear group

For a commutative ring R and a finite index type l, the matrices M with M J Mᵀ = J form Mathlib's Matrix.symplecticGroup l R, a Submonoid of the matrix monoid whose elements happen to be invertible: its inverse is a separate Inv instance, and its Group structure is built by hand. The algebraic-group development instead needs the symplectic group inside the general linear group — the concrete target that the points of the symplectic group scheme will be identified with, the way TauCeti.GL2Borel is the concrete target for the Borel coordinate Hopf algebra.

TauCeti.GLSymplectic is that subgroup of GL (l ⊕ l) R. Its carrier is literally membership of the underlying matrix in Matrix.symplecticGroup l R, so the defining conditions M J Mᵀ = J and Mᵀ J M = J transfer directly, and TauCeti.GLSymplectic.mulEquivSymplecticGroup identifies the subgroup with Mathlib's group so that neither view is reproved from the other. Invertibility costs nothing: Mathlib's symplectic group is a group, so MonoidHom.toHomUnits reads it into the general linear group, which is what makes the two carriers agree, and closure under the unit inverse is Mathlib's computation M⁻¹ = (-J) Mᵀ J (SymplecticGroup.inv_eq_symplectic_inv) transported across Matrix.coe_units_inv.

Everything works over an arbitrary commutative ring and an arbitrary finite index type, including the empty index type and the zero ring; there is no nontriviality, rank, or characteristic hypothesis. The index type is l ⊕ l throughout, matching Matrix.J.

The final sections construct the elementary one-parameter subgroups belonging to the long roots ±2eᵢ and the short roots eᵢ-eⱼ, eᵢ+eⱼ, and -eᵢ-eⱼ in Fin (m+m) coordinates. The symplectic coordinate Hopf algebra and group scheme live in TauCeti.Algebra.AlgebraicGroup.Symplectic.Basic; their root-subgroup morphisms live in TauCeti.Algebra.AlgebraicGroup.Symplectic.RootSubgroup.Basic.

Main declarations

• TauCeti.GLSymplectic: the symplectic matrices as a subgroup of GL (l ⊕ l) R.
• TauCeti.GLSymplectic.mem_iff and TauCeti.GLSymplectic.mem_iff': the two standard forms of the defining condition, M J Mᵀ = J and Mᵀ J M = J.
• TauCeti.GLSymplectic.ofSymplecticGroup: Mathlib's symplectic group, read into the general linear group as a monoid homomorphism.
• TauCeti.GLSymplectic.mulEquivSymplecticGroup: the group identification with Matrix.symplecticGroup.
• TauCeti.GLSymplectic.symJ: the standard alternating form, as an element of the subgroup.
• TauCeti.GLSymplectic.map: the group morphism induced by a ring morphism of value rings, restricting Matrix.GeneralLinearGroup.map.
• TauCeti.JFin and TauCeti.GLSymplecticFin: the alternating form and the symplectic subgroup in Fin (m + m) coordinates, transported along finSumFinEquiv, with TauCeti.GLSymplecticFin.mulEquivGLSymplectic identifying the two presentations. The Fin-indexed form is what the symplectic coordinate Hopf algebra cuts out of GLₘ₊ₘ, whose coordinate ring is Fin-indexed.
• TauCeti.GLSymplecticFin.positiveLongRootTransvectionHom and negativeLongRootTransvectionHom: the two families of long-root one-parameter subgroups.
• TauCeti.GLSymplecticFin.differenceShortRootHom, positiveSumShortRootHom, and negativeSumShortRootHom: the three families of short-root one-parameter subgroups.
• TauCeti.GLSymplecticFin.ShortRootFamily: a uniform index for the three short-root families.
• TauCeti.GLSymplecticFin.RootSubgroupIndex: a uniform index for all long- and short-root one-parameter subgroups.

References

• J. S. Milne, Algebraic Groups (2017), 2.10(c), where Sp₂ₙ is introduced as the subgroup of GL₂ₙ preserving a nondegenerate alternating form.

The identification with Mathlib's Matrix.symplecticGroup is routine and is not adapted from the reference.

def TauCeti.GLSymplectic (l : Type u_1) [DecidableEq l] [Fintype l] (R : Type u) [CommRing R] : Subgroup (GL (l ⊕ l) R)

The symplectic group as a subgroup of GL (l ⊕ l) R: the invertible matrices whose underlying matrix satisfies M J Mᵀ = J. TauCeti.GLSymplectic.mulEquivSymplecticGroup identifies it with Mathlib's submonoid form Matrix.symplecticGroup.

Equations

• TauCeti.GLSymplectic l R = { carrier := {M : GL (l ⊕ l) R | ↑M ∈ Matrix.symplecticGroup l R}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem TauCeti.GLSymplectic.mem_iff_mem_symplecticGroup {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u} [CommRing R] {M : GL (l ⊕ l) R} : M ∈ GLSymplectic l R ↔ ↑M ∈ Matrix.symplecticGroup l R

An invertible matrix lies in the symplectic subgroup exactly when its underlying matrix lies in Mathlib's Matrix.symplecticGroup.

theorem TauCeti.GLSymplectic.mem_iff {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u} [CommRing R] {M : GL (l ⊕ l) R} : M ∈ GLSymplectic l R ↔ ↑M * Matrix.J l R * (↑M).transpose = Matrix.J l R

Membership in the symplectic subgroup, in the form M J Mᵀ = J.

theorem TauCeti.GLSymplectic.mem_iff' {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u} [CommRing R] {M : GL (l ⊕ l) R} : M ∈ GLSymplectic l R ↔ (↑M).transpose * Matrix.J l R * ↑M = Matrix.J l R

Membership in the symplectic subgroup, in the transposed form Mᵀ J M = J.

def TauCeti.GLSymplectic.ofSymplecticGroup (l : Type u_1) [DecidableEq l] [Fintype l] (R : Type u) [CommRing R] : ↥(Matrix.symplecticGroup l R) →* GL (l ⊕ l) R

Mathlib's symplectic group, read into the general linear group: MonoidHom.toHomUnits of the inclusion of Matrix.symplecticGroup into the matrix monoid, whose inverses are the symplectic group's own.

Equations

• TauCeti.GLSymplectic.ofSymplecticGroup l R = (Matrix.symplecticGroup l R).subtype.toHomUnits

@[simp]

theorem TauCeti.GLSymplectic.coe_ofSymplecticGroup (l : Type u_1) [DecidableEq l] [Fintype l] (R : Type u) [CommRing R] (S : ↥(Matrix.symplecticGroup l R)) : ↑((ofSymplecticGroup l R) S) = ↑S

A symplectic matrix, read into the general linear group, has itself as underlying matrix.

theorem TauCeti.GLSymplectic.ofSymplecticGroup_mem (l : Type u_1) [DecidableEq l] [Fintype l] (R : Type u) [CommRing R] (S : ↥(Matrix.symplecticGroup l R)) : (ofSymplecticGroup l R) S ∈ GLSymplectic l R

A symplectic matrix, read into the general linear group, lies in the symplectic subgroup.

def TauCeti.GLSymplectic.mulEquivSymplecticGroup (l : Type u_1) [DecidableEq l] [Fintype l] (R : Type u) [CommRing R] : ↥(GLSymplectic l R) ≃* ↥(Matrix.symplecticGroup l R)

The symplectic subgroup of the general linear group is Mathlib's symplectic group. The two carriers agree because a symplectic matrix is invertible in Mathlib's symplectic group, so the equivalence is the identity on underlying matrices; its content is that the two group structures match.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GLSymplectic.coe_mulEquivSymplecticGroup (l : Type u_1) [DecidableEq l] [Fintype l] (R : Type u) [CommRing R] (M : ↥(GLSymplectic l R)) : ↑((mulEquivSymplecticGroup l R) M) = ↑↑M

The equivalence with Mathlib's symplectic group keeps the underlying matrix.

def TauCeti.GLSymplectic.symJ (l : Type u_1) [DecidableEq l] [Fintype l] (R : Type u) [CommRing R] : ↥(GLSymplectic l R)

The standard alternating form Matrix.J, as an element of the symplectic subgroup.

Equations

• TauCeti.GLSymplectic.symJ l R = ⟨(TauCeti.GLSymplectic.ofSymplecticGroup l R) (SymplecticGroup.symJ l R), ⋯⟩

@[simp]

theorem TauCeti.GLSymplectic.coe_symJ (l : Type u_1) [DecidableEq l] [Fintype l] (R : Type u) [CommRing R] : ↑↑(symJ l R) = Matrix.J l R

The underlying matrix of symJ is the standard alternating form Matrix.J.

theorem TauCeti.GLSymplectic.map_mem {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) {M : GL (l ⊕ l) R} (hM : M ∈ GLSymplectic l R) : (Matrix.GeneralLinearGroup.map f) M ∈ GLSymplectic l S

A ring morphism of value rings carries symplectic matrices to symplectic matrices.

def TauCeti.GLSymplectic.map (l : Type u_1) [DecidableEq l] [Fintype l] {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) : ↥(GLSymplectic l R) →* ↥(GLSymplectic l S)

The group morphism between symplectic subgroups induced by a ring morphism of value rings: the restriction of Matrix.GeneralLinearGroup.map, which acts entrywise.

Equations

• TauCeti.GLSymplectic.map l f = { toFun := fun (M : ↥(TauCeti.GLSymplectic l R)) => ⟨(Matrix.GeneralLinearGroup.map f) ↑M, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.GLSymplectic.coe_map {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (M : ↥(GLSymplectic l R)) : ↑((map l f) M) = (Matrix.GeneralLinearGroup.map f) ↑M

The underlying general-linear value of the induced morphism is Matrix.GeneralLinearGroup.map.

@[simp]

theorem TauCeti.GLSymplectic.map_id {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u} [CommRing R] : map l (RingHom.id R) = MonoidHom.id ↥(GLSymplectic l R)

The map induced by the identity ring morphism is the identity.

@[simp]

theorem TauCeti.GLSymplectic.map_comp {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] {T : Type u_3} [CommRing T] (f : R →+* S) (g : S →+* T) : map l (g.comp f) = (map l g).comp (map l f)

The map induced by a composite of ring morphisms is the composite of the induced maps.

The Fin-indexed presentation

The coordinate ring of GLₙ is indexed by Fin n, so the symplectic group scheme cuts its subgroup out of GL (Fin (m + m)) A rather than GL (Fin m ⊕ Fin m) A. This section transports the alternating form and the subgroup along finSumFinEquiv and records that nothing is lost.

def TauCeti.JFin (m : ℕ) (R : Type u) [CommRing R] : Matrix (Fin (m + m)) (Fin (m + m)) R

The standard alternating form in Fin (m + m) coordinates: Matrix.J, transported along finSumFinEquiv.

Equations

• TauCeti.JFin m R = (Matrix.J (Fin m) R).submatrix ⇑finSumFinEquiv.symm ⇑finSumFinEquiv.symm

@[simp]

theorem TauCeti.JFin_map (m : ℕ) {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) : (JFin m R).map ⇑f = JFin m S

Entrywise application of a ring morphism carries the transported alternating form to the transported alternating form.

@[simp]

theorem TauCeti.JFin_submatrix (m : ℕ) (R : Type u) [CommRing R] : (JFin m R).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = Matrix.J (Fin m) R

Transporting back along finSumFinEquiv recovers Matrix.J.

theorem TauCeti.JFin_two_eq (R : Type u) [CommRing R] : JFin 2 R = !![0, 0, -1, 0; 0, 0, 0, -1; 1, 0, 0, 0; 0, 1, 0, 0]

The transported alternating form of Sp₄, written out.

theorem TauCeti.JFin_mul_self (m : ℕ) (R : Type u) [CommRing R] : JFin m R * JFin m R = -1

The transported alternating form squares to -1, which is Mathlib's Matrix.J_squared read through the reindexing.

theorem TauCeti.submatrix_mem_symplecticGroup {m : ℕ} {R : Type u} [CommRing R] {g : Matrix (Fin (m + m)) (Fin (m + m)) R} (hg : g * JFin m R * g.transpose = JFin m R) : g.submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv ∈ Matrix.symplecticGroup (Fin m) R

A matrix preserving the transported alternating form is a symplectic matrix in Mathlib's sum-indexed coordinates. This is how a consumer reads off what the symplectic condition gives beyond the defining equation, rather than reproving it in Fin (m + m) coordinates.

theorem TauCeti.mul_JFin_mul_transpose_of_submatrix_mem_symplecticGroup {m : ℕ} {R : Type u} [CommRing R] {g : Matrix (Fin (m + m)) (Fin (m + m)) R} (hg : g.submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv ∈ Matrix.symplecticGroup (Fin m) R) : g * JFin m R * g.transpose = JFin m R

Conversely, a matrix that is symplectic in Mathlib's sum-indexed coordinates preserves the transported alternating form.

theorem TauCeti.submatrix_neg_JFin_mul_transpose_mul_JFin {m : ℕ} {R : Type u} [CommRing R] {g : Matrix (Fin (m + m)) (Fin (m + m)) R} : (-(JFin m R * g.transpose * JFin m R)).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = -Matrix.J (Fin m) R * (g.submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv).transpose * Matrix.J (Fin m) R

The symplectic adjoint, read in Mathlib's sum-indexed coordinates, is the adjoint of the reindexed matrix. This is the transport that identifies it with the inverse in Matrix.symplecticGroup.

theorem TauCeti.neg_JFin_mul_transpose_mul_JFin_mul_JFin_mul_transpose {m : ℕ} {R : Type u} [CommRing R] {g : Matrix (Fin (m + m)) (Fin (m + m)) R} (hg : g * JFin m R * g.transpose = JFin m R) : -(JFin m R * g.transpose * JFin m R) * JFin m R * (-(JFin m R * g.transpose * JFin m R)).transpose = JFin m R

The symplectic adjoint of a matrix preserving the transported alternating form preserves it too. The adjoint is the inverse, and Mathlib's symplectic matrices are closed under inversion.

theorem TauCeti.transpose_mul_JFin_mul_self {m : ℕ} {R : Type u} [CommRing R] {g : Matrix (Fin (m + m)) (Fin (m + m)) R} (hg : g * JFin m R * g.transpose = JFin m R) : g.transpose * JFin m R * g = JFin m R

The column form of the symplectic condition, which is Mathlib's SymplecticGroup.mem_iff' read through the reindexing.

def TauCeti.GLSymplecticFin (m : ℕ) (R : Type u) [CommRing R] : Subgroup (GL (Fin (m + m)) R)

The symplectic subgroup of GL (Fin (m + m)) R: the pullback of TauCeti.GLSymplectic along the reindexing isomorphism.

Equations

• TauCeti.GLSymplecticFin m R = Subgroup.comap (finSumFinEquiv.symm.reindexGL R).toMonoidHom (TauCeti.GLSymplectic (Fin m) R)

@[simp]

theorem TauCeti.GLSymplecticFin.mem_iff {m : ℕ} {R : Type u} [CommRing R] {M : GL (Fin (m + m)) R} : M ∈ GLSymplecticFin m R ↔ ↑M * JFin m R * (↑M).transpose = JFin m R

Membership in the Fin-indexed symplectic subgroup is the defining condition M J Mᵀ = J against the transported alternating form.

theorem TauCeti.GLSymplecticFin.mem_iff' {m : ℕ} {R : Type u} [CommRing R] {M : GL (Fin (m + m)) R} : M ∈ GLSymplecticFin m R ↔ (↑M).transpose * JFin m R * ↑M = JFin m R

Membership in the Fin-indexed symplectic subgroup, in the transposed form Mᵀ J M = J.

def TauCeti.GLSymplecticFin.mulEquivGLSymplectic (m : ℕ) (R : Type u) [CommRing R] : ↥(GLSymplecticFin m R) ≃* ↥(GLSymplectic (Fin m) R)

The two presentations of the symplectic subgroup agree: reindexing along finSumFinEquiv identifies the Fin (m + m)-indexed subgroup with the Fin m ⊕ Fin m-indexed one.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GLSymplecticFin.coe_mulEquivGLSymplectic (m : ℕ) (R : Type u) [CommRing R] (M : ↥(GLSymplecticFin m R)) : ↑((mulEquivGLSymplectic m R) M) = (finSumFinEquiv.symm.reindexGL R) ↑M

The identification of the two presentations reindexes the underlying invertible matrix along finSumFinEquiv.

def TauCeti.GLSymplecticFin.map (m : ℕ) (R : Type u) [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) : ↥(GLSymplecticFin m R) →* ↥(GLSymplecticFin m S)

A ring morphism carries Fin-indexed symplectic matrices to symplectic matrices.

Equations

• TauCeti.GLSymplecticFin.map m R f = { toFun := fun (M : ↥(TauCeti.GLSymplecticFin m R)) => ⟨(Matrix.GeneralLinearGroup.map f) ↑M, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.GLSymplecticFin.coe_map (m : ℕ) (R : Type u) [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (M : ↥(GLSymplecticFin m R)) : ↑((map m R f) M) = (Matrix.GeneralLinearGroup.map f) ↑M

The underlying general-linear element of a mapped symplectic matrix is its entrywise map.

Long-root transvections

theorem TauCeti.GLSymplecticFin.finSumFinEquiv_inl_ne_inr {m : ℕ} (i j : Fin m) : finSumFinEquiv (Sum.inl i) ≠ finSumFinEquiv (Sum.inr j)

An upper-block and a lower-block index have distinct images in Fin (m + m).

theorem TauCeti.GLSymplecticFin.finSumFinEquiv_inr_ne_inl {m : ℕ} (i j : Fin m) : finSumFinEquiv (Sum.inr i) ≠ finSumFinEquiv (Sum.inl j)

A lower-block and an upper-block index have distinct images in Fin (m + m).

@[simp]

theorem TauCeti.GLSymplecticFin.reindexGL_transvectionUnit {m : ℕ} {R : Type u} [CommRing R] (i j : Fin m ⊕ Fin m) (hij : i ≠ j) (c : R) : (finSumFinEquiv.symm.reindexGL R) (transvectionUnit ⋯ c) = transvectionUnit hij c

Reindexing a transvection from Fin (m + m) coordinates to sum coordinates recovers the transvection at the corresponding sum indices.

def TauCeti.GLSymplecticFin.positiveLongRootTransvectionUnit {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) (c : R) : ↥(GLSymplecticFin m R)

The symplectic matrix x_{2eᵢ}(c) = 1 + c E_{i,m+i}, in Fin (m + m) coordinates.

Equations

• TauCeti.GLSymplecticFin.positiveLongRootTransvectionUnit i c = ⟨TauCeti.transvectionUnit ⋯ c, ⋯⟩

@[simp]

theorem TauCeti.GLSymplecticFin.coe_positiveLongRootTransvectionUnit {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) (c : R) : ↑(positiveLongRootTransvectionUnit i c) = transvectionUnit ⋯ c

The matrix underlying the positive long-root transvection is the corresponding elementary transvection.

def TauCeti.GLSymplecticFin.negativeLongRootTransvectionUnit {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) (c : R) : ↥(GLSymplecticFin m R)

The symplectic matrix x_{-2eᵢ}(c) = 1 + c E_{m+i,i}, in Fin (m + m) coordinates.

Equations

• TauCeti.GLSymplecticFin.negativeLongRootTransvectionUnit i c = ⟨TauCeti.transvectionUnit ⋯ c, ⋯⟩

@[simp]

theorem TauCeti.GLSymplecticFin.coe_negativeLongRootTransvectionUnit {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) (c : R) : ↑(negativeLongRootTransvectionUnit i c) = transvectionUnit ⋯ c

The matrix underlying the negative long-root transvection is the corresponding elementary transvection.

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

The positive long-root transvections form a one-parameter subgroup.

Equations

• One or more equations did not get rendered due to their size.

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

The negative long-root transvections form a one-parameter subgroup.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GLSymplecticFin.positiveLongRootTransvectionHom_apply {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) (c : Multiplicative R) : (positiveLongRootTransvectionHom i) c = positiveLongRootTransvectionUnit i (Multiplicative.toAdd c)

The positive long-root one-parameter subgroup sends c to the transvection with parameter Multiplicative.toAdd c.

@[simp]

theorem TauCeti.GLSymplecticFin.negativeLongRootTransvectionHom_apply {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) (c : Multiplicative R) : (negativeLongRootTransvectionHom i) c = negativeLongRootTransvectionUnit i (Multiplicative.toAdd c)

The negative long-root one-parameter subgroup sends c to the transvection with parameter Multiplicative.toAdd c.

@[simp]

theorem TauCeti.GLSymplecticFin.positiveLongRootTransvectionUnit_add {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) (c d : R) : positiveLongRootTransvectionUnit i (c + d) = positiveLongRootTransvectionUnit i c * positiveLongRootTransvectionUnit i d

Adding parameters multiplies positive long-root transvections.

@[simp]

theorem TauCeti.GLSymplecticFin.positiveLongRootTransvectionUnit_inv {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) (c : R) : (positiveLongRootTransvectionUnit i c)⁻¹ = positiveLongRootTransvectionUnit i (-c)

Inverting a positive long-root transvection negates its parameter.

@[simp]

theorem TauCeti.GLSymplecticFin.negativeLongRootTransvectionUnit_add {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) (c d : R) : negativeLongRootTransvectionUnit i (c + d) = negativeLongRootTransvectionUnit i c * negativeLongRootTransvectionUnit i d

Adding parameters multiplies negative long-root transvections.

@[simp]

theorem TauCeti.GLSymplecticFin.negativeLongRootTransvectionUnit_inv {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) (c : R) : (negativeLongRootTransvectionUnit i c)⁻¹ = negativeLongRootTransvectionUnit i (-c)

Inverting a negative long-root transvection negates its parameter.

@[simp]

theorem TauCeti.GLSymplecticFin.map_positiveLongRootTransvectionUnit {m : ℕ} {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (i : Fin m) (c : R) : (map m R f) (positiveLongRootTransvectionUnit i c) = positiveLongRootTransvectionUnit i (f c)

Positive long-root transvections are natural in the coefficient ring.

@[simp]

theorem TauCeti.GLSymplecticFin.map_negativeLongRootTransvectionUnit {m : ℕ} {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (i : Fin m) (c : R) : (map m R f) (negativeLongRootTransvectionUnit i c) = negativeLongRootTransvectionUnit i (f c)

Negative long-root transvections are natural in the coefficient ring.

theorem TauCeti.GLSymplecticFin.positiveLongRootTransvectionUnit_injective {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) : Function.Injective (positiveLongRootTransvectionUnit i)

Distinct parameters give distinct positive long-root transvections.

theorem TauCeti.GLSymplecticFin.negativeLongRootTransvectionUnit_injective {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) : Function.Injective (negativeLongRootTransvectionUnit i)

Distinct parameters give distinct negative long-root transvections.

Short-root elements

theorem TauCeti.GLSymplecticFin.differenceShortRoot_first_indices_ne {m : ℕ} {i j : Fin m} (hij : i ≠ j) : finSumFinEquiv (Sum.inl i) ≠ finSumFinEquiv (Sum.inl j)

The two indices of the first transvection defining x_{eᵢ-eⱼ} are distinct.

theorem TauCeti.GLSymplecticFin.differenceShortRoot_second_indices_ne {m : ℕ} {i j : Fin m} (hij : i ≠ j) : finSumFinEquiv (Sum.inr j) ≠ finSumFinEquiv (Sum.inr i)

The two indices of the second transvection defining x_{eᵢ-eⱼ} are distinct.

theorem TauCeti.GLSymplecticFin.coe_differenceShortRootTransvectionUnits {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : R) : ↑(transvectionUnit ⋯ c * transvectionUnit ⋯ (-c)) = Matrix.fromBlocks (Matrix.transvection i j c) 0 0 (Matrix.transvection j i (-c))

In sum coordinates, the two elementary matrices defining a difference-root element form a block-diagonal pair of transvections.

def TauCeti.GLSymplecticFin.differenceShortRootHom {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) : Multiplicative R →* ↥(GLSymplecticFin m R)

The one-parameter subgroup attached to the short root eᵢ-eⱼ.

Equations

• TauCeti.GLSymplecticFin.differenceShortRootHom hij = (TauCeti.commutingTransvectionPairHom ⋯ ⋯ ⋯ ⋯ invMonoidHom).codRestrict (TauCeti.GLSymplecticFin m R) ⋯

def TauCeti.GLSymplecticFin.positiveSumShortRootHom {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (_hij : i ≠ j) : Multiplicative R →* ↥(GLSymplecticFin m R)

The one-parameter subgroup attached to the short root eᵢ+eⱼ.

Equations

• TauCeti.GLSymplecticFin.positiveSumShortRootHom _hij = TauCeti.GLSymplecticFin.positiveSumPairedHom✝ i j

def TauCeti.GLSymplecticFin.negativeSumShortRootHom {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (_hij : i ≠ j) : Multiplicative R →* ↥(GLSymplecticFin m R)

The one-parameter subgroup attached to the short root -eᵢ-eⱼ.

Equations

• TauCeti.GLSymplecticFin.negativeSumShortRootHom _hij = TauCeti.GLSymplecticFin.negativeSumPairedHom✝ i j

def TauCeti.GLSymplecticFin.differenceShortRootUnit {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : R) : ↥(GLSymplecticFin m R)

The symplectic short-root element x_{eᵢ-eⱼ}(c) = (1 + c E_{i,j})(1 - c E_{m+j,m+i}).

Equations

• TauCeti.GLSymplecticFin.differenceShortRootUnit hij c = (TauCeti.GLSymplecticFin.differenceShortRootHom hij) (Multiplicative.ofAdd c)

def TauCeti.GLSymplecticFin.positiveSumShortRootUnit {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : R) : ↥(GLSymplecticFin m R)

The paired symplectic element (1 + c E_{i,m+j})(1 + c E_{j,m+i}), which is x_{eᵢ+eⱼ}(c) when i ≠ j.

Equations

• TauCeti.GLSymplecticFin.positiveSumShortRootUnit hij c = (TauCeti.GLSymplecticFin.positiveSumShortRootHom hij) (Multiplicative.ofAdd c)

def TauCeti.GLSymplecticFin.negativeSumShortRootUnit {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : R) : ↥(GLSymplecticFin m R)

The paired symplectic element (1 + c E_{m+i,j})(1 + c E_{m+j,i}), which is x_{-eᵢ-eⱼ}(c) when i ≠ j.

Equations

• TauCeti.GLSymplecticFin.negativeSumShortRootUnit hij c = (TauCeti.GLSymplecticFin.negativeSumShortRootHom hij) (Multiplicative.ofAdd c)

@[simp]

theorem TauCeti.GLSymplecticFin.differenceShortRootHom_apply {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : Multiplicative R) : (differenceShortRootHom hij) c = differenceShortRootUnit hij (Multiplicative.toAdd c)

The difference short-root homomorphism evaluates to its paired transvection.

@[simp]

theorem TauCeti.GLSymplecticFin.positiveSumShortRootHom_apply {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : Multiplicative R) : (positiveSumShortRootHom hij) c = positiveSumShortRootUnit hij (Multiplicative.toAdd c)

The positive-sum short-root homomorphism evaluates to its paired transvection.

@[simp]

theorem TauCeti.GLSymplecticFin.negativeSumShortRootHom_apply {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : Multiplicative R) : (negativeSumShortRootHom hij) c = negativeSumShortRootUnit hij (Multiplicative.toAdd c)

The negative-sum short-root homomorphism evaluates to its paired transvection.

theorem TauCeti.GLSymplecticFin.differenceShortRootUnit_congr {m : ℕ} {R : Type u} [CommRing R] {i j i' j' : Fin m} (hij : i ≠ j) (hij' : i' ≠ j') (hi : i = i') (hj : j = j') (c : R) : differenceShortRootUnit hij c = differenceShortRootUnit hij' c

For a fixed parameter, the difference short-root element depends only on its index pair. Two proofs that the indices differ, and two spellings of the same indices, give the same element.

@[simp]

theorem TauCeti.GLSymplecticFin.coe_differenceShortRootUnit {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : R) : ↑(differenceShortRootUnit hij c) = transvectionUnit ⋯ c * transvectionUnit ⋯ (-c)

The general-linear matrix underlying x_{eᵢ-eⱼ}(c) is its two-transvection formula.

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

The matrix underlying x_{eᵢ-eⱼ}(c), as the identity plus two matrix units.

@[simp]

theorem TauCeti.GLSymplecticFin.coe_positiveSumShortRootUnit {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : R) : ↑(positiveSumShortRootUnit hij c) = transvectionUnit ⋯ c * transvectionUnit ⋯ c

The general-linear matrix underlying x_{eᵢ+eⱼ}(c) is its two-transvection formula.

@[simp]

theorem TauCeti.GLSymplecticFin.coe_negativeSumShortRootUnit {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : R) : ↑(negativeSumShortRootUnit hij c) = transvectionUnit ⋯ c * transvectionUnit ⋯ c

The general-linear matrix underlying x_{-eᵢ-eⱼ}(c) is its two-transvection formula.

theorem TauCeti.GLSymplecticFin.positiveSumShortRootHom_swap {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) : positiveSumShortRootHom hij = positiveSumShortRootHom ⋯

Swapping the two indices does not change a positive-sum short-root homomorphism.

theorem TauCeti.GLSymplecticFin.negativeSumShortRootHom_swap {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) : negativeSumShortRootHom hij = negativeSumShortRootHom ⋯

Swapping the two indices does not change a negative-sum short-root homomorphism.

@[simp]

theorem TauCeti.GLSymplecticFin.map_differenceShortRootUnit {m : ℕ} {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) {i j : Fin m} (hij : i ≠ j) (c : R) : (map m R f) (differenceShortRootUnit hij c) = differenceShortRootUnit hij (f c)

Difference short-root elements commute with change of coefficient ring.

@[simp]

theorem TauCeti.GLSymplecticFin.map_positiveSumShortRootUnit {m : ℕ} {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) {i j : Fin m} (hij : i ≠ j) (c : R) : (map m R f) (positiveSumShortRootUnit hij c) = positiveSumShortRootUnit hij (f c)

Positive-sum short-root elements commute with change of coefficient ring.

@[simp]

theorem TauCeti.GLSymplecticFin.map_negativeSumShortRootUnit {m : ℕ} {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) {i j : Fin m} (hij : i ≠ j) (c : R) : (map m R f) (negativeSumShortRootUnit hij c) = negativeSumShortRootUnit hij (f c)

Negative-sum short-root elements commute with change of coefficient ring.

theorem TauCeti.GLSymplecticFin.differenceShortRootUnit_apply_inl_inl {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : R) : ↑↑(differenceShortRootUnit hij c) (finSumFinEquiv (Sum.inl i)) (finSumFinEquiv (Sum.inl j)) = c

The (i,j) entry recovers the parameter of a difference short-root element.

theorem TauCeti.GLSymplecticFin.positiveSumShortRootUnit_apply_inl_inr {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : R) : ↑↑(positiveSumShortRootUnit hij c) (finSumFinEquiv (Sum.inl i)) (finSumFinEquiv (Sum.inr j)) = c

The (i,m+j) entry recovers the parameter of a positive-sum short-root element.

theorem TauCeti.GLSymplecticFin.negativeSumShortRootUnit_apply_inr_inl {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : R) : ↑↑(negativeSumShortRootUnit hij c) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inl j)) = c

The (m+i,j) entry recovers the parameter of a negative-sum short-root element.

theorem TauCeti.GLSymplecticFin.differenceShortRootUnit_injective {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) : Function.Injective (differenceShortRootUnit hij)

Distinct parameters give distinct difference short-root elements.

theorem TauCeti.GLSymplecticFin.positiveSumShortRootUnit_injective {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) : Function.Injective (positiveSumShortRootUnit hij)

Distinct parameters give distinct positive-sum short-root elements.

theorem TauCeti.GLSymplecticFin.negativeSumShortRootUnit_injective {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) : Function.Injective (negativeSumShortRootUnit hij)

Distinct parameters give distinct negative-sum short-root elements.

inductive TauCeti.GLSymplecticFin.ShortRootFamily : Type

The three uniform families of short roots in the standard type-Cₘ realization.

The difference family is ordered: swapping i and j changes eᵢ-eⱼ to its negative. The two sum families are symmetric in i and j.

• difference : ShortRootFamily
• positiveSum : ShortRootFamily
• negativeSum : ShortRootFamily

@[instance_reducible]

instance TauCeti.GLSymplecticFin.instDecidableEqShortRootFamily : DecidableEq ShortRootFamily

Equations

• TauCeti.GLSymplecticFin.instDecidableEqShortRootFamily x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TauCeti.GLSymplecticFin.ShortRootFamily.hom {m : ℕ} {R : Type u} [CommRing R] (family : ShortRootFamily) {i j : Fin m} (hij : i ≠ j) : Multiplicative R →* ↥(GLSymplecticFin m R)

The matrix one-parameter subgroup belonging to a family of short roots.

Equations

• TauCeti.GLSymplecticFin.ShortRootFamily.difference.hom hij = TauCeti.GLSymplecticFin.differenceShortRootHom hij
• TauCeti.GLSymplecticFin.ShortRootFamily.positiveSum.hom hij = TauCeti.GLSymplecticFin.positiveSumShortRootHom hij
• TauCeti.GLSymplecticFin.ShortRootFamily.negativeSum.hom hij = TauCeti.GLSymplecticFin.negativeSumShortRootHom hij

@[simp]

theorem TauCeti.GLSymplecticFin.ShortRootFamily.hom_difference {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) : difference.hom hij = differenceShortRootHom hij

The difference family specializes to the concrete difference short-root homomorphism.

@[simp]

theorem TauCeti.GLSymplecticFin.ShortRootFamily.hom_positiveSum {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) : positiveSum.hom hij = positiveSumShortRootHom hij

The positive-sum family specializes to the concrete positive-sum short-root homomorphism.

@[simp]

theorem TauCeti.GLSymplecticFin.ShortRootFamily.hom_negativeSum {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) : negativeSum.hom hij = negativeSumShortRootHom hij

The negative-sum family specializes to the concrete negative-sum short-root homomorphism.

@[simp]

theorem TauCeti.GLSymplecticFin.ShortRootFamily.map_hom_apply {m : ℕ} {R : Type u} [CommRing R] {S : Type v} [CommRing S] (family : ShortRootFamily) (f : R →+* S) {i j : Fin m} (hij : i ≠ j) (c : Multiplicative R) : (map m R f) ((family.hom hij) c) = (family.hom hij) (Multiplicative.ofAdd (f (Multiplicative.toAdd c)))

Evaluating a short-root one-parameter subgroup commutes with change of coefficients.

theorem TauCeti.GLSymplecticFin.ShortRootFamily.hom_injective {m : ℕ} {R : Type u} [CommRing R] (family : ShortRootFamily) {i j : Fin m} (hij : i ≠ j) : Function.Injective ⇑(family.hom hij)

Every short-root one-parameter subgroup is injective.

inductive TauCeti.GLSymplecticFin.RootSubgroupIndex (m : ℕ) : Type

An extensional index for the root one-parameter subgroups of the standard symplectic group.

Difference roots retain their ordered pair of indices. The symmetric positive- and negative-sum roots store their indices in increasing order, so each root has only one index.

• positiveLong {m : ℕ} (i : Fin m) : RootSubgroupIndex m
• negativeLong {m : ℕ} (i : Fin m) : RootSubgroupIndex m
• difference {m : ℕ} (i j : Fin m) (hij : i ≠ j) : RootSubgroupIndex m
• positiveSum {m : ℕ} (i j : Fin m) (hij : i < j) : RootSubgroupIndex m
• negativeSum {m : ℕ} (i j : Fin m) (hij : i < j) : RootSubgroupIndex m

def TauCeti.GLSymplecticFin.RootSubgroupIndex.short {m : ℕ} (family : ShortRootFamily) (i j : Fin m) (hij : i ≠ j) : RootSubgroupIndex m

The canonical root index for a short-root family and two distinct indices. Sum roots are normalized to increasing index order.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.GLSymplecticFin.RootSubgroupIndex.short TauCeti.GLSymplecticFin.ShortRootFamily.difference i j hij = TauCeti.GLSymplecticFin.RootSubgroupIndex.difference i j hij

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.short_difference {m : ℕ} (i j : Fin m) (hij : i ≠ j) : short ShortRootFamily.difference i j hij = difference i j hij

The canonical short-root index leaves a difference root ordered.

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.short_positiveSum_of_lt {m : ℕ} (i j : Fin m) (hij : i < j) : short ShortRootFamily.positiveSum i j ⋯ = positiveSum i j hij

Increasing indices are already the canonical order for a positive sum root.

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.short_negativeSum_of_lt {m : ℕ} (i j : Fin m) (hij : i < j) : short ShortRootFamily.negativeSum i j ⋯ = negativeSum i j hij

Increasing indices are already the canonical order for a negative sum root.

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.short_positiveSum_swap {m : ℕ} (i j : Fin m) (hij : i ≠ j) : short ShortRootFamily.positiveSum i j hij = short ShortRootFamily.positiveSum j i ⋯

Swapping the inputs gives the same canonical positive-sum root index.

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.short_negativeSum_swap {m : ℕ} (i j : Fin m) (hij : i ≠ j) : short ShortRootFamily.negativeSum i j hij = short ShortRootFamily.negativeSum j i ⋯

Swapping the inputs gives the same canonical negative-sum root index.

def TauCeti.GLSymplecticFin.RootSubgroupIndex.hom {m : ℕ} {R : Type u} [CommRing R] (root : RootSubgroupIndex m) : Multiplicative R →* ↥(GLSymplecticFin m R)

The matrix one-parameter subgroup selected by a symplectic root index.

Equations

• (TauCeti.GLSymplecticFin.RootSubgroupIndex.positiveLong i).hom = TauCeti.GLSymplecticFin.positiveLongRootTransvectionHom i
• (TauCeti.GLSymplecticFin.RootSubgroupIndex.negativeLong i).hom = TauCeti.GLSymplecticFin.negativeLongRootTransvectionHom i
• (TauCeti.GLSymplecticFin.RootSubgroupIndex.difference i j hij).hom = TauCeti.GLSymplecticFin.differenceShortRootHom hij
• (TauCeti.GLSymplecticFin.RootSubgroupIndex.positiveSum i j hij).hom = TauCeti.GLSymplecticFin.positiveSumShortRootHom ⋯
• (TauCeti.GLSymplecticFin.RootSubgroupIndex.negativeSum i j hij).hom = TauCeti.GLSymplecticFin.negativeSumShortRootHom ⋯

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.hom_positiveLong {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) : (positiveLong i).hom = positiveLongRootTransvectionHom i

The positive-long constructor selects the positive long-root homomorphism.

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.hom_negativeLong {m : ℕ} {R : Type u} [CommRing R] (i : Fin m) : (negativeLong i).hom = negativeLongRootTransvectionHom i

The negative-long constructor selects the negative long-root homomorphism.

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.hom_difference {m : ℕ} {R : Type u} [CommRing R] (i j : Fin m) (hij : i ≠ j) : (difference i j hij).hom = differenceShortRootHom hij

The difference-root constructor selects the corresponding difference-root homomorphism.

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.hom_positiveSum {m : ℕ} {R : Type u} [CommRing R] (i j : Fin m) (hij : i < j) : (positiveSum i j hij).hom = positiveSumShortRootHom ⋯

The positive-sum constructor selects the corresponding positive-sum homomorphism.

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.hom_negativeSum {m : ℕ} {R : Type u} [CommRing R] (i j : Fin m) (hij : i < j) : (negativeSum i j hij).hom = negativeSumShortRootHom ⋯

The negative-sum constructor selects the corresponding negative-sum homomorphism.

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.hom_short {m : ℕ} {R : Type u} [CommRing R] (family : ShortRootFamily) (i j : Fin m) (hij : i ≠ j) : (short family i j hij).hom = family.hom hij

The short constructor selects its family's short-root homomorphism.

@[simp]

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.map_hom_apply {m : ℕ} {R : Type u} [CommRing R] {S : Type v} [CommRing S] (root : RootSubgroupIndex m) (f : R →+* S) (c : Multiplicative R) : (map m R f) (root.hom c) = root.hom (Multiplicative.ofAdd (f (Multiplicative.toAdd c)))

Evaluating any root one-parameter subgroup commutes with change of coefficients.

theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.hom_injective {m : ℕ} {R : Type u} [CommRing R] (root : RootSubgroupIndex m) : Function.Injective ⇑root.hom

Every symplectic root one-parameter subgroup is injective.