namespace http://mathhub.info/MitM/core/algebra/groups ❚

import fnd http://mathhub.info/MitM/Foundation ❚
import core http://mathhub.info/MitM/core ❚
import sets hhttp://mathhub.info/MitM/core/sets ❚

theory GroupActions : fnd:?Logic = 
  include ../algebra?Group ❙
  include ?Subgroups ❙
//  include ?SymmetricGroup ❙
    
  theory RightGroupActionsTheory : fnd:?Logic > G : group, Ω : type ❘ =
    act : Ω ⟶ G.universe ⟶ Ω ❘ # 1 ^ 2 prec 10 ❙
    act_property_id : ⊦ ∀[ω : Ω] (ω ^ (G.unit)) ≐ ω ❙
    act_property_compose : ⊦ ∀[ω : Ω] ∀[g : G.universe] ∀[h : G.universe] ((ω ^ g) ^ h) ≐ (ω ^ ((G.op) g h)) ❙
  ❚
  rightGroupActions : group ⟶ type ⟶ type ❘ = [G,Ω] Mod `?GroupActions/RightGroupActionsTheory , G , Ω ❙
  
  asAction : {G : group, Ω : type, act : Ω ⟶ G.universe ⟶ Ω}{p1 :  ⊦ ∀[ω : Ω] (act ω (G.unit)) ≐ ω}
  		{p2 : ⊦ ∀[ω : Ω] ∀[g : G.universe] ∀[h : G.universe] (act (act ω g) h) ≐ (act ω ((G.op) g h))} rightGroupActions G Ω ❘
  		= [G, Ω, act, p1, p2] [' act := act, act_property_id := p1, act_property_compose := p2 '] ❙
  
  rightOrbit : {G : group, Ω : type} (rightGroupActions G Ω) ⟶ Ω ⟶ subtypeOf Ω ❘ # rorbit 3 4 ❙
  rightStabiliser : {G : group, Ω : type} (rightGroupActions G Ω) ⟶ Ω ⟶ subgroupOf G ❘ # rstab 3 4❙
  
  theory LeftGroupActionsTheory : fnd:?Logic > G : group, Ω : type ❘ =
    act : G.universe ⟶ Ω ⟶ Ω ❘ # 1 ^ 2 prec 10 ❙
    act_property_id : ⊦ ∀[ω : Ω] ((G.unit) ^ ω) ≐ ω ❙
    act_property_compose : ⊦ ∀[ω : Ω] ∀[g : G.universe] ∀[h : G.universe] (h ^ (g ^ ω)) ≐ (((G.op) h g) ^ ω) ❙
  ❚
  
//  ❙
//  theory GroupActionsByHomomorphismTheory : fnd:?Logic > G : group, Ω : type ❘=
//    acthom : hom G (SymmetricGroup Ω) ❙
//  ❚
//  theory GroupActionsByHomomorphismTheory : fnd?Logic > G : group, X : ??? ❘=
//  ❚
❚