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

(** Image of group homomorphisms *)

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.

(** The image of a group homomorphism between groups is a subgroup *)
Definition grp_image {A B : Group} (f : A $-> B) : Subgroup B.
A, B: Group
f: A $-> B
Subgroup B
Proof.
A, B: Group
f: A $-> B
Subgroup B
  snrapply (Build_Subgroup _ (fun b => hexists (fun a => f a = b))).
A, B: Group
f: A $-> B
IsSubgroup
  (fun b : B => hexists (fun a : A => f a = b))
  repeat split.
A, B: Group
f: A $-> B
forall x : B, IsHProp (hexists (fun a : A => f a = x))
A, B: Group
f: A $-> B
hexists (fun a : A => f a = mon_unit)
A, B: Group
f: A $-> B
forall x y : B,
hexists (fun a : A => f a = x) ->
hexists (fun a : A => f a = y) ->
hexists (fun a : A => f a = x * y)
A, B: Group
f: A $-> B
forall x : B,
hexists (fun a : A => f a = x) ->
hexists (fun a : A => f a = - x)
  1: exact _.
A, B: Group
f: A $-> B
hexists (fun a : A => f a = mon_unit)
A, B: Group
f: A $-> B
forall x y : B,
hexists (fun a : A => f a = x) ->
hexists (fun a : A => f a = y) ->
hexists (fun a : A => f a = x * y)
A, B: Group
f: A $-> B
forall x : B,
hexists (fun a : A => f a = x) ->
hexists (fun a : A => f a = - x)
  1: apply tr; exists mon_unit; apply grp_homo_unit.
A, B: Group
f: A $-> B
forall x y : B,
hexists (fun a : A => f a = x) ->
hexists (fun a : A => f a = y) ->
hexists (fun a : A => f a = x * y)
A, B: Group
f: A $-> B
forall x : B,
hexists (fun a : A => f a = x) ->
hexists (fun a : A => f a = - x)
  {
A, B: Group
f: A $-> B
forall x y : B,
hexists (fun a : A => f a = x) ->
hexists (fun a : A => f a = y) ->
hexists (fun a : A => f a = x * y) intros x y p q; strip_truncations; apply tr.
A, B: Group
f: A $-> B
x, y: B
q: {a : A & f a = y}
p: {a : A & f a = x}
{a : A & f a = x * y}
    destruct p as [a []], q as [b []].
A, B: Group
f: A $-> B
x, y: B
b, a: A
{a0 : A & f a0 = f a * f b}
    exists (a * b).
A, B: Group
f: A $-> B
x, y: B
b, a: A
f (a * b) = f a * f b
    apply grp_homo_op. }
A, B: Group
f: A $-> B
forall x : B,
hexists (fun a : A => f a = x) ->
hexists (fun a : A => f a = - x)
  intros b p.
A, B: Group
f: A $-> B
b: B
p: hexists (fun a : A => f a = b)
hexists (fun a : A => f a = - b)
  strip_truncations.
A, B: Group
f: A $-> B
b: B
p: {a : A & f a = b}
hexists (fun a : A => f a = - b)
  destruct p as [a []].
A, B: Group
f: A $-> B
b: B
a: A
hexists (fun a0 : A => f a0 = - f a)
  apply tr; exists (- a).
A, B: Group
f: A $-> B
b: B
a: A
f (- a) = - f a
  apply grp_homo_inv.
Defined.

Definition grp_image_in {A B : Group} (f : A $-> B) : A $-> grp_image f.
A, B: Group
f: A $-> B
A $-> grp_image f
Proof.
A, B: Group
f: A $-> B
A $-> grp_image f
  snrapply Build_GroupHomomorphism.
A, B: Group
f: A $-> B
A -> grp_image f
A, B: Group
f: A $-> B
IsSemiGroupPreserving ?f
  {
A, B: Group
f: A $-> B
A -> grp_image f intro x.
A, B: Group
f: A $-> B
x: A
grp_image f
    exists (f x).
A, B: Group
f: A $-> B
x: A
grp_image f (f x)
    srapply tr.
A, B: Group
f: A $-> B
x: A
{a : A & f a = f x}
    exists x.
A, B: Group
f: A $-> B
x: A
f x = f x
    reflexivity. }
A, B: Group
f: A $-> B
IsSemiGroupPreserving
  (fun x : A => (f x; tr (x; 1%path)))
  cbn.
