Timings for AbelianGroup.v
Require Import Basics Types.
Require Export Classes.interfaces.canonical_names (Zero, zero, Plus).
Require Export Classes.interfaces.abstract_algebra (IsAbGroup(..), abgroup_group, abgroup_commutative).
Require Export Algebra.Groups.Group.
Require Export Algebra.Groups.Subgroup.
Require Import Algebra.Groups.QuotientGroup.
Local Set Polymorphic Inductive Cumulativity.
Local Open Scope mc_scope.
Local Open Scope mc_add_scope.
(** * Abelian groups *)
(** Definition of an abelian group *)
Record AbGroup := {
abgroup_group : Group;
abgroup_commutative : Commutative (@group_sgop abgroup_group);
}.
Coercion abgroup_group : AbGroup >-> Group.
Global Existing Instance abgroup_commutative.
Global Instance isabgroup_abgroup {A : AbGroup} : IsAbGroup A.
Definition issig_abgroup : _ <~> AbGroup := ltac:(issig).
Global Instance zero_abgroup (A : AbGroup) : Zero A := group_unit.
Global Instance plus_abgroup (A : AbGroup) : Plus A := group_sgop.
Global Instance negate_abgroup (A : AbGroup) : Negate A := group_inverse.
(** ** Paths between abelian groups *)
Definition equiv_path_abgroup `{Univalence} {A B : AbGroup@{u}}
: GroupIsomorphism A B <~> (A = B).
refine (equiv_ap_inv issig_abgroup _ _ oE _).
refine (equiv_path_sigma_hprop _ _ oE _).
Definition equiv_path_abgroup_group `{Univalence} {A B : AbGroup}
: (A = B :> AbGroup) <~> (A = B :> Group)
:= equiv_path_group oE equiv_path_abgroup^-1.
(** ** Subgroups of abelian groups *)
(** Subgroups of abelian groups are abelian *)
Global Instance isabgroup_subgroup (G : AbGroup) (H : Subgroup G)
: IsAbGroup H.
(** Given any subgroup of an abelian group, we can coerce it to an abelian group. Note that Coq complains this coercion doesn't satisfy the uniform-inheritance condition, but in practice it works and doesn't cause any issue, so we ignore it. *)
Definition abgroup_subgroup (G : AbGroup) : Subgroup G -> AbGroup
:= fun H => Build_AbGroup H _.
#[warnings="-uniform-inheritance"]
Coercion abgroup_subgroup : Subgroup >-> AbGroup.
Global Instance isnormal_ab_subgroup (G : AbGroup) (H : Subgroup G)
: IsNormalSubgroup H.
intros x y; unfold in_cosetL, in_cosetR.
refine (_ oE equiv_subgroup_inverse _ _).
rewrite negate_involutive.
by rewrite (commutativity (-y) x).
(** ** Quotients of abelian groups *)
Global Instance isabgroup_quotient (G : AbGroup) (H : Subgroup G)
: IsAbGroup (QuotientGroup' G H (isnormal_ab_subgroup G H)).
srapply Quotient_ind_hprop.
srapply Quotient_ind_hprop.
Definition QuotientAbGroup (G : AbGroup) (H : Subgroup G) : AbGroup
:= (Build_AbGroup (QuotientGroup' G H (isnormal_ab_subgroup G H)) _).
Definition quotient_abgroup_rec {G : AbGroup}
(N : Subgroup G) (H : AbGroup)
(f : GroupHomomorphism G H) (h : forall n : G, N n -> f n = mon_unit)
: GroupHomomorphism (QuotientAbGroup G N) H
:= grp_quotient_rec G (Build_NormalSubgroup G N _) f h.
Theorem equiv_quotient_abgroup_ump {F : Funext} {G : AbGroup}
(N : Subgroup G) (H : Group)
: {f : GroupHomomorphism G H & forall (n : G), N n -> f n = mon_unit}
<~> (GroupHomomorphism (QuotientAbGroup G N) H).
exact (equiv_grp_quotient_ump (Build_NormalSubgroup G N _) _).
(** ** The wild category of abelian groups *)
Global Instance isgraph_abgroup : IsGraph AbGroup
:= isgraph_induced abgroup_group.
Global Instance is01cat_abgroup : Is01Cat AbGroup
:= is01cat_induced abgroup_group.
Global 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)
:= is0gpd_induced (@grp_homo_map A B).
Global Instance is2graph_abgroup : Is2Graph AbGroup
:= is2graph_induced abgroup_group.
(** AbGroup forms a 1Cat *)
Global Instance is1cat_abgroup : Is1Cat AbGroup
:= is1cat_induced _.
Global Instance hasmorext_abgroup `{Funext} : HasMorExt AbGroup
:= hasmorext_induced _.
Global Instance hasequivs_abgroup : HasEquivs AbGroup
:= hasequivs_induced _.
(** Zero object of AbGroup *)
Definition abgroup_trivial : AbGroup.
rapply (Build_AbGroup grp_trivial).
(** AbGroup is a pointed category *)
Global Instance ispointedcat_abgroup : IsPointedCat AbGroup.
apply Build_IsPointedCat with abgroup_trivial.
all: intro A; apply ispointedcat_group.
(** Image of group homomorphisms between abelian groups *)
Definition abgroup_image {A B : AbGroup} (f : A $-> B) : AbGroup
:= Build_AbGroup (grp_image f) _.
(** First isomorphism theorem of abelian groups *)
Definition abgroup_first_iso `{Funext} {A B : AbGroup} (f : A $-> B)
: GroupIsomorphism (QuotientAbGroup A (grp_kernel f)) (abgroup_image f).
apply grp_iso_quotient_normal.
(** ** Kernels of abelian groups *)
Definition ab_kernel {A B : AbGroup} (f : A $-> B) : AbGroup
:= Build_AbGroup (grp_kernel f) _.
(** ** Transporting in families related to abelian groups *)
Lemma transport_abgrouphomomorphism_from_const `{Univalence} {A B B' : AbGroup}
(p : B = B') (f : GroupHomomorphism A B)
: transport (Hom A) p f
= grp_homo_compose (equiv_path_abgroup^-1 p) f.
by apply equiv_path_grouphomomorphism.
Lemma transport_iso_abgrouphomomorphism_from_const `{Univalence} {A B B' : AbGroup}
(phi : GroupIsomorphism B B') (f : GroupHomomorphism A B)
: transport (Hom A) (equiv_path_abgroup phi) f
= grp_homo_compose phi f.
refine (transport_abgrouphomomorphism_from_const _ _ @ _).
Lemma transport_abgrouphomomorphism_to_const `{Univalence} {A A' B : AbGroup}
(p : A = A') (f : GroupHomomorphism A B)
: transport (fun G => Hom G B) p f
= grp_homo_compose f (grp_iso_inverse (equiv_path_abgroup^-1 p)).
by apply equiv_path_grouphomomorphism.
Lemma transport_iso_abgrouphomomorphism_to_const `{Univalence} {A A' B : AbGroup}
(phi : GroupIsomorphism A A') (f : GroupHomomorphism A B)
: transport (fun G => Hom G B) (equiv_path_abgroup phi) f
= grp_homo_compose f (grp_iso_inverse phi).
refine (transport_abgrouphomomorphism_to_const _ _ @ _).
(** ** Operations on abelian groups *)
(** The negation automorphism of an abelian group *)
Definition ab_homo_negation {A : AbGroup} : GroupIsomorphism A A.
snrapply Build_GroupIsomorphism.
snrapply Build_GroupHomomorphism.
refine (grp_inv_op x y @ _).
srapply isequiv_adjointify.
1-2: exact negate_involutive.
(** Multiplication by [n : nat] defines an endomorphism of any abelian group [A]. *)
Definition ab_mul_nat {A : AbGroup} (n : nat) : GroupHomomorphism A A.
snrapply Build_GroupHomomorphism.
1: exact (fun a => grp_pow a n).
1: exact (grp_unit_l _)^.
refine (_ @ associativity _ _ _).
refine (_ @ ap _ (associativity _ _ _)^).
rewrite (commutativity (grp_pow a n) b).
refine (_ @ ap _ (associativity _ _ _)).
refine (_ @ (associativity _ _ _)^).
Definition ab_mul_nat_homo {A B : AbGroup}
(f : GroupHomomorphism A B) (n : nat)
: f o ab_mul_nat n == ab_mul_nat n o f
:= grp_pow_homo 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
:= {| normalsubgroup_subgroup := grp_image_embedding f; normalsubgroup_isnormal := _ |}.
Definition ab_image_in_embedding {A B : AbGroup} (f : A $-> B) `{IsEmbedding f}
: GroupIsomorphism A (ab_image_embedding f)
:= grp_image_in_embedding f.
(** The cokernel of a homomorphism into an abelian group. *)
Definition ab_cokernel {G : Group@{u}} {A : AbGroup@{u}} (f : GroupHomomorphism G A)
: AbGroup := QuotientAbGroup _ (grp_image f).
Definition ab_cokernel_embedding {G : Group} {A : AbGroup} (f : G $-> A) `{IsEmbedding f}
: AbGroup := QuotientAbGroup _ (grp_image_embedding f).
Definition ab_cokernel_embedding_rec {G: Group} {A B : AbGroup} (f : G $-> A) `{IsEmbedding f}
(h : A $-> B) (p : grp_homo_compose h f $== grp_homo_const)
: ab_cokernel_embedding f $-> B.
snrapply (grp_quotient_rec _ _ h).