defining partial group actions

Stream: maths

[Bernd Losert]

I'm trying to define partial group actions in lean (see pg. 5 of https://arxiv.org/pdf/1604.06393.pdf for a definition). This is what I have so far, but I'm stuck:

import tactic
import order.filter.partial
import algebra.support

noncomputable theory
open set filter classical
open_locale classical filter

variables {X Y : Type*}

class partial_group_action (G X : Type*) [group G] :=
(X' : G → set X)
(X'1 : X' 1 = univ)
(α : ∀ (g : G), X' (g⁻¹) → X' g)
(α1 : α 1 = id) <-- Complains here because the types don't match.

I'm not sure how to proceed here.

[Anne Baanen]

I would unbundle the subset requirement from the type of α:

class partial_group_action (G X : Type*) [group G] :=
(X' : G → set X)
(X'1 : X' 1 = univ)
(α : ∀ (g : G), X → X)
(α_subset : ∀ (g : G) (x ∈ X' (g⁻¹)), α g x ∈ X' g)
(α1 : α 1 = id)

[Eric Wieser]

I assume you mean (α_subset : ∀ (g : G), x ∈ X' (g⁻¹) → α g x ∈ X' g)?

[Anne Baanen]

Not really? We need to introduce x, no?

[Alex J. Best]

I think Anne's approach might work better in the long run, but one alternative is to do

import tactic
import order.filter.partial
import algebra.support

noncomputable theory
open set filter classical
open_locale classical filter

variables {X Y : Type*}

class partial_group_action (G X : Type*) [group G] :=
(X' : G → set X)
(X'1 : X' 1 = univ)
(α : ∀ (g : G), X' (g⁻¹) → X' g)
(α1 : ∀ t : X, α 1 ⟨t, by simp [X'1]⟩ = ⟨t, by simp [X'1]⟩) -- Complains here because the types don't match.

[Yaël Dillies]

Maybe have a look at #10497 for a similar case where I need to define homomorphisms which partially respect some condition.

[Reid Barton]

Maybe the simplest approach is to replace the α by a family of relations

[Adam Topaz]

Does the following definition (or something similar) work?

import tactic
import order.filter.partial
import algebra.support

noncomputable theory
open set filter classical
open_locale classical filter

variables {X Y : Type*}

class partial_group_action (G X : Type*) [group G] :=
(μ_def : G → X → Prop)
(μ (g x) (h : μ_def g x) : X)
(μ_def_id (x) : μ_def 1 x)
(μ_def_inv (g x) (h : μ_def g x) : μ_def g⁻¹ x)
(μ_id (x) : μ 1 x (μ_def_id x) = x)
(μ_def_assoc (g₁ g₂ x) (h : μ_def g₂ x) (h' : μ_def g₁ (μ g₂ x h)) : μ_def (g₁ * g₂) x)
(μ_assoc (g₁ g₂ x) (h : μ_def g₂ x) (h' : μ_def g₁ (μ g₂ x h)) :
  μ g₁ (μ g₂ x h) h' = μ (g₁ * g₂) x (μ_def_assoc g₁ g₂ x h h'))

[Adam Topaz]

Maybe μ_def_inv isn't actually needed?

[Adam Topaz]

Presumably one should start by defining a partial monoid action...

[Adam Topaz]

Why the :oh_no: ?

[Yaël Dillies]

That sounds like a long-winded way.

[Bernd Losert]

I haven't seen a definition of partial monoid action.

[Adam Topaz]

class partial_monoid_action (G X : Type*) [monoid G] :=
(μ_def : G → X → Prop)
(μ (g x) (h : μ_def g x) : X)
(μ_def_id (x) : μ_def 1 x)
(μ_id (x) : μ 1 x (μ_def_id x) = x)
(μ_def_assoc (g₁ g₂ x) (h : μ_def g₂ x) (h' : μ_def g₁ (μ g₂ x h)) : μ_def (g₁ * g₂) x)
(μ_assoc (g₁ g₂ x) (h : μ_def g₂ x) (h' : μ_def g₁ (μ g₂ x h)) :
  μ g₁ (μ g₂ x h) h' = μ (g₁ * g₂) x (μ_def_assoc g₁ g₂ x h h'))

[Adam Topaz]

I'm just guessing that would be the right definition...

[Yaël Dillies]

Is there really no way we can recycle usual actions to make partial ones?

[Bernd Losert]

I thought about it, but I can't think of a way to do it.

[Bernd Losert]

(μ (g x) (h : μ_def g x) : X)

I've never seen this kind of expression before. What's going on here?

[Adam Topaz]

This is saying that the action of g on x will only be defined when \mu_def g x holds, and will be an element of X.

[Yaël Dillies]

It's simply not naming the hypothesis of type g x and putting stuff before the :.

[Bernd Losert]

(α1 : ∀ t : X, α 1 ⟨t, by simp [X'1]⟩ = ⟨t, by simp [X'1]⟩)

This solves the problem I'm currently having. Is this not an OK approach?

[Adam Topaz]

Here are all the types:

import tactic
import order.filter.partial
import algebra.support

noncomputable theory
open set filter classical
open_locale classical filter

variables {X Y : Type*}

class partial_monoid_action (G X : Type*) [monoid G] :=
(μ_def : G → X → Prop)
(μ (g : G) (x : X) (h : μ_def g x) : X)
(μ_def_id (x : X) : μ_def 1 x)
(μ_id (x : X) : μ 1 x (μ_def_id x) = x)
(μ_def_assoc (g₁ g₂ : G) (x : X) (h : μ_def g₂ x) (h' : μ_def g₁ (μ g₂ x h)) :
  μ_def (g₁ * g₂) x)
(μ_assoc (g₁ g₂ : G) (x : X) (h : μ_def g₂ x) (h' : μ_def g₁ (μ g₂ x h)) :
  μ g₁ (μ g₂ x h) h' = μ (g₁ * g₂) x (μ_def_assoc g₁ g₂ x h h'))

[Bernd Losert]

Ah, that makes it clear. Thanks.

[Adam Topaz]

Bernd Losert said:

(α1 : ∀ t : X, α 1 ⟨t, by simp [X'1]⟩ = ⟨t, by simp [X'1]⟩)

This solves the problem I'm currently having. Is this not an OK approach?

You are working with subtypes with this approach, which can get annoying in the long run.

[Bernd Losert]

But the partial action stuff relies on subsets everywhere. I can't really escape it.

[Adam Topaz]

The subset $X_g$ you defined would become set_of (μ_def g)

[Bernd Losert]

Yes.

[Adam Topaz]

The issue with using sets is that terms of X_g are not terms of X, so if you start by using such subsets, you will always need to rely on coercions..

[Bernd Losert]

I like your relation approach involving μ_def. I'll have to try it out.

[Bernd Losert]

Ultimately, I need to define continuous versions of partial group actions and then I need to talk about convergent filters on the "domain" of the partial action.

[Adam Topaz]

I see... Is there an analogue of the group chunk theorem for convergence spaces?

[Bernd Losert]

I can't tell if using μ_def will be easier than dealing with subsets.

[Bernd Losert]

A lot of the theory of partial group actions can be generalized to convergence spaces.

[Bernd Losert]

I don't know what the "group chunk theorem" is.

[Adam Topaz]

The context of this paper is probably the closest:
https://projecteuclid.org/journals/illinois-journal-of-mathematics/volume-34/issue-1/Weils-group-chunk-theorem-A-topological-setting/10.1215/ijm/1255988498.full

[Bernd Losert]

OK.

[Alex J. Best]

The reason my suggestion is maybe bad is because while it works in this case you may well end up hitting other similar issues with X' (g\inv * g * h) not being the same type as X' h or other goals like this. Probably you can always make the statements work in the same way assuming x : X and hx : x \in X' g, but as a general principle having the types of things depend on your variables that you are applying algebraic operations too causes headaches.

[Bernd Losert]

Indeed. I'm already feeling the pain.

[Bernd Losert]

Thanks everyone. I will go with the relation approach for now and see where it takes me.

[Reid Barton]

The approach I had in mind was something like

import algebra.group
import logic.relation

class partial_group_action (G X : Type*) [group G] :=
(ρ : G → X → X → Prop)          -- ρ g x y ↔ (α g x = y). X_{g⁻¹} = {x | ∃ y, ρ g x y}.
(ρ_bij (g) : relator.bi_unique (ρ g))
(ρ_1 : ρ 1 = (=))
(ρ_mul (g h) : relation.comp (ρ g) (ρ h) ≤ ρ (g * h))
(ρ_inv (g) : flip (ρ g) = ρ (g⁻¹))

[Reid Barton]

though it's likely I have the relation.comp arguments backwards, and I didn't actually check that this is what the definition of a partial group action is, but I assume it ought to be

[Reid Barton]

The main disadvantage is you can't just apply $\alpha$ as a function

[Reid Barton]

Adam's definition is basically the same as your original one except that instead of taking a single argument of type which is a subtype, the operation takes two separate arguments.

[Bernd Losert]

The main disadvantage is you can't just apply α as a function

That's going to be troublesome since I want to map α to a filter. In fact, I am already going to run into a problem with Adam's definition since it requires of proof that the action is defined. There is also the problem that it's not uncurried.

[Bernd Losert]

Yaël Dillies said:

Is there really no way we can recycle usual actions to make partial ones?

Maybe I can define actions on option X?

[Yaël Dillies]

Or docs#part, but I'm not sure that works.

[Bernd Losert]

I think one problem with part that I'll have is mapping the action over a filter.

[Reid Barton]

Bernd Losert said:

That's going to be troublesome since I want to map α to a filter.

Mathematically this shouldn't be a problem (a relation can be viewed as a kind of span, and you can comap and then map across the legs of the span) but mathlib might not have good existing support for this operation.