Eichler transvections of a quadratic form

Let Q be a quadratic form on M with un-halved polar form B = polar Q, so that B x x = 2 • Q x. For an isotropic vector u (Q u = 0) and a vector w orthogonal to it (B u w = 0), the Eichler transvection (also called a Siegel transformation) is

E_{u,w} x = x + B x u • w - B x w • u - (Q w * B x u) • u.

It is a proper isometry of Q. It fixes u and every vector orthogonal to both u and w, and it depends on w only through its class modulo R ∙ u. For fixed u, the map w ↦ E_{u,w} turns addition into composition. So the Eichler transvections with isotropic vector u are the image of a homomorphism from the additive group u^⊥ / R ∙ u into SO(Q). This homomorphism is injective as soon as the polar form pairs u with some vector to a unit; over a field, as soon as u is not in the kernel of the polar form. The orthogonal group acts on these subgroups by conjugation, moving the pair (u, w).

Nothing here assumes that 2 is invertible or that the scalars form a field. The formula uses B and Q, never B / 2, so it makes sense verbatim for integral quadratic forms.

Main definitions

• QuadraticMap.transvection Q hu huw: the Eichler transvection E_{u,w}, as a linear automorphism of M with determinant 1.
• QuadraticMap.transvectionHom Q hu: the homomorphism w ↦ E_{u,w} from the additive group of u^⊥ / R ∙ u into specialOrthogonalGroup Q.

Main results

• QuadraticMap.transvection_apply: the defining formula.
• QuadraticMap.transvection_mem_specialOrthogonalGroup: E_{u,w} is a proper isometry.
• QuadraticMap.transvection_add: E_{u,w + w'} = E_{u,w} * E_{u,w'}.
• QuadraticMap.transvection_add_smul: E_{u,w + c • u} = E_{u,w}.
• QuadraticMap.transvection_conj: g * E_{u,w} * g⁻¹ = E_{g u, g w} for g ∈ O(Q).
• QuadraticMap.IsometryEquiv.transvectionParameterEquiv: an isometry transports the parameter space u^⊥ / ((R ∙ u) ∩ u^⊥) to the corresponding space for e u; when u is isotropic, this is u^⊥ / R ∙ u.
• QuadraticMap.IsometryEquiv.specialOrthogonalGroupCongr_comp_transvectionHom: Eichler root-subgroup homomorphisms are natural under isometric equivalences.
• QuadraticMap.transvection_eq_one_iff_of_isUnit: if polar Q x u is a unit for some x, then E_{u,w} = 1 exactly when w ∈ R ∙ u. Hence transvectionHom_injective_of_isUnit.
• QuadraticMap.transvection_eq_one_iff: over a field, if polarBilin Q u ≠ 0, then E_{u,w} = 1 exactly when w ∈ K ∙ u. Hence transvectionHom_injective.
• QuadraticMap.finrank_transvectionParameter: for an isotropic vector outside the polar radical, the parameter space u^⊥ / K ∙ u has dimension dim V - 2.
• QuadraticMap.subsingleton_transvectionParameter_of_finrank_eq_two: for an isotropic vector outside the polar radical in a binary quadratic space, the parameter space u^⊥ / K ∙ u is trivial; consequently every Eichler transvection is the identity.

References

• M. Eichler, Quadratische Formen und orthogonale Gruppen, Springer (1952).

noncomputable def QuadraticMap.IsometryEquiv.transvectionParameterEquiv {R : Type u_1} [CommRing R] {M₁ : Type u_2} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q₁ Q₂) (u : M₁) : (↥((polarBilin Q₁) u).ker ⧸ Submodule.comap ((polarBilin Q₁) u).ker.subtype (R ∙ u)) ≃ₗ[R] ↥((polarBilin Q₂) (e u)).ker ⧸ Submodule.comap ((polarBilin Q₂) (e u)).ker.subtype (R ∙ e u)

An isometric equivalence transports the quotient u^⊥ / ((R ∙ u) ∩ u^⊥) to the corresponding quotient for e u. When u is isotropic, this is the Eichler-transvection parameter space u^⊥ / R ∙ u.

