Library UniMath.CategoryTheory.categories.monoids
Category of monoids
Contents
- Precategory of monoids
- Category of monoids
- Forgetful functor to HSET
- Free functor from HSET
- Free/forgetful adjunction
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Foundations.UnivalenceAxiom.
Require Import UniMath.Algebra.BinaryOperations.
Require Import UniMath.Algebra.Monoids.
Require Import UniMath.Algebra.Free_Monoids_and_Groups.
Require Import UniMath.Combinatorics.Lists.
Require Import UniMath.Algebra.IteratedBinaryOperations.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Local Open Scope cat.
Section def_monoid_precategory.
Definition monoid_fun_space (A B : monoid) : hSet :=
make_hSet (monoidfun A B) (isasetmonoidfun A B).
Definition monoid_precategory_ob_mor : precategory_ob_mor :=
tpair (λ ob : UU, ob -> ob -> UU) monoid (λ A B : monoid, monoid_fun_space A B).
Definition monoid_precategory_data : precategory_data :=
make_precategory_data
monoid_precategory_ob_mor (λ (X : monoid), ((idmonoidiso X) : monoidfun X X))
(fun (X Y Z : monoid) (f : monoidfun X Y) (g : monoidfun Y Z) => monoidfuncomp f g).
Local Lemma monoid_id_left {X Y : monoid} (f : monoidfun X Y) :
monoidfuncomp (idmonoidiso X) f = f.
Show proof.
Opaque monoid_id_left.
Local Lemma monoid_id_right {X Y : monoid} (f : monoidfun X Y) :
monoidfuncomp f (idmonoidiso Y) = f.
Show proof.
Opaque monoid_id_right.
Local Lemma monoid_assoc (X Y Z W : monoid) (f : monoidfun X Y) (g : monoidfun Y Z)
(h : monoidfun Z W) :
monoidfuncomp f (monoidfuncomp g h) = monoidfuncomp (monoidfuncomp f g) h.
Show proof.
Opaque monoid_assoc.
Lemma is_precategory_monoid_precategory_data : is_precategory monoid_precategory_data.
Show proof.
use make_is_precategory_one_assoc.
- intros a b f. use monoid_id_left.
- intros a b f. use monoid_id_right.
- intros a b c d f g h. use monoid_assoc.
- intros a b f. use monoid_id_left.
- intros a b f. use monoid_id_right.
- intros a b c d f g h. use monoid_assoc.
Definition monoid_precategory : precategory :=
make_precategory monoid_precategory_data is_precategory_monoid_precategory_data.
Lemma has_homsets_monoid_precategory : has_homsets monoid_precategory.
Show proof.
End def_monoid_precategory.
Section def_monoid_category.
Definition monoid_category : category := make_category _ has_homsets_monoid_precategory.
Definition monoid_category : category := make_category _ has_homsets_monoid_precategory.
Lemma monoid_z_iso_is_equiv (A B : ob monoid_category) (f : z_iso A B) : isweq (pr1 (pr1 f)).
Show proof.
use isweq_iso.
- exact (pr1monoidfun _ _ (inv_from_z_iso f)).
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_inv_after_z_iso f)) x).
intros x0. use isapropismonoidfun.
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_after_z_iso_inv f)) x).
intros x0. use isapropismonoidfun.
Opaque monoid_z_iso_is_equiv.- exact (pr1monoidfun _ _ (inv_from_z_iso f)).
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_inv_after_z_iso f)) x).
intros x0. use isapropismonoidfun.
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_after_z_iso_inv f)) x).
intros x0. use isapropismonoidfun.
Lemma monoid_z_iso_equiv (X Y : ob monoid_category) : z_iso X Y -> monoidiso X Y.
Show proof.
intro f.
use make_monoidiso.
- exact (make_weq (pr1 (pr1 f)) (monoid_z_iso_is_equiv X Y f)).
- exact (pr2 (pr1 f)).
use make_monoidiso.
- exact (make_weq (pr1 (pr1 f)) (monoid_z_iso_is_equiv X Y f)).
- exact (pr2 (pr1 f)).
Lemma monoid_equiv_is_z_iso (X Y : ob monoid_category) (f : monoidiso X Y) :
@is_z_isomorphism monoid_precategory X Y (monoidfunconstr (pr2 f)).
Show proof.
exists (monoidfunconstr (pr2 (invmonoidiso f))).
split.
- use monoidfun_paths. use funextfun. intros x. use homotinvweqweq.
- use monoidfun_paths. use funextfun. intros y. use homotweqinvweq.
Opaque monoid_equiv_is_z_iso.split.
- use monoidfun_paths. use funextfun. intros x. use homotinvweqweq.
- use monoidfun_paths. use funextfun. intros y. use homotweqinvweq.
Lemma monoid_equiv_z_iso (X Y : ob monoid_category) : monoidiso X Y -> z_iso X Y.
Show proof.
Lemma monoid_z_iso_equiv_is_equiv (X Y : monoid_category) : isweq (monoid_z_iso_equiv X Y).
Show proof.
use isweq_iso.
- exact (monoid_equiv_z_iso X Y).
- intros x. use z_iso_eq. use monoidfun_paths. use idpath.
- intros y. use monoidiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ use idpath.
Opaque monoid_z_iso_equiv_is_equiv.- exact (monoid_equiv_z_iso X Y).
- intros x. use z_iso_eq. use monoidfun_paths. use idpath.
- intros y. use monoidiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ use idpath.
Definition monoid_z_iso_equiv_weq (X Y : ob monoid_category) : (z_iso X Y) ≃ (monoidiso X Y).
Show proof.
Lemma monoid_equiv_z_iso_is_equiv (X Y : ob monoid_category) : isweq (monoid_equiv_z_iso X Y).
Show proof.
use isweq_iso.
- exact (monoid_z_iso_equiv X Y).
- intros y. use monoidiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ use idpath.
- intros x. use z_iso_eq. use monoidfun_paths. use idpath.
Opaque monoid_equiv_z_iso_is_equiv.- exact (monoid_z_iso_equiv X Y).
- intros y. use monoidiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ use idpath.
- intros x. use z_iso_eq. use monoidfun_paths. use idpath.
Definition monoid_equiv_weq_z_iso (X Y : ob monoid_precategory) : (monoidiso X Y) ≃ (z_iso X Y).
Show proof.
Definition monoid_category_isweq (X Y : ob monoid_category) :
isweq (λ p : X = Y, idtoiso p).
Show proof.
use (@isweqhomot
(X = Y) (z_iso X Y)
(pr1weq (weqcomp (monoid_univalence X Y) (monoid_equiv_weq_z_iso X Y)))
_ _ (weqproperty (weqcomp (monoid_univalence X Y) (monoid_equiv_weq_z_iso X Y)))).
intros e. induction e.
use (pathscomp0 weqcomp_to_funcomp_app).
use total2_paths_f.
- use idpath.
- use proofirrelevance. use isaprop_is_z_isomorphism.
Opaque monoid_category_isweq.(X = Y) (z_iso X Y)
(pr1weq (weqcomp (monoid_univalence X Y) (monoid_equiv_weq_z_iso X Y)))
_ _ (weqproperty (weqcomp (monoid_univalence X Y) (monoid_equiv_weq_z_iso X Y)))).
intros e. induction e.
use (pathscomp0 weqcomp_to_funcomp_app).
use total2_paths_f.
- use idpath.
- use proofirrelevance. use isaprop_is_z_isomorphism.
Definition monoid_category_is_univalent : is_univalent monoid_category.
Show proof.
Definition monoid_univalent_category : univalent_category :=
make_univalent_category monoid_category monoid_category_is_univalent.
End def_monoid_category.
Definition monoid_forgetful_functor : functor monoid_precategory HSET.
Show proof.
use make_functor.
- use make_functor_data.
+ intro; exact (pr1setwithbinop (pr1monoid ltac:(assumption))).
+ intros ? ? f; exact (pr1monoidfun _ _ f).
- split.
+
- use make_functor_data.
+ intro; exact (pr1setwithbinop (pr1monoid ltac:(assumption))).
+ intros ? ? f; exact (pr1monoidfun _ _ f).
- split.
+
Identity axiom
intro; reflexivity.
+
+
Composition axiom
intros ? ? ? ? ?; reflexivity.
Lemma monoid_forgetful_functor_is_faithful : faithful monoid_forgetful_functor.
Show proof.
Definition monoid_free_functor : functor HSET monoid_precategory.
Show proof.
use make_functor.
- use make_functor_data.
+ intros s; exact (free_monoid s).
+ intros ? ? f; exact (free_monoidfun f).
- split.
+
- use make_functor_data.
+ intros s; exact (free_monoid s).
+ intros ? ? f; exact (free_monoidfun f).
- split.
+
Identity axiom
Composition axiom
Definition monoid_free_forgetful_unit :
nat_trans (functor_identity _)
(functor_composite monoid_free_functor monoid_forgetful_functor).
Show proof.
nat_trans (functor_identity _)
(functor_composite monoid_free_functor monoid_forgetful_functor).
Show proof.
use make_nat_trans.
- intro; exact singleton.
- intros ? ? ?.
abstract (apply funextfun; intro; reflexivity).
- intro; exact singleton.
- intros ? ? ?.
abstract (apply funextfun; intro; reflexivity).
This amounts to naturality of the counit: mapping commutes with folding
Lemma iterop_list_mon_map {m n : monoid} (f : monoidfun m n) :
∏ l, ((iterop_list_mon ∘ map (pr1monoidfun m n f)) l =
(pr1monoidfun _ _ f ∘ iterop_list_mon) l)%functions.
Show proof.
∏ l, ((iterop_list_mon ∘ map (pr1monoidfun m n f)) l =
(pr1monoidfun _ _ f ∘ iterop_list_mon) l)%functions.
Show proof.
apply list_ind.
- apply pathsinv0, monoidfununel.
- intros x xs H.
simpl in *.
refine (maponpaths iterop_list_mon (map_cons _ _ _) @ _).
refine (iterop_list_mon_step _ _ @ _).
refine (_ @ !maponpaths _ (iterop_list_mon_step _ _)).
refine (_ @ !binopfunisbinopfun f _ _).
apply maponpaths.
assumption.
- apply pathsinv0, monoidfununel.
- intros x xs H.
simpl in *.
refine (maponpaths iterop_list_mon (map_cons _ _ _) @ _).
refine (iterop_list_mon_step _ _ @ _).
refine (_ @ !maponpaths _ (iterop_list_mon_step _ _)).
refine (_ @ !binopfunisbinopfun f _ _).
apply maponpaths.
assumption.
The counit of this adjunction is the "folding" function
[a, b, …, z] ↦ a · b · ⋯ · z
(This is known to Haskell programmers as mconcat.)
Definition monoid_free_forgetful_counit :
nat_trans (functor_composite monoid_forgetful_functor monoid_free_functor )
(functor_identity _).
Show proof.
Definition monoid_free_forgetful_adjunction_data :
adjunction_data HSET monoid_category .
Show proof.
Lemma monoid_free_forgetful_adjunction :
form_adjunction' monoid_free_forgetful_adjunction_data.
Show proof.
nat_trans (functor_composite monoid_forgetful_functor monoid_free_functor )
(functor_identity _).
Show proof.
use make_nat_trans.
- intro.
use tpair.
+ intro; apply iterop_list_mon; assumption.
+ split.
* intros ? ?; apply iterop_list_mon_concatenate.
* reflexivity.
- intros ? ? f; apply monoidfun_paths.
apply funextfun; intro; simpl in *.
apply (iterop_list_mon_map f).
- intro.
use tpair.
+ intro; apply iterop_list_mon; assumption.
+ split.
* intros ? ?; apply iterop_list_mon_concatenate.
* reflexivity.
- intros ? ? f; apply monoidfun_paths.
apply funextfun; intro; simpl in *.
apply (iterop_list_mon_map f).
Definition monoid_free_forgetful_adjunction_data :
adjunction_data HSET monoid_category .
Show proof.
use tpair; [|use tpair]. - exact monoid_free_functor.
- exact monoid_forgetful_functor.
- split.
+ exact monoid_free_forgetful_unit.
+ exact monoid_free_forgetful_counit.
- exact monoid_forgetful_functor.
- split.
+ exact monoid_free_forgetful_unit.
+ exact monoid_free_forgetful_counit.
Lemma monoid_free_forgetful_adjunction :
form_adjunction' monoid_free_forgetful_adjunction_data.
Show proof.
split; intro.
- apply monoidfun_paths.
apply funextfun.
simpl.
unfold homot; apply list_ind; [reflexivity|].
intros x xs ?.
simpl.
rewrite map_cons.
refine (iterop_list_mon_step (_ : pr1hSet (free_monoid _)) _ @ _).
apply maponpaths; assumption.
- reflexivity.
- apply monoidfun_paths.
apply funextfun.
simpl.
unfold homot; apply list_ind; [reflexivity|].
intros x xs ?.
simpl.
rewrite map_cons.
refine (iterop_list_mon_step (_ : pr1hSet (free_monoid _)) _ @ _).
apply maponpaths; assumption.
- reflexivity.