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 Subgroups : fnd:?Logic =
  include ../algebra?Group ❙
  theory subgroups_theory : fnd:?Logic? > G : group ❘ =
  	 universe : subtypeOf (G.universe) ❘ # U ❙
  	 
  	 op : U ⟶ U ⟶ U ❘ # 1 ∘ 2 ❙
  	 op_closure : ⊦ ∀ [x : U] ∀ [y : U] (G.op) x y ≐ op x y ❙
  	 
	 unit : U ❘ # e prec -1 ❙
	 unit_closure : ⊦ (G.unit) ≐ e ❙
	 
	 inverse : U ⟶ U ❘ # 1 ⁻¹  prec 24 ❙
	 inverse_property : ⊦ ∀ [x] x ∘ x ⁻¹ ≐ e ❙
	 inverse_closure : ⊦ ∀ [x : U] (G.inverse) x ≐ x ⁻¹ ❙
	 
	 associative : ⊦ ∀[x : U]∀[y : U]∀[z : U] (x ∘ (y ∘ z)) ≐ ((x ∘ y) ∘ z) ❙
	 leftunital : ⊦ ∀[x : U] e ∘ x ≐ x ❙
	 rightunital : ⊦ ∀[x : U] x ∘ e ≐ x ❙
  ❚

  elementsOf : group ⟶ type ❘ = [G] G.universe ❙
  subsetsOf : group ⟶ type ❘ = [G] subtypeOf (elementsOf G) ❙
  subgroupOf : group ⟶ type ❘ // = [G:group] Mod `?Subgroups?subgroups_theory , G ❙
  index : {G : group} subgroupOf G ⟶ ℕ+ ❙
 	 
❚

// theory ActionsOnSubgroups : fnd:?Logic =
	include ?Group ❙
	include ?Subgroups ❙
	include ?GroupActions ❙
	
	subgroupConjugation : {G : group} rightGroupActions G (subgroupOf G) ❙
	elementConjugation : {G : group} rightGroupActions G (elementsOf G) ❙
	
	normaliser : {G : group} (subgroupOf G) → (subgroupOf G) ❘ 
						 = [G] [U : subgroupOf G] rstab (subgroupConjugation G) U ❙   
	
	conjugacyClass : {G : group} (subgroupOf G) → subtypeOf (subgroupOf G) ❘
	           = [G] [U : subgroupOf G] rorbit (subgroupConjugation G) U ❙
						 
  centraliser : {G : group} G.domain → (subgroupOf G) ❘
	           = [G] [x : G.domain] rstab (elementConjugation G) x ❙
❚

// theory NormalSubgroups : fnd:?Logic =
	include ?Subgroups ❙
	
	theory NormalSubgroupsTheory : fnd:?Logic > G : group ❘=
		include ?Subgroups/SubgroupsTheory ❙
		
		normal_prop : ⊦ ∀[g : G.domain] ∀[n : domain] ∃[n2 : domain] ((G.op) ((G.op) ((G.inverse) g) n) g) ≐ n2 ❙ 
	❚
	
	// This is a HACK ❙
	normalSubgroupOf : group → type ❘ = [g] (ModelsOf `?NormalSubgroups/NormalSubgroupsTheory ) g g ❙
❚

// theory SylowSubgroups : fnd:?Logic = 
	include ?Subgroups ❙
	include core:/arithmetics?intarith ❙
	SylowSubgroups : {G : group} {p : Primes} subtypeOf (subgroupOf G) ❙ 
❚

// theory GroupHomomorphisms : fnd:?Logic = 
	include ?Group ❙
	include ?Subgroups ❙
	include ?NormalSubgroups ❙

	theory GroupHomomorphismsTheory : fnd:?Logic > G : group, H : group ❘ = 
		map : G.domain → H.domain ❙
    morphism_property : ⊦ ∀[x : G.domain] ∀[y : G.domain] (H.op) (map x) (map y) ≐ map ((G.op) x y)❙
  ❚ // 
  hom : group → group → type ❘ = ModelsOf `?GroupHomomorphisms/GroupHomomorphismsTheory ❘ # 1 --> 2 ❙

  // Of course the type of kernel should be more precise! ❙
  // kernel : {G : group} {H : group} hom G H → (subgroupOf G) ❙
	kernel : {G : group} {H : group} (hom G H) → (normalSubgroupOf G) ❙
  image : {G : group} {H : group} (hom G H) → (subgroupOf H) ❙	
❚