Base change of Eichler transvections

An Eichler transvection is defined by a polynomial formula in the quadratic form and its polar form. Extending scalars therefore carries the transvection determined by u and w to the one determined by their pure tensors. The corresponding statement for SO(Q) follows from this identity and the existing base-change homomorphism of special orthogonal groups. The quotient parameter map also makes the entire root-subgroup homomorphism commute with scalar extension. These formulas let the same transvection be used over a rational quadratic space and at each of its completions.

@[simp]

theorem QuadraticMap.transvection_baseChange {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) {u w : M} (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) : LinearEquiv.baseChange R A M M (transvection Q hu huw) = transvection (QuadraticForm.baseChange A Q) ⋯ ⋯

Base change carries E_{u,w} to E_{1 ⊗ u,1 ⊗ w} over commutative rings in which 2 is invertible; neither nondegeneracy nor finite dimensionality is needed.

@[simp]

theorem QuadraticMap.specialOrthogonalGroupBaseChange_transvection {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) {u w : M} [Module.Free R M] [Module.Finite R M] (hu : Q u = 0) (huw : polar (⇑Q) u w = 0) : (TauCeti.QuadraticMap.specialOrthogonalGroupBaseChange Q) ⟨transvection Q hu huw, ⋯⟩ = ⟨transvection (QuadraticForm.baseChange A Q) ⋯ ⋯, ⋯⟩

The special-orthogonal base-change homomorphism carries the class of an Eichler transvection to the class of the base-changed transvection.

theorem TauCeti.QuadraticMap.specialOrthogonalGroupBaseChange_comp_transvectionHom {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] [Module.Free R M] [Module.Finite R M] (Q : QuadraticForm R M) {u : M} (hu : Q u = 0) : (MonoidHom.toAdditive (specialOrthogonalGroupBaseChange Q)).comp (QuadraticMap.transvectionHom Q hu) = (QuadraticMap.transvectionHom (QuadraticForm.baseChange A Q) ⋯).comp (transvectionParameterBaseChange Q u).toAddMonoidHom

Extending scalars of the Eichler root-subgroup homomorphism agrees with extending its quotient parameters. This holds over commutative rings, without nondegeneracy.