Library HoTT.Algebra.AbGroups.Z
Require Import Basics.
Require Import Spaces.Pos.Core Spaces.Int.
Require Import Algebra.AbGroups.AbelianGroup.
Require Import Spaces.Pos.Core Spaces.Int.
Require Import Algebra.AbGroups.AbelianGroup.
The group of integers
Local Open Scope int_scope.
Section MinimizationToSet.
Local Set Universe Minimization ToSet.
Definition abgroup_Z@{} : AbGroup@{Set}.
Proof.
snrapply Build_AbGroup.
- refine (Build_Group Int int_add 0 int_negation _); repeat split.
+ exact _.
+ exact int_add_assoc.
+ exact int_add_0_r.
+ exact int_add_negation_l.
+ exact int_add_negation_r.
- exact int_add_comm.
Defined.
End MinimizationToSet.
Definition ab_mul (n : Int) {A : AbGroup} : GroupHomomorphism A A.
Proof.
induction n.
- exact (grp_homo_compose ab_homo_negation (ab_mul_nat (pos_to_nat p))).
- exact grp_homo_const.
- exact (ab_mul_nat (pos_to_nat p)).
Defined.
Proof.
induction n.
- exact (grp_homo_compose ab_homo_negation (ab_mul_nat (pos_to_nat p))).
- exact grp_homo_const.
- exact (ab_mul_nat (pos_to_nat p)).
Defined.
Homomorphisms respect multiplication.
Lemma ab_mul_homo {A B : AbGroup} (n : Int) (f : GroupHomomorphism A B)
: grp_homo_compose f (ab_mul n) == grp_homo_compose (ab_mul n) f.
Proof.
intro x.
induction n.
- cbn. refine (grp_homo_inv _ _ @ _).
refine (ap negate _).
apply grp_pow_homo.
- cbn. apply grp_homo_unit.
- cbn. apply grp_pow_homo.
Defined.
: grp_homo_compose f (ab_mul n) == grp_homo_compose (ab_mul n) f.
Proof.
intro x.
induction n.
- cbn. refine (grp_homo_inv _ _ @ _).
refine (ap negate _).
apply grp_pow_homo.
- cbn. apply grp_homo_unit.
- cbn. apply grp_pow_homo.
Defined.
Multiplication by zero gives the constant group homomorphism.
Definition ab_mul_const `{Funext} {A : AbGroup} : ab_mul 0 (A:=A) = grp_homo_const.
Proof.
apply equiv_path_grouphomomorphism.
reflexivity.
Defined.
Proof.
apply equiv_path_grouphomomorphism.
reflexivity.
Defined.