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 ❙
❚