Base change of an invariant bilinear form #
Extending the scalars of a representation along an algebra R → A extends the scalars of its
invariant forms: the base change LinearMap.BilinForm.baseChange of an invariant form is invariant
for the base-changed representation Representation.baseChange. Invariance is elementwise the
statement that each ρ g is an isometry of the form, so this is
TauCeti.BilinForm.IsIsometry.baseChange applied one group element at a time.
Main results #
TauCeti.Representation.IsInvariantForm.baseChange: the base change of an invariant form is invariant.
theorem
TauCeti.Representation.IsInvariantForm.baseChange
{R : Type u_1}
{A : Type u_2}
{G : Type u_3}
{W : Type u_4}
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
[Monoid G]
[AddCommMonoid W]
[Module R W]
{σ : Representation R G W}
{B : LinearMap.BilinForm R W}
(hB : IsInvariantForm σ B)
:
The base change of an invariant form is invariant for the base-changed representation:
each base-changed action (σ g).baseChange A is an isometry of the base-changed form, by
TauCeti.BilinForm.IsIsometry.baseChange.