Regular.v: categories in which one can do diagram chasing

jdchristensen · ThomatoTomato · jdchristensen · commit 237ebdd0582a · 2025-12-21T19:10:47.000-05:00
Co-authored-by: Thomas Wilskow Thorbjørnsen &lt;thomas.w.thorbjornsen@gmail.com&gt;
diff --git a/theories/WildCat/Core.v b/theories/WildCat/Core.v
@@ -150,13 +150,125 @@ Definition cat_comp2 {A} `{Is1Cat A} {a b c : A}
 
 Notation "q $@@ p" := (cat_comp2 q p).
 
-(** Monomorphisms and epimorphisms. *)
+(** Epimorphisms and monomorphisms. *)
 
-Definition Monic {A} `{Is1Cat A} {b c: A} (f : b $-> c)
-  := forall a (g h : a $-> b), f $o g $== f $o h -> g $== h.
+Class Epic {A} `{Is1Cat A} {a b : A} (f : a $-> b)
+  := isepic : forall {c} (g h : b $-> c), g $o f $== h $o f -> g $== h.
 
-Definition Epic {A} `{Is1Cat A} {a b : A} (f : a $-> b)
-  := forall c (g h : b $-> c), g $o f $== h $o f -> g $== h.
+Arguments isepic {A}%_type_scope {IsGraph0 Is2Graph0 Is01Cat0 H a b} f {Epic c} g h _.
+
+Section Epimorphisms.
+
+  Context {A : Type} `{Is1Cat A}.
+
+  #[export]
+  Instance epic_id (P : A) : Epic (Id P).
+  Proof.
+    intros B b b' h.
+    exact ((cat_idr _)^$ $@ h $@ cat_idr _).
+  Defined.
+
+  Definition epic_homotopic {P P'} (f g : P $-> P') `{!Epic f} (h : f $== g)
+    : Epic g.
+  Proof.
+    intros Q x x' h'.
+    apply (isepic f).
+    exact ((x $@L h) $@ h' $@ (x' $@L h^$)).
+  Defined.
+
+  #[export]
+  Instance epic_compose {P P' P'' : A} (f : P $-> P') (g : P' $-> P'')
+    `{!Epic f} `{!Epic g}
+    : Epic (g $o f).
+  Proof.
+    intros Q x x' h.
+    apply (isepic g).
+    apply (isepic f).
+    exact ((cat_assoc f g x) $@ h $@ (cat_assoc_opp f g x')).
+  Defined.
+
+  Definition epic_cancel {P P' P'' : A} (f : P $-> P') (g : P' $-> P'')
+    `{!Epic (g $o f)}
+    : Epic g.
+  Proof.
+    intros Q x x' h.
+    rapply isepic.
+    exact ((cat_assoc_opp f g x) $@ (h $@R f) $@ (cat_assoc f g x')).
+  Defined.
+
+  Definition Epi (P' P : A) := { e : P' $-> P & Epic e }.
+
+  Definition hom_epi {P' P} (e : Epi P' P) := pr1 e : P' $-> P.
+  Coercion hom_epi : Epi >-> Hom.
+
+  #[export]
+  Instance epic_epi {P' P} (e : Epi P' P) : Epic e := pr2 e.
+
+  Definition id_epi P : Epi P P := (Id P; epic_id P).
+
+End Epimorphisms.
+
+Notation "P' $->> P" := (Epi P' P) (at level 99).
+
+(** Monomorphisms could be defined as epimorphisms in the opposite category, which would allow us to reuse the proofs below.  We'd have to move the material on epis and monos to a separate file. *)
+
+Class Monic {A} `{Is1Cat A} {b c: A} (f : b $-> c)
+  := ismonic : forall {a} (g h : a $-> b), f $o g $== f $o h -> g $== h.
+
+Arguments ismonic {A}%_type_scope {IsGraph0 Is2Graph0 Is01Cat0 H b c} f {Monic a} g h _.
+
+Section Monomorphisms.
+
+  Context {A : Type} `{Is1Cat A}.
+
+  #[export]
+  Instance monic_id (P : A) : Monic (Id P).
+  Proof.
+    intros B b b' h.
+    exact ((cat_idl _)^$ $@ h $@ cat_idl _).
+  Defined.
+
+  Definition monic_homotopic {P P'} (f g : P $-> P') `{!Monic f} (h : f $== g)
+    : Monic g.
+  Proof.
+    intros Q x x' h'.
+    apply (ismonic f).
+    exact ((h $@R x) $@ h' $@ (h^$ $@R x')).
+  Defined.
+
+  #[export]
+  Instance monic_compose {P P' P'' : A} (f : P $-> P') (g : P' $-> P'')
+    `{!Monic f} `{!Monic g}
+    : Monic (g $o f).
+  Proof.
+    intros Q x x' h.
+    apply (ismonic f).
+    apply (ismonic g).
+    exact ((cat_assoc_opp x f g) $@ h $@ (cat_assoc x' f g)).
+  Defined.
+
+  Definition monic_cancel {P P' P'' : A} (f : P $-> P') (g : P' $-> P'')
+    `{!Monic (g $o f)}
+    : Monic f.
+  Proof.
+    intros Q x x' h.
+    rapply ismonic.
+    exact ((cat_assoc x f g) $@ (g $@L h) $@ (cat_assoc_opp x' f g)).
+  Defined.
+
+  Definition Mono (P' P : A) := { e : P' $-> P & Monic e }.
+
+  Definition hom_mono {P' P} (m : Mono P' P) := pr1 m : P' $-> P.
+  Coercion hom_mono : Mono >-> Hom.
+
+  #[export]
+  Instance monic_mono {P' P} (e : Mono P' P) : Monic e := pr2 e.
+
+  Definition id_mono P : Mono P P := (Id P; monic_id P).
+
+End Monomorphisms.
+
+Notation "P' $>-> P" := (Mono P' P) (at level 99).
 
 (** Section might be a clearer name but it's better to avoid confusion with Coq keywords. *)
 
diff --git a/theories/WildCat/Regular.v b/theories/WildCat/Regular.v
@@ -0,0 +1,258 @@
+Require Import WildCat.SetoidRewrite.
+Require Import Basics.Overture Basics.Tactics Basics.Equivalences.
+Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd WildCat.PointedCat
+  WildCat.Yoneda WildCat.Graph WildCat.ZeroGroupoid WildCat.Pullbacks
+  WildCat.AbEnriched WildCat.FunctorCat.
+
+(** * A variant of regular categories in which one can do diagram chasing *)
+
+(** ** Definition *)
+
+(** We study a type of wild category that is similar to a regular category.  We assume that the category has all pullbacks and that epimorphisms are preserved by pullbacks.  Note that we are dealing with the ordinary epimorphisms rather than the effective epimorphisms.  This is simply because they are easier to formalize.  Also note that we don't assume that kernel pairs have co-equalizers. *)
+
+Class IsRegular (A : Type) `{Is1Cat A} := {
+    haspullbacks :: HasPullbacks A;
+    stable_epic :: forall {a b c} (f : a $-> c) (g : b $-> c) {ep : Epic f},
+        Epic (cat_pb_pr2 (CatPullback:=haspullbacks a b c f g));
+  }.
+
+(** ** Diagram chasing in a regular category *)
+
+(** One can do a certain amount of diagram chasing in a regular category.  We'll see below that more can be done with an enrichment over abelian groups. *)
+
+Section Regular.
+
+  Context {A : Type} `{IsRegular A}.
+
+  (** A generalized element of [B] with domain [P]. *)
+  Definition elt (P B : A) := P $-> B.
+
+  (** A generalized lift of a generalized element. *)
+  Definition Lift {B C P : A} (c : elt P C) (f : B $-> C)
+    := { P' : A & { e : P' $->> P & { b : elt P' B & f $o b $== c $o e }}}.
+
+  Definition epic_elt_lift {B C : A} (f : B $-> C)
+    (lift : forall P (c : elt P C), Lift c f)
+    : Epic f.
+  Proof.
+    specialize (lift C (Id C)).
+    destruct lift as [P' [[e ep] [b h]]].
+    cbn in h.
+    pose proof (h' := h $@ cat_idl e); clear h.
+    rapply (epic_cancel b f).
+    apply (epic_homotopic _ _ h'^$).
+  Defined.
+
+  (** For the converse, we need the pullback epi of an epi. *)
+  Definition cat_pb_pr2_epi {a b c : A} (f : a $->> c) (g : b $-> c)
+    : cat_pb f g $->> b.
+  Proof.
+    exists (cat_pb_pr2 (f:=f) (g:=g)).
+    exact _.
+  Defined.
+
+  Definition elt_lift_epic {B C : A} (f : B $-> C) {ef : Epic f}
+    {P} (c : elt P C)
+    : Lift c f.
+  Proof.
+    exists (cat_pb f c).
+    exists (cat_pb_pr2_epi (f; ef) c).
+    exists (cat_pb_pr1 (f:=f) (g:=c)).
+    apply cat_pb_glue.
+  Defined.
+
+  (** The definition of [Monic] already implicitly involves generalized elements.  So this result isn't really needed, but might become more useful if we have a separate notation for applying a function to an [elt]. *)
+  Definition monic_via_elt {B C : A} (f : B $-> C)
+    (m : forall P (b b' : elt P B), f $o b $== f $o b' -> b $== b')
+    : Monic f
+    := m.
+
+  (** To lift [b] along [f], it's enough to lift a pullback of [b] along an epi. *)
+  Definition lift_helper {B C P P' : A} {b : elt P C} {f : B $-> C}
+    (e : P' $->> P) (l : Lift (b $o e) f)
+    : Lift b f.
+  Proof.
+    destruct l as [P'' [[e' ep] [b' h]]].
+    exists P''.
+    exists (e $o e'; epic_compose _ _).
+    exists b'.
+    rhs' apply (cat_assoc_opp e' e b).
+    exact h.
+  Defined.
+
+End Regular.
+
+(** ** Regular categories enriched in abelian groups *)
+
+Class IsAbRegular (A : Type) `{Is1Cat A} := {
+    isregular_abregular :: IsRegular A;
+    isabenriched_abregular :: IsAbEnriched A;
+  }.
+
+Section AbRegular.
+
+  Context {A : Type} `{IsAbRegular A}.
+
+  Open Scope mc_add_scope.
+
+  (** We *define* exactness using generalized elements, which avoids needing to assume the existence of kernels, cokernels or images (or even define them).  In a category with kernels and images, you can show that this implies that the natural map from the image to the kernel is monic and epic, so in a nice enough category it is an isomorphism. *)
+
+  Class CatIsAbExact {B C D : A} (f : B $-> C) (g : C $-> D) :=
+    {
+      isabcomplex : g $o f $== 0;
+      isabexact : forall P (b : elt P C), g $o b $== 0 -> Lift b f;
+    }.
+
+  (** If a sequence [B $-> C] and [0 : C $-> D] is exact, then [B $-> C] is epi. *)
+  Definition epic_isabexact_nil_morphism {B C D : A} (f : B $-> C)
+    `{!CatIsAbExact f (0 : C $-> D)}
+    : Epic f.
+  Proof.
+    apply epic_elt_lift.
+    intros P c.
+    apply isabexact.
+    apply precomp_zero.
+  Defined.
+
+  (** If [B $-> C] is epi, then the sequence [B $-> C] and [0 : C$-> D] is exact. *)
+  Definition isabexact_nil_morphism_epic {B C D : A} (f : B $->> C)
+    : CatIsAbExact f (0 : C $-> D).
+  Proof.
+    refine {| isabcomplex := precomp_zero _ |}.
+    intros P c h.
+    rapply elt_lift_epic.
+  Defined.
+
+  (** This is a variant of [ismonic], where the RHS is [0]. *)
+  Definition ismonic' {B C : A} (f : B $-> C) `{!Monic f}
+    {P} (b : elt P B) (h : f $o b $== 0)
+    : b $== 0.
+  Proof.
+    apply (ismonic f).
+    lhs' exact h.
+    symmetry.
+    apply postcomp_zero.
+  Defined.
+
+  (** Monics can be detected if only the zero map is mapped to zero by post composition. *)
+  Definition monic_via_elt_isemb_ab {B C : A} (f : B $-> C)
+   (h : forall P : A, forall b : elt P B, f $o b $== 0 -> b $== 0)
+    : Monic f.
+  Proof.
+    apply monic_via_elt; intros P b' b'' h'.
+    apply inverse_r_homotopy_0gpd in h'.
+    apply (fun x => postcomp_op_inv f b' b'' $@ x) in h'.
+    apply moveL_0M_0gpd.
+    exact (h P (b' - b'') h').
+  Defined.
+
+  (** If [C $-> D] is mono, then the sequence [0 : B $-> C] and [C $-> D] is exact. *)
+  Definition isabexact_nil_morphism_monic {B C D : A} (f : C $>-> D)
+    : CatIsAbExact (0 : B $-> C) f.
+  Proof.
+    refine {| isabcomplex := postcomp_zero _ |}.
+    intros P b h.
+    exists P; exists (id_epi P); exists 0.
+    lhs' apply postcomp_zero.
+    rhs' apply cat_idr.
+    exact (ismonic' f b h)^$.
+  Defined.
+
+  (** If the sequence [0 : B $-> C] and [C $-> D] is exact, then [C $-> D] is a mono. *)
+  Definition monic_isabexact_nil_morphism {B C D : A} (f : C $-> D)
+    `{!CatIsAbExact (0 : B $-> C) f}
+    : Monic f.
+  Proof.
+    apply monic_via_elt.
+    intros P b b' h.
+    apply inverse_r_homotopy_0gpd in h.
+    rewrite <- postcomp_op_inv in h.
+    apply isabexact in h.
+    destruct h as [P' [e [b'' h]]].
+    apply moveL_0M_0gpd.
+    apply (isepic e).
+    rhs' apply precomp_zero.
+    rhs_V' apply (precomp_zero b'').
+    exact h^$.
+  Defined.
+
+End AbRegular.
+
+(** ** Tactics *)
+
+(** The [fix_left] tactic is the key to smooth diagram chasing in an [IsAbRegular] category.  Given [lift : Lift ? ?]; we extract the lifted element using the provided name [d] and the proof it is a lift using the name [l].  Then we update all other generalized elements to have the same domain as [d].  We could also have a limited version of this tactic for an [IsRegular] category. *)
+Ltac fix_lift lift d l :=
+  let P2 := fresh "P" in
+  let e := fresh "e" in
+  let ee := fresh "ee" in
+  destruct lift as [P2 [[e ee] [d l]]];
+  unfold hom_epi, ".1" in l;
+  match type of e with
+  | P2 $-> ?P =>
+      (* Adjust everything involving the domain [P] to have domain [P2]: *)
+      repeat match goal with
+        | [ |- @Lift _ _ _ _ _ _ _ P ?c ?f ] => apply (lift_helper (e; ee)); unfold hom_epi, ".1"
+        | [ |- @GpdHom (@Hom _ _ P _) _ _ _ _ _ ] => apply ee
+        | [ |- @GpdHom (@elt _ _ P _) _ _ _ _ _ ] => apply ee
+        | [ h : @GpdHom (@Hom _ _ P _) _ _ _ _ _ |- _ ] =>
+            apply (fun w => cat_prewhisker w e) in h
+        end;
+      clear ee;
+      (* Reassociate all homotopies so that [e] is right against the map to its left: *)
+      rewrite ? (cat_assoc e);
+      repeat match goal with
+        | [ h : @GpdHom (@Hom _ _ P2 _) _ _ _ _ _ |- _ ] =>
+            rewrite ! (cat_assoc e) in h
+        | [ h : @GpdHom (@Hom _ _ P2 _) _ _ _ _ _ |- _ ] =>
+            rewrite ! (precomp_op_inv e) in h
+        | [ h : @GpdHom (@Hom _ _ P2 _) _ _ _ _ _ |- _ ] =>
+            rewrite ! (precomp_op e) in h
+        | [ h : @GpdHom (@Hom _ _ P2 _) _ _ _ _ _ |- _ ] =>
+            rewrite ! (precomp_inv e) in h
+        end;
+      (* At this point, all generalized elements [c] with domain [P] should only appear in the form [c $o e], so by generalizing [c $o e] we can replace them with elements with domain [P2]. *)
+      repeat match goal with
+        | [ c : elt P ?C |- _ ] =>
+            let tmp := fresh in
+            set (tmp := c $o e : elt P2 _) in *; clearbody tmp; clear c; rename tmp into c
+        end;
+      (* We may also have expressions of the form [0 $o e], so we replace those with [0]. *)
+      rewrite ? (precomp_zero e) in *;
+      (* Now we can get rid of [e] and [P]. Add [try] before these two lines when debugging. *)
+      clear e P;
+      rename P2 into P
+  end.
+
+(** Ideas for making the above tactic faster:
+    - In localized tests, defining and using things like
+        [pose (cp := fun c f g w => cat_prewhisker (c:=c) (f:=f) (g:=g) w e).]
+      made things faster, maybe because typeclass inference of the wild category structure didn't need to be repeated.  But when done here, the overall speed does not improve.
+    - In the last clause of the first [repeat match], we could add "revert h".  Then instead of the second [repeat match] we would just need to do rewriting in the goal, without scanning the context for appropriate terms, using something like:
+        [repeat progress rewrite ? (cat_assoc e), ? (precomp_op_inv e), ? (precomp_op e), ? (precomp_inv e).]
+      For this to work, we need to extend setoid rewriting to handle [->].
+   - Alternatively, in the second [repeat match], we could make the matches more specific to ensure that the lemmas we try apply to the situation.
+*)
+
+Ltac elt_lift_epic f a b l := fix_lift (elt_lift_epic f a) b l.
+
+Tactic Notation "elt_lift_exact" constr(f) constr(g) constr(a) ident(b) ident(l) :=
+  let lift := fresh in
+  unshelve epose proof (lift := isabexact (f:=f) (g:=g) _ a _);
+  only 2: fix_lift lift b l.
+
+(** This allows us to insert a tactic [tac] before [fix_lift] is called.  Typically this is used to clear unneeded hypotheses from the context, which speeds up [fix_lift]. *)
+Tactic Notation "elt_lift_exact" constr(f) constr(g) constr(a) ident(b) ident(l) "using" tactic3(tac) :=
+  let lift := fresh in
+  unshelve epose proof (lift := isabexact (f:=f) (g:=g) _ a _);
+  only 2: (tac; fix_lift lift b l).
+
+(** Given a homotopy [h : a $o b = a' $o b'], use associativity to change [a $o (b $o c)] to [a' $o (b' $o c)]. *)
+Ltac rewrite_with_assoc h :=
+  rewrite (cat_assoc_opp _ _ _ $@ cat_prewhisker h _ $@ cat_assoc _ _ _).
+
+Ltac rewrite_with_assoc_opp h :=
+  rewrite (cat_assoc _ _ _ $@ cat_postwhisker _ h $@ cat_assoc_opp _ _ _).
+
+Ltac provide_lift a :=
+  refine (_; id_epi _; a; _);
+  try rhs' napply cat_idr.
