Combine coproducts

Stream: Is there code for X?

[Christian Merten]

Is there something like this:

import Mathlib

open CategoryTheory Limits Functor

variable {C : Type u} [Category.{v, u} C]

def comb (α : Type*) (f : α → Type*) (g : (a : α) → f a → C)
    (t : ∀ a, ColimitCocone (Discrete.functor (g a)))
    (s : ColimitCocone (Discrete.functor (fun a ↦ (t a).cocone.pt))) :
    Cocone (Discrete.functor (Sigma.uncurry g : Sigma f → C)) := sorry

i.e. given a family of coproduct diagrams indexed over some type α and a coproduct of the cone points, is there one big coproduct on Sigma f?
I tried to formulate this for arbitrary functors first (indead of restricting to Discrete.functor) but I struggled to emulate the dependence on the value of f.
There is docs#CategoryTheory.Limits.combineCocones but there the index categories are the same for every diagram (i.e. f above would have to be constant).

[Joël Riou]

I prove something similar in PR #8242:
https://github.com/leanprover-community/mathlib4/pull/8242/files#diff-872c679954b062c45a489c6ba4184c58b3220532467f779d8859dcc80692358dR435-R444

[Christian Merten]

@Joël Riou To clean up some code, I tried to replace my ad-hoc proof of the sorry above by using the GradedObject API, in particular I tried to use docs#CategoryTheory.GradedObject.isColimitCofanMapObjComp that you added in the above mentioned PR.

This is the very much horrible result:

import Mathlib

variable {C : Type} [Category C]

def blaequiv1 (ι : Type) (X : ι → C) :
    Discrete ((fun x : ι ↦ ())⁻¹' {()}) ≌ Discrete ι := sorry

def blaequiv2 (ι : Type) (X : ι → C) :
    ((blaequiv1 ι X).functor ⋙ Discrete.functor X)
    ≅
    Discrete.functor (X ∘ Subtype.val) := sorry

def blaequiv3 (ι : Type) (X : ι → C) :
    GradedObject.CofanMapObjFun X (fun _ ↦ ()) ()
    ≌ Cofan X := by
  symm
  apply Cocones.equivalenceOfReindexing (blaequiv1 ι X) (blaequiv2 ι X)

def fooequiv1 (ι : Type) (t : ι → Type)
    (f : (i : ι) → (a : t i) → C) (i : ι) :
    Discrete ((fun x : Sigma t ↦ x.fst)⁻¹' {i}) ≌ Discrete (t i) := sorry

def fooequiv2 (ι : Type) (t : ι → Type)
    (f : (i : ι) → (a : t i) → C) (i : ι) :
    ((fooequiv1 ι t f i).functor ⋙ Discrete.functor (f i))
    ≅ Discrete.functor (Sigma.uncurry f ∘ Subtype.val) :=
  sorry

def fooequiv3 (ι : Type) (t : ι → Type)
    (f : (i : ι) → (a : t i) → C) (i : ι) :
    GradedObject.CofanMapObjFun (Sigma.uncurry f) Sigma.fst i
    ≌ Cofan (f i) := by
  symm
  apply Cocones.equivalenceOfReindexing (fooequiv1 ι t f i) (fooequiv2 ι t f i)

def combCofans (ι : Type) (t : ι → Type)
    (f : (i : ι) → (a : t i) → C)
    (cf : (i : ι) → Cofan (f i))
    (cg : Cofan (fun i ↦ (cf i).pt)) :
    Cofan (Sigma.uncurry f) := by
  let I : Type := Sigma t
  let X : GradedObject I C := Sigma.uncurry f
  let J : Type := ι
  let K : Type := Unit
  let p : I → J := fun ⟨i, _⟩ ↦ i
  let q : J → K := fun _ ↦ ()
  let r : I → K := q ∘ p
  have hpqr (i : I) : q (p i) = r i := rfl
  let k : K := ()
  let c (j : J) (_ : q j = k) : GradedObject.CofanMapObjFun X p j :=
    (fooequiv3 ι t f j).inverse.obj (cf j)
  let c' : Cofan (fun j : (q⁻¹' {k}) ↦ (c j rfl).pt) :=
    (blaequiv3 J (fun j ↦ (c j rfl).pt)).inverse.obj cg
  let cfm := X.cofanMapObjComp p q r hpqr k c c'
  exact (blaequiv3 _ X).functor.obj cfm