@[simp]

theorem QuadraticMap.IsometryEquiv.transvectionParameterEquiv_mk {R : Type u_1} [CommRing R] {M₁ : Type u_2} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q₁ Q₂) (u : M₁) (w : ↥((polarBilin Q₁) u).ker) : (e.transvectionParameterEquiv u) (Submodule.Quotient.mk w) = Submodule.Quotient.mk ⟨e ↑w, ⋯⟩

Transport of Eichler-transvection parameters sends the class of w to the class of e w.

@[simp]

theorem QuadraticMap.IsometryEquiv.transvectionParameterEquiv_symm_mk {R : Type u_1} [CommRing R] {M₁ : Type u_2} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q₁ Q₂) (u : M₁) (w : ↥((polarBilin Q₂) (e u)).ker) : (e.transvectionParameterEquiv u).symm (Submodule.Quotient.mk w) = Submodule.Quotient.mk ⟨e.symm ↑w, ⋯⟩

Inverse transport of Eichler-transvection parameters sends the class of w to the class of e.symm w.

theorem QuadraticMap.IsometryEquiv.transvectionParameterEquiv_refl {R : Type u_1} [CommRing R] {M₁ : Type u_2} [AddCommGroup M₁] [Module R M₁] (Q₁ : QuadraticForm R M₁) (u : M₁) : (refl Q₁).transvectionParameterEquiv u = LinearEquiv.refl R (↥((polarBilin Q₁) u).ker ⧸ Submodule.comap ((polarBilin Q₁) u).ker.subtype (R ∙ u))

The identity isometry induces the identity equivalence on Eichler-transvection parameters.

theorem QuadraticMap.IsometryEquiv.transvectionParameterEquiv_trans {R : Type u_1} [CommRing R] {M₁ : Type u_2} [AddCommGroup M₁] [Module R M₁] {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {M₃ : Type u_4} [AddCommGroup M₃] [Module R M₃] {Q₃ : QuadraticForm R M₃} (e : IsometryEquiv Q₁ Q₂) (f : IsometryEquiv Q₂ Q₃) (u : M₁) : (e.trans f).transvectionParameterEquiv u = e.transvectionParameterEquiv u ≪≫ₗ f.transvectionParameterEquiv (e u)

Transport of Eichler-transvection parameters respects composition of isometries.

noncomputable def QuadraticMap.transvection {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) : M ≃ₗ[R] M

The Eichler transvection E_{u,w} x = x + B x u • w - B x w • u - (Q w * B x u) • u, for an isotropic vector u and a vector w orthogonal to it, where B = polar Q. It is a proper isometry of Q.

theorem QuadraticMap.transvection_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) (x : M) : (transvection Q hu huw) x = x + polar (⇑Q) x u • w - polar (⇑Q) x w • u - (Q w * polar (⇑Q) x u) • u

The Eichler transvection acts by E_{u,w} x = x + B x u • w - B x w • u - (Q w * B x u) • u, where B = polar Q.

@[simp]

theorem QuadraticMap.det_transvection {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) : LinearEquiv.det (transvection Q hu huw) = 1

The determinant of an Eichler transvection is 1, on any module.

theorem QuadraticMap.transvection_mem_orthogonalGroup {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) : transvection Q hu huw ∈ TauCeti.QuadraticMap.orthogonalGroup Q

An Eichler transvection is an isometry of Q.

theorem QuadraticMap.transvection_mem_specialOrthogonalGroup {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) : transvection Q hu huw ∈ TauCeti.QuadraticMap.specialOrthogonalGroup Q

An Eichler transvection is a proper isometry of Q.

@[simp]

theorem QuadraticMap.transvection_apply_self {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) : (transvection Q hu huw) u = u

An Eichler transvection E_{u,w} fixes its isotropic vector u.

@[simp]

