Scalar extension of Eichler-transvection parameters

The pure-tensor map sends vectors orthogonal to u to vectors orthogonal to 1 ⊗ u, and sends the span of u into the span of 1 ⊗ u. It therefore induces a semilinear map on the quotient parameter spaces. For isotropic u, these are the spaces u^⊥ / R ∙ u that parametrize Eichler transvections and their canonical Spin lifts. The map lets entire root subgroups, rather than just individual elements, be transported by extension of scalars.

The maps are TauCeti.QuadraticMap.polarKernelBaseChange and TauCeti.QuadraticMap.transvectionParameterBaseChange, alongside the orthogonal-group base-change maps. Use function application, for example TauCeti.QuadraticMap.transvectionParameterBaseChange (A := A) Q u.

def TauCeti.QuadraticMap.transvectionParameterBaseChange {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] (Q : QuadraticForm R M) (u : M) : ↥((QuadraticMap.polarBilin Q) u).ker ⧸ Submodule.comap ((QuadraticMap.polarBilin Q) u).ker.subtype (R ∙ u) →ₛₗ[algebraMap R A] ↥((QuadraticMap.polarBilin (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] u)).ker ⧸ Submodule.comap ((QuadraticMap.polarBilin (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] u)).ker.subtype (A ∙ 1 ⊗ₜ[R] u)

Scalar extension on the quotient parameter space of Eichler transvections. The class of w is sent to the class of 1 ⊗ w; the map is semilinear along algebraMap R A.

@[simp]

theorem TauCeti.QuadraticMap.transvectionParameterBaseChange_mk {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] (Q : QuadraticForm R M) (u : M) (w : ↥((QuadraticMap.polarBilin Q) u).ker) : (transvectionParameterBaseChange Q u) (Submodule.Quotient.mk w) = Submodule.Quotient.mk ⟨1 ⊗ₜ[R] ↑w, ⋯⟩

Extension of a quotient parameter is computed on representatives by pure tensors.