2
$\begingroup$

I have a group $G$ and $G$-sets $X$ and $Y$. I would like to let $G$ act on the type $(X\to Y)$ by the usual rule $(g\bullet u)(x)=g\bullet u(g^{-1}\bullet x)$. I define a MulAction instance as shown below, and I try to persuade Lean to use it (using code which is a fairly direct translation of things that worked correctly in Lean 3). However, Lean accepts rfl as a proof of smul_map below, which indicates that it is not in fact using my instance. Instead, it thinks that $(g\bullet u)(x)= g\bullet u(x)$, which suggests that it is using Pi.smul' from Mathlib.GroupTheory.GroupAction.Pi even though I tried to disable that. The typeclass inference trace is enormous and I have not succeeded in understanding it. What is the recommended approach for this sort of thing?

import Mathlib.GroupTheory.GroupAction.Basic

universe uG uX uY

variable {G : Type uG} [Group G ]
variable {X : Type uX} {Y : Type uY}
variable [MulAction G X] [MulAction G Y]

attribute [-instance] Pi.smul'

@[default_instance 500]
instance map_action : MulAction G (X → Y) := {
 smul := λ g u x => g • (u (g⁻¹ • x)),
 one_smul := λ u => funext $ λ x => by
  change (1 : G) • (u ((1 : G)⁻¹ • x)) = u x
  rw [inv_one, one_smul, one_smul]
 mul_smul := λ a b u => funext $ λ x => by
  change (a * b) • (u _) = a • (b • (u _))
  rw [mul_inv_rev, mul_smul, mul_smul]
}

lemma smul_map (g : G) (u : X → Y) (x : X) :
  (g • u) x = g • (u x) := rfl
$\endgroup$

1 Answer 1

4
$\begingroup$

A common solution to this problem is to define a type synonym with its own instances. You can find this throughout mathlib, for example with Multiplicative and Additive to switch whether to use a multiplicative or additive notation, or Lex to use a lexicographic order on a type.

Here, I define a type synonym ConjPi for a pi type with a conjugation action:

import Mathlib.GroupTheory.GroupAction.Basic

universe uG uX uY

variable {G : Type uG} [Group G]
variable {X : Type uX} {Y : Type uY}
variable [MulAction G X] [MulAction G Y]

def ConjPi (X : Type uX) (Y : Type uY) := X → Y

instance map_action : MulAction G (ConjPi X Y) := {
 smul := λ g u x => g • (u (g⁻¹ • x)),
 one_smul := λ u => funext $ λ x => by
  change (1 : G) • (u ((1 : G)⁻¹ • x)) = u x
  rw [inv_one, one_smul, one_smul]
 mul_smul := λ a b u => funext $ λ x => by
  change (a * b) • (u _) = a • (b • (u _))
  rw [mul_inv_rev, mul_smul, mul_smul]
}

lemma smul_map (g : G) (u : ConjPi X Y) (x : X) :
  (g • u) x = g • (u (g⁻¹ • x)) := rfl

As another example of a type synonym in mathlib, I'll mention that for a group G, ConjAct G is G itself but acts on G by conjugation. It's conceivable using ConjAct for your action, where you define an action of ConjAct G on X → Y, and the tradeoff is whether you need to be careful to work with ConjAct G or with ConjPi X Y.

Here's another possible design, using the fairly common approach of type synonyms using a custom identity function:

def Conj (α : Type*) := α

instance map_action : MulAction G (Conj (X → Y)) := {
 smul := λ g u x => g • (u (g⁻¹ • x)),
 one_smul := λ u => funext $ λ x => by
  change (1 : G) • (u ((1 : G)⁻¹ • x)) = u x
  rw [inv_one, one_smul, one_smul]
 mul_smul := λ a b u => funext $ λ x => by
  change (a * b) • (u _) = a • (b • (u _))
  rw [mul_inv_rev, mul_smul, mul_smul]
}

lemma smul_map (g : G) (u : Conj (X → Y)) (x : X) :
  (g • u) x = g • (u (g⁻¹ • x)) := rfl
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.