feat(category_theory/category/{Pointed,Bipointed}): The categories of…

… pointed/bipointed types (#11777)

Define
* `Pointed`, the category of pointed types
* `Bipointed`, the category of bipointed types
* the forgetful functors from `Bipointed` to `Pointed` and from `Pointed` to `Type*`
* `Type_to_Pointed`, the functor from `Type*` to `Pointed` induced by `option`
* `Bipointed.swap_equiv` the equivalence between `Bipointed` and itself induced by `prod.swap` both ways.

src/category_theory/category/Bipointed.lean

@@ -0,0 +1,149 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import category_theory.category.Pointed
+
+/-!
+# The category of bipointed types
+
+This defines `Bipointed`, the category of bipointed types.
+
+## TODO
+
+Monoidal structure
+-/
+
+open category_theory
+
+universes u
+variables {α β : Type*}
+
+/-- The category of bipointed types. -/
+structure Bipointed : Type.{u + 1} :=
+(X : Type.{u})
+(to_prod : X × X)
+
+namespace Bipointed
+
+instance : has_coe_to_sort Bipointed Type* := ⟨X⟩
+
+attribute [protected] Bipointed.X
+
+/-- Turns a bipointing into a bipointed type. -/
+def of {X : Type*} (to_prod : X × X) : Bipointed := ⟨X, to_prod⟩
+
+alias of ← prod.Bipointed
+
+instance : inhabited Bipointed := ⟨of ((), ())⟩
+
+/-- Morphisms in `Bipointed`. -/
+@[ext] protected structure hom (X Y : Bipointed.{u}) : Type u :=
+(to_fun : X → Y)
+(map_fst : to_fun X.to_prod.1 = Y.to_prod.1)
+(map_snd : to_fun X.to_prod.2 = Y.to_prod.2)
+
+namespace hom
+
+/-- The identity morphism of `X : Bipointed`. -/
+@[simps] def id (X : Bipointed) : hom X X := ⟨id, rfl, rfl⟩
+
+instance (X : Bipointed) : inhabited (hom X X) := ⟨id X⟩
+
+/-- Composition of morphisms of `Bipointed`. -/
+@[simps] def comp {X Y Z : Bipointed.{u}} (f : hom X Y) (g : hom Y Z) : hom X Z :=
+⟨g.to_fun ∘ f.to_fun, by rw [function.comp_apply, f.map_fst, g.map_fst],
+  by rw [function.comp_apply, f.map_snd, g.map_snd]⟩
+
+end hom
+
+instance large_category : large_category Bipointed :=
+{ hom := hom,
+  id := hom.id,
+  comp := @hom.comp,
+  id_comp' := λ _ _ _, hom.ext _ _ rfl,
+  comp_id' := λ _ _ _, hom.ext _ _ rfl,
+  assoc' := λ _ _ _ _ _ _ _, hom.ext _ _ rfl }
+
+instance concrete_category : concrete_category Bipointed :=
+{ forget := { obj := Bipointed.X, map := @hom.to_fun },
+  forget_faithful := ⟨@hom.ext⟩ }
+
+/-- Swaps the pointed elements of a bipointed type. `prod.swap` as a functor. -/
+@[simps] def swap : Bipointed ⥤ Bipointed :=
+{ obj := λ X, ⟨X, X.to_prod.swap⟩, map := λ X Y f, ⟨f.to_fun, f.map_snd, f.map_fst⟩ }
+
+/-- The equivalence between `Bipointed` and itself induced by `prod.swap` both ways. -/
+@[simps] def swap_equiv : Bipointed ≌ Bipointed :=
+equivalence.mk swap swap
+  (nat_iso.of_components (λ X, { hom := ⟨id, rfl, rfl⟩, inv := ⟨id, rfl, rfl⟩ }) $ λ X Y f, rfl)
+  (nat_iso.of_components (λ X, { hom := ⟨id, rfl, rfl⟩, inv := ⟨id, rfl, rfl⟩ }) $ λ X Y f, rfl)
+
+@[simp] lemma swap_equiv_symm : swap_equiv.symm = swap_equiv := rfl
+
+end Bipointed
+
+/-- The forgetful functor from `Bipointed` to `Pointed` which forgets about the second point. -/
+def Bipointed_to_Pointed_fst : Bipointed ⥤ Pointed :=
+{ obj := λ X, ⟨X, X.to_prod.1⟩, map := λ X Y f, ⟨f.to_fun, f.map_fst⟩ }
+
+/-- The forgetful functor from `Bipointed` to `Pointed` which forgets about the first point. -/
+def Bipointed_to_Pointed_snd : Bipointed ⥤ Pointed :=
+{ obj := λ X, ⟨X, X.to_prod.2⟩, map := λ X Y f, ⟨f.to_fun, f.map_snd⟩ }
+
+@[simp] lemma Bipointed_to_Pointed_fst_comp_forget :
+  Bipointed_to_Pointed_fst ⋙ forget Pointed = forget Bipointed := rfl
+
+@[simp] lemma Bipointed_to_Pointed_snd_comp_forget :
+  Bipointed_to_Pointed_snd ⋙ forget Pointed = forget Bipointed := rfl
+
+@[simp] lemma swap_comp_Bipointed_to_Pointed_fst :
+  Bipointed.swap ⋙ Bipointed_to_Pointed_fst = Bipointed_to_Pointed_snd := rfl
+
+@[simp] lemma swap_comp_Bipointed_to_Pointed_snd :
+  Bipointed.swap ⋙ Bipointed_to_Pointed_snd = Bipointed_to_Pointed_fst := rfl
+
+--TODO: This is actually an equivalence
+/-- The functor from `Pointed` to `Bipointed` which adds a second point. -/
+def Pointed_to_Bipointed_fst : Pointed.{u} ⥤ Bipointed :=
+{ obj := λ X, ⟨option X, X.point, none⟩,
+  map := λ X Y f, ⟨option.map f.to_fun, congr_arg _ f.map_point, rfl⟩,
+  map_id' := λ X, Bipointed.hom.ext _ _ option.map_id,
+  map_comp' := λ X Y Z f g, Bipointed.hom.ext _ _ (option.map_comp_map  _ _).symm }
+
+--TODO: This is actually an equivalence
+/-- The functor from `Pointed` to `Bipointed` which adds a first point. -/
+def Pointed_to_Bipointed_snd : Pointed.{u} ⥤ Bipointed :=
+{ obj := λ X, ⟨option X, none, X.point⟩,
+  map := λ X Y f, ⟨option.map f.to_fun, rfl, congr_arg _ f.map_point⟩,
+  map_id' := λ X, Bipointed.hom.ext _ _ option.map_id,
+  map_comp' := λ X Y Z f g, Bipointed.hom.ext _ _ (option.map_comp_map  _ _).symm }
+
+@[simp] lemma Pointed_to_Bipointed_fst_comp :
+  Pointed_to_Bipointed_fst ⋙ Bipointed.swap = Pointed_to_Bipointed_snd := rfl
+
+@[simp] lemma Pointed_to_Bipointed_snd_comp :
+  Pointed_to_Bipointed_snd ⋙ Bipointed.swap = Pointed_to_Bipointed_fst := rfl
+
+/-- The free/forgetful adjunction between `Pointed_to_Bipointed_fst` and `Bipointed_to_Pointed_fst`.
+-/
+def Pointed_to_Bipointed_fst_Bipointed_to_Pointed_fst_adjunction :
+  Pointed_to_Bipointed_fst ⊣ Bipointed_to_Pointed_fst :=
+adjunction.mk_of_hom_equiv
+{ hom_equiv := λ X Y, { to_fun := λ f, ⟨f.to_fun ∘ option.some, f.map_fst⟩,
+                        inv_fun := λ f, ⟨λ o, o.elim Y.to_prod.2 f.to_fun, f.map_point, rfl⟩,
+                        left_inv := λ f, by { ext, cases x, exact f.map_snd.symm, refl },
+                        right_inv := λ f, Pointed.hom.ext _ _ rfl },
+  hom_equiv_naturality_left_symm' := λ X' X Y f g, by { ext, cases x; refl } }
+
+/-- The free/forgetful adjunction between `Pointed_to_Bipointed_snd` and `Bipointed_to_Pointed_snd`.
+-/
+def Pointed_to_Bipointed_snd_Bipointed_to_Pointed_snd_adjunction :
+  Pointed_to_Bipointed_snd ⊣ Bipointed_to_Pointed_snd :=
+adjunction.mk_of_hom_equiv
+{ hom_equiv := λ X Y, { to_fun := λ f, ⟨f.to_fun ∘ option.some, f.map_snd⟩,
+                        inv_fun := λ f, ⟨λ o, o.elim Y.to_prod.1 f.to_fun, rfl, f.map_point⟩,
+                        left_inv := λ f, by { ext, cases x, exact f.map_fst.symm, refl },
+                        right_inv := λ f, Pointed.hom.ext _ _ rfl },
+  hom_equiv_naturality_left_symm' := λ X' X Y f g, by { ext, cases x; refl } }

src/category_theory/category/Pointed.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import category_theory.concrete_category.basic
+
+/-!
+# The category of pointed types
+
+This defines `Pointed`, the category of pointed types.
+
+## TODO
+
+* Monoidal structure
+* Upgrade `Type_to_Pointed` to an equivalence
+-/
+
+open category_theory
+
+universes u
+variables {α β : Type*}
+
+/-- The category of pointed types. -/
+structure Pointed : Type.{u + 1} :=
+(X : Type.{u})
+(point : X)
+
+namespace Pointed
+
+instance : has_coe_to_sort Pointed Type* := ⟨X⟩
+
+attribute [protected] Pointed.X
+
+/-- Turns a point into a pointed type. -/
+def of {X : Type*} (point : X) : Pointed := ⟨X, point⟩
+
+alias of ← prod.Pointed
+
+instance : inhabited Pointed := ⟨of ((), ())⟩
+
+/-- Morphisms in `Pointed`. -/
+@[ext] protected structure hom (X Y : Pointed.{u}) : Type u :=
+(to_fun : X → Y)
+(map_point : to_fun X.point = Y.point)
+
+namespace hom
+
+/-- The identity morphism of `X : Pointed`. -/
+@[simps] def id (X : Pointed) : hom X X := ⟨id, rfl⟩
+
+instance (X : Pointed) : inhabited (hom X X) := ⟨id X⟩
+
+/-- Composition of morphisms of `Pointed`. -/
+@[simps] def comp {X Y Z : Pointed.{u}} (f : hom X Y) (g : hom Y Z) : hom X Z :=
+⟨g.to_fun ∘ f.to_fun, by rw [function.comp_apply, f.map_point, g.map_point]⟩
+
+end hom
+
+instance large_category : large_category Pointed :=
+{ hom := hom,
+  id := hom.id,
+  comp := @hom.comp,
+  id_comp' := λ _ _ _, hom.ext _ _ rfl,
+  comp_id' := λ _ _ _, hom.ext _ _ rfl,
+  assoc' := λ _ _ _ _ _ _ _, hom.ext _ _ rfl }
+
+instance concrete_category : concrete_category Pointed :=
+{ forget := { obj := Pointed.X, map := @hom.to_fun },
+  forget_faithful := ⟨@hom.ext⟩ }
+
+end Pointed
+
+--TODO: This is actually an equivalence
+/-- `option` as a functor from types to pointed types. This is the free functor. -/
+@[simps] def Type_to_Pointed : Type.{u} ⥤ Pointed.{u} :=
+{ obj := λ X, ⟨option X, none⟩,
+  map := λ X Y f, ⟨option.map f, rfl⟩,
+  map_id' := λ X, Pointed.hom.ext _ _ option.map_id,
+  map_comp' := λ X Y Z f g, Pointed.hom.ext _ _ (option.map_comp_map _ _).symm }
+
+/-- `Type_to_Pointed` is the free functor. -/
+def Type_to_Pointed_forget_adjunction : Type_to_Pointed ⊣ forget Pointed :=
+adjunction.mk_of_hom_equiv
+{ hom_equiv := λ X Y, { to_fun := λ f, f.to_fun ∘ option.some,
+                        inv_fun := λ f, ⟨λ o, o.elim Y.point f, rfl⟩,
+                        left_inv := λ f, by { ext, cases x, exact f.map_point.symm, refl },
+                        right_inv := λ f, funext $ λ _, rfl },
+  hom_equiv_naturality_left_symm' := λ X' X Y f g, by { ext, cases x; refl }, }