A general proposition for group invariance

Stream: general

[Joseph Tooby-Smith]

An important part of physics (and therefore, one day, PhysLean) is invariance of a definition or a proposition under a group action.

My question is the following, given

variable {G : Type} [Group G]

is it possible within the type theory of Lean to define a proposition of the form

def Invariance (α : Type) : Prop := sorry

such that the following properties hold:

import Mathlib

variable {G : Type} [Group G]

variable {α1 : Type} [MulAction G α1]
variable {α2 : Type} [MulAction G α1]
variable {β γ : Type}  {ρ : Prop}

def Invariance (α : Type) : Prop := sorry

def def1 (a1 : α1) : γ := by sorry

-- `Invariance def1` should be true if and only if
-- for all `∀ g ∈ G, ∀ a1, def1 (g • a1) = def1 a1`

def def2 (a1 : α1) (b : β) : α2 →  γ := by sorry

-- `Invariance def2` should be true if and only if
-- for all `∀ g ∈ G, ∀ a1 b a2, def2 (g • a1) b (g • a2)  = def2 a1 b a2`

lemma prop1 (a1 : α1) (b : β) (a2 : α2) : ρ := sorry

-- `Invariance prop1` should be true if and only if
-- for all `∀ g ∈ G, ∀ a1 b a2, prop1 (g • a1) b (g • a2) ↔ prop1 a1 b a2`

That is to say, every input to the definition or proposition which carries a MulAction is acted on by the same group element for the test of invariance.

[Joseph Tooby-Smith]

(Ideally Invariance should be able to deal with sums and integrals in the sam way - although I understand this is a very tall ask.)

[Joseph Tooby-Smith]

I think this may be actually quite easy to do with an appropriate typeclass.

[Kenny Lau]

@Joseph Tooby-Smith the type signatures are a bit messed up because you have sorry and didn't include the variables

[Kenny Lau]

import Mathlib

variable {G : Type} [Group G]

variable {α1 : Type} [MulAction G α1]
variable {α2 : Type} [MulAction G α1]
variable {β γ : Type}  {ρ : Prop}

def Invariant (G : Type) [Group G] {α : Type} [MulAction G α] {β : Sort*} (f : α → β) : Prop :=
  ∀ (g : G) (x : α), f (g • x) = f x

def def1 (a1 : α1) : γ := by sorry

-- `Invariance def1` should be true if and only if
-- for all `∀ g ∈ G, ∀ a1, def1 (g • a1) = def1 a1`
example : Invariant G (def1 (α1 := α1) (γ := γ)) ↔ ∀ g : G, ∀ a1 : α1, def1 (γ := γ) (g • a1) = def1 a1 :=
  Iff.rfl

[Kenny Lau]

for the other ones you'll need to curry the action

[Kenny Lau]

i.e. you need to make the domain α1 \x α2

[Eric Wieser]

Another option would be to state this as forall g, DomMulAct.mk g • f = f

[Joseph Tooby-Smith]

Kenny Lau said:

Joseph Tooby-Smith the type signatures are a bit messed up because you have sorry and didn't include the variables

Yes sorry, my bad.

[Joseph Tooby-Smith]

This was my idea using type-classes, which I think will work for all of my cases:

import Mathlib

variable {G : Type} [Group G]

variable {α1 : Type} [MulAction G α1]
variable {α2 : Type} [MulAction G α1]
variable {β γ : Type}  {ρ : Prop}

class ActionLifts (G : Type) [Group G] (M : Type) where
  lifts : M → G → M

instance  {α1 : Type} [MulAction G α1] :  ActionLifts G α1 where
  lifts := fun m g => g • m

instance  {α1 α2 : Type} [MulAction G α1] :  ActionLifts G (α1 → α2) where
  lifts := fun f g x => f (g • x)

instance  {α1 α2 : Type} [ActionLifts G α2] :  ActionLifts G (α1 → α2) where
  lifts := fun f g x => ActionLifts.lifts (f x) g

instance  {α1 α2 : Type} [ActionLifts G α2] [MulAction G α1] :  ActionLifts G (α1 → α2) where
  lifts := fun f g x => ActionLifts.lifts (f (g • x)) g

def Invariance {α : Type} [ActionLifts G α] (m : α) : Prop :=
  ∀ (g : G), ActionLifts.lifts m g = m

[Joseph Tooby-Smith]

Here is an explicit example with an example of an additive action:

Additive action

import Mathlib

variable {G : Type} [AddGroup G]

variable {α1 : Type} [AddAction G α1]
variable {α2 : Type} [AddAction G α1]
variable {β γ : Type}  {ρ : Prop}

class ActionLifts (G : Type) [AddGroup G] (M : Type) where
  lifts : M → G → M

instance  {α1 : Type} [AddAction G α1] :  ActionLifts G α1 where
  lifts := fun m g => g +ᵥ m

instance  {α1 α2 : Type} [AddAction G α1] :  ActionLifts G (α1 → α2) where
  lifts := fun f g x => f (g +ᵥ x)

instance  {α1 α2 : Type} [ActionLifts G α2] :  ActionLifts G (α1 → α2) where
  lifts := fun f g x => ActionLifts.lifts (f x) g

instance  {α1 α2 : Type} [ActionLifts G α2] [AddAction G α1] :  ActionLifts G (α1 → α2) where
  lifts := fun f g x => ActionLifts.lifts (f (g +ᵥ x)) g

def Invariant (G : Type) [AddGroup G] {α : Type} [ActionLifts G α] (m : α) : Prop :=
  ∀ (g : G), ActionLifts.lifts m g = m

def SubEqZero (a b : ℝ) (x : ℕ) : Prop := a - b = x

lemma subEqZero_invariant : Invariant ℝ SubEqZero := by
  simp [Invariant]
  intro g
  simp [ActionLifts.lifts]
  ext r r2 y
  simp [SubEqZero]