Zulip Chat Archive

Stream: maths

Topic: defining partial group actions


Bernd Losert (Dec 21 2021 at 15:15):

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 (Dec 21 2021 at 15:25):

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 (Dec 21 2021 at 15:26):

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

Anne Baanen (Dec 21 2021 at 15:28):

Not really? We need to introduce x, no?

Alex J. Best (Dec 21 2021 at 15:29):

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 (Dec 21 2021 at 15:36):

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

Reid Barton (Dec 21 2021 at 15:38):

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

Adam Topaz (Dec 21 2021 at 15:52):

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 (Dec 21 2021 at 15:54):

Maybe μ_def_inv isn't actually needed?

Adam Topaz (Dec 21 2021 at 15:54):

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

Adam Topaz (Dec 21 2021 at 15:57):

Why the :oh_no: ?

Yaël Dillies (Dec 21 2021 at 15:57):

That sounds like a long-winded way.

Bernd Losert (Dec 21 2021 at 15:57):

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

Adam Topaz (Dec 21 2021 at 15:57):

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 (Dec 21 2021 at 15:58):

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

Yaël Dillies (Dec 21 2021 at 15:59):

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

Bernd Losert (Dec 21 2021 at 15:59):

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

Bernd Losert (Dec 21 2021 at 16:01):

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

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

Adam Topaz (Dec 21 2021 at 16:01):

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 (Dec 21 2021 at 16:03):

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

Bernd Losert (Dec 21 2021 at 16:03):

(α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 (Dec 21 2021 at 16:04):

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 (Dec 21 2021 at 16:05):

Ah, that makes it clear. Thanks.

Adam Topaz (Dec 21 2021 at 16:05):

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 (Dec 21 2021 at 16:05):

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

Adam Topaz (Dec 21 2021 at 16:06):

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

Bernd Losert (Dec 21 2021 at 16:07):

Yes.

Adam Topaz (Dec 21 2021 at 16:08):

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 (Dec 21 2021 at 16:10):

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

Bernd Losert (Dec 21 2021 at 16:10):

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 (Dec 21 2021 at 16:11):

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

Bernd Losert (Dec 21 2021 at 16:11):

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

Bernd Losert (Dec 21 2021 at 16:11):

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

Bernd Losert (Dec 21 2021 at 16:12):

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

Adam Topaz (Dec 21 2021 at 16:13):

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 (Dec 21 2021 at 16:14):

OK.

Alex J. Best (Dec 21 2021 at 16:16):

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 (Dec 21 2021 at 16:17):

Indeed. I'm already feeling the pain.

Bernd Losert (Dec 21 2021 at 16:18):

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

Reid Barton (Dec 21 2021 at 16:23):

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 (Dec 21 2021 at 16:24):

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 (Dec 21 2021 at 16:25):

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

Reid Barton (Dec 21 2021 at 16:26):

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 (Dec 21 2021 at 16:31):

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 (Dec 21 2021 at 16:51):

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 (Dec 21 2021 at 16:53):

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

Bernd Losert (Dec 21 2021 at 16:57):

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

Reid Barton (Dec 21 2021 at 17:10):

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.


Last updated: Dec 20 2023 at 11:08 UTC