Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Algebra.Groups.Group.
Require Import Algebra.Groups.Subgroup.
Require Import WildCat.Core.

(** * Kernels of group homomorphisms *)

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.

Definition grp_kernel {A B : Group} (f : GroupHomomorphism A B) : NormalSubgroup A.
A, B: Group
f: GroupHomomorphism A B
NormalSubgroup A
Proof.
A, B: Group
f: GroupHomomorphism A B
NormalSubgroup A
  snrapply Build_NormalSubgroup.
A, B: Group
f: GroupHomomorphism A B
Subgroup A
A, B: Group
f: GroupHomomorphism A B
IsNormalSubgroup ?normalsubgroup_subgroup
  -
A, B: Group
f: GroupHomomorphism A B
Subgroup A srapply (Build_Subgroup' (fun x => f x = group_unit)).
A, B: Group
f: GroupHomomorphism A B
(fun x : A => f x = group_unit) mon_unit
A, B: Group
f: GroupHomomorphism A B
forall x y : A,
(fun x0 : A => f x0 = group_unit) x ->
(fun x0 : A => f x0 = group_unit) y ->
(fun x0 : A => f x0 = group_unit) (x * - y)
    1: apply grp_homo_unit.
A, B: Group
f: GroupHomomorphism A B
forall x y : A,
(fun x0 : A => f x0 = group_unit) x ->
(fun x0 : A => f x0 = group_unit) y ->
(fun x0 : A => f x0 = group_unit) (x * - y)
    intros x y p q; cbn in p, q; cbn.
A, B: Group
f: GroupHomomorphism A B
x, y: A
p: f x = group_unit
q: f y = group_unit
f (x * - y) = group_unit
    refine (grp_homo_op _ _ _ @ ap011 _ p _ @ _).
A, B: Group
f: GroupHomomorphism A B
x, y: A
p: f x = group_unit
q: f y = group_unit
f (- y) = ?Goal
A, B: Group
f: GroupHomomorphism A B
x, y: A
p: f x = group_unit
q: f y = group_unit
group_unit * ?Goal = group_unit
    1: apply grp_homo_inv.
A, B: Group
f: GroupHomomorphism A B
x, y: A
p: f x = group_unit
q: f y = group_unit
group_unit * - f y = group_unit
    rewrite q; apply right_inverse.
  -
A, B: Group
f: GroupHomomorphism A B
IsNormalSubgroup
  (Build_Subgroup' (fun x : A => f x = group_unit)
     (grp_homo_unit f)
     (fun (x y : A)
        (p : (fun x0 : A => f x0 = group_unit) x)
        (q : (fun x0 : A => f x0 = group_unit) y) =>
      (grp_homo_op f x (- y) @
       ap011 sg_op p (grp_homo_inv f y)) @
      internal_paths_rew_r
        (fun g : B => group_unit * - g = group_unit)
        (right_inverse group_unit) q
      :
      (fun x0 : A => f x0 = group_unit) (x * - y))) intros x y; cbn.
A, B: Group
f: GroupHomomorphism A B
x, y: A
f (- x * y) = group_unit <~> f (x * - y) = group_unit
    rewrite 2 grp_homo_op.
A, B: Group
f: GroupHomomorphism A B
x, y: A
f (- x) * f y = group_unit <~>
f x * f (- y) = group_unit
    rewrite 2 grp_homo_inv.
A, B: Group
f: GroupHomomorphism A B
x, y: A
- f x * f y = group_unit <~> f x * - f y = group_unit
    refine (_^-1 oE grp_moveL_M1).
A, B: Group
f: GroupHomomorphism A B
x, y: A
f x * - f y = group_unit <~> f y = f x
    refine (_ oE equiv_path_inverse _ _).
A, B: Group
f: GroupHomomorphism A B
x, y: A
group_unit = f x * - f y <~> f y = f x
    apply grp_moveR_1M.
  Defined.

(** ** Corecursion principle for group kernels *)

Proposition grp_kernel_corec {A B G : Group} {f : A $-> B} (g : G $-> A)
            (h : f $o g == grp_homo_const) : G $-> grp_kernel f.
A, B, G: Group
f: A $-> B
g: G $-> A
h: f $o g == grp_homo_const
G $-> grp_kernel f
Proof.
A, B, G: Group
f: A $-> B
g: G $-> A
h: f $o g == grp_homo_const
G $-> grp_kernel f
  snrapply Build_GroupHomomorphism.
A, B, G: Group
f: A $-> B
g: G $-> A
h: f $o g == grp_homo_const
G -> grp_kernel f
A, B, G: Group
f: A $-> B
g: G $-> A
h: f $o g == grp_homo_const
IsSemiGroupPreserving ?f
  -
A, B, G: Group
f: A $-> B
g: G $-> A
h: f $o g == grp_homo_const
G -> grp_kernel f exact (fun x:G => (g x; h x)).
  -
A, B, G: Group
f: A $-> B
g: G $-> A
h: f $o g == grp_homo_const
IsSemiGroupPreserving (fun x : G => (g x; h x)) intros x x'.
A, B, G: Group
f: A $-> B
g: G $-> A
h: f $o g == grp_homo_const
x, x': G
(g (x * x'); h (x * x')) = (g x; h x) * (g x'; h x')
    apply path_sigma_hprop; cbn.
A, B, G: Group
f: A $-> B
g: G $-> A
h: f $o g == grp_homo_const
x, x': G
g (x * x') = g x * g x'
    apply grp_homo_op.
Defined.

Theorem equiv_grp_kernel_corec `{Funext} {A B G : Group} {f : A $-> B}
  : (G $-> grp_kernel f) <~> (exists g : G $-> A, f $o g == grp_homo_const).
H: Funext
A, B, G: Group
f: A $-> B
(G $-> grp_kernel f) <~>
{g : G $-> A & f $o g == grp_homo_const}
Proof.
H: Funext
A, B, G: Group
f: A $-> B
(G $-> grp_kernel f) <~>
{g : G $-> A & f $o g == grp_homo_const}
  srapply equiv_adjointify.
H: Funext
A, B, G: Group
f: A $-> B
(G $-> grp_kernel f) ->
{g : G $-> A & f $o g == grp_homo_const}
H: Funext
A, B, G: Group
f: A $-> B
{g : G $-> A & f $o g == grp_homo_const} ->
G $-> grp_kernel f
H: Funext
A, B, G: Group
f: A $-> B
?f o ?g == idmap
H: Funext
A, B, G: Group
f: A $-> B
?g o ?f == idmap
  -
H: Funext
A, B, G: Group
f: A $-> B
(G $-> grp_kernel f) ->
{g : G $-> A & f $o g == grp_homo_const} intro k.
H: Funext
A, B, G: Group
f: A $-> B
k: G $-> grp_kernel f
{g : G $-> A & f $o g == grp_homo_const}
    srefine (_ $o k; _).
H: Funext
A, B, G: Group
f: A $-> B
k: G $-> grp_kernel f
grp_kernel f $-> A
H: Funext
A, B, G: Group
f: A $-> B
k: G $-> grp_kernel f
(fun g : G $-> A => f $o g == grp_homo_const)
  (?Goal $o k)
    1: apply subgroup_incl.
H: Funext
A, B, G: Group
f: A $-> B
k: G $-> grp_kernel f
(fun g : G $-> A => f $o g == grp_homo_const)
  (subgroup_incl (grp_kernel f) $o k)
    intro x; cbn.
H: Funext
A, B, G: Group
f: A $-> B
k: G $-> grp_kernel f
x: G
f (k x).1 = group_unit
    exact (k x).2.
  -
H: Funext
A, B, G: Group
f: A $-> B
{g : G $-> A & f $o g == grp_homo_const} ->
G $-> grp_kernel f intros [g p].
H: Funext
A, B, G: Group
f: A $-> B
g: G $-> A
p: f $o g == grp_homo_const
G $-> grp_kernel f
    exact (grp_kernel_corec _ p).
  -
H: Funext
A, B, G: Group
f: A $-> B
(fun k : G $-> grp_kernel f =>
 (subgroup_incl (grp_kernel f) $o k;
 (fun x : G =>
  (k x).2
  :
  (f $o (subgroup_incl (grp_kernel f) $o k)) x =
  grp_homo_const x)
 :
 (fun g : G $-> A => f $o g == grp_homo_const)
   (subgroup_incl (grp_kernel f) $o k)))
o (fun X : {g : G $-> A & f $o g == grp_homo_const} =>
   (fun (g : G $-> A) (p : f $o g == grp_homo_const)
    => grp_kernel_corec g p) X.1 X.2) == idmap intros [g p].
H: Funext
A, B, G: Group
f: A $-> B
g: G $-> A
p: f $o g == grp_homo_const
(subgroup_incl (grp_kernel f) $o grp_kernel_corec g p;
fun x : G => (grp_kernel_corec g p x).2) = (g; p)
    apply path_sigma_hprop; unfold pr1.
H: Funext
A, B, G: Group
f: A $-> B
g: G $-> A
p: f $o g == grp_homo_const
subgroup_incl (grp_kernel f) $o grp_kernel_corec g p =
g
    apply equiv_path_grouphomomorphism; intro; reflexivity.
  -
H: Funext
A, B, G: Group
f: A $-> B
(fun X : {g : G $-> A & f $o g == grp_homo_const} =>
 (fun (g : G $-> A) (p : f $o g == grp_homo_const) =>
  grp_kernel_corec g p) X.1 X.2)
o (fun k : G $-> grp_kernel f =>
   (subgroup_incl (grp_kernel f) $o k;
   (fun x : G =>
    (k x).2
    :
    (f $o (subgroup_incl (grp_kernel f) $o k)) x =
    grp_homo_const x)
   :
   (fun g : G $-> A => f $o g == grp_homo_const)
     (subgroup_incl (grp_kernel f) $o k))) == idmap intro k.
H: Funext
A, B, G: Group
f: A $-> B
k: G $-> grp_kernel f
grp_kernel_corec (subgroup_incl (grp_kernel f) $o k)
  (fun x : G => (k x).2) = k
    apply equiv_path_grouphomomorphism; intro x.
H: Funext
A, B, G: Group
f: A $-> B
k: G $-> grp_kernel f
x: G
grp_kernel_corec (subgroup_incl (grp_kernel f) $o k)
  (fun x : G => (k x).2) x = k x
    apply path_sigma_hprop; reflexivity.
Defined.

(** ** Characterisation of group embeddings *)
Proposition equiv_kernel_isembedding `{Univalence} {A B : Group} (f : A $-> B)
  : (grp_kernel f = trivial_subgroup :> Subgroup A) <~> IsEmbedding f.
H: Univalence
A, B: Group
f: A $-> B
grp_kernel f = trivial_subgroup <~> IsEmbedding f
Proof.
H: Univalence
A, B: Group
f: A $-> B
grp_kernel f = trivial_subgroup <~> IsEmbedding f
  refine (_ oE (equiv_path_subgroup' _ _)^-1%equiv).
H: Univalence
A, B: Group
f: A $-> B
(forall g : A, grp_kernel f g <-> trivial_subgroup g) <~>
IsEmbedding f
  apply equiv_iff_hprop_uncurried.
H: Univalence
A, B: Group
f: A $-> B
(forall g : A, grp_kernel f g <-> trivial_subgroup g) <->
IsEmbedding f
  refine (iff_compose _ (isembedding_grouphomomorphism f)); split.
H: Univalence
A, B: Group
f: A $-> B
(forall g : A, grp_kernel f g <-> trivial_subgroup g) ->
forall a : A, f a = group_unit -> a = group_unit
H: Univalence
A, B: Group
f: A $-> B
(forall a : A, f a = group_unit -> a = group_unit) ->
forall g : A, grp_kernel f g <-> trivial_subgroup g
  -
H: Univalence
A, B: Group
f: A $-> B
(forall g : A, grp_kernel f g <-> trivial_subgroup g) ->
forall a : A, f a = group_unit -> a = group_unit intros E ? ?.
H: Univalence
A, B: Group
f: A $-> B
E: forall g : A,
grp_kernel f g <-> trivial_subgroup g
a: A
X: f a = group_unit
a = group_unit
    by apply E.
  -
H: Univalence
A, B: Group
f: A $-> B
(forall a : A, f a = group_unit -> a = group_unit) ->
forall g : A, grp_kernel f g <-> trivial_subgroup g intros e a; split.
H: Univalence
A, B: Group
f: A $-> B
e: forall a : A, f a = group_unit -> a = group_unit
a: A
grp_kernel f a -> trivial_subgroup a
H: Univalence
A, B: Group
f: A $-> B
e: forall a : A, f a = group_unit -> a = group_unit
a: A
trivial_subgroup a -> grp_kernel f a
    +
H: Univalence
A, B: Group
f: A $-> B
e: forall a : A, f a = group_unit -> a = group_unit
a: A
grp_kernel f a -> trivial_subgroup a apply e.
    +
H: Univalence
A, B: Group
f: A $-> B
e: forall a : A, f a = group_unit -> a = group_unit
a: A
trivial_subgroup a -> grp_kernel f a intro p.
H: Univalence
A, B: Group
f: A $-> B
e: forall a : A, f a = group_unit -> a = group_unit
a: A
p: trivial_subgroup a
grp_kernel f a
      exact (ap _ p @ grp_homo_unit f).
Defined.