Torsors

Stream: maths

[Bryan Wang]

In mathlib there is docs#AddTorsor but no "MulTorsor", and furthermore AddTorsor is defined in a different (but I presume equivalent) way. I guess the more common definition of torsor is via a free, transitive group action, so something like

import Mathlib.Algebra.Group.Action.Pretransitive

class AddTorsor
    (G : Type*) [AddGroup G] (F : Type*) [AddAction G F]
    extends AddAction.IsPretransitive G F where
  nonempty : Nonempty F
  free : ∀ (f : F) (g : G), g +ᵥ f = f → g = 0

@[to_additive (attr := mk_iff)]
class MulTorsor
    (G : Type*) [Group G] (F : Type*) [MulAction G F]
    extends MulAction.IsPretransitive G F where
  nonempty : Nonempty F
  free : ∀ (f : F) (g : G), g • f = f → g = 1

Would this be a good definition to have? Surely this has been discussed before, but I'm not sure what is the opinion now.

[Kenny Lau]

your proposed definition has different "data"

[Bryan Wang]

you mean the IsPretransitive vs free?

[Bryan Wang]

If we go with this definition then I will also define free actions separately (right now there are faithful group actions, but not free actions as far as I can tell)

[Bryan Wang]

(deleted)

[Kenny Lau]

it's missing the vsub

[Bryan Wang]

Yeah I think I see the issue, basically the definition above is more like IsTorsor

[Bryan Wang]

We can show that the original docs#AddTorsor satisfies IsAddTorsor, and also show things like the equiv to group given a base point, rough sketch:

import Mathlib.Algebra.Group.Action.Pretransitive
import Mathlib.Algebra.AddTorsor.Defs
import Mathlib.GroupTheory.GroupAction.Hom

class IsAddTorsor
    (G : Type*) [AddGroup G] (F : Type*) [AddAction G F]
    extends AddAction.IsPretransitive G F where
  nonempty : Nonempty F
  free : ∀ (f : F) (g : G), g +ᵥ f = f → g = 0

@[to_additive (attr := mk_iff)]
class IsMulTorsor
    (G : Type*) [Group G] (F : Type*) [MulAction G F]
    extends MulAction.IsPretransitive G F where
  nonempty : Nonempty F
  free : ∀ (f : F) (g : G), g • f = f → g = 1

instance AddTorsor.isAddTorsor {G : Type*} [AddGroup G] {F : Type*} [AddTorsor G F] :
    IsAddTorsor G F where
  exists_vadd_eq x y := ⟨y -ᵥ x, vsub_vadd' _ _⟩
  nonempty := nonempty
  free f g h := (vsub_self f) ▸ (h ▸ (vadd_vsub' g f)).symm

@[to_additive]
noncomputable def IsMulTorsor.equiv_group (G : Type*) [Group G] (F : Type*)
    [MulAction G F] [IsMulTorsor G F]
    (b : F) :
    F ≃ G where
  toFun f := (toIsPretransitive.exists_smul_eq b f).choose
  invFun g := g • b
  left_inv := by
    refine Function.leftInverse_iff_comp.mpr ?_
    ext f; simpa using (toIsPretransitive.exists_smul_eq b f).choose_spec
  right_inv := by
    refine Function.rightInverse_iff_comp.mpr ?_
    ext g; simp only [Function.comp_apply, id_eq]
    apply inv_mul_eq_one.mp
    apply free b _
    rw [mul_smul]
    exact inv_smul_eq_iff.mpr
      (toIsPretransitive.exists_smul_eq b (g • b)).choose_spec.symm

if this looks ok then maybe I will open a PR with this definition.