def combCofansIsColimit (ι : Type) (t : ι → Type)
    (f : (i : ι) → (a : t i) → C)
    (cf : (i : ι) → Cofan (f i))
    (hcf : (i : ι) → IsColimit (cf i))
    (cg : Cofan (fun i ↦ (cf i).pt))
    (hcg : IsColimit cg) : IsColimit (combCofans ι t f cf cg) := by
  let I : Type := Sigma t
  let X : GradedObject I C := Sigma.uncurry f
  let J : Type := ι
  let K : Type := Unit
  let p : I → J := fun ⟨i, _⟩ ↦ i
  let q : J → K := fun _ ↦ ()
  let r : I → K := q ∘ p
  have hpqr (i : I) : q (p i) = r i := rfl
  let k : K := ()
  let c (j : J) (_ : q j = k) : GradedObject.CofanMapObjFun X p j :=
    (fooequiv3 ι t f j).inverse.obj (cf j)
  let c' : Cofan (fun j : (q⁻¹' {k}) ↦ (c j rfl).pt) :=
    (blaequiv3 J (fun j ↦ (c j rfl).pt)).inverse.obj cg
  let cfm := X.cofanMapObjComp p q r hpqr k c c'
  have : IsColimit cfm := by
    apply GradedObject.isColimitCofanMapObjComp
    · intro j h
      show IsColimit (c j h)
      apply (IsColimit.ofCoconeEquiv (fooequiv3 ι t f j).symm).symm (hcf j)
    · show IsColimit ((blaequiv3 J (fun j ↦ (c j rfl).pt)).inverse.obj cg)
      apply (IsColimit.ofCoconeEquiv (blaequiv3 J (fun j ↦ (c j rfl).pt)).symm).symm hcg
  exact (IsColimit.ofCoconeEquiv (blaequiv3 _ X)).symm this

[Christian Merten]

I made it extra verbose to see what's going on. Do you think this can be optimized (more on a global scale, of course this can be golfed)? Or should I simply go with a direct implementation (which is not hard and definitely shorter than the above (even if one golfs away all the verboseness).

[Joël Riou]

If I had to do this, I think would first prove the following variant of GradedObject.isColimitCofanMapObjComp, and then deduce the case of sigma types:

