Model of Isomorphism

Stream: Infinity-Cosmos

[Nima Rasekh]

Following the suggestion of @Emily Riehl we (@Matej Penciak and I) have been working on defining finite models of coherent isomorphisms along with appropriate maps to ``the" coherent iso, which should later all be proven to be equivalences.

We did construct two models using appropriate pushouts (and I think with the existing stuff, it shouldn't be too hard to construct further ones if one is so inclined). We also started constructing the maps between them and to the coherent iso, however, everything is defined via colimits, meaning constructing the map requires checking certain diagrams commute.

In some cases aesop or aesop_cat will do the trick, however, there 2-3 cases where it does not. We realized before we start hacking on this too much, we could ask around if there is any suggestion or experience how to approach proving commutativity of a diagram. In case it would help, here is what we did: https://github.com/emilyriehl/infinity-cosmos/blob/pushouts/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIsoModels.lean

[Emily Riehl]

Congrats. I'm glad to see some progress on this.

A small comment: an alternate way to define maps between representable simplicial sets is as standardSimplex.map yourFavoriteMapInTheSimplexCategory. This might be advantageous because standardSimplex is the name of a functor (the Yoneda embedding). Is there a reason you prefer to input a simplex in a representable instead?

[Emily Riehl]

Regarding your commutative diagrams, could you pull out an example or two for us and show it to us using a codeblock here?

[Nima Rasekh]

Emily Riehl said:

Congrats. I'm glad to see some progress on this.

A small comment: an alternate way to define maps between representable simplicial sets is as standardSimplex.map yourFavoriteMapInTheSimplexCategory. This might be advantageous because standardSimplex is the name of a functor (the Yoneda embedding). Is there a reason you prefer to input a simplex in a representable instead?

I see, that's a good suggestion. No, there was no particular reason for our approach, just what worked. We could adjust that in future updates.

[Nima Rasekh]

I don't know how easy it is to follow the example in isolation, but for example we have the following:

noncomputable def map2dModelto3dModel : Model2dCoherentIso ⟶ Model3dCoherentIso :=
  pushout.desc
    -- Δ[1] ---> Model3dCoherentIso
    (pushout.desc
      -- Δ[2] ---> Model3dCoherentIso
      ((yonedaEquiv _ _ |>.invFun (triangle 0 1 2 (by decide) (by decide))) ≫ (pushout.inl map12Coprod13Coprod02 map01Coprod00Coprod11))
      -- Δ[2] ---> Model3dCoherentIso
      ((yonedaEquiv _ _ |>.invFun (triangle 1 2 3 (by decide) (by decide))) ≫ (pushout.inl map12Coprod13Coprod02 map01Coprod00Coprod11))
      (sorry))
    -- Δ[0] ⨿ Δ[0] ---> Model3dCoherentIso
    (coprod.desc
      -- Δ[0] ---> Model3dCoherentIso
     ((yonedaEquiv Δ[3] [0] |>.invFun (const 3 1 (Opposite.op [0]))) ≫ (pushout.inl map12Coprod13Coprod02 map01Coprod00Coprod11))
      -- Δ[0] ---> Model3dCoherentIso
     ((yonedaEquiv Δ[3] [0] |>.invFun (const 3 2 (Opposite.op [0]))) ≫ (pushout.inl map12Coprod13Coprod02 map01Coprod00Coprod11)))
   (sorry)

Here Model2dCoherentIso is the simplicial set given by gluing two 2-simplices and the crushing two of the boundary edges. So, a map out of it is determined via universal property of pushouts, and so what I would want is to construct the maps out of the legs (which we did) and check that the resulting diagram of simplicial sets commutes (which has proven trickier than expected).

[Joël Riou]

About the glueing of two copies of Δ[2] along an edge, is not it isomorphic to Δ[1] ⊗ Δ[1]? If so, an alternative approach would be not to introduce the "abstract pushout", but to understand this pushout inside Δ[1] ⊗ Δ[1]. I have some draft code https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/NonDegenerateProdSimplex.lean which describes the nondegenerate simplices in Δ[p] ⊗ Δ[q] (and more specifically in Δ[1] ⊗ Δ[q]). Then, Δ[1] ⊗ Δ[1] has two nondegenerate 2-simplices, and using the subpresheaves/gluing API I am working on (it should enter mathlib soon...), it mostly follows that Δ[1] ⊗ Δ[1] is the pushout of two copies of Δ[2] along their intersection.

[Nima Rasekh]

Joël Riou said:

About the glueing of two copies of Δ[2] along an edge, is not it isomorphic to Δ[1] ⊗ Δ[1]? If so, an alternative approach would be not to introduce the "abstract pushout", but to understand this pushout inside Δ[1] ⊗ Δ[1]. I have some draft code https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/NonDegenerateProdSimplex.lean which describes the nondegenerate simplices in Δ[p] ⊗ Δ[q] (and more specifically in Δ[1] ⊗ Δ[q]). Then, Δ[1] ⊗ Δ[1] has two nondegenerate 2-simplices, and using the subpresheaves/gluing API I am working on (it should enter mathlib soon...), it mostly follows that Δ[1] ⊗ Δ[1] is the pushout of two copies of Δ[2] along their intersection.

Hi @Joël Riou thanks for the suggestion. I think what you are describing is generally useful, however, not for our specific case.

What we want is to glue two Delta[2]s so that the edge between 1 and 2 is identified to the edge between 0 and 1. So, I am creating "three composable edges along with a choice of composition for each two consecutive ones of them". However, the product would give me the "commutative square".

[Joël Riou]

Ok, it is a different gluing. It seems yours could be alternatively identified to a subcomplex of Δ[3] (it is contained in both inner horns).

[Nima Rasekh]

Joël Riou said:

Ok, it is a different gluing. It seems yours could be alternatively identified to a subcomplex of Δ[3] (it is contained in both inner horns).

Great observation!
In fact, this one is named "Model2dCoherentIso" precisely because we also define a "Model3dCoherentIso" in the file, which is exactly a copy of Delta[3] plus some conditions. So, in fact we do both (based on applications in the literature).

[Emily Riehl]

@Nima Rasekh you make a good point: could you submit this as a (draft) PR to our repository to make it easier to check out and play around with. I promise I won't merge it before you are ready ;)

BTW I just bumped Mathlib in InfinityCosmos so we can take advantage of the more compact names discussed on the thread standardSimplex -> stdSimplex.

[Matej Penciak]

Oh great! I'll rebase on the new changes, clean things up with the new features, and we'll open up a draft pr

[Nima Rasekh]

Emily Riehl said:

Nima Rasekh you make a good point: could you submit this as a (draft) PR to our repository to make it easier to check out and play around with. I promise I won't merge it before you are ready ;)

BTW I just bumped Mathlib in InfinityCosmos so we can take advantage of the more compact names discussed on the thread standardSimplex -> stdSimplex.

Yes, I think it makes sense to do a draft PR after some more adjustments.

[Matej Penciak]

We just opened the draft PR by the way: https://github.com/emilyriehl/infinity-cosmos/pull/83,

In the short term I think I'm going to try to understand how to define maps between standard simplices better than the mess that's in the file right now... I think that will go a long way towards making the proofs easier.

[Joël Riou]

It seems you are trying to define a morphism from a standard n-simplex to the nerve of a category. Using SSet.yonedaEquiv, it corresponds to an n-simplex in the nerve, which is the exact same as a term in ComposableArrows, and there you can use ComposableArrows.mk₂, ComposableArrows.mk₃, etc.

[Nima Rasekh]

Joël Riou said:

It seems you are trying to define a morphism from a standard n-simplex to the nerve of a category. Using SSet.yonedaEquiv, it corresponds to an n-simplex in the nerve, which is the exact same as a term in ComposableArrows, and there you can use ComposableArrows.mk₂, ComposableArrows.mk₃, etc.

I think that's the part we did manage to do.
However, having defined various maps out of standard simplices we then need to show they commute (i.e. certain maps are equal), to get a morphism out of the pushout.

It is correct that one can equivalently show (via Yoneda) that two specific elements (i.e the images of the identity) are equal, but that has also not worked.

[Joël Riou]

My suggestion was about improving the code at https://github.com/emilyriehl/infinity-cosmos/pull/83/files#diff-3c66ab18c69bcbf68a7119d2d168824234121ec364dda9064e9e49a2e0a95165R187-R198
Also, instead of the generic lemma Limits.colimit.hom_ext, it would be easier to use the more specialized ext lemmas like pushout.hom_ext (two equalities required instead of three).

[Joël Riou]

Also, if you need to compare simplices in nerves of categories (or equivalent types), there are specific extensionality lemmas for ComposableArrows.

[Nima Rasekh]

Joël Riou said:

Also, if you need to compare simplices in nerves of categories (or equivalent types), there are specific extensionality lemmas for ComposableArrows.

I think that might be what we are looking for. We'll look into this then.

[Emily Riehl]

@Nima Rasekh and @Matej Penciak I just pushed a few additions to your PR. A few comments:

[Emily Riehl]

Most importantly, one of your definitions is wrong:

-- ER: Warning: this is wrong: replace the lefthand instances of delta01 with delta02!
noncomputable def map01Coprod34 : (Δ[1] ⨿ Δ[1] ⟶ Sq : Type u) :=
  coprod.desc (delta01 ≫ (pushout.inl delta12 delta01)) (delta01 ≫ (pushout.inr delta12 delta01))
noncomputable def map01Coprod34' : (Δ[1] ⨿ Δ[1] ⟶ Sq' : Type u) :=
  coprod.desc
    ((stdSimplex.δ 1) ≫ (pushout.inl (stdSimplex.δ 0) (stdSimplex.δ 2)))
    ((stdSimplex.δ 1) ≫ (pushout.inr (stdSimplex.δ 0) (stdSimplex.δ 2)))

