GrpPullback.v

Require Import Basics Types Limits.Pullback Cubical.PathSquare.

Require Import Algebra.Groups.Group.

Require Import WildCat.Core.


(** Pullbacks of groups are formalized by equipping the set-pullback with the desired group structure. The universal property in the category of groups is proved by saying that the corecursion principle [grp_pullback_corec] is an equivalence. *)

Local Open Scope mc_scope.

Local Open Scope mc_mult_scope.


Section GrpPullback.


  (* Variables are named to correspond with Limits.Pullback. *)

Context {A B C : Group} (f : B $-> A) (g : C $-> A).


  Local Instance grp_pullback_sgop : SgOp (Pullback f g).

  Proof.

    intros [b [c p]] [d [e q]].

    refine (b * d; c * e; _).

    exact (grp_homo_op_agree _ _ p q).

  Defined.


  Local Instance grp_pullback_sgop_associative
    : Associative grp_pullback_sgop.

  Proof.

    intros [x1 [x2 p]] [y1 [y2 q]] [z1 [z2 u]].

    apply equiv_path_pullback; simpl.

    refine (associativity _ _ _; associativity _ _ _; _).

    apply equiv_sq_path.

    apply path_ishprop.

  Defined.


  Local Instance grp_pullback_issemigroup : IsSemiGroup (Pullback f g) := {}.

  
  Local Instance grp_pullback_mon_unit : MonUnit (Pullback f g)
    := (1; 1; grp_homo_unit f @ (grp_homo_unit g)^).


  Local Instance grp_pullback_leftidentity
    : LeftIdentity grp_pullback_sgop grp_pullback_mon_unit.

  Proof.

    intros [b [c p]]; simpl.

    apply equiv_path_pullback; simpl.

    refine (left_identity _; left_identity _; _).

    apply equiv_sq_path.

    apply path_ishprop.

  Defined.


  Local Instance grp_pullback_rightidentity
    : RightIdentity grp_pullback_sgop grp_pullback_mon_unit.

  Proof.

    intros [b [c p]]; simpl.

    apply equiv_path_pullback; simpl.

    refine (right_identity _; right_identity _; _).

    apply equiv_sq_path.

    apply path_ishprop.

  Defined.


  Local Instance ismonoid_grp_pullback : IsMonoid (Pullback f g) := {}.


  Local Instance grp_pullback_inverse : Inverse (Pullback f g).

  Proof.

    intros [b [c p]].

    refine (b^; c^; grp_homo_inv f b @ _ @ (grp_homo_inv g c)^).

    exact (ap (^) p).

  Defined.


  Local Instance grp_pullback_leftinverse : LeftInverse (.*.) (^) mon_unit.

  Proof.

    unfold LeftInverse.

    intros [b [c p]].

    unfold grp_pullback_sgop; simpl.

    apply equiv_path_pullback; simpl.

    refine (left_inverse _; left_inverse _; _).

    apply equiv_sq_path.

    apply path_ishprop.

  Defined.


  Local Instance grp_pullback_rightinverse : RightInverse (.*.) (^) mon_unit.

  Proof.

    intros [b [c p]].

    unfold grp_pullback_sgop; simpl.

    apply equiv_path_pullback; simpl.

    refine (right_inverse _; right_inverse _; _).

    apply equiv_sq_path.

    apply path_ishprop.

  Defined.


  #[export] Instance isgroup_grp_pullback : IsGroup (Pullback f g) := {}.


  Definition grp_pullback : Group
    := Build_Group (Pullback f g) _ _ _ _.


  Definition grp_pullback_pr1 : grp_pullback $-> B.

  Proof.

    snapply Build_GroupHomomorphism.

 exact pullback_pr1.

 intros x y.

 reflexivity.

  Defined.


  Definition grp_pullback_pr2 : grp_pullback $-> C.

  Proof.

    snapply Build_GroupHomomorphism.

 exact pullback_pr2.

 intros x y.

 reflexivity.

  Defined.


  Proposition grp_pullback_corec {X : Group}
              (b : X $-> B) (c : X $-> C)
              (p : f o b == g o c)
    : X $-> grp_pullback.

  Proof.

    snapply Build_GroupHomomorphism.

 exact (fun x => (b x; c x; p x)).

 intros x y.

      srapply path_sigma.

 simpl.

        apply (grp_homo_op b).

 unfold pr2.

        refine (transport_sigma' _ _ @ _).

 unfold pr1.

        apply path_sigma_hprop.

        simpl.

        apply (grp_homo_op c).

  Defined.


  Corollary grp_pullback_corec' (X : Group)
    : {b : X $-> B & { c : X $-> C & f o b == g o c}}
      -> (X $-> grp_pullback).

  Proof.

    intros [b [c p]]; exact (grp_pullback_corec b c p).

  Defined.


End GrpPullback.


Definition functor_grp_pullback {A A' B B' C C' : Group}
           (f : B $-> A) (f' : B' $-> A')
           (g : C $-> A) (g' : C' $-> A')
           (alpha : A $-> A') (beta : B $-> B') (gamma : C $-> C')
           (h : f' o beta == alpha o f)
           (k : alpha o g == g' o gamma)
  : grp_pullback f g $-> grp_pullback f' g'.

Proof.

  srapply grp_pullback_corec.

 exact (beta $o grp_pullback_pr1 f g).

 exact (gamma $o grp_pullback_pr2 f g).

 intro x; cbn.

    refine (h _ @ ap alpha _ @ k _).

    apply pullback_commsq.

Defined.


Definition equiv_functor_grp_pullback {A A' B B' C C' : Group}
           (f : B $-> A) (f' : B' $-> A')
           (g : C $-> A) (g' : C' $-> A')
           (alpha : GroupIsomorphism A A')
           (beta : GroupIsomorphism B B')
           (gamma : GroupIsomorphism C C')
           (h : f' o beta == alpha o f)
           (k : alpha o g == g' o gamma)
  : GroupIsomorphism (grp_pullback f g) (grp_pullback f' g').

Proof.

  srapply Build_GroupIsomorphism.

  1: exact (functor_grp_pullback f f' g g' _ _ _ h k).

  srapply isequiv_adjointify.

 srapply (functor_grp_pullback f' f g' g).

    1-3: rapply grp_iso_inverse; assumption.

 rapply (equiv_ind beta); intro b.

      refine (ap f (eissect _ _) @ _).

      apply (equiv_ap' alpha _ _)^-1.

      exact ((h b)^ @ (eisretr _ _)^).

 rapply (equiv_ind gamma); intro c.

      refine (_ @ ap g (eissect _ _)^).

      apply (equiv_ap' alpha _ _)^-1.

      exact (eisretr _ _ @ (k c)^).

  all: intro x;
    apply equiv_path_pullback_hset; split; cbn.

  1-2: apply eisretr.

  1-2: apply eissect.

Defined.


(** Pulling back along some [g : Y $-> Z] and then [g' : Y' $-> Y] is the same as pulling back along [g $o g']. *)

Definition equiv_grp_pullback_compose_r {X Z Y Y' : Group} (f : X $-> Z) (g' : Y' $-> Y) (g : Y $-> Z)
  : GroupIsomorphism (grp_pullback (grp_pullback_pr2 f g) g') (grp_pullback f (g $o g')).

Proof.

  srapply Build_GroupIsomorphism.

 srapply grp_pullback_corec.

 exact (grp_pullback_pr1 _ _ $o grp_pullback_pr1 _ _).

 apply grp_pullback_pr2.

 intro x; cbn.

      exact (pullback_commsq _ _ _ @ ap g (pullback_commsq _ _ _)).

 srapply isequiv_adjointify.

 srapply grp_pullback_corec.

 srapply functor_grp_pullback.

        1,2: exact grp_homo_id.

        1: exact g'.

        all: reflexivity.

 apply grp_pullback_pr2.

 reflexivity.

 intro x; cbn.

      by srapply equiv_path_pullback_hset.

 intros [[x [y z0]] [y' z1]]; srapply equiv_path_pullback_hset; split; cbn.

      2: reflexivity.

      srapply equiv_path_pullback_hset; split; cbn.

      1: reflexivity.

      symmetry; exact z1.

Defined.


Section IsEquivGrpPullbackCorec.


  (* New section with Funext at the start of the Context. *)

Context `{Funext} {A B C : Group} (f : B $-> A) (g : C $-> A).


  Lemma grp_pullback_corec_pr1 {X : Group}
        (b : X $-> B) (c : X $-> C)
        (p : f o b == g o c)
    : grp_pullback_pr1 f g $o grp_pullback_corec f g b c p = b.

  Proof.

    apply equiv_path_grouphomomorphism; reflexivity.

  Defined.


  Lemma grp_pullback_corec_pr2 {X : Group}
        (b : X $-> B) (c : X $-> C)
        (p : f o b == g o c)
    : grp_pullback_pr2 f g $o grp_pullback_corec f g b c p = c.

  Proof.

    apply equiv_path_grouphomomorphism; reflexivity.

  Defined.


  Theorem isequiv_grp_pullback_corec (X : Group)
    : IsEquiv (grp_pullback_corec' f g X).

  Proof.

    snapply isequiv_adjointify.

 intro phi.

      refine (grp_pullback_pr1 f g $o phi; grp_pullback_pr2 f g $o phi; _).

      intro x; exact (pullback_commsq f g (phi x)).

 intro phi.

      apply equiv_path_grouphomomorphism; reflexivity.

 intro bcp; simpl.

      srapply path_sigma.

 simpl.

 apply grp_pullback_corec_pr1.

 refine (transport_sigma' _ _ @ _).

        apply path_sigma_hprop; simpl pr1.

        simpl.

 apply grp_pullback_corec_pr2.

  Defined.


End IsEquivGrpPullbackCorec.

Timings for GrpPullback.v