Proving equality in a nerve

Stream: Infinity-Cosmos

[Arnoud van der Leer]

Hi, I thought I'd try my hand at working on the coherent iso. Not because it is currently the most relevant part, but because it looks "doable" for me (ample experience in UniMath, but almost none with mathlib).

I tried proving that the morphisms into coherentIso have some "coherence" (Note that WalkingIso is just a category structure on Fin 2):

def coherentIso.pt (i : WalkingIso) : Δ[0] ⟶ coherentIso :=
  yonedaEquiv.symm (ComposableArrows.mk₀ i)

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

def coherentIso.hom_pt (i : Fin 2) : stdSimplex.δ i ≫ coherentIso.hom = coherentIso.pt i := by
  sorry

I have advanced the proof up to

((nerve WalkingIso).map (SimplexCategory.δ 0).op (ComposableArrows.mk₁ PUnit.unit)).obj 0 = 0

but am not entirely sure how to proceed. dsimp gives

⊢ (match
    (Preord.Hom.hom
        ((forget₂ PartOrd Preord).map
          ((forget₂ Lat PartOrd).map
            ((forget₂ LinOrd Lat).map
              ((forget₂ NonemptyFinLinOrd LinOrd).map
                (NonemptyFinLinOrd.ofHom (SimplexCategory.Hom.toOrderHom (SimplexCategory.δ 0))))))))
      0 with
  | ⟨0, isLt⟩ => WalkingIso.zero
  | ⟨1, isLt⟩ => WalkingIso.one) =
  0

It seems like something that is "almost, but not quite" definitionally true. I have tried unfolding a couple of the terms here, but that seems to only increase the complexity of the goal.
Which triviality am I missing? Should I delve deeper into the definition, or instead use a more high-level lemma?

[Kevin Buzzard]

What does simp do?

[Arnoud van der Leer]

If I let simp run on the "match ... 0 with ... = 0" goal:

`simp` made no progress

[Joël Riou]

If you use the injectivity of yonedaEquiv, the equality should translate as an equality in ComposableArrows _ 2, and there you may use ComposableArrows.ext₂ https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/ComposableArrows/Basic.html#CategoryTheory.ComposableArrows.ext%E2%82%82 and five goals will appear: the first three are likely to be provable by rfl.

[Arnoud van der Leer]

Ah, I used ComposableArrows.ext, which got me in this place. I will try the 2 version

[Arnoud van der Leer]

Ah, It is actually an equality in ComposableArrows _ 0. So

def coherentIso.hom_pt (i : Fin 2) : stdSimplex.δ i ≫ coherentIso.hom = coherentIso.pt i := by
  unfold pt hom yonedaEquiv CosimplicialObject.δ stdSimplex
  rw [← Equiv.apply_eq_iff_eq_symm_apply]
  rw [show (SimplexCategory.δ i) = (SimplexCategory.δ i).op.unop from rfl]
  rw [← uliftYonedaEquiv_naturality _ (SimplexCategory.δ i).op]
  rw [Equiv.apply_symm_apply]
  apply ComposableArrows.ext₀
  revert i
  simp
  constructor
  · unfold coherentIso

gives exactly

((nerve WalkingIso).map (SimplexCategory.δ 0).op (ComposableArrows.mk₁ PUnit.unit)).obj 0 = 0

again.

[Joël Riou]

Have you tried rfl?

[Arnoud van der Leer]

Tactic rfl failed: The left-hand side
((nerve WalkingIso).map (SimplexCategory.δ 0).op (ComposableArrows.mk₁ PUnit.unit)).obj 0
is not definitionally equal to the right-hand side
0

[Joël Riou]

Ok, I will have a closer look.

[Joël Riou]

Ah, please also try fin_cases i because there is a "for all".

[Arnoud van der Leer]

Ah, I did that with revert i; simp; constructor, but fin_cases is shorter indeed. Again, this gives the same goal as the two times before (the previous goals also did not contain an i) (every time, there is a similar goal where two zeroes have been replaced by ones):

(coherentIso.map (SimplexCategory.δ 0).op (ComposableArrows.mk₁ PUnit.unit)).obj 0 = 0

[Arnoud van der Leer]

CoherentIso.lean
Here is my current file

[Joël Riou]

Maybe the statement is wrong. The zeroth face "forgets" the index 0, while the first face "forgets" the index 1: the zeroth face of this map is one and the first face is zero.

