From 31c8d596c9222b2c505de7f20944d42d40e408c7 Mon Sep 17 00:00:00 2001 From: Carlo Angiuli Date: Fri, 2 Aug 2024 09:26:25 -0500 Subject: [PATCH] Add Favonia's exercises/solutions. --- .../circle_exercises.v | 240 ++++++++++++ .../circle_solutions.v | 360 ++++++++++++++++++ README.md | 3 + 3 files changed, 603 insertions(+) create mode 100644 2024-07-Minneapolis/7_Synthetic-Homotopy-Theory/circle_exercises.v create mode 100644 2024-07-Minneapolis/7_Synthetic-Homotopy-Theory/circle_solutions.v diff --git a/2024-07-Minneapolis/7_Synthetic-Homotopy-Theory/circle_exercises.v b/2024-07-Minneapolis/7_Synthetic-Homotopy-Theory/circle_exercises.v new file mode 100644 index 0000000..0e8d33a --- /dev/null +++ b/2024-07-Minneapolis/7_Synthetic-Homotopy-Theory/circle_exercises.v @@ -0,0 +1,240 @@ +Require Export UniMath.Foundations.All. +Require Export UniMath.MoreFoundations.All. + +(** Start of the emulated S1. Don't touch!!! *) +Module Export S1. + Private Inductive S1 : UU := base : S1. + Axiom loop : base = base. + Definition S1_ind (P : S1 -> UU) (b : P base) (l : PathOver loop b b) (x : S1) : P x := + match x with base => b end. + Definition S1_rec (A : UU) (b : A) (l : b = b) : S1 -> A := + S1_ind (λ _, A) b (PathOverConstant_map1 loop l). + Axiom S1_ind_beta_loop : forall (P : S1 -> UU) (b : P base) (l : PathOver loop b b), apd (S1_ind P b l) loop = l. + Axiom S1_rec_beta_loop : forall (A : UU) (b : A) (l : b = b), maponpaths (S1_rec A b l) loop = l. +End S1. +(** End of the emulated S1. Don't touch!!! *) + +(** The definition of Z we will use. It is essentially `coprod nat nat`, but + * with more memorable names `Pos` and `NegS` instead of `inl` and `inr`. + * `NegS 1` means -2. *) +Inductive Z : UU := + | Pos : nat -> Z + | NegS : nat -> Z. + +(** We define the `succ` function that increment integers by 1. *) +Definition succ (i : Z) : Z := + match i with + | Pos n => Pos (S n) + | NegS 0 => Pos 0 + | NegS (S n) => NegS n + end. + +(** [Exercise] We then define the `pred` function that decrement + * integers by 1. *) +Definition pred (i : Z) : Z. (* Change the dot `.` to `:=` *) +Proof. Admitted. + +(** [Exercise] `pred` is a left inverse of `succ` *) +Lemma pred_succ (i : Z) : pred (succ i) = i. +Proof. Admitted. + +(** [Exercise] `pred` is a right inverse of `succ` *) +Lemma succ_pred (i : Z) : succ (pred i) = i. +Proof. Admitted. + +(** Therefore, `succ` is an equivalence! *) +Definition succ_equiv : Z ≃ Z := + make_weq succ (isweq_iso succ pred pred_succ succ_pred). + +(** Decoding: from numbers to paths *) + +(** The definition for non-negative numbers `Pos n`. *) +Fixpoint loopexpPos (n : nat) : base = base := + match n with + | 0 => idpath base + | S n => loopexpPos n @ loop + end. + +(** The definition for negative numbers `NegS n`. *) +Fixpoint loopexpNegS (n : nat) : base = base := + match n with + | 0 => ! loop + | S n => loopexpNegS n @ ! loop + end. + +(** The conversion from loops to numbers. Think about the numbers as + * an "encoding" of loops. In the case of the circle, this is also + * called "winding numbers". *) +Definition loopexp (x : Z) : base = base := + match x with + | Pos n => loopexpPos n + | NegS n => loopexpNegS n + end. + +(** Encoding: from paths to numbers. This is not trivial at all, + * as it seems we have no way to recover the number from seemingly + * "unstructured" paths. We summon covering spaces to help us. *) + +(** The (universal) covering space of the circle. *) +Definition Cover : S1 -> UU := + S1_rec UU Z (weqtopaths succ_equiv). + +(** Transporting along `loop` is the same as applying `succ`. + * (We will not use this lemma in the final theorems.) *) +Lemma loop_transport (x : Z) : transportf Cover loop x = succ x. +Proof. + etrans. + - exact (functtransportf Cover (idfun UU) loop x). + - unfold Cover. rewrite S1_rec_beta_loop. + refine (toforallpaths _ _ _ _ x). + apply weqpath_transport. +Defined. + +(** A very useful lemma that mimics the existing lemma `weqpath_transport` *) +Lemma invweqpath_transport {A B : UU} (e : A ≃ B) + : transportf (λ A, A) (! (weqtopaths e)) = pr1 (invweq e). +Proof. + etrans. + - symmetry. refine (pr1_eqweqmap2 _). + - rewrite eqweqmap_pathsinv0. + rewrite eqweqmap_weqtopaths. + reflexivity. +Defined. + +(** [Exercise] prove that transporting along the inverse of + * `loop` is the same as applying `pred`. *) +Lemma invloop_transport (x : Z) : transportf Cover (! loop) x = pred x. +Proof. Admitted. + +(** Now we are ready to define the encoding function.*) + +Definition encode' {x : S1} (p : base = x) (start : Z) : Cover x := + transportf Cover p start. + +Definition encode {x : S1} (p : base = x) : Cover x := + encode' p (Pos 0). + +(** This section proves that `encode` is the right inverse of `loopexp`. + * That is, we can encode a loop back to its representing number. *) + +(** [Exercise] A useful lemma. + * + * Hint: `Search (transportf _ _ (transportf _ _ _)).` *) +Lemma encode'_encode (p : base = base) (q : base = base) + : encode' q (encode p) = encode (p @ q). +Proof. Admitted. + +(** [Exercise] Another lemma. *) +Lemma encode'_loop (i : Z) : encode' loop i = succ i. +Proof. Admitted. + +(** [Exercise] Yet another lemma. *) +Lemma encode'_invloop (i : Z) : encode' (! loop) i = pred i. +Proof. Admitted. + +(** [Exercise, difficult] Putting all these lemmas together... *) +Lemma encode_loopexp (i : Z) : encode (loopexp i) = i. +Proof. Admitted. + +(** Now, we wish to prove that `encode` is also the right inverse of + `loopexp` as follows: *) + +Lemma loopexp_encode (p : base = base): (loopexp (encode p)) = p. + +(** However, this is incredibly hard because we cannot do induction + * on `p` (why?). To overcome the difficulty, we have to loose at least + * one end point of `p` to an arbitrary point in `S1`. While `encode` + * can handle arbitrary path from `base` to an arbitrary point, `loopexp` + * needs to be generalized to handle such a free end point. We will call + * the generalized `loopexp` as `decode`, and revisit the lemma later. *) + +Abort. (* We will prove this lemma after a long journey. *) + +(** [Exercise] prove how `loopexp` and `succ` work with each other. + * + * Hint: `Search (_ @ _ @ _ = _).` *) +Lemma loopexp_succ (i : Z) : loopexp (succ i) = loopexp i @ loop. +Proof. Admitted. + +(** [Exercise, optional] You can also prove the opposite case, + * though we will not use this lemma. *) +Lemma loopexp_pred (i : Z) : loopexp (pred i) = loopexp i @ ! loop. +Proof. Admitted. + +(** [Exercise] A very useful lemma that can be proved in 2 tactics. *) +Lemma transportf_arrow {A : Type} {B C : A -> Type} + {x y : A} (p : x = y) (f : B x -> C x) (b' : B y) + : (transportf (λ x, B x -> C x) p f) b' + = transportf C p (f (transportf B (! p) b')). +Proof. Admitted. + +(** [Exercise, very difficult] This is the generalized `loopexp` that + * works for all elements of type `Cover x`, not just `Cover base` + * which is `Z`. *) +Definition decode {x : S1} : Cover x -> base = x. +Proof. + refine (S1_ind (λ x, Cover x -> base = x) loopexp _ x). + apply transportf_to_pathover. + apply funextsec. intro i. + (** [Exercise] Finish the rest of the definition. *) +Admitted. + +(** [Exercise] After all the preparation, this is a one-liner. *) +Lemma decode_encode {x : S1} (p : base = x): (decode (encode p)) = p. +Proof. Admitted. + +(** [Exercise] Finally... *) +Lemma loopexp_encode (p : base = base): (loopexp (encode p)) = p. +Proof. Admitted. + +(** [Exercise] We proved it! *) +Theorem Omega1S1 : (base = base) ≃ Z. +Proof. Admitted. + +(** BONUS: We can prove that S1 has h-level 3 but not 2, thanks + * to the constructions and the theorem we just established. *) + +Lemma invmaponpathsPos {n m : nat} : Pos n = Pos m -> n = m. +Proof. + intro p. + set (f := λ n, match n with Pos n => n | _ => 0 end). + exact (maponpaths f p). +Defined. + +Lemma invmaponpathsNegS {n m : nat} : NegS n = NegS m -> n = m. +Proof. + intro p. + set (f := λ n, match n with NegS n => n | _ => 0 end). + exact (maponpaths f p). +Defined. + +Lemma negpathPosNegS {n m : nat} : ¬ (Pos n = NegS m). +Proof. + intro p. + set (f := λ i, match i with Pos _ => true | NegS _ => false end). + exact (nopathstruetofalse (maponpaths f p)). +Defined. + +(** [Exercise, difficult] Prove that `Z` has decidable equality. *) +Theorem isdeceqZ : isdeceq Z. +Proof. Admitted. + +(** Okay, `Z` is a set. *) +Theorem isasetZ : isaset Z. +Proof. exact (isasetifdeceq _ isdeceqZ). Defined. + +(** Therefore, `base = base` is also a set. *) +Lemma isasetOmega1S1 : isaset (base = base). +Proof. exact (isofhlevelweqb 2 Omega1S1 isasetZ). Defined. + +(** [Exercise, extremely difficult] Prove that S1 has h-level 3. *) +Theorem isagroupoidS1 : isofhlevel 3 S1. +Proof. Admitted. + +(** [Exercise] Prove that `loop` is not the constant path. *) +Lemma negpathsloopidpath : ¬ (loop = idpath base). +Proof. Admitted. + +(** [Exercise] Prove that `S1` is not a set. *) +Theorem negisasetS1 : ¬ isaset S1. +Proof. Admitted. diff --git a/2024-07-Minneapolis/7_Synthetic-Homotopy-Theory/circle_solutions.v b/2024-07-Minneapolis/7_Synthetic-Homotopy-Theory/circle_solutions.v new file mode 100644 index 0000000..244cb63 --- /dev/null +++ b/2024-07-Minneapolis/7_Synthetic-Homotopy-Theory/circle_solutions.v @@ -0,0 +1,360 @@ +Require Export UniMath.Foundations.All. +Require Export UniMath.MoreFoundations.All. + +(** Start of the emulated S1. Don't touch!!! *) +Module Export S1. + Private Inductive S1 : UU := base : S1. + Axiom loop : base = base. + Definition S1_ind (P : S1 -> UU) (b : P base) (l : PathOver loop b b) (x : S1) : P x := + match x with base => b end. + Definition S1_rec (A : UU) (b : A) (l : b = b) : S1 -> A := + S1_ind (λ _, A) b (PathOverConstant_map1 loop l). + Axiom S1_ind_beta_loop : forall (P : S1 -> UU) (b : P base) (l : PathOver loop b b), apd (S1_ind P b l) loop = l. + Axiom S1_rec_beta_loop : forall (A : UU) (b : A) (l : b = b), maponpaths (S1_rec A b l) loop = l. +End S1. +(** End of the emulated S1. Don't touch!!! *) + +(** The definition of Z we will use. It is essentially `coprod nat nat`, but + * with more memorable names `Pos` and `NegS` instead of `inl` and `inr`. + * `NegS 1` means -2. *) +Inductive Z : UU := + | Pos : nat -> Z + | NegS : nat -> Z. + +(** We define the `succ` function that increment integers by 1. *) +Definition succ (i : Z) : Z := + match i with + | Pos n => Pos (S n) + | NegS 0 => Pos 0 + | NegS (S n) => NegS n + end. + +(** [Exercise] We then define the `pred` function that decrement + * integers by 1. *) +Definition pred (i : Z) : Z := + match i with + | Pos (S n) => Pos n + | Pos 0 => NegS 0 + | NegS n => NegS (S n) + end. + +(** [Exercise] `pred` is a left inverse of `succ` *) +Lemma pred_succ (i : Z) : pred (succ i) = i. +Proof. + induction i. + - reflexivity. + - induction n. + + reflexivity. + + reflexivity. +Defined. + +(** [Exercise] `pred` is a right inverse of `succ` *) +Lemma succ_pred (i : Z) : succ (pred i) = i. +Proof. + induction i. + - induction n. + + reflexivity. + + reflexivity. + - reflexivity. +Defined. + +(** Therefore, `succ` is an equivalence! *) +Definition succ_equiv : Z ≃ Z := + make_weq succ (isweq_iso succ pred pred_succ succ_pred). + +(** Decoding: from numbers to paths *) + +(** The definition for non-negative numbers `Pos n`. *) +Fixpoint loopexpPos (n : nat) : base = base := + match n with + | 0 => idpath base + | S n => loopexpPos n @ loop + end. + +(** The definition for negative numbers `NegS n`. *) +Fixpoint loopexpNegS (n : nat) : base = base := + match n with + | 0 => ! loop + | S n => loopexpNegS n @ ! loop + end. + +(** The conversion from loops to numbers. Think about the numbers as + * an "encoding" of loops. In the case of the circle, this is also + * called "winding numbers". *) +Definition loopexp (x : Z) : base = base := + match x with + | Pos n => loopexpPos n + | NegS n => loopexpNegS n + end. + +(** Encoding: from paths to numbers. This is not trivial at all, + * as it seems we have no way to recover the number from seemingly + * "unstructured" paths. We summon covering spaces to help us. *) + +(** The (universal) covering space of the circle. *) +Definition Cover : S1 -> UU := + S1_rec UU Z (weqtopaths succ_equiv). + +(** Transporting along `loop` is the same as applying `succ`. + * (We will not use this lemma in the final theorems.) *) +Lemma loop_transport (x : Z) : transportf Cover loop x = succ x. +Proof. + etrans. + - exact (functtransportf Cover (idfun UU) loop x). + - unfold Cover. rewrite S1_rec_beta_loop. + refine (toforallpaths _ _ _ _ x). + apply weqpath_transport. +Defined. + +(** A very useful lemma that mimics the existing lemma `weqpath_transport` *) +Lemma invweqpath_transport {A B : UU} (e : A ≃ B) + : transportf (λ A, A) (! (weqtopaths e)) = pr1 (invweq e). +Proof. + etrans. + - symmetry. refine (pr1_eqweqmap2 _). + - rewrite eqweqmap_pathsinv0. + rewrite eqweqmap_weqtopaths. + reflexivity. +Defined. + +(** [Exercise] prove that transporting along the inverse of + * `loop` is the same as applying `pred`. *) +Lemma invloop_transport (x : Z) : transportf Cover (! loop) x = pred x. +Proof. + etrans. + - exact (functtransportf Cover (idfun UU) (! loop) x). + - rewrite maponpathsinv0. + unfold Cover. rewrite S1_rec_beta_loop. + refine (toforallpaths _ _ _ _ x). + apply invweqpath_transport. +Defined. + +(** Now we are ready to define the encoding function.*) + +Definition encode' {x : S1} (p : base = x) (start : Z) : Cover x := + transportf Cover p start. + +Definition encode {x : S1} (p : base = x) : Cover x := + encode' p (Pos 0). + +(** This section proves that `encode` is the right inverse of `loopexp`. + * That is, we can encode a loop back to its representing number. *) + +(** [Exercise] A useful lemma. + * + * Hint: `Search (transportf _ _ (transportf _ _ _)).` *) +Lemma encode'_encode (p : base = base) (q : base = base) + : encode' q (encode p) = encode (p @ q). +Proof. + unfold encode. unfold encode'. + apply transport_f_f. +Defined. + +(** [Exercise] Another lemma. *) +Lemma encode'_loop (i : Z) : encode' loop i = succ i. +Proof. + unfold encode'. + rewrite (transport_idfun Cover loop i). + unfold Cover. rewrite S1_rec_beta_loop. + refine (toforallpaths _ _ _ _ i). + apply weqpath_transport. +Defined. + +(** [Exercise] Yet another lemma. *) +Lemma encode'_invloop (i : Z) : encode' (! loop) i = pred i. +Proof. + unfold encode'. + rewrite (transport_idfun Cover (! loop) i). + rewrite maponpathsinv0. + unfold Cover. rewrite S1_rec_beta_loop. + refine (toforallpaths _ _ _ _ i). + apply invweqpath_transport. +Defined. + +(** [Exercise, difficult] Putting all these lemmas together... *) +Lemma encode_loopexp (i : Z) : encode (loopexp i) = i. +Proof. + induction i. + - induction n. + + reflexivity. + + simpl in *. etrans. + * symmetry. exact (encode'_encode (loopexpPos n) loop). + * rewrite IHn. apply encode'_loop. + - induction n. + + apply (encode'_invloop (Pos 0)). + + simpl in *. etrans. + * symmetry. exact (encode'_encode (loopexpNegS n) (! loop)). + * rewrite IHn. apply encode'_invloop. +Defined. + +(** Now, we wish to prove that `encode` is also the right inverse of + `loopexp` as follows: *) + +Lemma loopexp_encode (p : base = base): (loopexp (encode p)) = p. + +(** However, this is incredibly hard because we cannot do induction + * on `p` (why?). To overcome the difficulty, we have to loose at least + * one end point of `p` to an arbitrary point in `S1`. While `encode` + * can handle arbitrary path from `base` to an arbitrary point, `loopexp` + * needs to be generalized to handle such a free end point. We will call + * the generalized `loopexp` as `decode`, and revisit the lemma later. *) + +Abort. (* We will prove this lemma after a long journey. *) + +(** [Exercise] prove how `loopexp` and `succ` work with each other. + * + * Hint: `Search (_ @ _ @ _ = _).` *) +Lemma loopexp_succ (i : Z) : loopexp (succ i) = loopexp i @ loop. +Proof. + induction i. + - reflexivity. + - induction n. + + simpl. symmetry. apply pathsinv0l. + + simpl. rewrite <- (path_assoc _ (! loop) loop). + rewrite (pathsinv0l loop). + rewrite pathscomp0rid. + reflexivity. +Defined. + +(** [Exercise, optional] You can also prove the opposite case, + * though we will not use this lemma. *) +Lemma loopexp_pred (i : Z) : loopexp (pred i) = loopexp i @ ! loop. +Proof. + induction i. + - induction n. + + reflexivity. + + simpl. rewrite <- (path_assoc _ loop (! loop)). + rewrite (pathsinv0r loop). + rewrite pathscomp0rid. + reflexivity. + - reflexivity. +Defined. + +(** [Exercise] A very useful lemma that can be proved in 2 tactics. *) +Lemma transportf_arrow {A : Type} {B C : A -> Type} + {x y : A} (p : x = y) (f : B x -> C x) (b' : B y) + : (transportf (λ x, B x -> C x) p f) b' + = transportf C p (f (transportf B (! p) b')). +Proof. + induction p. reflexivity. +Defined. + +(** [Exercise, very difficult] This is the generalized `loopexp` that + * works for all elements of type `Cover x`, not just `Cover base` + * which is `Z`. *) +Definition decode {x : S1} : Cover x -> base = x. +Proof. + refine (S1_ind (λ x, Cover x -> base = x) loopexp _ x). + apply transportf_to_pathover. + apply funextsec. intro i. + (** [Exercise] Finish the rest of the definition. *) + rewrite transportf_arrow. + rewrite transportf_id1. + etrans. + - apply maponpaths_2, maponpaths, invloop_transport. + - rewrite <- (loopexp_succ (pred i)). + apply maponpaths. + exact (succ_pred i). +Defined. + +(** [Exercise] After all the preparation, this is a one-liner. *) +Lemma decode_encode {x : S1} (p : base = x): (decode (encode p)) = p. +Proof. + induction p. reflexivity. +Defined. + +(** [Exercise] Finally... *) +Lemma loopexp_encode (p : base = base): (loopexp (encode p)) = p. +Proof. + use decode_encode. +Defined. + +(** [Exercise] We proved it! *) +Theorem Omega1S1 : (base = base) ≃ Z. +Proof. + refine (make_weq encode (isweq_iso _ _ _ _)). + - exact loopexp_encode. + - exact encode_loopexp. +Defined. + +(** BONUS: We can prove that S1 has h-level 3 but not 2, thanks + * to the constructions and the theorem we just established. *) + +Lemma invmaponpathsPos {n m : nat} : Pos n = Pos m -> n = m. +Proof. + intro p. + set (f := λ n, match n with Pos n => n | _ => 0 end). + exact (maponpaths f p). +Defined. + +Lemma invmaponpathsNegS {n m : nat} : NegS n = NegS m -> n = m. +Proof. + intro p. + set (f := λ n, match n with NegS n => n | _ => 0 end). + exact (maponpaths f p). +Defined. + +Lemma negpathPosNegS {n m : nat} : ¬ (Pos n = NegS m). +Proof. + intro p. + set (f := λ i, match i with Pos _ => true | NegS _ => false end). + exact (nopathstruetofalse (maponpaths f p)). +Defined. + +(** [Exercise, difficult] Prove that `Z` has decidable equality. *) +Theorem isdeceqZ : isdeceq Z. +Proof. + intros i j. + induction i as [n1 | n1]. + - induction j as [n2 | n2]. + + assert (natdeceq := isdeceqnat n1 n2). + induction natdeceq as [eq | neq]. + * left. rewrite eq. reflexivity. + * right. intro eq. apply neq. exact (invmaponpathsPos eq). + + right. apply negpathPosNegS. + - induction j as [n2 | n2]. + + right. intro eq. apply (negpathPosNegS (! eq)). + + assert (natdeceq := isdeceqnat n1 n2). + induction natdeceq as [eq | neq]. + * left. rewrite eq. reflexivity. + * right. intro eq. apply neq. exact (invmaponpathsNegS eq). +Defined. + +(** Okay, `Z` is a set. *) +Theorem isasetZ : isaset Z. +Proof. exact (isasetifdeceq _ isdeceqZ). Defined. + +(** Therefore, `base = base` is also a set. *) +Lemma isasetOmega1S1 : isaset (base = base). +Proof. exact (isofhlevelweqb 2 Omega1S1 isasetZ). Defined. + +(** [Exercise, extremely difficult] Prove that S1 has h-level 3. *) +Theorem isagroupoidS1 : isofhlevel 3 S1. +Proof. + simple refine (S1_ind (λ x, forall y, isaset (x = y)) _ _). + + simpl. simple refine (S1_ind (λ y, isaset (base = y)) _ _). + * exact isasetOmega1S1. + * apply transportf_to_pathover, proofirrelevance. + refine (isapropisofhlevel 2 (base = base)). + + apply transportf_to_pathover, proofirrelevance. + apply impred_isaprop. intro y. + refine (isapropisofhlevel 2 (base = y)). +Defined. + +(** [Exercise] Prove that `loop` is not the constant path. *) +Lemma negpathsloopidpath : ¬ (loop = idpath base). +Proof. + intro eq. + assert (p : Pos 1 = Pos 0). + - etrans. + + symmetry. apply (encode'_loop (Pos 0)). + + rewrite eq. reflexivity. + - apply (negpathssx0 0), invmaponpathsPos. exact p. +Defined. + +(** [Exercise] Prove that `S1` is not a set. *) +Theorem negisasetS1 : ¬ isaset S1. +Proof. + intro isasetS1. + apply negpathsloopidpath, isasetS1. +Defined. diff --git a/README.md b/README.md index 626b9a2..2f83623 100644 --- a/README.md +++ b/README.md @@ -31,6 +31,9 @@ - [Exercises](2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_exercises.v) - [Exercises with solutions](2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_solutions.v) +### Lecture 7: Synthetic Homotopy Theory (by Favonia) +- [Exercises](2024-07-Minneapolis/7_Synthetic-Homotopy-Theory/circle_exercises.v) +- [Solutions](2024-07-Minneapolis/7_Synthetic-Homotopy-Theory/circle_solutions.v) ## School on Univalent Mathematics, Cortona, 2022