MulAction for Subgroup

Stream: new members

[Dominic Steinitz]

I am trying to create a MulAction instance for the orthogonal group. It's easy enough to do this for the general linear group but I am struggling to see how to then use this to get the instance I actually want.

import Mathlib

open MulAction Set

open LinearMap Matrix UnitaryGroup

noncomputable
instance : MulAction (GeneralLinearGroup  ℝ (Fin n -> ℝ)) (Fin n -> ℝ)  where
  smul := λ g x => g.toLinearEquiv x
  one_smul := λ x => by rfl
  mul_smul := λ f g x => by rfl

instance : MulAction (orthogonalGroup (Fin n) ℝ) (Fin n -> ℝ) where
  smul := λ g x => (UnitaryGroup.toGL g).toLinearEquiv x
  one_smul := λ x => by
    have h1 : (1 : GeneralLinearGroup ℝ (Fin n → ℝ)) • x = x := by rfl
    sorry
  mul_smul := λ f g x => by
    have h1 : ((UnitaryGroup.toGL g) * (UnitaryGroup.toGL f)) • x = (UnitaryGroup.toGL g) • (UnitaryGroup.toGL f) • x := by rfl
    have h2 : ((UnitaryGroup.toGL g) * (UnitaryGroup.toGL f)) = UnitaryGroup.toGL (g * f) := by simp
    have h3 : UnitaryGroup.toGL (g * f) • x = (UnitaryGroup.toGL g) • (UnitaryGroup.toGL f) • x := by
      rw [<-h2, h1]
    sorry

[Dominic Steinitz]

Maybe this?

variables {G : Type*} [Group G] {X : Type*} [MulAction G X]

variables {H : Subgroup G}

instance : MulAction H X where
  smul := λ h x => h • x
  one_smul := λ x => one_smul _ x
  mul_smul := λ h₁ h₂ x => mul_smul h₁ h₂ x

[Dominic Steinitz]

But maybe Mathlib does not know that the orthogonal group is a subgroup of the general linear group?

[Dominic Steinitz]

import Mathlib

open MulAction Set

open LinearMap Matrix UnitaryGroup

instance : MulAction (orthogonalGroup (Fin n) ℝ) (Fin n -> ℝ) where
  smul := λ g x => g.1.mulVec x
  one_smul := λ x => by
    have h1 : (1 : orthogonalGroup (Fin n) ℝ).1.mulVec x = x := by
      simp [Matrix.mulVec_one]
    exact h1
  mul_smul := λ f g x => by
    show (f * g).1.mulVec x = f.1.mulVec (g.1.mulVec x)
    simp [Matrix.mulVec_mulVec]

[Dominic Steinitz]

In case anyone is interested

[Dominic Steinitz]

Oh and there are two general linear groups: a matrix one and a linear map one.