Library QuotientGroup

Section QuotientGroup.

Require Import EnsembleFacts.
Require Import Groups.
Require Import EnsembleAsType.
Require Import types.

Require Import Coq.Sets.Ensembles.
Require Import Coq.Logic.ClassicalEpsilon.
Require Import Coq.Logic.FunctionalExtensionality.

Definition SubgroupOperation (U:Type) (f:Operation U)
(H:Ensemble U) (f':Operation (EAT U H)):= forall (a b:EAT U H),
EAT_fout U H (f' a b)=f (EAT_fout U H a) (EAT_fout U H b).

Lemma SubgroupOperation_same: forall (U:Type) (f:Operation U)
(H:Ensemble U) (g h:Operation (EAT U H)),
SubgroupOperation U f H g ->
SubgroupOperation U f H h ->
g=h.

Definition Subgroup (U:Type) (f:Operation U) (H:Ensemble U):=
Group U f /\ exists f':Operation (EAT U H),
SubgroupOperation U f H f'/\ Group (EAT U H) f'.

Lemma Subgroup_unique_operation: forall (U:Type)
(f:Operation U) (H:Ensemble U), Subgroup U f H->
exists! f':Operation (EAT U H),
SubgroupOperation U f H f'/\ Group (EAT U H) f'.

Lemma Subgroup_operation_Group: forall (U:Type)
(f:Operation U) (H:Ensemble U), Subgroup U f H->
forall f':Operation (EAT U H),
SubgroupOperation U f H f'-> Group (EAT U H) f'.

Theorem Subgroup_nonempty: forall (U:Type) (f:Operation U),
~Subgroup U f (Empty_set U).

Lemma Subgroup_existsin: forall (U:Type) (f:Operation U)
(H:Ensemble U), Subgroup U f H -> exists Hin:U->EAT U H,
EAT_in U H Hin.

Definition Subgroup_in (U:Type) (f:Operation U) (H:Ensemble U)
(SUBG:Subgroup U f H):U->EAT U H.

Definition Subgroup_out (U:Type) (f:Operation U) (H:Ensemble U)
(SUBG:Subgroup U f H):=EAT_fout U H.

Lemma Subgroup_in_ETA: forall (U:Type) (f:Operation U) (H:Ensemble U)
(SUBG:Subgroup U f H), EAT_in U H (Subgroup_in U f H SUBG).

Definition Subgroup_op(U:Type) (f:Operation U) (H:Ensemble U)
(SUBG:Subgroup U f H):=
(fun a b:EAT U H=>(Subgroup_in U f H SUBG)
(f ((Subgroup_out U f H SUBG) a) ((Subgroup_out U f H SUBG) b))).

Lemma Subgroup_op_InH: forall (U:Type) (f:Operation U)
(H:Ensemble U) (SUBG:Subgroup U f H) (a b:EAT U H),
In U H (f (EAT_fout U H a) (EAT_fout U H b)).

Theorem Subgroup_op_operation: forall (U:Type) (f:Operation U)
(H:Ensemble U) (SUBG:Subgroup U f H),
SubgroupOperation U f H (Subgroup_op U f H SUBG).

Lemma Subgroup_uniqueop: forall (U:Type) (f:Operation U)
(H:Ensemble U) (SUBG:Subgroup U f H), forall f':Operation (EAT U H),
SubgroupOperation U f H f' -> f'= Subgroup_op U f H SUBG.

Theorem SubgroupInternalOperation: forall (U:Type)
(f:Operation U) (H:Ensemble U) (f':Operation (EAT U H))
(a b:U),
Subgroup U f H -> SubgroupOperation U f H f' ->
In U H a -> In U H b -> In U H (f a b).


Definition LeftCoset (U:Type) (f:Operation U) (g:U) (H:Ensemble U):=
apply_func U U (fun x:U=>f g x) H.

Definition RightCoset (U:Type) (f:Operation U) (g:U) (H:Ensemble U):=
apply_func U U (fun x:U=>f x g) H.

Lemma LeftCosetSym: forall (U:Type) (f:Operation U) (H:Ensemble U)
(a b:U), Group U f-> Subgroup U f H ->
 In U (LeftCoset U f a H) b -> In U (LeftCoset U f b H) a.
End QuotientGroup.