Skip to content

Commit

Permalink
Merge branch 'patch-2' into patch-3
Browse files Browse the repository at this point in the history
  • Loading branch information
Patrick Nicodemus committed Mar 3, 2025
2 parents 5da3bea + 3f4692d commit 16c51b8
Show file tree
Hide file tree
Showing 162 changed files with 1,457 additions and 1,443 deletions.
39 changes: 20 additions & 19 deletions theories/Algebra/AbGroups/AbHom.v
View file
Original file line number Diff line number Diff line change
@@ -1,21 +1,21 @@
Require Import Basics Types.
Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse.
Require Import Groups.QuotientGroup AbelianGroup Biproduct.
Require Import Groups.Group Groups.QuotientGroup AbelianGroup Biproduct.

(** * Homomorphisms from a group to an abelian group form an abelian group. *)

(** In this file, we use additive notation for the group operation, even though some of the groups we deal with are not assumed to be abelian. *)
Local Open Scope mc_add_scope.

(** The sum of group homomorphisms [f] and [g] is [fun a => f(a) + g(a)]. While the group *laws* require [Funext], the operations do not, so we make them instances. *)
Global Instance sgop_hom {A : Group} {B : AbGroup} : SgOp (A $-> B).
Instance sgop_hom {A : Group} {B : AbGroup} : SgOp (A $-> B).
Proof.
intros f g.
exact (grp_homo_compose ab_codiagonal (grp_prod_corec f g)).
Defined.

(** We can negate a group homomorphism [A -> B] by post-composing with [ab_homo_negation : B -> B]. *)
Global Instance inverse_hom {A : Group} {B : AbGroup}
Instance inverse_hom {A : Group} {B : AbGroup}
: Inverse (@Hom Group _ A B) := grp_homo_compose ab_homo_negation.

(** For [A] and [B] groups, with [B] abelian, homomorphisms [A $-> B] form an abelian group. *)
Expand Down Expand Up @@ -43,12 +43,12 @@ Defined.
Definition ab_coeq {A B : AbGroup} (f g : GroupHomomorphism A B)
:= ab_cokernel ((-f) + g).

Definition ab_coeq_in {A B} {f g : A $-> B} : B $-> ab_coeq f g.
Definition ab_coeq_in {A B : AbGroup} {f g : A $-> B} : B $-> ab_coeq f g.
Proof.
snrapply grp_quotient_map.
Defined.

Definition ab_coeq_glue {A B} {f g : A $-> B}
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.
Expand Down Expand Up @@ -97,7 +97,7 @@ Proof.
exact p.
Defined.

Definition functor_ab_coeq {A B} {f g : A $-> B} {A' B'} {f' g' : A' $-> B'}
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.
Expand All @@ -109,7 +109,7 @@ Proof.
nrapply ab_coeq_glue.
Defined.

Definition functor2_ab_coeq {A B} {f g : A $-> B} {A' B'} {f' g' : A' $-> B'}
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)
Expand All @@ -121,10 +121,10 @@ Proof.
exact (ap ab_coeq_in (s x)).
Defined.