[Emily Riehl]

I discovered this when trying to define the map below and realizing that the required coherences were false!

noncomputable def map2dModel'toCoherentIso : Model2dCoherentIso' ⟶ coherentIso := by
  refine pushout.desc ?_ ?_ ?_
  · refine pushout.desc ?_ ?_ ?_
    · exact (coherentIso.twoSimplex WalkingIso.zero WalkingIso.one WalkingIso.zero)
    · exact (coherentIso.twoSimplex WalkingIso.one WalkingIso.zero WalkingIso.one)
    · rw [coherentIso.twoSimplex_δ0 WalkingIso.zero WalkingIso.one WalkingIso.zero]
      rw [← coherentIso.twoSimplex_δ2 WalkingIso.one WalkingIso.zero WalkingIso.one]
  · exact coprod.desc (coherentIso.pt WalkingIso.zero) (coherentIso.pt WalkingIso.one)
  · unfold map0Coprod0' map01Coprod34'
    apply coprod.hom_ext
    · simp only [coprod.desc_comp, Category.assoc, colimit.ι_desc, PushoutCocone.mk_pt,
        PushoutCocone.mk_ι_app, BinaryCofan.ι_app_left, BinaryCofan.mk_inl, coprod.map_desc]
      rw [coherentIso.twoSimplex_δ1 _ _ _, ← coherentIso.oneSimplex_const]
    · simp only [coprod.desc_comp, Category.assoc, colimit.ι_desc,
        PushoutCocone.mk_pt, PushoutCocone.mk_ι_app,
        BinaryCofan.mk_pt, BinaryCofan.ι_app_right, BinaryCofan.mk_inr, coprod.map_desc]
      rw [coherentIso.twoSimplex_δ1 _ _ _, ← coherentIso.oneSimplex_const]