theorem QuadraticMap.transvection_apply_of_polar_eq_zero {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) {x : M} (hxu : polar (⇑Q) x u = 0) (hxw : polar (⇑Q) x w = 0) : (transvection Q hu huw) x = x

An Eichler transvection fixes every vector orthogonal to both u and w.

@[simp]

theorem QuadraticMap.transvection_zero {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u : M} (hu : Q u = 0) : transvection Q hu ⋯ = 1

The Eichler transvection with w = 0 is the identity.

@[simp]

theorem QuadraticMap.transvection_eq_one_of_mem_span {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) (hw : w ∈ R ∙ u) : transvection Q hu huw = 1

The Eichler transvection E_{u,w} is trivial when w is a multiple of u.

@[simp]

theorem QuadraticMap.transvection_add {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w w' : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) (huw' : polar (⇑Q) u w' = 0) : transvection Q hu ⋯ = transvection Q hu huw * transvection Q hu huw'

The Eichler transvections with a fixed isotropic vector u compose additively in w.

@[simp]

theorem QuadraticMap.transvection_neg {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) : transvection Q hu ⋯ = (transvection Q hu huw)⁻¹

The inverse of an Eichler transvection is the Eichler transvection of -w.

theorem QuadraticMap.transvection_add_smul {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) (c : R) : transvection Q hu ⋯ = transvection Q hu huw

An Eichler transvection depends on w only through its class modulo R ∙ u.

theorem QuadraticMap.transvection_conj {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) {g : M ≃ₗ[R] M} (hg : g ∈ TauCeti.QuadraticMap.orthogonalGroup Q) : g * transvection Q hu huw * g⁻¹ = transvection Q ⋯ ⋯

The conjugation law. Conjugating an Eichler transvection by an isometry moves the defining pair of vectors: g * E_{u,w} * g⁻¹ = E_{g u, g w}.

@[simp]

theorem QuadraticMap.IsometryEquiv.specialOrthogonalGroupCongr_transvection {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} {M₂ : Type u_1} [AddCommGroup M₂] [Module R M₂] {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q Q₂) (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) : e.specialOrthogonalGroupCongr ⟨transvection Q hu huw, ⋯⟩ = ⟨transvection Q₂ ⋯ ⋯, ⋯⟩

Transporting an Eichler transvection along an isometric equivalence transports both of its defining vectors.

noncomputable def QuadraticMap.transvectionHom {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {u : M} (hu : Q u = 0) : ↥((polarBilin Q) u).ker ⧸ Submodule.comap ((polarBilin Q) u).ker.subtype (R ∙ u) →+ Additive ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)

The Eichler transvections with a fixed isotropic vector u, as a homomorphism w ↦ E_{u,w} from the additive group of u^⊥ / R ∙ u into SO(Q). It is injective when the polar form pairs u with some vector to a unit (transvectionHom_injective_of_isUnit).

@[simp]

theorem QuadraticMap.coe_transvectionHom_mk {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) : ↑(Additive.toMul ((transvectionHom Q hu) (Submodule.Quotient.mk ⟨w, ⋯⟩))) = transvection Q hu huw

The quotient homomorphism sends the class of w to the Eichler transvection E_{u,w}.

theorem QuadraticMap.toMul_transvectionHom_mk {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) : Additive.toMul ((transvectionHom Q hu) (Submodule.Quotient.mk ⟨w, ⋯⟩)) = ⟨transvection Q hu huw, ⋯⟩

The quotient homomorphism sends the class of w to the Eichler transvection E_{u,w} as an element of the special orthogonal group.

theorem QuadraticMap.IsometryEquiv.specialOrthogonalGroupCongr_comp_transvectionHom {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u : M} {M₂ : Type u_1} [AddCommGroup M₂] [Module R M₂] {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q Q₂) (hu : Q u = 0) : (MonoidHom.toAdditive e.specialOrthogonalGroupCongr.toMonoidHom).comp (transvectionHom Q hu) = (transvectionHom Q₂ ⋯).comp (↑(e.transvectionParameterEquiv u)).toAddMonoidHom

Eichler root-subgroup homomorphisms are natural under isometric equivalences of quadratic forms.

theorem QuadraticMap.transvection_eq_one_iff_of_isUnit {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) (hu₀ : ∃ (x : M), IsUnit (polar (⇑Q) x u)) : transvection Q hu huw = 1 ↔ w ∈ R ∙ u

An Eichler transvection E_{u,w} is trivial exactly when w is a multiple of u, provided the polar form pairs u with some vector to a unit.

theorem QuadraticMap.transvectionHom_injective_of_isUnit {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u : M} (hu : Q u = 0) (hu₀ : ∃ (x : M), IsUnit (polar (⇑Q) x u)) : Function.Injective ⇑(transvectionHom Q hu)

The Eichler transvections with isotropic vector u form a copy of the additive group u^⊥ / R ∙ u inside SO(Q), provided the polar form pairs u with some vector to a unit.

theorem QuadraticMap.transvection_eq_one_iff {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {u w : V} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) (hu₀ : (polarBilin Q) u ≠ 0) : transvection Q hu huw = 1 ↔ w ∈ K ∙ u

Over a field, an Eichler transvection E_{u,w} is trivial exactly when w is a multiple of u, provided u is not in the kernel of the polar form (for instance, u ≠ 0 and Q nondegenerate).

theorem QuadraticMap.transvectionHom_injective {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {u : V} (hu : Q u = 0) (hu₀ : (polarBilin Q) u ≠ 0) : Function.Injective ⇑(transvectionHom Q hu)

Over a field, the Eichler transvections with isotropic vector u form a copy of the additive group u^⊥ / K ∙ u inside SO(Q), provided u is not in the kernel of the polar form.

theorem QuadraticMap.exists_polar_eq_zero_not_mem_span_of_finrank_ge_three {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {u : V} (Q : QuadraticForm K V) (hpolar : (polarBilin Q) u ≠ 0) (hdim : 3 ≤ Module.finrank K V) : ∃ (w : V), polar (⇑Q) u w = 0 ∧ w ∉ K ∙ u

In dimension at least three, a vector outside the polar radical has an orthogonal vector outside its span. For an isotropic vector, this gives a nontrivial transvection parameter.

theorem QuadraticMap.finrank_transvectionParameter {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {u : V} [FiniteDimensional K V] (hu : Q u = 0) (hpolar : (polarBilin Q) u ≠ 0) : Module.finrank K (↥((polarBilin Q) u).ker ⧸ Submodule.comap ((polarBilin Q) u).ker.subtype (K ∙ u)) = Module.finrank K V - 2

The Eichler-transvection parameter space u^⊥ / K ∙ u of an isotropic vector outside the polar radical has dimension dim V - 2.

theorem QuadraticMap.subsingleton_transvectionParameter_of_finrank_eq_two {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {u : V} (hV : Module.finrank K V = 2) (hu : Q u = 0) (hpolar : (polarBilin Q) u ≠ 0) : Subsingleton (↥((polarBilin Q) u).ker ⧸ Submodule.comap ((polarBilin Q) u).ker.subtype (K ∙ u))

In a binary quadratic space, the Eichler-transvection parameter space u^⊥ / K ∙ u of an isotropic vector outside the polar radical is trivial. This is the low-dimensional exception to the nontrivial transvection families available in dimension at least three.

theorem QuadraticMap.transvection_eq_one_of_finrank_eq_two {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {u w : V} (hV : Module.finrank K V = 2) (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) (hpolar : (polarBilin Q) u ≠ 0) : transvection Q hu huw = 1

Every Eichler transvection in a binary quadratic space whose isotropic direction is outside the polar radical is the identity.

theorem QuadraticMap.transvectionHom_eq_zero_of_finrank_eq_two {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {u : V} (hV : Module.finrank K V = 2) (hu : Q u = 0) (hpolar : (polarBilin Q) u ≠ 0) : transvectionHom Q hu = 0

The Eichler root-subgroup homomorphism is zero in a binary quadratic space when its isotropic direction is outside the polar radical.