[Joël Riou]

(In general, it should be possible to prove equalities in the nerve of coherentIso by decide, as it suffices to check equalities of objects (as there is always a unique map between two objects), and there is an obvious DecidableEq instance on objects).

[Arnoud van der Leer]

Joël Riou said:

Maybe the statement is wrong. The zeroth face "forgets" the index 0, while the first face "forgets" the index 1: the zeroth face of this map is one and the first face is zero.

Ooooh, of course :man_facepalming:

[Arnoud van der Leer]

Yep, that was the problem. Thanks!

[Arnoud van der Leer]

Joël Riou said:

(In general, it should be possible to prove equalities in the nerve of coherentIso by decide, as it suffices to check equalities of objects (as there is always a unique map between two objects), and there is an obvious DecidableEq instance on objects).

What is exactly the setup for calling decide? Because if I try to just throw that tactic somewhere in the middle of my proof, I get

Decidable
    (uliftYoneda.{0, 0, 0}.map (SimplexCategory.δ 1) ≫ uliftYonedaEquiv.symm (ComposableArrows.mk₁ PUnit.unit) =
      uliftYonedaEquiv.symm (ComposableArrows.mk₀ 0))

[Joël Riou]

You may look at https://github.com/leanprover-community/mathlib4/blob/725c803ee924f55342e93f2c75976051ab902b54/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean#L61

[Arnoud van der Leer]

By the Yoneda lemma, we also have decidable equality on the natural transformations to coherentIso. Is it a bad idea to create this instance?

instance (n : ℕ) : DecidableEq (coherentIso _⦋n⦌) :=
  fun _ _ ↦ decidable_of_iff _ (Equiv.apply_eq_iff_eq coherentIso_equiv_fun)

instance (n : ℕ) : DecidableEq (Δ[n] ⟶ coherentIso) :=
  fun _ _ ↦ decidable_of_iff _ (Equiv.apply_eq_iff_eq yonedaEquiv)

[Robin Carlier]

If we go down that route, shouldn't we instead introduce a general class for "decidable" simplicial sets (those for which the value on each [n] are decidable) and have it derive instances for homs from standard simplices?

[Arnoud van der Leer]

Is this a rhetorical question?
I have too little experience with the typeclass system to determine the best amount of abstraction to wield here.

[Robin Carlier]

It’s not rethorical. I genuinely feel like we could use some general abstraction here because the coherent iso is not the only simplicial set on which we’ll want to decide that kind of low-dimensional computations/coherence, but at the same time I’m wary of making it a "proper" proposal because we also don’t have a lot of decidability/computability for the rest of the category-theory side of the library; I don’t think we bothered defining DecidableEq instances on underlying type and hom-type of many "explicit" small diagrams categories, and to properly leverage it on the simplicial side one would need to go around registering instances in the category-theory side as well (at least if we want to use that nerves of "decidable categories" are "decidable simplicial sets").

[Emily Riehl]

Could we back up this conversation a bit to explain some more of the background. How does mathlib think about which types support DecidableEq? I thought the whole system was meant to be classical, so why not have this on all types?

[Aaron Liu]

it's so you can decide things

[Aaron Liu]

and also so you can run code

[Aaron Liu]

if you want to use the classical instance you can always open scoped Classical in

[Chris Henson]

To rephrase another way: you can have a noncomputable instance for any type classically, but it is still valuable to distinguish for tactics like decide that actually use the computation.

[Aaron Liu]

and then it will be on all types

[Joël Riou]

Recently, I had already added a few more DecidableEq instances (like https://github.com/leanprover-community/mathlib4/blob/cfceff41988aab4846af3b0f67e2a44b030be117/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean#L121-L123). In the very draft RFC/PR #33386 I show that if Arrow C has a DecidableEq instance, then the simplices of the nerve of C also have DecidableEq instances.

[Emily Riehl]

Is decide a tactic that gives you a non-computable element? I've never used it so I don't know how it works.

Aside: I know the mathlib/lean folks are working on improving documentation, which is great, but I still haven't the slightest idea where I should be looking for tactic documentation.

[Chris Henson]

docs#Lean.Parser.Tactic.decide has docs for the tactic

[Chris Henson]

There is some subtlety in that you can configure where the calculation happens (elaborator, kernel, or compiler), but how I would phrase it is that if you have an instance of docs#Decidable, essentially an explicit procedure for computation, the tactic then uses this to derive a proof.