[Emily Riehl]

To do this, I made several additions to the general coherentIso infrastructure, some of which have sorries.

[Emily Riehl]

Specifically:

def oneSimplex (X₀ X₁ : WalkingIso) : Δ[1] ⟶ coherentIso :=
  (yonedaEquiv coherentIso _).symm
    (ComposableArrows.mk₁ (X₀ := X₀) (X₁ := X₁) ⟨⟩)

theorem oneSimplex_ext {X₀ X₁ Y₀ Y₁ : WalkingIso} (e₀ : X₀ = Y₀) (e₁ : X₁ = Y₁) :
    oneSimplex X₀ X₁ = oneSimplex Y₀ Y₁ :=
  congrArg (yonedaEquiv coherentIso _).symm (ComposableArrows.ext₁ e₀ e₁ rfl)

def twoSimplex (X₀ X₁ X₂ : WalkingIso) : Δ[2] ⟶ coherentIso :=
  (yonedaEquiv coherentIso _).symm
    (ComposableArrows.mk₂ (X₀ := X₀) (X₁ := X₁) (X₂ := X₂) ⟨⟩ ⟨⟩)

theorem oneSimplex_const (X₀ : WalkingIso) :
    oneSimplex X₀ X₀ = stdSimplex.map ([1].const [0] 0) ≫ pt X₀ := by
  unfold oneSimplex pt
  sorry

