Linear isometries acting on the additive group

LinearIsometryEquiv.multiplicativeAutHom bundles the evaluation action of linear isometries on the additive group. It uses Multiplicative to supply the action homomorphism required by SemidirectProduct, in particular for the affine isometry group decomposition. The construction reuses AddEquiv.toMultiplicative and forgets the scalar and norm structure of each linear isometry.

def LinearIsometryEquiv.multiplicativeAutHom {R : Type u_1} {E : Type u_2} [Semiring R] [SeminormedAddCommGroup E] [Module R E] : (E ≃ₗᵢ[R] E) →* MulAut (Multiplicative E)

The usual action of linear isometries on the additive group, written multiplicatively for use in a semidirect product.

@[simp]

theorem LinearIsometryEquiv.multiplicativeAutHom_apply {R : Type u_1} {E : Type u_2} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (L : E ≃ₗᵢ[R] E) (v : Multiplicative E) : (multiplicativeAutHom L) v = Multiplicative.ofAdd (L (Multiplicative.toAdd v))

The multiplicative action is evaluation of the linear isometry.