Proving pullbacks are levelwise in SSet

Stream: new members

[Fedor Pavutnitskiy]

Hi, I am trying to prove that pullbacks are levelwise in the category of simplicial sets. SSet is a functor category so it should follow from evaluationJointlyReflectsLimits, but I ran into the problem of equality between terms of equal types.

import Mathlib.AlgebraicTopology.SimplicialSet
import Mathlib.CategoryTheory.Limits.Shapes.CommSq

open CategoryTheory Limits

noncomputable section

variable {W X Y Z : SSet.{0}} (f : W ⟶ X) (g : W ⟶ Y) (h : X ⟶ Z) (i : Y ⟶ Z)

variable (sq : CommSq f g h i)

variable (sq_m : (m : SimplexCategoryᵒᵖ) →  IsPullback (f.app m) (g.app m) (h.app m) (i.app m))

lemma main : IsPullback f g h i := by
  fapply IsPullback.of_isLimit'
  · exact sq
  · apply evaluationJointlyReflectsLimits
    intro m
    convert (sq_m m).isLimit
    · sorry -- cospan h i ⋙ (evaluation SimplexCategoryᵒᵖ Type).obj m = cospan (h.app m) (i.app m)
    · sorry -- some HEq

I was able to prove the first sorry, although it is an equality between functors, which should be avoided (?). I have no idea what to do with the second one. I tried various rws, substs, casts and theorems for HEq but no luck. Am I missing something obvious here ?

[Fedor Pavutnitskiy]

I guess a follow up question will be : can we deduce a HEq between "same" structures (Cone in this example) from HEqs between their fields ?

[Markus Himmel]

The solution here is to not use equality, but instead rely on isomorphisms and lemmas that tell you that everything is well-behaved under isomorphism. Instead of convert (sq_m m).isLimit, you should use docs#CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso Your first sorry is then just a natural isomorphism of the diagrams instead of an equality and your second sorry turns into an isomorphism of cones after transfer with the natural isomorphisms. For showing isomorphism of cones, we have docs#CategoryTheory.Limits.Cones.ext

[Markus Himmel]

Here is the full proof for reference:

lemma main : IsPullback f g h i := by
  fapply IsPullback.of_isLimit'
  · exact sq
  · apply evaluationJointlyReflectsLimits
    intro m
    refine IsLimit.equivOfNatIsoOfIso (cospanCompIso _ _ _).symm _ _ ?_ (sq_m m).isLimit
    refine Cones.ext (Iso.refl _) ?_
    rintro (⟨⟩|(⟨⟩|⟨⟩))
    · simp
    · simp
    · simp

[Fedor Pavutnitskiy]

this is perfect, thank you

[Fedor Pavutnitskiy]

The problem reappears for a particular choice of pullback : suppose I want to prove lemma pull : (pullback f f).obj m ≅ pullback (f.app m) (f.app m) . Here if we want to use something like limit.isoLimitCone, we need to provide a choice of LimitCone over exactly cospan (f.app m) (f.app m) , but we can find only an isomorphic ((evaluation SimplexCategoryᵒᵖ Type).obj m).mapCone (limit.cone (cospan p p)). I am quite confused tbh.

[Kevin Buzzard]

That doesn't look like a lemma by the way, it looks like a definition (an isomorphism is data not a true-false statement).

[Markus Himmel]

@Fedor Pavutnitskiy Assuming f means the same thing as before, I think you're looking for

import Mathlib.AlgebraicTopology.SimplicialSet
import Mathlib.CategoryTheory.Limits.Shapes.CommSq

open CategoryTheory Limits

noncomputable section

variable {W X Y Z : SSet.{0}} (f : W ⟶ X)

def pull : (pullback f f).obj m ≅ pullback (f.app m) (f.app m) :=
  limitObjIsoLimitCompEvaluation _ _ ≪≫ HasLimit.isoOfNatIso (cospanCompIso _ _ _)

[Fedor Pavutnitskiy]

ah, there is a specific def for it, cool, thank you. Interestingly, could not find it using moogle.ai :thinking:

[Fedor Pavutnitskiy]

@Markus Himmel where do you recommend to read about the stuff like rintro (⟨⟩|(⟨⟩|⟨⟩)) ? I want to understand how to generalize it for cones and cocones over other diagrams like parallels pairs.

[Fedor Pavutnitskiy]

for example in the example above rintro (_|_|_) also works. But in mathlib people use ⟨⟩ instead of _ in situations like this.

[Markus Himmel]

I think the most complete and up-to-date documentation for the syntax of rcases/obtain/rintro is available by hovering over an rcases invocation in VS Code or the web editor. There are often multiple ways to do the same thing with rcases patterns, and it often comes down to personal preference. I read my version as "I expect there to be two cases, the second of which should again have two cases, and in all three resulting cases there should be nothing to name". Your version reads to me like "there should be three cases, and in none of them I care how the introduced thing (if it exists) is named". The end result is the same.

[Fedor Pavutnitskiy]

Markus Himmel said:

I think the most complete and up-to-date documentation for the syntax of rcases/obtain/rintro is available by hovering over an rcases invocation in VS Code or the web editor. There are often multiple ways to do the same thing with rcases patterns, and it often comes down to personal preference. I read my version as "I expect there to be two cases, the second of which should again have two cases, and in all three resulting cases there should be nothing to name". Your version reads to me like "there should be three cases, and in none of them I care how the introduced thing (if it exists) is named". The end result is the same.

thank you for the explanation. I thought that there may be a deeper meaning behind using (⟨⟩|(⟨⟩|⟨⟩)) instead of (_|_|_).