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

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

theory SymmetricGroup : fnd:?Logic =
  include ../algebra?Group ❙
  include ../typedsets?Functions ❙
  include ../typedsets?Bijective ❙
  
    has_inverse : {Ω : type} ⊦ ∀ [x : bijections Ω Ω] (x ° (bijinv x)) ≐ ([y : Ω] y) ❘ # has_inv 1 ❙
	is_leftunital : {Ω : type} ⊦ ∀ [x : bijections Ω Ω] ([y] y) ° x ≐ x ❘ # is_lu 1 ❙
	is_rightunital : {Ω : type} ⊦ ∀ [x : bijections Ω Ω] x ° ([y] y) ≐ x ❘ # is_ru 1 ❙
	
  
  symmetricGroup : type ⟶ group ❘ // = [Ω] ['
    domain := bijections Ω Ω,
    op := function_composition Ω Ω Ω,

    associative := isassoc Ω Ω Ω Ω,
    
    unit := ([ω : Ω] ω),
    leftunital := is_lu Ω, 
    rightunital := is_ru Ω, 
    
    inverse := ([x : domain] inverse_bijections Ω Ω x),
    inverse_property := has_inv Ω
    '] ❙
    
❚
  
theory SymmetricGroupOfN : fnd:?Logic =
  include ?SymmetricGroup ❙
  include arith:?NaturalArithmetics ❙
  
  symmetricGroupOfN : ℕ+ ⟶ group ❘ = [N] symmetricGroup (fromOneTo N) ❙
❚