Merge pull request HoTT#2346 from jdchristensen/isabepistable_abgroup

The wild category AbGroup satisfies IsAbEpiStable

Author: jdchristensen

test/WildCat/SetoidRewrite.v

@@ -1,5 +1,3 @@
-#[warnings="-deprecated-from-Coq"]
-From Coq Require Init.Tactics. (* TODO: Can remove this line and previous once Rocq 9.0 is our minimum. *)
 From HoTT Require Import Basics.Overture Basics.Tactics.
 From HoTT.WildCat Require Import Core NatTrans Equiv SetoidRewrite.
 

theories/Algebra/AbGroups.v

@@ -8,6 +8,7 @@ Require Export HoTT.Algebra.AbGroups.AbPullback.
 Require Export HoTT.Algebra.AbGroups.AbPushout.
 Require Export HoTT.Algebra.AbGroups.Biproduct.
 Require Export HoTT.Algebra.AbGroups.AbHom.
+Require Export HoTT.Algebra.AbGroups.Coequalizer.
 Require Export HoTT.Algebra.AbGroups.Cyclic.
 Require Export HoTT.Algebra.AbGroups.Centralizer.
 Require Export HoTT.Algebra.AbGroups.FiniteSum.

theories/Algebra/AbGroups/AbHom.v

@@ -1,7 +1,7 @@
 From HoTT Require Import Basics Types.
-From HoTT.WildCat Require Import Core Opposite Bifunctor Square Equiv.
+From HoTT.WildCat Require Import Core Opposite Bifunctor AbEnriched.
 Require Import HSet Truncations.Core Modalities.ReflectiveSubuniverse.
-Require Import Groups.Group Groups.QuotientGroup AbelianGroup Biproduct.
+Require Import Groups.Group AbelianGroup Biproduct.
 
 (** * Homomorphisms from a group to an abelian group form an abelian group. *)
 
@@ -38,126 +38,6 @@ Proof.
   apply commutativity.
 Defined.
 
-(** ** Coequalizers *)
-
-(** Using the cokernel and addition and negation for the homs of abelian groups, we can define the coequalizer of two group homomorphisms as the cokernel of their difference. *)
-Definition ab_coeq {A B : AbGroup} (f g : A $-> B)
-  := ab_cokernel ((-f) + g).
-
-Definition ab_coeq_in {A B : AbGroup} {f g : A $-> B} : B $-> ab_coeq f g.
-Proof.
-  exact grp_quotient_map.
-Defined.
-
-Definition ab_coeq_glue {A B : AbGroup} {f g : A $-> B}
-  : ab_coeq_in (f:=f) (g:=g) $o f $== ab_coeq_in $o g.
-Proof.
-  intros x.
-  napply qglue.
-  apply tr.
-  by exists x.
-Defined.
-
-Definition ab_coeq_rec {A B : AbGroup} {f g : A $-> B}
-  {C : AbGroup} (i : B $-> C) (p : i $o f $== i $o g) 
-  : ab_coeq f g $-> C.
-Proof.
-  snapply (grp_quotient_rec _ _ i).
-  cbn.
-  intros b H.
-  strip_truncations.
-  destruct H as [a q].
-  destruct q; simpl.
-  lhs napply grp_homo_op.
-  lhs napply (ap (+ _)).
-  1: apply grp_homo_inv.
-  apply grp_moveL_M1^-1.
-  exact (p a)^.
-Defined.
-
-Definition ab_coeq_rec_beta_in {A B : AbGroup} {f g : A $-> B}
-  {C : AbGroup} (i : B $-> C) (p : i $o f $== i $o g)
-  : ab_coeq_rec i p $o ab_coeq_in $== i
-  := fun _ => idpath.
-
-Definition ab_coeq_ind_hprop {A B f g} (P : @ab_coeq A B f g -> Type)
-  `{forall x, IsHProp (P x)}
-  (i : forall b, P (ab_coeq_in b))
-  : forall x, P x.
-Proof.
-  rapply Quotient_ind_hprop.
-  exact i.
-Defined.
-
-Definition ab_coeq_ind_homotopy {A B C f g}
-  {l r : @ab_coeq A B f g $-> C}
-  (p : l $o ab_coeq_in $== r $o ab_coeq_in) 
-  : l $== r.
-Proof.
-  srapply ab_coeq_ind_hprop.
-  exact p.
-Defined.
-
-Definition functor_ab_coeq {A B : AbGroup} {f g : A $-> B} {A' B' : AbGroup} {f' g' : A' $-> B'}
-  (a : A $-> A') (b : B $-> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
-  : ab_coeq f g $-> ab_coeq f' g'.
-Proof.
-  snapply ab_coeq_rec.
-  1: exact (ab_coeq_in $o b).
-  refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _).
-  refine ((_ $@L p^$) $@ _ $@ (_ $@L q)).
-  refine (cat_assoc_opp _ _ _ $@ (_ $@R a) $@ cat_assoc _ _ _).
-  exact ab_coeq_glue.
-Defined.
-
-Definition functor2_ab_coeq {A B : AbGroup} {f g : A $-> B} {A' B' : AbGroup} {f' g' : A' $-> B'}
-  {a a' : A $-> A'} {b b' : B $-> B'}
-  (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
-  (p' : f' $o a' $== b' $o f) (q' : g' $o a' $== b' $o g)
-  (s : b $== b')
-  : functor_ab_coeq a b p q $== functor_ab_coeq a' b' p' q'.
-Proof.
-  snapply ab_coeq_ind_homotopy.
-  intros x.
-  exact (ap ab_coeq_in (s x)).
-Defined.
-
-Definition functor_ab_coeq_compose {A B : AbGroup} {f g : A $-> B}
-  {A' B' : AbGroup} {f' g' : A' $-> B'} 
-  (a : A $-> A') (b : B $-> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
-  {A'' B'' : AbGroup} {f'' g'' : A'' $-> B''}
-  (a' : A' $-> A'') (b' : B' $-> B'')
-  (p' : f'' $o a' $== b' $o f') (q' : g'' $o a' $== b' $o g')
-  : functor_ab_coeq a' b' p' q' $o functor_ab_coeq a b p q
-  $== functor_ab_coeq (a' $o a) (b' $o b) (hconcat p p') (hconcat q q').
-Proof.
-  snapply ab_coeq_ind_homotopy.
-  simpl; reflexivity.
-Defined.
-
-Definition functor_ab_coeq_id {A B : AbGroup} (f g : A $-> B)
-  : functor_ab_coeq (Id _) (Id _) (hrefl f) (hrefl g) $== Id _.
-Proof.
-  snapply ab_coeq_ind_homotopy.
-  reflexivity.
-Defined.
-
-Definition grp_iso_ab_coeq {A B : AbGroup} {f g : A $-> B}
-  {A' B' : AbGroup} {f' g' : A' $-> B'}
-  (a : A $<~> A') (b : B $<~> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
-  : ab_coeq f g $<~> ab_coeq f' g'.
-Proof.
-  snapply cate_adjointify.
-  - exact (functor_ab_coeq a b p q).
-  - exact (functor_ab_coeq a^-1$ b^-1$ (hinverse a _ p) (hinverse a _ q)).
-  - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
-      $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
-    exact (cate_isretr b).
-  - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
-      $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
-    exact (cate_issect b).
-Defined.
-
 (** ** The bifunctor [ab_hom] *)
 
 Instance is0functor_ab_hom01 `{Funext} {A : Group^op}
