Shamrock-Frost · October 12, 2023 06:56 · Oct 12, 2023 · Oct 10, 2023 · Oct 10, 2023
diff --git a/Profunctors.lean b/Profunctors.lean
@@ -4,53 +4,175 @@ import Mathlib.CategoryTheory.DiscreteCategory
 import Mathlib.CategoryTheory.Functor.Category
 import Mathlib.CategoryTheory.Functor.Hom
 import Mathlib.CategoryTheory.Sigma.Basic
+import Mathlib.CategoryTheory.Limits.Shapes.Types
 
-open CategoryTheory Equiv
-
-def ProfHom (C D : Type _) [Category C] [Category D] := Dᵒᵖ × C ⥤ Type _
-
-instance (C D : Type _) [Category C] [Category D] : Category (ProfHom C D) := Functor.category
-
-def ProfHom.precomp {A B C D : Type _} [Category A] [Category B] [Category C] [Category D] 
-  (F : A ⥤ C) (G : B ⥤ D) (H : ProfHom C D) : ProfHom A B := Functor.prod (Functor.op G) F ⋙ H
-
-def square {A B C D : Type _} [Category A] [Category B] [Category C] [Category D] 
-  (F : A ⥤ C) (G : B ⥤ D) (H : ProfHom A B) (K : ProfHom C D) := H ⟶ K.precomp F G
-
-def ProfId (C : Type _) [Category C] : ProfHom C C := Functor.hom C
-
-def Sigma.inv {J : Type _} (f : J → Type _) [∀ j : J, Groupoid (f j)] {X Y : Σ j, f j} : (X ⟶ Y) → (Y ⟶ X)
-| Sigma.SigmaHom.mk f => Sigma.SigmaHom.mk (Groupoid.inv f)
-
-instance Sigma.sigma' {J : Type _} (f : J → Type _) [∀ j : J, Groupoid (f j)] : Groupoid (Σ j, f j) := {
-  inv := Sigma.inv f
-  inv_comp := by 
-    intros X Y
-    apply Sigma.SigmaHom.rec
-    clear X Y
-    intros j X Y f
-    simp [Sigma.inv]
-    apply Eq.trans (Sigma.SigmaHom.comp_def j Y X Y _ _) 
-    simp
-    exact Eq.refl _
-  comp_inv := by 
-    intros X Y
-    apply Sigma.SigmaHom.rec
-    clear X Y
-    intros j X Y f
-    simp [Sigma.inv]
-    apply Eq.trans (Sigma.SigmaHom.comp_def j X Y X _ _) 
-    simp
-    exact Eq.refl _
-}
-
-def PermGrpd := Σ (n : ℕ), SingleObj (Perm (Fin n))
-instance : Groupoid PermGrpd := Sigma.sigma' _
-def PermGrpdCover := Σ (n : ℕ), ActionCategory (Perm (Fin n)) (Perm (Fin n))
-noncomputable
-instance : Groupoid PermGrpdCover := Sigma.sigma' _
-
-def incl_to_PermGrpd : Discrete ℕ ⥤ PermGrpd := Discrete.functor (fun n => ⟨n, SingleObj.star⟩)
-noncomputable
-def incl_to_PermGrpdCover : Discrete ℕ ⥤ PermGrpdCover := Discrete.functor (fun n => ⟨n, ActionCategory.objEquiv _ _ (Equiv.refl (Fin n))⟩)
+open CategoryTheory CategoryTheory.Limits Equiv
 