variable {I J C : Type*} [Category C] (X : I → C) (p : I → J)
  (c : ∀ (j : J), Cofan (fun (i : p ⁻¹' {j}) => X i))
  (hc : ∀ (j : J), IsColimit (c j))
  (c' : Cofan (fun j => (c j).pt))
  (hc' : IsColimit c')

def cofanCombine : Cofan X := Cofan.mk c'.pt (fun i => (c (p i)).inj ⟨i, rfl⟩ ≫ c'.inj _)

def isColimitCofanCombine : IsColimit (cofanCombine X p c c') := sorry

Actually, this variant could be added first in CategoryTheory.GradedObject because this would basically show how GradedObject.total interacts with GradedObject.map.

[Christian Merten]

Thanks!
Joël Riou said:

Actually, this variant could be added first in CategoryTheory.GradedObject because this would basically show how GradedObject.total interacts with GradedObject.map.

Are you saying that GradedObject.isColimitCofanMapObjComp should be deduced from the variant you gave above?

[Christian Merten]

And this is the code for the sigma types using your combineCofan from above:

variable {J C : Type*} [Category C] (t : J → Type)
  (X : (i : J) → (a : t i) → C)
  (c : ∀ (i : J), Cofan (X i))
  (hc : ∀ (i : J), IsColimit (c i))
  (c' : Cofan (fun j => (c j).pt))
  (hc' : IsColimit c')

@[simp]
def fooequiv0 (i : J) : @Sigma.fst _ t ⁻¹' {i} ≃ t i where
  toFun := by rintro ⟨⟨j, a⟩, rfl : j = i⟩; exact a
  invFun a := ⟨⟨i, a⟩, rfl⟩
  left_inv := by rintro ⟨⟨j, a⟩, rfl : j = i⟩; rfl
  right_inv x := rfl

def fooequiv2 (i : J) :
    ((Discrete.equivalence (fooequiv0 t i)).functor ⋙ Discrete.functor (X i))
    ≅ Discrete.functor (Sigma.uncurry X ∘ Subtype.val) := by
  apply Discrete.natIso
  rintro ⟨⟨⟨j, a⟩, rfl : j = i⟩⟩
  exact eqToIso rfl

def fooequiv3 (i : J) :
    Cofan (X i) ≌ Cofan (fun (⟨⟨j, a⟩, _⟩ : Sigma.fst⁻¹' {i}) => X j a) :=
  Cocones.equivalenceOfReindexing (Discrete.equivalence (fooequiv0 t i)) (fooequiv2 t X i)

def cofanCombine' : Cofan (Sigma.uncurry X) :=
  cofanCombine (Sigma.uncurry X) (fun ⟨i, _⟩ => i)
    (fun i => (fooequiv3 t X i).functor.obj (c i)) c'

def isColimitCofanCombine' : IsColimit (cofanCombine' t X c c') := by
  apply isColimitCofanCombine
  · intro j
    apply (IsColimit.ofCoconeEquiv (fooequiv3 t X j)).symm (hc j)
  · exact hc'

I still need some auxiliary equivs, can this be avoided? The issue is that Cocones.equivalenceOfReindexing seems to be quite slow.

[Joël Riou]

Christian Merten said:

Are you saying that GradedObject.isColimitCofanMapObjComp should be deduced from the variant you gave above?

If it is convenient to do so, this could be a good idea.

The ingredients you suggest all seem relevant to me. However, I ended up with a more simple definition of cofanCombine' which is not defeq to yours:

variable {J C : Type*} [Category C] (t : J → Type*)
  (X : (i : J) → (a : t i) → C) (c : ∀ (i : J), Cofan (X i)) (hc : ∀ (i : J), IsColimit (c i))
  (c' : Cofan (fun j => (c j).pt)) (hc' : IsColimit c')

def cofanCombine' : Cofan (Sigma.uncurry X) :=
  Cofan.mk c'.pt (fun x => (c x.1).inj x.2 ≫ c'.inj x.1)

As the definition here is quite basic, it would make sense to put the necessary auxiliary definitions inside the definition of isColimitCofanCombine' .

[Christian Merten]

The reason why I defined cofanCombine' as above, was because then isColimitCofanCombine applies directly. With your cofanCombine' I need to show an isomorphism with my version to apply isColimitCofanCombine. All of this makes we wonder if its worth the going back and forth with equivalences, because this:

variable {J C : Type*} [Category C] (t : J → Type*)
  (X : (i : J) → (a : t i) → C) (c : ∀ (i : J), Cofan (X i)) (hc : ∀ (i : J), IsColimit (c i))
  (c' : Cofan (fun j => (c j).pt)) (hc' : IsColimit c')

@[simp]
def cofanCombine' : Cofan (Sigma.uncurry X) :=
  Cofan.mk c'.pt (fun x => (c x.1).inj x.2 ≫ c'.inj x.1)

def isColimitCofanCombine'' : IsColimit (cofanCombine' t X c c') := mkCofanColimit _
  (fun s => Cofan.IsColimit.desc hc' <| fun j ↦ by
    apply Cofan.IsColimit.desc (hc j) (fun a ↦ s.inj ⟨j, a⟩))
  (fun s => by aesop)
  (fun s m hm => Cofan.IsColimit.hom_ext hc' _ _ <| fun j ↦ by
    refine Cofan.IsColimit.hom_ext (hc j) _ _ (fun j ↦ ?_)
    simp only [← hm, Cofan.IsColimit.fac, cofanCombine', cofan_mk_inj, Category.assoc])

is shorter than anything I have done before using isColimitCofanCombine.

[Joël Riou]

This looks good to me.