Profunctor naturality

Poly.lean

@@ -5,6 +5,5 @@ import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Presheaf
 -- import Poly.LCCC.BeckChevalley
 -- import Poly.LCCC.Presheaf
 -- import Poly.Type.Univariate
--- import Poly.Basic
 -- import Poly.Exponentiable
-import Poly.UvPoly
+import Poly.UvPoly.Basic

Poly/Bifunctor/Basic.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2025 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Nawrocki
+-/
+import Mathlib.CategoryTheory.Adjunction.Basic
+
+import Poly.ForMathlib.CategoryTheory.NatIso
+import Poly.ForMathlib.CategoryTheory.Types
+
+/-! ## Composition of bifunctors -/
+
+namespace CategoryTheory.Functor
+
+variable {𝒞 𝒟' 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟'] [Category 𝒟] [Category ℰ]
+
+/-- Precompose a bifunctor in the second argument.
+Note that `G ⋙₂ F ⋙ P = F ⋙ G ⋙₂ P` definitionally. -/
+@[simps]
+def comp₂ (F : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : 𝒞 ⥤ 𝒟' ⥤ ℰ where
+  obj Γ := F ⋙ P.obj Γ
+  map f := whiskerLeft F (P.map f)
+
+@[inherit_doc]
+scoped [CategoryTheory] infixr:80 " ⋙₂ " => Functor.comp₂
+
+@[simp]
+theorem comp_comp₂ {𝒟'' : Type*} [Category 𝒟'']
+    (F : 𝒟'' ⥤ 𝒟') (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) :
+    (F ⋙ G) ⋙₂ P = F ⋙₂ (G ⋙₂ P) := by
+  rfl
+
+/-- Composition with `F,G` ordered like the arguments of `P` is considered `simp`ler. -/
+@[simp]
+theorem comp₂_comp {𝒞' : Type*} [Category 𝒞']
+    (F : 𝒞' ⥤ 𝒞) (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) :
+    G ⋙₂ (F ⋙ P) = F ⋙ (G ⋙₂ P) := by
+  rfl
+
+@[simps!]
+def comp₂_iso {F₁ F₂ : 𝒟' ⥤ 𝒟} {P₁ P₂ : 𝒞 ⥤ 𝒟 ⥤ ℰ}
+    (i : F₁ ≅ F₂) (j : P₁ ≅ P₂) : F₁ ⋙₂ P₁ ≅ F₂ ⋙₂ P₂ :=
+  NatIso.ofComponents₂ (fun C D => (j.app C).app (F₁.obj D) ≪≫ (P₂.obj C).mapIso (i.app D))
+    (fun _ _ => by simp [NatTrans.naturality_app_assoc])
+    (fun C f => by
+      have := congr_arg (P₂.obj C).map (i.hom.naturality f)
+      simp only [map_comp] at this
+      simp [this])
+
+@[simps!]
+def comp₂_isoWhiskerLeft {P₁ P₂ : 𝒞 ⥤ 𝒟 ⥤ ℰ} (F : 𝒟' ⥤ 𝒟) (i : P₁ ≅ P₂) :
+    F ⋙₂ P₁ ≅ F ⋙₂ P₂ :=
+  comp₂_iso (Iso.refl F) i
+
+@[simps!]
+def comp₂_isoWhiskerRight {F₁ F₂ : 𝒟' ⥤ 𝒟} (i : F₁ ≅ F₂) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) :
+    F₁ ⋙₂ P ≅ F₂ ⋙₂ P :=
+  comp₂_iso i (Iso.refl P)
+
+end CategoryTheory.Functor
+
+/-! ## Natural isomorphisms of bifunctors -/
+
+namespace CategoryTheory
+universe v u
+variable {𝒞 : Type u} [Category.{v} 𝒞]
+variable {𝒟 : Type*} [Category 𝒟]
+
+namespace coyoneda
+
+theorem comp₂_naturality₂_left (F : 𝒟 ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v)
+    (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X Y : 𝒞) (Z : 𝒟) (f : X ⟶ Y) (g : Y ⟶ F.obj Z) :
+    -- The `op`s really are a pain. Why can't they be definitional like in Lean 3 :(
+    (i.app <| .op X).app Z (f ≫ g) = (P.map f.op).app Z ((i.app <| .op Y).app Z g) := by
+  simp [← FunctorToTypes.naturality₂_left]
+
+theorem comp₂_naturality₂_right (F : 𝒟 ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v)
+    (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X : 𝒞) (Y Z : 𝒟) (f : X ⟶ F.obj Y) (g : Y ⟶ Z) :
+    (i.app <| .op X).app Z (f ≫ F.map g) = (P.obj <| .op X).map g ((i.app <| .op X).app Y f) := by
+  simp [← FunctorToTypes.naturality₂_right]
+
+end coyoneda
+
+namespace Adjunction
+
+variable {𝒟 : Type*} [Category 𝒟]
+
+/-- For `F ⊣ G`, `𝒟(FX, Y) ≅ 𝒞(X, GY)`. -/
+def coyoneda_iso {F : 𝒞 ⥤ 𝒟} {G : 𝒟 ⥤ 𝒞} (A : F ⊣ G) :
+    F.op ⋙ coyoneda (C := 𝒟) ≅ G ⋙₂ coyoneda (C := 𝒞) :=
+  NatIso.ofComponents₂ (fun C D => Equiv.toIso <| A.homEquiv C.unop D)
+    (fun _ _ => by ext : 1; simp [A.homEquiv_naturality_left])
+    (fun _ _ => by ext : 1; simp [A.homEquiv_naturality_right])
+
+end Adjunction
+end CategoryTheory

Poly/Bifunctor/Sigma.lean

@@ -0,0 +1,182 @@
+/-
+Copyright (c) 2025 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Nawrocki
+-/
+import Mathlib.CategoryTheory.Comma.Over.Basic
+import Mathlib.CategoryTheory.Functor.Currying
+
+import SEq.Tactic.DepRewrite
+
+import Poly.ForMathlib.CategoryTheory.Elements
+import Poly.ForMathlib.CategoryTheory.Comma.Over.Basic
+import Poly.Bifunctor.Basic
+
+/-! ## Dependent sums of functors -/
+
+namespace CategoryTheory.Functor
+
+universe w v u t s r
+
+variable {𝒞 : Type t} [Category.{u} 𝒞] {𝒟 : Type r} [Category.{s} 𝒟]
+
+/-- Given functors `F : 𝒞 ⥤ Type v` and `G : ∫F ⥤ 𝒟 ⥤ Type v`,
+produce the functor `(C, D) ↦ (a : F(C)) × G((C, a))(D)`.
+
+This is a dependent sum that varies naturally
+in a parameter `C` of the first component,
+and a parameter `D` of the second component.
+
+We use this to package and compose natural equivalences
+where one side (or both) is a dependent sum, e.g.
+```
+H(C) ⟶ I(D)
+=========================
+(a : F(C)) × (G(C, a)(D))
+```
+is a natural isomorphism of bifunctors `𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v`
+given by `(C, D) ↦ H(C) ⟶ I(D)` and `G.Sigma`. -/
+@[simps!]
+/- Q: Is it necessary to special-case bifunctors?
+(1) General case `G : F.Elements ⥤ Type v` needs
+a functor `F'` s.t. `F'.Elements ≅ F.Elements × 𝒟`; very awkward.
+(2) General case `F : 𝒞 ⥤ 𝒟`, `G : ∫F ⥤ 𝒟`:
+- what conditions are needed on `𝒟` for `∫F` to make sense?
+- what about for `ΣF. G : 𝒞 ⥤ 𝒟` to make sense?
+- known concrete instances are `𝒟 ∈ {Type, Cat, Grpd}` -/
+def Sigma {F : 𝒞 ⥤ Type w} (G : F.Elements ⥤ 𝒟 ⥤ Type v) : 𝒞 ⥤ 𝒟 ⥤ Type (max w v) := by
+  refine curry.obj {
+    obj := fun (C, D) => (a : F.obj C) × (G.obj ⟨C, a⟩).obj D
+    map := fun (f, g) ⟨a, b⟩ =>
+      ⟨F.map f a, (G.map ⟨f, rfl⟩).app _ ((G.obj ⟨_, a⟩).map g b)⟩
+    map_id := ?_
+    map_comp := ?_
+  } <;> {
+    intros
+    ext ⟨a, b⟩ : 1
+    dsimp
+    congr! 1 with h
+    . simp
+    . rw! [h]; simp [FunctorToTypes.naturality]
+  }
+
+def Sigma.isoCongrLeft {F₁ F₂ : 𝒞 ⥤ Type w}
+    /- Q: What kind of map `F₂.Elements ⥤ F₁.Elements`
+    could `NatTrans.mapElements i.hom` generalize to?
+    We need to send `x ∈ F₂(C)` to something in `F₁(C)`;
+    so maybe the map has to at least be over `𝒞`. -/
+    (G : F₁.Elements ⥤ 𝒟 ⥤ Type v) (i : F₂ ≅ F₁) :
+    Sigma (NatTrans.mapElements i.hom ⋙ G) ≅ Sigma G := by
+  refine NatIso.ofComponents₂
+    (fun C D => Equiv.toIso {
+      toFun := fun ⟨a, b⟩ => ⟨i.hom.app C a, b⟩
+      invFun := fun ⟨a, b⟩ => ⟨i.inv.app C a, cast (by simp) b⟩
+      left_inv := fun ⟨_, _⟩ => by simp
+      right_inv := fun ⟨_, _⟩ => by simp
+    }) ?_ ?_ <;> {
+      intros
+      ext : 1
+      dsimp
+      apply have h := ?_; Sigma.ext h ?_
+      . simp [FunctorToTypes.naturality]
+      . dsimp [Sigma] at h ⊢
+        rw! [← h]
+        simp [NatTrans.mapElements]
+    }
+
+def Sigma.isoCongrRight {F : 𝒞 ⥤ Type w} {G₁ G₂ : F.Elements ⥤ 𝒟 ⥤ Type v} (i : G₁ ≅ G₂) :
+    Sigma G₁ ≅ Sigma G₂ := by
+  refine NatIso.ofComponents₂
+    (fun C D => Equiv.toIso {
+      toFun := fun ⟨a, b⟩ => ⟨a, (i.hom.app ⟨C, a⟩).app D b⟩
+      invFun := fun ⟨a, b⟩ => ⟨a, (i.inv.app ⟨C, a⟩).app D b⟩
+      left_inv := fun ⟨_, _⟩ => by simp
+      right_inv := fun ⟨_, _⟩ => by simp
+    }) ?_ ?_ <;> {
+      intros
+      ext : 1
+      dsimp
+      apply have h := ?_; Sigma.ext h ?_
+      . simp
+      . dsimp [Sigma] at h ⊢
+        simp [FunctorToTypes.naturality₂_left, FunctorToTypes.naturality₂_right]
+    }
+
+theorem comp₂_Sigma {𝒟' : Type*} [Category 𝒟']
+    {F : 𝒞 ⥤ Type w} (G : 𝒟' ⥤ 𝒟) (P : F.Elements ⥤ 𝒟 ⥤ Type v) :
+    G ⋙₂ Sigma P = Sigma (G ⋙₂ P) := by
+  apply Functor.hext
+  . intro C
+    apply Functor.hext
+    . intro; simp
+    . intros
+      apply heq_of_eq
+      ext : 1
+      apply Sigma.ext <;> simp
+  . intros
+    apply heq_of_eq
+    ext : 3
+    apply Sigma.ext <;> simp
+
+end CategoryTheory.Functor
+
+/-! ## Over categories -/
+
+namespace CategoryTheory.Over
+
+universe v u
+variable {𝒞 : Type u} [Category.{v} 𝒞]
+
+-- Q: is this in mathlib?
+@[simps]
+def equiv_Sigma {A : 𝒞} (X : 𝒞) (U : Over A) : (X ⟶ U.left) ≃ (b : X ⟶ A) × (Over.mk b ⟶ U) where
+  toFun g := ⟨g ≫ U.hom, Over.homMk g rfl⟩
+  invFun p := p.snd.left
+  left_inv _ := by simp
+  right_inv := fun _ => by
+    dsimp; congr! 1 with h
+    . simp
+    . rw! [h]; simp
+
+@[simps]
+def equivalence_Elements (A : 𝒞) : (yoneda.obj A).Elements ≌ (Over A)ᵒᵖ where
+  functor := {
+    obj := fun x => .op <| Over.mk x.snd
+    map := fun f => .op <| Over.homMk f.val.unop (by simpa using f.property)
+  }
+  inverse := {
+    obj := fun U => ⟨.op U.unop.left, U.unop.hom⟩
+    map := fun f => ⟨.op f.unop.left, by simp⟩
+  }
+  unitIso := NatIso.ofComponents Iso.refl (by simp)
+  counitIso := NatIso.ofComponents Iso.refl
+    -- TODO: `simp` fails to unify `id_comp`/`comp_id`
+    (fun f => by simp [Category.comp_id f, Category.id_comp f])
+
+/-- For `X ∈ 𝒞` and `f ∈ 𝒞/A`, `𝒞(X, Over.forget f) ≅ Σ(g: X ⟶ A), 𝒞/A(g, f)`. -/
+def forget_iso_Sigma (A : 𝒞) :
+    Over.forget A ⋙₂ coyoneda (C := 𝒞) ≅
+    Functor.Sigma ((equivalence_Elements A).functor ⋙ coyoneda (C := Over A)) := by
+  refine NatIso.ofComponents₂ (fun X U => Equiv.toIso <| equiv_Sigma X.unop U) ?_ ?_
+  . intros X Y U f
+    ext : 1
+    dsimp
+    apply have h := ?_; Sigma.ext h ?_
+    . simp
+    . dsimp at h ⊢
+      rw! [h]
+      simp
+  . intros X Y U f
+    ext : 1
+    dsimp
+    apply have h := ?_; Sigma.ext h ?_
+    . simp
+    . dsimp at h ⊢
+      rw! [h]
+      apply heq_of_eq
+      ext : 1
+      simp
+
+end CategoryTheory.Over
+
+#min_imports

Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean

@@ -1,24 +1,44 @@
 /-
 Copyright (c) 2025 Sina Hazratpour. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sina Hazratpour
+Authors: Sina Hazratpour, Wojciech Nawrocki
 -/
 import Mathlib.CategoryTheory.Comma.Over.Basic
 import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
 import Mathlib.CategoryTheory.Category.Cat
 
 namespace CategoryTheory
 
+-- morphism levels before object levels. See note [CategoryTheory universes].
 universe v₁ v₂ v₃ u₁ u₂ u₃
 
--- morphism levels before object levels. See note [CategoryTheory universes].
 variable {T : Type u₁} [Category.{v₁} T]
 
 namespace Over
 
-/-- `Over.Sigma Y U` a shorthand for `(Over.map Y.hom).obj U`. This is the categoy-theoretic
-analogue of `Sigma` for types.
--/
+@[simp]
+theorem mk_eta {X : T} (U : Over X) : mk U.hom = U := by
+  rfl
+
+/-- A variant of `homMk_comp` that can trigger in `simp`. -/
+@[simp]
+lemma homMk_comp' {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) :
+    homMk (U := mk (f ≫ g ≫ h)) (f ≫ g) fgh_comp =
+    homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g :=
+  rfl
+
+@[simp]
+lemma homMk_comp'_assoc {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) :
+    homMk (U := mk ((f ≫ g) ≫ h)) (f ≫ g) fgh_comp =
+    homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := by
+  rfl
+
+@[simp]
+lemma homMk_id {X B : T} (f : X ⟶ B) (h : 𝟙 X ≫ f = f) : homMk (𝟙 X) h = 𝟙 (mk f) :=
+  rfl
+
+/-- `Over.Sigma Y U` is a shorthand for `(Over.map Y.hom).obj U`.
+This is a category-theoretic analogue of `Sigma` for types. -/
 abbrev Sigma {X : T} (Y : Over X) (U : Over (Y.left)) : Over X :=
   (map Y.hom).obj U
 
@@ -32,6 +52,7 @@ lemma hom {Y : Over X} (Z : Over (Y.left)) : (Sigma Y Z).hom = Z.hom ≫ Y.hom :
 def map {Y : Over X} {Z Z' : Over (Y.left)} (g : Z ⟶ Z') : (Sigma Y Z) ⟶ (Sigma Y Z') :=
   (Over.map Y.hom).map g
 
+@[simp]
 lemma map_left {Y : Over X} {Z Z' : Over (Y.left)} {g : Z ⟶ Z'} :
     ((Over.map Y.hom).map g).left = g.left := Over.map_map_left
 
@@ -43,6 +64,7 @@ lemma map_homMk_left {Y : Over X} {Z Z' : Over (Y.left)} {g : Z ⟶ Z'} :
 @[simps!]
 def fst {Y : Over X} (Z : Over (Y.left)) : (Sigma Y Z) ⟶ Y := Over.homMk Z.hom
 
+@[simp]
 lemma map_comp_fst {Y : Over X} {Z Z' : Over (Y.left)} (g : Z ⟶ Z') :
     (Over.map Y.hom).map g ≫ fst Z' = fst Z := by
   ext

Poly/ForMathlib/CategoryTheory/Elements.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Nawrocki
+-/
+import Mathlib.CategoryTheory.Elements
+
+namespace CategoryTheory.CategoryOfElements
+
+variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟]
+variable (F : 𝒞 ⥤ Type*) (G : F.Elements ⥤ 𝒟)
+
+-- FIXME(mathlib): `NatTrans.mapElements` and `CategoryOfElements.map` are the same thing
+
+@[simp]
+theorem map_homMk_id {X : 𝒞} (a : F.obj X) (eq : F.map (𝟙 X) a = a) :
+    -- NOTE: without `α := X ⟶ X`, a bad discrimination tree key involving `⟨X, a⟩.1` is generated.
+    G.map (Subtype.mk (α := X ⟶ X) (𝟙 X) eq) = 𝟙 (G.obj ⟨X, a⟩) :=
+  show G.map (𝟙 _) = 𝟙 _ by simp
+
+@[simp]
+theorem map_homMk_comp {X Y Z : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) eq :
+    G.map (Y := ⟨Z, F.map g (F.map f a)⟩) (Subtype.mk (α := X ⟶ Z) (f ≫ g) eq) =
+    G.map (X := ⟨X, a⟩) (Y := ⟨Y, F.map f a⟩) (Subtype.mk (α := X ⟶ Y) f rfl) ≫
+    G.map (Subtype.mk (α := Y ⟶ Z) g (by rfl)) := by
+  set X : F.Elements := ⟨X, a⟩
+  set Y : F.Elements := ⟨Y, F.map f a⟩
+  set Z : F.Elements := ⟨Z, F.map g (F.map f a)⟩
+  set f : X ⟶ Y := ⟨f, rfl⟩
+  set g : Y ⟶ Z := ⟨g, rfl⟩
+  show G.map (f ≫ g) = G.map f ≫ G.map g
+  simp
+
+end CategoryTheory.CategoryOfElements