theorem twoSimplex_δ0 (X₀ X₁ X₂ : WalkingIso) :
    stdSimplex.δ 0 ≫ twoSimplex X₀ X₁ X₂ = oneSimplex X₁ X₂ := rfl

theorem twoSimplex_δ1 (X₀ X₁ X₂ : WalkingIso) :
    stdSimplex.δ 1 ≫ twoSimplex X₀ X₁ X₂ = oneSimplex X₀ X₂ := by
  unfold twoSimplex oneSimplex
  sorry

theorem twoSimplex_δ2 (X₀ X₁ X₂ : WalkingIso) :
    stdSimplex.δ 2 ≫ twoSimplex X₀ X₁ X₂ = oneSimplex X₀ X₁ := by
  unfold twoSimplex oneSimplex
  sorry

[Emily Riehl]

These sorries shouldn't be that hard to fill. Essentially it's just by naturality of yonedaEquiv. Does anyone know if this is a theorem somewhere?

[Emily Riehl]

I also explored the idea of proving that coherentIso is 0-coskeletal but decided it might be easier to just directly define the constructions (eg oneSimplex, twoSimplex) that follow from coskeletality.

These sorts of results generalize to

def simplex {n : ℕ} (obj : Fin (n + 1) → WalkingIso) : Δ[n] ⟶ coherentIso := by
  refine (yonedaEquiv coherentIso _).symm ?_
  exact {
    obj := obj
    map := fun _ => ⟨⟩
  }

theorem simplex_map {n m : ℕ}
    (obj : Fin (n + 1) → WalkingIso) (α : ([m] : SimplexCategory) ⟶ [n]) :
    stdSimplex.map α ≫ simplex obj = simplex (obj ∘ α.toOrderHom) := sorry

[Emily Riehl]

I guess in general my advice is to
(a) use Mathlib infrastructure where possible; eg rather than giving special names to the maps between the simplices, use the standard names
(b) when you get stuck constructing/proving something think about whether it would be easier to just do so more generally. This is what led to all the stuff I added to the CoherentIso file in your PR.

[Joël Riou]

Emily Riehl said:

These sorries shouldn't be that hard to fill. Essentially it's just by naturality of yonedaEquiv. Does anyone know if this is a theorem somewhere?

We have a lot of missing lemmas regarding SSet.yonedaEquiv. If we need more, we may use the same names as in CategoryTheory.Yoneda. (SSet.yonedaEquiv uses an extra ulift layer as compared to CategoryTheory.yonedaEquiv.)

[Emily Riehl]

Does anyone want to try to adapt some of the code here to SSet.yonedaEquiv? This would be a useful PR to mathlib.

[Nima Rasekh]

Emily Riehl said:

I guess in general my advice is to
(a) use Mathlib infrastructure where possible; eg rather than giving special names to the maps between the simplices, use the standard names
(b) when you get stuck constructing/proving something think about whether it would be easier to just do so more generally. This is what led to all the stuff I added to the CoherentIso file in your PR.

Thanks for all the suggestions, yeah that sounds reasonable!

[Nima Rasekh]

I guess the mistake in the file is clearly my fault and I missed something.
I think we'll give it another try based on these suggestions, after correcting the mistake.
Our main aim until now was constructing Model3dCoherentIso ⟶ coherentIso, which was not affected by this mistake, but can benefit from more facts about coherentIso, as you have suggested.

[Nima Rasekh]

Emily Riehl said:

Does anyone want to try to adapt some of the code here to SSet.yonedaEquiv? This would be a useful PR to mathlib.

Maybe this could be its own topic?

[Emily Riehl]

@Matej Penciak has been developing some useful API about the coherent isomorphism. Does the following exist in Mathlib (for an arbitrary type in place of WalkingIso):

def f₀₁ (X₀ X₁ : WalkingIso) : Fin (1 + 1) → WalkingIso := fun
  | 0 => X₀
  | 1 => X₁

If not, how would one inline an argument of this form? It occurs to me I have no idea.

[Joël Riou]

example {α : Type*} (a₀ a₁ : α) : Fin 2 → α := ![a₀, a₁]

[Matej Penciak]

I didn't realize that notation existed.

[Edward van de Meent]

it is defined in Mathlib.Data.Fin.VecNotation

[Emily Riehl]

@Matej Penciak I was playing around with your new code and filled in a few more sorries (plus implemented the vector notation).