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

import fnd http://mathhub.info/MitM/Foundation ❚

theory SylowSubgroup : fnd:?Logic =
  // theory SylowSubgroupTheory : 
❚
	
	
  
theory right_coset : fnd:?Logic = 
  include ?subgroup ❙
  theory right_coset_theory : fnd:?Logic > g:G =
    element : G ❘ # g ❙
    type_of_coset : type ❙
  ❚
  FromTheory right_coset : right_coset_theory ❙
  is_right_coset : ⊦ ∀ [el:right_coset.type_of_coset] ∃[h:H] el ≐ h ∘ g ❙
❚
  
theory left_coset : fnd:?Logic = 
  include ?subgroup ❙
  theory left_coset_theory : fnd:?Logic > g:G =
    element : G ❘ # g ❙
    left_coset : type ❙
  ❚
  FromTheory left_coset : left_coset_theory ❙
  is_left_coset : ⊦ ∀ [el:left_coset.type_of_coset] ∃[h:H] el ≐ g ∘ h ❙
❚
  
theory normal_subgroup : fnd:?Logic =
  include ?subgroup ❙
  include ?left_coset ❙
  include ?right_coset ❙
  include ?set_equality ❙
  is_normal_subgroup : ⊦ ∀[g:G] left_coset g = right_coset g ❙
❚

	//T how to handle properties of groups? Being abelian is a property
❙

theory abeliangroup : fnd:?Logic =
	abelian_property : {U : type}{op : U → U → U}prop ❘ = [U][op]∀[x]∀[y] op x y ≐ op y x ❙
	theory abeliangroup_theory : base:?Logic =
		include ?group/group_theory ❙
		
		abelianax : ⊦ abelian_property U op ❙
	❚
	FromTheory abeliangroup : abeliangroup_theory ❙
	
	include ?group ❙
	
	is_abelian : {G : abeliangroup} ⊦ commutative G ❘ = [G] (G.abelianax) ❙
❚
	
theory group_homomorphism : fnd:?Logic =
  include ?group❙
  
  theory group_homomorphism_theory : fnd:?Logic = 
    from: group ❘# A❙
    to: group ❘# B❙
    map: dom A → dom B❙
    morphism_property : ⊦ ∀[x: dom A] ∀[y: dom A] (map x) ∘ (map y) ≐ map (x ∘ y)❙
  ❚
  FromTheory grouphomomorphism : group_homomorphism_theory❙
❚

theory group_action : fnd:?Logic =
  include ?group ❙
  
  theory right_group_action_theory : fnd:?Logic > G : group , Ω : type =
    acting: group ❘ = G ❘ # G ❙
    actee: type ❘ = Ω ❘ # Ω ❙
    map: actee → dom acting → actee ❘ # 1 ^ 2 prec 15 ❙
    right_group_action_property_id : ⊦ ∀[ω : actee] (ω ^ (unit acting) ≐ ω ) ❙
    right_group_action_property_prod : ⊦ ∀[ω : actee] ∀[g : dom acting] ∀[h : dom acting] (ω^g)^h ≐ ω^(g∘h) ❙      
  ❚
  FromTheory rightgroupaction : right_group_action_theory ❙
  
  theory left_group_action_theory : fnd:?Logic > G : group, Ω : type =
    acting : group ❘ = G ❘ # G ❙
    actee : type ❘ = Ω ❘ # Ω ❙
    map : dom acting → actee → actee ❙
    left_group_action_property_id : ⊦ ∀[ω : actee] map (unit acting) ω ≐ ω ❙
  ❚
  FromTheory leftgroupaction :  left_group_action_theory ❙
 
  include ?permutation_representation ❙
  action_from_representation : permutation_representation → rightgroupaction ❘
    = [pa] ❙
❚
  
theory permutation_representation : fnd:?Logic =
  include ?group ❙
  include ?group_homomorphism ❙
  include ?SymmetricGroup ❙
  theory permutation_representation_theory : fnd:?Logic > G : group, Ω : type =
    acting_group : group ❘ = G ❙
    actee_set : type ❘ = Ω ❙
    hom : acting_group → SymmetricGroup actee_set ❙
  ❚
  FromTheory permutation_representation : permutation_representation_theory ❙
❚
  
/T   all other fields of both action and representation are deduced from the group and the set, so i guess this is enough? ❚
view group_action_is_permutation_representation : ?group_action/rightgroupaction → ?permutation_representation/permutation_representation =
  acting_group = acting ❙
  actee_set = actee ❙
❚
  
view permutation_representation_is_group_action : ?permutation_representation/permutation_representation → ?group_action/rightgroupaction =
  acting = acting_group ❙
  actee = actee_set ❙
❚
  
theory group_action_orbit : fnd:?Logic =
  include ?group_action ❙
  theory orbit_theory : fnd:?Logic > action : rightgroupaction, α : action.actee =
    ga : rightgroupaction ❘ = action ❙
    element : ga.actee ❘ = α ❙
    set : {type : ga.actee} ❙
    orbit_set_binding : {orb : orbit} ⊦ ∀[x:orb] ∃[g:ga.acting] ga.map α g ≐ x ❙  
    order : ℕ ❙
  ❚
  FromTheory orbit : orbit_theory ❙
❚
  
theory group_action_stabilizer : fnd:?Logic =
  include ?group_action ❙
  theory stabilizer_theory : fnd:?Logic > action : rightgroupaction, α : action.actee =
    ga : rightgroupaction ❘ = action ❙
    element : ga.actee ❘ = α ❙
    stabilizer : {type : ga.acting} ❙
    stabilizer_set_binding : ⊦ ∀[g:stabilizer] ga.map α g ≐ α ❙
    order : ℕ ❙
  ❚
❚
  
theory orbit_stabilizer_theorem : fnd:?Logic =
  include ?group_action ❙
  include ?group_action_orbit ❙
  include ?group_action_stabilizer ❙
  Omega : type ❙
  G : group ❙
  action : rightgroupaction G Omega ❙
  theorem : ⊦ ∀[α:Omega] ((orbit action α).order) × ((stabilizer action α).order) ≐ (G.order) ❙
❚
  
theory conjugation : fnd:?Logic =
  include ?group ❙
  include ?group_action ❙
  G : group ❙
  Ω : G.dom ❙
  la : leftgroupaction G Ω ❙
  ra : rightgroupaction G Ω ❙
  conjugation : Ω → G.dom → Ω ❘ = [α, g] ra (la (inverseOf g) α) g ❙ 
❚
  
// view conjugation : rightgroupaction =
  acting = G ❙
  actee = Ω ❙
❚
  
theory conjugation_centralizer : fnd:?Logic =
  include ?conjugation ❙
  include ?group_action_stabilizer ❙
  centralizer : {G : group, α : G.dom} type ❘ = stabilizer (conjugation G) α ❙    
❚