Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse.Require Import AbelianGroup Biproduct.(** * Homomorphisms from a group to an abelian group form an abelian group. *)(** We can add group homomorphisms. *)
A: Group B: AbGroup f, g: A $-> B
A $-> B
A: Group B: AbGroup f, g: A $-> B
A $-> B
A: Group B: AbGroup f, g: A $-> B
GroupHomomorphism A (ab_biprod B B)
(** [fun a => f(a) + g(a)] **)exact (grp_prod_corec f g).Defined.(** We can negate a group homomorphism by composing with [ab_homo_negation]. *)Global Instancenegate_hom {A : Group} {B : AbGroup}
: Negate (@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. *)
H: Funext A: Group B: AbGroup
Group
H: Funext A: Group B: AbGroup
Group
H: Funext A: Group B: AbGroup
IsGroup (GroupHomomorphism A B)
H: Funext A: Group B: AbGroup
IsHSet (GroupHomomorphism A B)
H: Funext A: Group B: AbGroup
Associative sg_op
H: Funext A: Group B: AbGroup
LeftIdentity sg_op mon_unit
H: Funext A: Group B: AbGroup
RightIdentity sg_op mon_unit
H: Funext A: Group B: AbGroup
LeftInverse sg_op negate mon_unit
H: Funext A: Group B: AbGroup
RightInverse sg_op negate mon_unit
H: Funext A: Group B: AbGroup
Associative sg_op
H: Funext A: Group B: AbGroup
LeftIdentity sg_op mon_unit
H: Funext A: Group B: AbGroup
RightIdentity sg_op mon_unit
H: Funext A: Group B: AbGroup
LeftInverse sg_op negate mon_unit
H: Funext A: Group B: AbGroup
RightInverse sg_op negate mon_unit
H: Funext A: Group B: AbGroup x, y, z: GroupHomomorphism A B x0: A
sg_op (x x0) (sg_op (y x0) (z x0)) =
sg_op (sg_op (x x0) (y x0)) (z x0)
H: Funext A: Group B: AbGroup y: GroupHomomorphism A B x: A
sg_op group_unit (y x) = y x
H: Funext A: Group B: AbGroup x: GroupHomomorphism A B x0: A
sg_op (x x0) group_unit = x x0
H: Funext A: Group B: AbGroup x: GroupHomomorphism A B x0: A
sg_op (negate (x x0)) (x x0) = group_unit
H: Funext A: Group B: AbGroup x: GroupHomomorphism A B x0: A
sg_op (x x0) (negate (x x0)) = group_unit
H: Funext A: Group B: AbGroup x, y, z: GroupHomomorphism A B x0: A
sg_op (x x0) (sg_op (y x0) (z x0)) =
sg_op (sg_op (x x0) (y x0)) (z x0)
apply associativity.
H: Funext A: Group B: AbGroup y: GroupHomomorphism A B x: A
sg_op group_unit (y x) = y x
apply left_identity.
H: Funext A: Group B: AbGroup x: GroupHomomorphism A B x0: A
sg_op (x x0) group_unit = x x0
apply right_identity.
H: Funext A: Group B: AbGroup x: GroupHomomorphism A B x0: A
sg_op (negate (x x0)) (x x0) = group_unit
apply left_inverse.
H: Funext A: Group B: AbGroup x: GroupHomomorphism A B x0: A
sg_op (x x0) (negate (x x0)) = group_unit
apply right_inverse.Defined.
H: Funext A: Group B: AbGroup
AbGroup
H: Funext A: Group B: AbGroup
AbGroup
H: Funext A: Group B: AbGroup
Commutative group_sgop
H: Funext A: Group B: AbGroup f, g: grp_hom A B
ab_homo_add f g = ab_homo_add g f
H: Funext A: Group B: AbGroup f, g: grp_hom A B x: A
sg_op (f x) (g x) = sg_op (g x) (f x)
apply commutativity.Defined.(** ** The bifunctor [ab_hom] *)
H: Funext A: Group^op
Is0Functor (ab_hom A)
H: Funext A: Group^op
Is0Functor (ab_hom A)
H: Funext A: Group^op B, B': AbGroup f: B $-> B'
ab_hom A B $-> ab_hom A B'
H: Funext A: Group^op B, B': AbGroup f: B $-> B'
ab_hom A B -> ab_hom A B'
H: Funext A: Group^op B, B': AbGroup f: B $-> B'
IsSemiGroupPreserving ?f
H: Funext A: Group^op B, B': AbGroup f: B $-> B'
IsSemiGroupPreserving
(fung : ab_hom A B => grp_homo_compose f g)
H: Funext A: Group^op B, B': AbGroup f: B $-> B' phi, psi: ab_hom A B
grp_homo_compose f (sg_op phi psi) =
sg_op (grp_homo_compose f phi)
(grp_homo_compose f psi)
H: Funext A: Group^op B, B': AbGroup f: B $-> B' phi, psi: ab_hom A B a: A
f (sg_op (phi a) (psi a)) =
sg_op (f (phi a)) (f (psi a))
exact (grp_homo_op f _ _).Defined.
H: Funext B: AbGroup
Is0Functor
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
H: Funext B: AbGroup
Is0Functor
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
H: Funext B: AbGroup A, A': Group^op f: A $-> A'
flip (ab_hom : Group^op -> AbGroup -> AbGroup) B A $->
flip (ab_hom : Group^op -> AbGroup -> AbGroup) B A'
H: Funext B: AbGroup A, A': Group^op f: A $-> A'
flip (ab_hom : Group^op -> AbGroup -> AbGroup) B A ->
flip (ab_hom : Group^op -> AbGroup -> AbGroup) B A'
H: Funext B: AbGroup A, A': Group^op f: A $-> A'
IsSemiGroupPreserving ?f
H: Funext B: AbGroup A, A': Group^op f: A $-> A'
IsSemiGroupPreserving
(fung : flip
(ab_hom : Group^op -> AbGroup -> AbGroup) B
A => grp_homo_compose g f)
H: Funext B: AbGroup A, A': Group^op f: A $-> A' phi, psi: flip ab_hom B A
forall (ab : AbGroup) (fg : a $-> b),
f $== g -> fmap (ab_hom A) f $== fmap (ab_hom A) g
H: Funext A: Group^op
foralla : AbGroup,
fmap (ab_hom A) (Id a) $== Id (ab_hom A a)
H: Funext A: Group^op
forall (abc : AbGroup) (f : a $-> b) (g : b $-> c),
fmap (ab_hom A) (g $o f) $==
fmap (ab_hom A) g $o fmap (ab_hom A) f
H: Funext A: Group^op
forall (ab : AbGroup) (fg : a $-> b),
f $== g -> fmap (ab_hom A) f $== fmap (ab_hom A) g
H: Funext A: Group^op B, B': AbGroup f, g: B $-> B' p: f $== g phi: ab_hom A B
fmap (ab_hom A) f phi = fmap (ab_hom A) g phi
H: Funext A: Group^op B, B': AbGroup f, g: B $-> B' p: f $== g phi: ab_hom A B a: A
f (phi a) = g (phi a)
exact (p (phi a)).
H: Funext A: Group^op
foralla : AbGroup,
fmap (ab_hom A) (Id a) $== Id (ab_hom A a)
H: Funext A: Group^op B: AbGroup phi: ab_hom A B
fmap (ab_hom A) (Id B) phi = Id (ab_hom A B) phi
byapply equiv_path_grouphomomorphism.
H: Funext A: Group^op
forall (abc : AbGroup) (f : a $-> b) (g : b $-> c),
fmap (ab_hom A) (g $o f) $==
fmap (ab_hom A) g $o fmap (ab_hom A) f
H: Funext A: Group^op B, C, D: AbGroup f: B $-> C g: C $-> D phi: ab_hom A B
fmap (ab_hom A) (g $o f) phi =
(fmap (ab_hom A) g $o fmap (ab_hom A) f) phi
byapply equiv_path_grouphomomorphism.Defined.
H: Funext B: AbGroup
Is1Functor
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
H: Funext B: AbGroup
Is1Functor
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
H: Funext B: AbGroup
forall (ab : Group^op) (fg : a $-> b),
f $== g ->
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) f $==
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) g
H: Funext B: AbGroup
foralla : Group^op,
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
(Id a) $== Id (flip ab_hom B a)
H: Funext B: AbGroup
forall (abc : Group^op) (f : a $-> b) (g : b $-> c),
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
(g $o f) $==
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) g $o
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) f
H: Funext B: AbGroup
forall (ab : Group^op) (fg : a $-> b),
f $== g ->
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) f $==
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) g
H: Funext B: AbGroup A, A': Group^op f, g: A $-> A' p: f $== g phi: flip ab_hom B A
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) f
phi =
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) g
phi
H: Funext B: AbGroup A, A': Group^op f, g: A $-> A' p: f $== g phi: flip ab_hom B A a: A'
phi (f a) = phi (g a)
exact (ap phi (p a)).
H: Funext B: AbGroup
foralla : Group^op,
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
(Id a) $== Id (flip ab_hom B a)
H: Funext B: AbGroup A: Group^op phi: flip ab_hom B A
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
(Id A) phi = Id (flip ab_hom B A) phi
byapply equiv_path_grouphomomorphism.
H: Funext B: AbGroup
forall (abc : Group^op) (f : a $-> b) (g : b $-> c),
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
(g $o f) $==
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) g $o
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B) f
H: Funext B: AbGroup A, C, D: Group^op f: A $-> C g: C $-> D phi: flip ab_hom B A
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
(g $o f) phi =
(fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
g $o
fmap
(flip (ab_hom : Group^op -> AbGroup -> AbGroup) B)
f) phi
forall (a0a1 : Group^op) (f : a0 $-> a1)
(b0b1 : AbGroup) (g : b0 $-> b1),
fmap01 ab_hom a1 g $o fmap10 ab_hom f b0 $==
fmap10 ab_hom f b1 $o fmap01 ab_hom a0 g
H: Funext
forall (a0a1 : Group^op) (f : a0 $-> a1)
(b0b1 : AbGroup) (g : b0 $-> b1),
fmap01 ab_hom a1 g $o fmap10 ab_hom f b0 $==
fmap10 ab_hom f b1 $o fmap01 ab_hom a0 g
H: Funext A, A': Group^op f: A $-> A' B, B': AbGroup g: B $-> B' phi: ab_hom A B
grp_homo_compose g (grp_homo_compose phi f) =
grp_homo_compose (grp_homo_compose g phi) f
byapply equiv_path_grouphomomorphism.Defined.(** ** Properties of [ab_hom] *)(** 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. *)
H: Funext A, B, C: AbGroup f: A $-> B IsSurjection0: IsConnMap (Tr (-1)) f
IsEmbedding (fmap10 ab_hom f C)
H: Funext A, B, C: AbGroup f: A $-> B IsSurjection0: IsConnMap (Tr (-1)) f
IsEmbedding (fmap10 ab_hom f C)
H: Funext A, B, C: AbGroup f: A $-> B IsSurjection0: IsConnMap (Tr (-1)) f g0, g1: ab_hom B C p: fmap10 ab_hom f C g0 = fmap10 ab_hom f C g1
g0 = g1
H: Funext A, B, C: AbGroup f: A $-> B IsSurjection0: IsConnMap (Tr (-1)) f g0, g1: ab_hom B C p: fmap10 ab_hom f C g0 = fmap10 ab_hom f C g1
g0 == g1
H: Funext A, B, C: AbGroup f: A $-> B IsSurjection0: IsConnMap (Tr (-1)) f g0, g1: ab_hom B C p: fmap10 ab_hom f C g0 = fmap10 ab_hom f C g1