+universe u₁ u₂ u₃ u₄ v₁ v₂ v₃ v₄ w
+
+def Prof (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
+  := Dᵒᵖ × C ⥤ Type w
+def Prof.Id (C : Type u₁) [Category.{v₁} C] : Prof C C := Functor.hom C
+
+instance (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
+  : Category (Prof C D) := Functor.category
+
+variable {A : Type u₁} [Category.{v₁} A] {B : Type u₂} [Category.{v₂} B]
+         {C : Type u₃} [Category.{v₃} C] {D : Type u₄} [Category.{v₄} D]
+
+def Prof.precomp (F : A ⥤ C) (G : B ⥤ D) (H : Prof.{u₃, u₄, v₃, v₄, w} C D)
+  : Prof A B := Functor.prod (Functor.op G) F ⋙ H
+
+def square (F : A ⥤ C) (G : B ⥤ D)
+  (H : Prof.{u₁, u₂, v₁, v₂, w} A B) (K : Prof.{u₃, u₄, v₃, v₄, w} C D)
+  := H ⟶ K.precomp F G
+
+def UniversalCover (G : Type u₁) [Monoid G] := ActionCategory G G
+
+instance (G : Type u₁) [Monoid G] : Category (UniversalCover G) :=
+  instCategoryActionCategory _ _
+instance (G : Type u₁) [Monoid G] : CoeTC G (UniversalCover G) :=
+  ActionCategory.instCoeTCActionCategory
+instance (G : Type u₁) [Group G] : Groupoid (UniversalCover G) :=
+  ActionCategory.instGroupoidActionCategoryToMonoidToDivInvMonoid
+
+def UniversalCover.π (G : Type u₁) [Monoid G]
+  : UniversalCover G ⥤ SingleObj G := ActionCategory.π G G
+
+def IsThin (C : Type u₁) [Category.{v₁} C] := ∀ X Y : C, Subsingleton (X ⟶ Y)
+lemma UniversalCover.IsThin (G : Type u₁) [RightCancelMonoid G] : IsThin (UniversalCover G)
+| Sigma.mk _ g, Sigma.mk _ h => by
+  dsimp at g h
+  constructor
+  intros p q
+  obtain ⟨p, hyp1⟩ := p; obtain ⟨q, hyp2⟩ := q
+  apply Subtype.ext
+  exact mul_left_injective g (Eq.trans hyp1 hyp2.symm)
+
+instance UniversalCover.HomUnique (G : Type u₁) [Group G]
+  (x y : UniversalCover G) : Unique (x ⟶ y) :=
+  @uniqueOfSubsingleton _ (UniversalCover.IsThin G x y)
+                        ⟨y.back * x.back⁻¹, inv_mul_cancel_right y.back x.back⟩
+
+instance UniversalCover.IsConnected (G : Type u₁) [Group G] : IsConnected (UniversalCover G) :=
+  ActionCategory.instIsConnectedActionCategoryInstCategoryActionCategory
+
+def SingleObj.OpIso (G : Type u₁) [Monoid G]
+  : @CategoryTheory.Iso Cat _ (Bundled.of (SingleObj G)ᵒᵖ)
+                              (Bundled.of (SingleObj Gᵐᵒᵖ))
+  where
+    hom := {
+      obj := fun _ => SingleObj.star G
+      map := fun g => MulOpposite.op (Opposite.unop g)
+    }
+    inv := {
+      obj := fun _ => Opposite.op (SingleObj.star _)
+      map := fun g => Opposite.op (MulOpposite.unop g)
+    }
+
+-- def Sigma.ToOp {J : Type w} {C : J → Type u₁} [(j : J) → Category.{v₁, u₁} (C j)]
+--   : (Σ j, C j)ᵒᵖ ⥤ Σ j, (C j)ᵒᵖ
+--   where
+--     hom := CategoryTheory.Sigma.desc _
+--     inv := sorry
+
+def Sigma.OpIso {J : Type w} {C : J → Type u₁} [(j : J) → Category.{v₁, u₁} (C j)]
+  : @CategoryTheory.Iso Cat _ (Bundled.of (Σ j, C j)ᵒᵖ)
+                              (Bundled.of (Σ j, (C j)ᵒᵖ))
+  where
+    hom := (Sigma.desc (fun j => (@Sigma.incl _ (fun j' => (C j')ᵒᵖ) _ j).rightOp)).leftOp
+    inv := Sigma.desc (fun j => Functor.leftOp (Sigma.incl j ⋙ opOp _))
+    hom_inv_id := by
+      apply Functor.hext
+      . intros
+        exact Eq.refl _
+      . apply Opposite.rec'; intro X
+        apply Opposite.rec'; intro Y
+        apply Opposite.rec'; intro f
+        change Y ⟶ X at f
+        induction f
+        exact HEq.refl _
+    inv_hom_id := by
+      apply Functor.hext
+      . intros
+        exact Eq.refl _
+      . intros X Y f
+        induction f
+        exact HEq.refl _
+
+def SingleObj.Inv (G : Type u₁) [Group G] : (SingleObj G)ᵒᵖ ⥤ SingleObj G where
+  obj _        := SingleObj.star _
+  map g        := g.unop⁻¹
+  map_id _     := inv_one
+  map_comp _ _ := mul_inv_rev _ _
+
+def UniversalCover.Inv (G : Type u₁) [Group G] : UniversalCover G ⥤ UniversalCover G where
+  obj g := (g.back⁻¹ : G)
+  map {g h} _ := ⟨h.back⁻¹ * g.back, mul_inv_cancel_right h.back⁻¹ g.back⟩
+  map_comp := by { intros; apply Subsingleton.elim }
+
+variable {J : Type u₂} (G : J → Type u₁) [∀ j, Group (G j)]
+abbrev Tot := Σ j, SingleObj (G j)
+abbrev Cov := Σ j, UniversalCover (G j)
+
+def Cov.Inv : Cov G ⥤ Cov G :=
+  Sigma.Functor.sigma (fun j => UniversalCover.Inv (G j))
+
+def Sigma.Functor.sigma' {I : Type w}
+  {C : I → Type u₁} [(i : I) → Category.{v₁} (C i)]
+  {D : I → Type u₂} [(i : I) → Category.{v₁} (D i)]
+  (F : (i : I) → C i ⥤ D i) : (Σi, C i) ⥤ Σi, D i :=
+  Sigma.desc (fun i => F i ⋙ Sigma.incl i)
+
+def Cov.π : Cov G ⥤ Tot G := Sigma.Functor.sigma' (fun j => UniversalCover.π (G j))
+
+def Pt (C : Type u₁) [Category.{v₂} C] : Prof C C := (Functor.const _).obj PUnit
+def CofreeBiAct : Prof.{u₂, u₂, max u₁ u₂, max u₁ u₂} (Tot G) (Tot G) :=
+  Functor.prod (Sigma.OpIso.hom ⋙ Sigma.desc (fun j => (SingleObj.OpIso (G j)).hom
+                                                       ⋙ actionAsFunctor (G j)ᵐᵒᵖ (G j)))
+               (Sigma.desc (fun j => actionAsFunctor (G j) (G j)))
+  ⋙ uncurry.obj Types.binaryProductFunctor
+
+def TheMap : square (Cov.π G) (Cov.π G) (Pt (Cov G)) (CofreeBiAct G) where
+  app
+  | ⟨⟨⟨i, ⟨_, s⟩⟩⟩, ⟨j, ⟨_, t⟩⟩⟩ => fun _ => (@Inv.inv (G i) _ s, t)
+  naturality
+  | ⟨⟨X⟩, Y⟩, ⟨⟨X'⟩, Y'⟩, ⟨⟨p⟩, q⟩ => by
+    dsimp at p q
+    induction p with | @mk j₁ s₁ t₁ p =>
+    induction q with | @mk j₂ s₂ t₂ q =>
+    obtain ⟨_, s₁⟩ := s₁; obtain ⟨_, t₁⟩ := t₁
+    obtain ⟨_, s₂⟩ := s₂; obtain ⟨_, t₂⟩ := t₂
+    obtain ⟨g, hyp1⟩ := p
+    obtain ⟨h, hyp2⟩ := q
+    ext
+    refine Prod.mk.inj_iff.mpr ⟨?_, hyp2.symm⟩
+    change (G j₁) at t₁
+    change (G j₁) at s₁
+    change s₁⁻¹ = t₁⁻¹ * g
+    exact eq_inv_mul_of_mul_eq (mul_inv_eq_of_eq_mul hyp1.symm)
+
+-- abbrev PermGrpd := Σ (n : ℕ), SingleObj (Perm (Fin n))
+-- abbrev PermGrpdCover := Σ (n : ℕ), UniversalCover (Perm (Fin n))
+-- def I : Discrete ℕ ⥤ PermGrpd := Discrete.functor (fun n => ⟨n, SingleObj.star _⟩)
+-- def J : Discrete ℕ ⥤ PermGrpdCover := Discrete.functor (fun n => ⟨n, ActionCategory.objEquiv _ _ (Equiv.refl (Fin n))⟩)
+-- def π : PermGrpdCover ⥤ PermGrpd := Sigma.Functor.sigma (fun _ => ActionCategory.π _ _)
+-- def A : PermGrpdCover ⥤ PermGrpdCover := Sigma.Functor.sigma (fun _ => UniversalCover.Inv _)
+-- def r : PermGrpd ⥤ Discrete ℕ := Sigma.desc (fun n => (Functor.const _).obj (Discrete.mk n))
+
+-- lemma lem1 : I ⋙ r = 𝟭 (Discrete ℕ) := by
+--   apply Functor.hext
+--   . intro n; cases n
+--     exact Eq.refl _
+--   . intro n m f; cases n; cases m
+--     obtain ⟨⟨h⟩⟩ := f
+--     exact HEq.refl _
+
+-- lemma lem2 : J ⋙ π = I := by
+--   apply Functor.hext
+--   . intro n; cases n
+--     exact Eq.refl _
+--   . intro n m f; cases n; cases m
+--     obtain ⟨⟨h⟩⟩ := f; dsimp at h
+--     subst h
+--     exact HEq.refl _
diff --git a/Profunctors.lean b/Profunctors.lean
@@ -50,7 +50,7 @@ def PermGrpdCover := Σ (n : ℕ), ActionCategory (Perm (Fin n)) (Perm (Fin n))
 noncomputable
 instance : Groupoid PermGrpdCover := Sigma.sigma' _
 
-def incl_to_PermGrpd : Discrete ℕ ⥤ PermGrpd := Discrete.functor (fun n => ⟨n, ⟨⟩⟩)
+def incl_to_PermGrpd : Discrete ℕ ⥤ PermGrpd := Discrete.functor (fun n => ⟨n, SingleObj.star⟩)
 noncomputable
 def incl_to_PermGrpdCover : Discrete ℕ ⥤ PermGrpdCover := Discrete.functor (fun n => ⟨n, ActionCategory.objEquiv _ _ (Equiv.refl (Fin n))⟩)
 
diff --git a/Profunctors.lean b/Profunctors.lean
@@ -0,0 +1,56 @@
+import Mathlib.CategoryTheory.Action
+import Mathlib.CategoryTheory.Category.Cat
+import Mathlib.CategoryTheory.DiscreteCategory
+import Mathlib.CategoryTheory.Functor.Category
+import Mathlib.CategoryTheory.Functor.Hom
+import Mathlib.CategoryTheory.Sigma.Basic
+
+open CategoryTheory Equiv
+
+def ProfHom (C D : Type _) [Category C] [Category D] := Dᵒᵖ × C ⥤ Type _
+
+instance (C D : Type _) [Category C] [Category D] : Category (ProfHom C D) := Functor.category
+
+def ProfHom.precomp {A B C D : Type _} [Category A] [Category B] [Category C] [Category D] 
+  (F : A ⥤ C) (G : B ⥤ D) (H : ProfHom C D) : ProfHom A B := Functor.prod (Functor.op G) F ⋙ H
+
+def square {A B C D : Type _} [Category A] [Category B] [Category C] [Category D] 
+  (F : A ⥤ C) (G : B ⥤ D) (H : ProfHom A B) (K : ProfHom C D) := H ⟶ K.precomp F G
+
+def ProfId (C : Type _) [Category C] : ProfHom C C := Functor.hom C
+
+def Sigma.inv {J : Type _} (f : J → Type _) [∀ j : J, Groupoid (f j)] {X Y : Σ j, f j} : (X ⟶ Y) → (Y ⟶ X)
+| Sigma.SigmaHom.mk f => Sigma.SigmaHom.mk (Groupoid.inv f)
+
+instance Sigma.sigma' {J : Type _} (f : J → Type _) [∀ j : J, Groupoid (f j)] : Groupoid (Σ j, f j) := {
+  inv := Sigma.inv f
+  inv_comp := by 
+    intros X Y
+    apply Sigma.SigmaHom.rec
+    clear X Y
+    intros j X Y f
+    simp [Sigma.inv]
+    apply Eq.trans (Sigma.SigmaHom.comp_def j Y X Y _ _) 
+    simp
+    exact Eq.refl _
+  comp_inv := by 
+    intros X Y
+    apply Sigma.SigmaHom.rec
+    clear X Y
+    intros j X Y f
+    simp [Sigma.inv]
+    apply Eq.trans (Sigma.SigmaHom.comp_def j X Y X _ _) 
+    simp
+    exact Eq.refl _
+}
+
+def PermGrpd := Σ (n : ℕ), SingleObj (Perm (Fin n))
+instance : Groupoid PermGrpd := Sigma.sigma' _
+def PermGrpdCover := Σ (n : ℕ), ActionCategory (Perm (Fin n)) (Perm (Fin n))
+noncomputable
+instance : Groupoid PermGrpdCover := Sigma.sigma' _
+
+def incl_to_PermGrpd : Discrete ℕ ⥤ PermGrpd := Discrete.functor (fun n => ⟨n, ⟨⟩⟩)
+noncomputable
+def incl_to_PermGrpdCover : Discrete ℕ ⥤ PermGrpdCover := Discrete.functor (fun n => ⟨n, ActionCategory.objEquiv _ _ (Equiv.refl (Fin n))⟩)
+
No results found