A, B: Group
f: A $-> B
IsSemiGroupPreserving
  (fun x : A => (f x; tr (x; 1%path))) grp_auto.
Defined.

(** When the homomorphism is an embedding, we don't need to truncate. *)
Definition grp_image_embedding {A B : Group} (f : A $-> B) `{IsEmbedding f} : Subgroup B.
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
Subgroup B
Proof.
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
Subgroup B
  snrapply (Build_Subgroup _ (hfiber f)).
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
IsSubgroup (hfiber f)
  repeat split.
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
forall x : B, IsHProp (hfiber f x)
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
hfiber f mon_unit
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
forall x y : B,
hfiber f x -> hfiber f y -> hfiber f (x * y)
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
forall x : B, hfiber f x -> hfiber f (- x)
  -
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
forall x : B, IsHProp (hfiber f x) exact _.
  -
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
hfiber f mon_unit exact (mon_unit; grp_homo_unit f).
  -
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
forall x y : B,
hfiber f x -> hfiber f y -> hfiber f (x * y) intros x y [a []] [b []].
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
x, y: B
a, b: A
hfiber f (f a * f b)
    exists (a * b).
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
x, y: B
a, b: A
f (a * b) = f a * f b
    apply grp_homo_op.
  -
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
forall x : B, hfiber f x -> hfiber f (- x) intros b [a []].
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
b: B
a: A
hfiber f (- f a)
    exists (-a).
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
b: B
a: A
f (- a) = - f a
    apply grp_homo_inv.
Defined.

Definition grp_image_in_embedding {A B : Group} (f : A $-> B) `{IsEmbedding f}
  : GroupIsomorphism A (grp_image_embedding f).
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
GroupIsomorphism A (grp_image_embedding f)
Proof.
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
GroupIsomorphism A (grp_image_embedding f)
  snrapply Build_GroupIsomorphism.
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
GroupHomomorphism A (grp_image_embedding f)
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
IsEquiv ?grp_iso_homo
  -
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
GroupHomomorphism A (grp_image_embedding f) snrapply Build_GroupHomomorphism.
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
A -> grp_image_embedding f
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
IsSemiGroupPreserving ?f
    +
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
A -> grp_image_embedding f intro x.
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
x: A
grp_image_embedding f
      exists (f x).
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
x: A
grp_image_embedding f (f x)
      exists x.
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
x: A
f x = f x
      reflexivity.
    +
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
IsSemiGroupPreserving (fun x : A => (f x; x; 1%path)) cbn; grp_auto.
  -
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
IsEquiv
  (Build_GroupHomomorphism
     (fun x : A => (f x; x; 1%path))) apply isequiv_surj_emb.
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
ReflectiveSubuniverse.IsConnMap 
  (Tr (-1))
  (Build_GroupHomomorphism
     (fun x : A => (f x; x; 1%path)))
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
IsEmbedding
  (Build_GroupHomomorphism
     (fun x : A => (f x; x; 1%path)))
    2: apply (cancelL_isembedding (g:=pr1)).
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
ReflectiveSubuniverse.IsConnMap 
  (Tr (-1))
  (Build_GroupHomomorphism
     (fun x : A => (f x; x; 1%path)))
    intros [b [a p]]; cbn.
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
b: B
a: A
p: f a = b
ReflectiveSubuniverse.IsConnected 
  (Tr (-1))
  (hfiber (fun x : A => (f x; x; 1%path)) (b; a; p))
    rapply contr_inhabited_hprop.
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
b: B
a: A
p: f a = b
Tr (-1)
  (hfiber (fun x : A => (f x; x; 1%path)) (b; a; p))
    refine (tr (a; _)).
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
b: B
a: A
p: f a = b
(f a; a; 1%path) = (b; a; p)
    srapply path_sigma'.
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
b: B
a: A
p: f a = b
f a = b
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
b: B
a: A
p: f a = b
transport (hfiber f) ?p (a; 1%path) = (a; p)
    1: exact p.
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
b: B
a: A
p: f a = b
transport (hfiber f) p (a; 1%path) = (a; p)
    refine (transport_sigma' _ _ @ _).
A, B: Group
f: A $-> B
IsEmbedding0: IsEmbedding f
b: B
a: A
p: f a = b
((a; 1%path).1;
transport (fun x : B => f (a; 1%path).1 = x) p
  (a; 1%path).2) = (a; p)
    by apply path_sigma_hprop.
Defined.