Definition functor_ab_coeq_compose {A B} {f g : A $-> B}
{A' B'} {f' g' : A' $-> B'}
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''} {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')
: functor_ab_coeq a' b' p' q' $o functor_ab_coeq a b p q
Expand All @@ -134,14 +134,15 @@ Proof.
simpl; reflexivity.
Defined.

Definition functor_ab_coeq_id {A B} (f g : A $-> B)
Definition functor_ab_coeq_id {A B : AbGroup} (f g : A $-> B)
: functor_ab_coeq (f:=f) (g:=g) (Id _) (Id _) (hrefl _) (hrefl _) $== Id _.
Proof.
snrapply ab_coeq_ind_homotopy.
reflexivity.
Defined.

Definition grp_iso_ab_coeq {A B} {f g : A $-> B} {A' B'} {f' g' : A' $-> B'}
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.
Expand All @@ -158,7 +159,7 @@ Defined.

(** ** The bifunctor [ab_hom] *)

Global Instance is0functor_ab_hom01 `{Funext} {A : Group^op}
Instance is0functor_ab_hom01 `{Funext} {A : Group^op}
: Is0Functor (ab_hom A).
Proof.
snrapply (Build_Is0Functor _ AbGroup); intros B B' f.
Expand All @@ -169,7 +170,7 @@ Proof.
exact (grp_homo_op f _ _).
Defined.

Global Instance is0functor_ab_hom10 `{Funext} {B : AbGroup@{u}}
Instance is0functor_ab_hom10 `{Funext} {B : AbGroup@{u}}
: Is0Functor (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B).
Proof.
snrapply (Build_Is0Functor (Group^op) AbGroup); intros A A' f.
Expand All @@ -179,7 +180,7 @@ Proof.
by apply equiv_path_grouphomomorphism.
Defined.

Global Instance is1functor_ab_hom01 `{Funext} {A : Group^op}
Instance is1functor_ab_hom01 `{Funext} {A : Group^op}
: Is1Functor (ab_hom A).
Proof.
nrapply Build_Is1Functor.
Expand All @@ -192,7 +193,7 @@ Proof.
by apply equiv_path_grouphomomorphism.
Defined.

Global Instance is1functor_ab_hom10 `{Funext} {B : AbGroup@{u}}
Instance is1functor_ab_hom10 `{Funext} {B : AbGroup@{u}}
: Is1Functor (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B).
Proof.
nrapply Build_Is1Functor.
Expand All @@ -205,13 +206,13 @@ Proof.
by apply equiv_path_grouphomomorphism.
Defined.

Global Instance is0bifunctor_ab_hom `{Funext}
Instance is0bifunctor_ab_hom `{Funext}
: Is0Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
Proof.
rapply Build_Is0Bifunctor''.
Defined.

Global Instance is1bifunctor_ab_hom `{Funext}
Instance is1bifunctor_ab_hom `{Funext}
: Is1Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
Proof.
nrapply Build_Is1Bifunctor''.
Expand All @@ -224,7 +225,7 @@ Defined.

(** Precomposition with a surjection is an embedding. *)
(* This could be deduced from [isembedding_precompose_surjection_hset], but relating precomposition of homomorphisms with precomposition of the underlying maps is tedious, so we give a direct proof. *)
Global Instance isembedding_precompose_surjection_ab `{Funext} {A B C : AbGroup}
Instance isembedding_precompose_surjection_ab `{Funext} {A B C : AbGroup}
(f : A $-> B) `{IsSurjection f}
: IsEmbedding (fmap10 (A:=Group^op) ab_hom f C).
Proof.
Expand Down
2 changes: 1 addition & 1 deletion theories/Algebra/AbGroups/AbPullback.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Section AbPullback.
(* Variables are named to correspond with Limits.Pullback. *)
Context {A B C : AbGroup} (f : B $-> A) (g : C $-> A).

Global Instance ab_pullback_commutative
Instance ab_pullback_commutative
: Commutative (@group_sgop (grp_pullback f g)).
Proof.
unfold Commutative.
Expand Down
3 changes: 2 additions & 1 deletion theories/Algebra/AbGroups/AbPushout.v
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
Require Import Basics Types Truncations.Core.
Require Import WildCat.Core HSet.
Require Import Algebra.Groups.Group.
Require Export Algebra.Groups.QuotientGroup.
Require Import AbGroups.AbelianGroup AbGroups.Biproduct.

Expand Down Expand Up @@ -166,7 +167,7 @@ Defined.
(** ** Properties of pushouts of maps *)

(** The pushout of an epimorphism is an epimorphism. *)
Global Instance ab_pushout_surjection_inr {A B C : AbGroup}
Instance ab_pushout_surjection_inr {A B C : AbGroup}
(f : A $-> B) (g : A $-> C) `{S : IsSurjection f}
: IsSurjection (ab_pushout_inr (f:=f) (g:=g)).
Proof.
Expand Down
32 changes: 16 additions & 16 deletions theories/Algebra/AbGroups/AbelianGroup.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ Record AbGroup := {
}.

Coercion abgroup_group : AbGroup >-> Group.
Global Existing Instance abgroup_commutative.
Existing Instance abgroup_commutative.

Definition zero_abgroup (A : AbGroup) : Zero A := mon_unit.
Definition negate_abgroup (A : AbGroup) : Negate A := inv.
Expand All @@ -37,7 +37,7 @@ Module Import AdditiveInstances.
#[export] Hint Immediate plus_abgroup : typeclass_instances.
End AdditiveInstances.

Global Instance isabgroup_abgroup {A : AbGroup} : IsAbGroup A.
Instance isabgroup_abgroup {A : AbGroup} : IsAbGroup A.
Proof.
split; exact _.
Defined.
Expand Down Expand Up @@ -83,7 +83,7 @@ Definition equiv_path_abgroup_group `{Univalence} {A B : AbGroup}
Local Hint Immediate canonical_names.inverse_is_negate : typeclass_instances.

(** Subgroups of abelian groups are abelian *)
Global Instance isabgroup_subgroup (G : AbGroup) (H : Subgroup G)
Instance isabgroup_subgroup (G : AbGroup) (H : Subgroup G)
: IsAbGroup H.
Proof.
nrapply Build_IsAbGroup.
Expand All @@ -99,7 +99,7 @@ Definition abgroup_subgroup (G : AbGroup) : Subgroup G -> AbGroup
#[warnings="-uniform-inheritance"]
Coercion abgroup_subgroup : Subgroup >-> AbGroup.

Global Instance isnormal_ab_subgroup (G : AbGroup) (H : Subgroup G)
Instance isnormal_ab_subgroup (G : AbGroup) (H : Subgroup G)
: IsNormalSubgroup H.
Proof.
intros x y h.
Expand All @@ -108,7 +108,7 @@ Defined.

(** ** Quotients of abelian groups *)

Global Instance isabgroup_quotient (G : AbGroup) (H : Subgroup G)
Instance isabgroup_quotient (G : AbGroup) (H : Subgroup G)
: IsAbGroup (QuotientGroup' G H (isnormal_ab_subgroup G H)).
Proof.
nrapply Build_IsAbGroup.
Expand Down Expand Up @@ -139,29 +139,29 @@ Defined.

(** ** The wild category of abelian groups *)

Global Instance isgraph_abgroup : IsGraph AbGroup
Instance isgraph_abgroup : IsGraph AbGroup
:= isgraph_induced abgroup_group.

Global Instance is01cat_abgroup : Is01Cat AbGroup
Instance is01cat_abgroup : Is01Cat AbGroup
:= is01cat_induced abgroup_group.

Global Instance is01cat_grouphomomorphism {A B : AbGroup} : Is01Cat (A $-> B)
Instance is01cat_grouphomomorphism {A B : AbGroup} : Is01Cat (A $-> B)
:= is01cat_induced (@grp_homo_map A B).

Global Instance is0gpd_grouphomomorphism {A B : AbGroup} : Is0Gpd (A $-> B)
Instance is0gpd_grouphomomorphism {A B : AbGroup} : Is0Gpd (A $-> B)
:= is0gpd_induced (@grp_homo_map A B).

Global Instance is2graph_abgroup : Is2Graph AbGroup
Instance is2graph_abgroup : Is2Graph AbGroup
:= is2graph_induced abgroup_group.

(** AbGroup forms a 1Cat *)
Global Instance is1cat_abgroup : Is1Cat AbGroup
Instance is1cat_abgroup : Is1Cat AbGroup
:= is1cat_induced _.

Global Instance hasmorext_abgroup `{Funext} : HasMorExt AbGroup
Instance hasmorext_abgroup `{Funext} : HasMorExt AbGroup
:= hasmorext_induced _.

Global Instance hasequivs_abgroup : HasEquivs AbGroup
Instance hasequivs_abgroup : HasEquivs AbGroup
:= hasequivs_induced _.

(** Zero object of AbGroup *)
Expand All @@ -173,17 +173,17 @@ Proof.
Defined.

(** AbGroup is a pointed category *)
Global Instance ispointedcat_abgroup : IsPointedCat AbGroup.
Instance ispointedcat_abgroup : IsPointedCat AbGroup.
Proof.
apply Build_IsPointedCat with abgroup_trivial.
all: intro A; apply ispointedcat_group.
Defined.

(** [abgroup_group] is a functor *)
Global Instance is0functor_abgroup_group : Is0Functor abgroup_group
Instance is0functor_abgroup_group : Is0Functor abgroup_group
:= is0functor_induced _.

Global Instance is1functor_abgroup_group : Is1Functor abgroup_group
Instance is1functor_abgroup_group : Is1Functor abgroup_group
:= is1functor_induced _.

(** Image of group homomorphisms between abelian groups *)
Expand Down
Loading

0 comments on commit 16c51b8

Please sign in to comment.