namespace http://mathhub.info/MitM/core/algebra/permutationgroup 

import base http://mathhub.info/MitM/Foundation 
import sets http://mathhub.info/MitM/core/typedsets 
import algebra http://mathhub.info/MitM/core/algebra

theory Permutations : base:?Logic =
	include ☞base:?Lists 
	include ☞base:?NatLiterals 
	cycle = List ℕ+ 
	permutation : type 
	PermList : (List cycle) ⟶ permutation 
	fromImage : (List ℕ+) ⟶ permutation 


theory GroupAction : base:?Logic =
  include ☞sets:?Bijective
  include ☞algebra:?Group

  theory groupAction_theory : base:?Logic = 
    include ☞algebra:?Group/group_theory 
    X : type
    phi : U ⟶ (bijections X X)  # Φ
    inner_notation : {g : U, x : X} X = [g,x] (Φ g) x # 1 < 2 >    
    is_action : ⊦  ∀[g: U] ∀[h: U] ∀[x:X] g<h<x>> ≐ (g ∘ h)<x>
  
  groupAction = Mod ☞GroupAction/groupAction_theory
  outer_notation : {GX : groupAction, g : dom GX, x : GX.X} GX.X = [GX,g,x] ((GX.phi) g) x # 2 < 3 >    
  
  include ☞../algebra?RationalPolynomials 
  
  polynomialOrbit : {r : ring} group ⟶ multi_polynomial r ⟶ List (multi_polynomial r)  # orbit 2 3  


theory PermutationGroup : base:?Logic =
  include ☞algebra:?Group
  include ☞sets:?Bijective 
  include ?Permutations 
  include ?GroupAction 
  
  theory permutationGroup_theory : base:?Logic =
    include ?GroupAction/groupAction_theory 
    is_injective_action : ⊦ is_injective Φ 
  
  permutationGroup = Mod ☞?PermutationGroup/permutationGroup_theory 
  
  fromPerm: (List permutation) ⟶ permutationGroup 
  generators : permutationGroup ⟶ List permutation 
  dihedralGroup : ℤ ⟶ permutationGroup 
  

theory TransitiveGroupAction : base:?Logic =
  include ?GroupAction
  theory transitiveGroupAction_theory : base:?Logic = 
    include ?GroupAction/groupAction_theory 
    is_transitive : ⊦ ∀[x:X] ∀[y:X] ∃[g:U] (Φ g) x ≐ y 
  
  transitiveGroupAction = Mod ☞?TransitiveGroupAction/transitiveGroupAction_theory 
  
  
  tr_value : transitiveGroupAction ⟶ ℕ 
  transitiveGroup : ℤ ⟶ ℤ ⟶ transitiveGroupAction 	 meta /MitM/Foundation?Metadata?constructorargument degree
  																					 meta /MitM/Foundation?Metadata?constructorargument tr_value