@@ -220,6 +100,34 @@ Proof.
   by apply equiv_path_grouphomomorphism.
 Defined.
 
+(** ** [AbGroup] has a wild enrichment in wild abelian groups *)
+
+(** Using arguments very similar to the above, but without using [Funext], we can show that [AbGroup] is enriched in the wild sense.  We could use this combined with [Funext] to deduce the results above, but we wouldn't get the extra generality where the domain group does not need to be abelian.  And conversely we don't want to use the above results here, since we don't need to rely on [Funext]. *)
+
+Instance abenriched_abgroup : IsAbEnriched AbGroup.
+Proof.
+  snapply Build_IsAbEnriched.
+  - intros A B.
+    snapply (Build_IsAbGroup_0gpd _ _ _ _ sgop_hom grp_homo_const inverse_hom).
+    3-8: hnf; intros; intro; cbn.
+    + srapply Build_Is0Bifunctor'.
+      snapply Build_Is0Functor.
+      intros [f f'] [g g'] [p p'] a; cbn in *.
+      exact (ap011 _ (p a) (p' a)).
+    + snapply Build_Is0Functor.
+      intros f g p a; cbn.
+      apply (ap _ (p a)).
+    + symmetry; apply associativity.
+    + apply left_identity.
+    + apply right_identity.
+    + apply left_inverse.
+    + apply right_inverse.
+    + apply commutativity.
+  - intros A B C g f f' a; cbn.
+    apply grp_homo_op.
+  - intros A B C f g g' a; cbn. reflexivity.
+Defined.
+
 (** ** Properties of [ab_hom] *)
 
 (** Precomposition with a surjection is an embedding. *)

theories/Algebra/AbGroups/AbPullback.v

@@ -1,8 +1,9 @@
-From HoTT Require Import Basics.
+From HoTT Require Import Basics Types.Universe.
+Require Import Truncations.Core HIT.epi Modalities.ReflectiveSubuniverse.
 Require Import Limits.Pullback Cubical.PathSquare.
 Require Export Algebra.Groups.GrpPullback.
-Require Import Algebra.AbGroups.AbelianGroup.
-Require Import WildCat.Core.
+Require Import AbelianGroup AbHom.
+Require Import WildCat.Core WildCat.Pullbacks WildCat.EpiStable.
 
 Local Open Scope mc_add_scope.
 
@@ -28,3 +29,29 @@ Section AbPullback.
   (** The corecursion principle is inherited from [Group]; use [grp_pullback_corec] and friends from Groups/GrpPullback.v. *)
 
 End AbPullback.
+
+Instance haspullbacks_abgroup : HasPullbacks AbGroup.
+Proof.
+  rapply (haspullbacks_induced abgroup_group).
+  intros A B C f g.
+  exists (ab_pullback f g).
+  reflexivity.
+Defined.
+
+Instance isepistable_abgroup `{Univalence} : IsEpiStable AbGroup.
+Proof.
+  srapply Build_IsEpiStable.
+  1: exact _. (* By the above, [AbGroup] has pullbacks. *)
+  (* We have to show that the categorical epimorphisms are stable under pullback. *)
+  intros A B C f g ef.
+  intros Z k1 k2.
+  (* Since surjections are epimorphisms in [Type], it's enough to show that the pulled back map is a surjection. *)
+  rapply issurj_isepi_funext.
+  (* Since surjections are stable under pullback, it's enough to show that [f] is a surjection. *)
+  apply issurj_pullback_pr2.
+  (* This follows from the fact the epimorphisms of abelian groups are surjections. *)
+  by apply ab_issurj_epi.
+Defined.
+
+(** Combining [isepistable_abgroup] with [abenriched_abgroup] from AbHom.v gives: *)
+Instance isabepistable_abgroup `{Univalence} : IsAbEpiStable AbGroup := {}.

theories/Algebra/AbGroups/AbelianGroup.v

@@ -1,5 +1,6 @@
 From HoTT Require Import Basics Types.
 From HoTT.WildCat Require Import Core Universe Equiv Induced PointedCat.
+Require Import Truncations.Core Modalities.ReflectiveSubuniverse.
 Require Import Spaces.Nat.Core Spaces.Int.
 Require Export Classes.interfaces.canonical_names (Zero, zero, Plus, plus, Negate, negate, Involutive, involutive).
 Require Export Classes.interfaces.abstract_algebra (IsAbGroup(..), abgroup_group, abgroup_commutative).
@@ -275,8 +276,12 @@ Definition ab_mul_natural {A B : AbGroup}
   : f o ab_mul n == ab_mul n o f
   := grp_pow_natural f n.
 
-(** The image of an inclusion is a normal subgroup. *)
-Definition ab_image_embedding {A B : AbGroup} (f : A $-> B) `{IsEmbedding f} : NormalSubgroup B
+(** The image of a homomorphism as a normal subgroup. *)
+Definition ab_image {A : Group} {B : AbGroup} (f : A $-> B) : NormalSubgroup B
+  := {| normalsubgroup_subgroup := grp_image f; normalsubgroup_isnormal := _ |}.
+
+(** The image of an inclusion as a normal subgroup. *)
+Definition ab_image_embedding {A : Group} {B : AbGroup} (f : A $-> B) `{IsEmbedding f} : NormalSubgroup B
   := {| normalsubgroup_subgroup := grp_image_embedding f; normalsubgroup_isnormal := _ |}.
 
 Definition ab_image_in_embedding {A B : AbGroup} (f : A $-> B) `{IsEmbedding f}
@@ -299,3 +304,30 @@ Proof.
   induction q.
   exact (p g).
 Defined.
+
+(** An epimorphism of abelian groups is surjective.  This is likely true for general groups as well, but the proof is more complicated, probably needing an argument like the one given by Trimble, using a lemma by Lumsdaine, here: https://mathoverflow.net/questions/41208/are-all-group-monomorphisms-regular-constructively .  However, the elementary proof for abelian groups also works when the domain is non-abelian, at the cost of having to explicitly state what we mean by epimorphism in this case.  We state this version first. *)
+Definition grp_issurj_epi_ab `{Univalence} {A : Group} {B : AbGroup} (f : A $-> B)
+  {ef : forall (C : AbGroup) (g h : Hom (A:=Group) B C), g $o f $== h $o f -> g $== h}
+  : IsSurjection f.
+Proof.
+  apply issurj_ismaximal_image.
+  apply (ismaximalsubgroup_istrivial_grp_quotient_map _ (ab_image f)).
+  (* The previous line uses univalence, the rest do not. *)
+  change (grp_quotient_map (N:=ab_image f) $== grp_homo_const).
+  rapply (ef (ab_cokernel f)).
+  intro b.
+  apply grp_quotient_map_trivial.
+  apply (grp_homo_image_in f b).
+Defined.
+
+(** The version when both [A] and [B] are abelian immediately follows, where here we assume that [f] is epic in the category of abelian groups. *)
+Definition ab_issurj_epi `{Univalence} {A B : AbGroup} (f : A $-> B) {ef : Epic f}
+  : IsSurjection f
+  := @grp_issurj_epi_ab _ A B f ef.
+
+(** We can also restate [grp_issurj_epi] using the a priori stronger assumption that [f] is epic in the category of groups. *)
+Definition grp_issurj_epi' `{Univalence} {A : Group} {B : AbGroup} (f : A $-> B) {ef : Epic f}
+  : IsSurjection f
+  := @grp_issurj_epi_ab _ A B f (ef o abgroup_group).
+
+(** Note that by [issurj_pullback_pr2], every surjection is an epimorphism in the wild category [Type], so it follows that a surjection of groups or abelian groups is an epimorphism in [Group] or [AbGroup]. *)