maximum number of heartbeats (200000) has been reached

Stream: new members

[Klaus Gy]

import Mathlib.CategoryTheory.Subobject.Basic
import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
import Mathlib.CategoryTheory.Topos.Classifier

universe u v

open CategoryTheory Functor Limits MonoidalCategory Opposite

variable {ℰ : Type u} [Category.{v} ℰ] [HasPullbacks ℰ] [CartesianMonoidalCategory ℰ]

def PowerObject (B : ℰ) : ℰᵒᵖ ⥤ Type (max u v) :=
  ⟨ ⟨ fun A ↦ Subobject (B ⊗ unop A), fun f ↦ (Subobject.pullback (B ◁ unop f)).obj ⟩,
    fun A ↦ by
      have : (Subobject.pullback (B ◁ unop (𝟙 A))).obj = 𝟙 (Subobject (B ⊗ unop A)) := by
        calc
          _ = (Subobject.pullback (B ◁ 𝟙 (unop A))).obj := sorry
          _ = 𝟙 (Subobject (B ⊗ unop A)) := sorry
      sorry,
    fun f f' ↦ by
      let F : (Subobject (B ⊗ unop _) ⟶ Subobject (B ⊗ unop _)) :=
        (Subobject.pullback (B ◁ unop f)).obj
      let F' : (Subobject (B ⊗ unop _) ⟶ Subobject (B ⊗ unop _)) :=
        (Subobject.pullback (B ◁ unop f')).obj
      have : (Subobject.pullback (B ◁ unop (f ≫ f'))).obj = F ≫ F' := by
        calc
          _ = (Subobject.pullback ((B ◁ unop f) ≫ (B ◁ unop f'))).obj := sorry
          _ = F ≫ F' := by exact funext (Subobject.pullback_comp (B ◁ unop f) (B ◁ unop f')); unfold F F'
      sorry ⟩

any idea why i get

(deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

here? i already filled out the sorries, but then i thought maybe the simp lemmas take too long (which are now taken out), but apparently this was not the case?

[Kyle Miller]

I haven't checked out your example here, but it probably doesn't help that obj isn't giving actual morphisms, but function types.

What I mean in
Kyle Miller said:

This suggests you need a function that gives a Subobject morphism.

is that you want some function that represents (Subobject.pullback ...).obj in the correct form. All the type ascriptions you have to write is a symptom of this.

[Klaus Gy]

i see, thanks for your answer, ill try to create more helper functions (type wrappers)!

[Klaus Gy]

i even get the timeout for this stub :/

def PowerObject (B : ℰ) : ℰᵒᵖ ⥤ Type (max u v) :=
  let obj {X Y} (F : Subobject X ⥤ Subobject Y) : Subobject X ⟶ Subobject Y := sorry
  let comp f g : obj (Subobject.pullback (f ≫ g)) = (obj (Subobject.pullback f)) ≫ (obj (Subobject.pullback g)) := sorry
  sorry

[Klaus Gy]

i could fix this stub, but still keep running into these timeouts. could it be that some bug leads to non-termination here? should i report it on github?

[Edison Xie]

import Mathlib

universe u v

open CategoryTheory Limits MonoidalCategory Opposite

variable {ℰ : Type u} [Category.{v} ℰ] [HasPullbacks ℰ] [CartesianMonoidalCategory ℰ]

noncomputable def PowerObject (B : ℰ) : ℰᵒᵖ ⥤ Type (max u v) where
  obj A := Subobject (B ⊗ unop A)
  map f := (Subobject.pullback (B ◁ unop f)).obj
  map_id A := by
    ext1 x
    simp [show unop (𝟙 A) = 𝟙 (unop _) from rfl, Subobject.pullback_id]
  map_comp {X Y Z} f f' := by
    ext1 x
    simp [show unop (f ≫ f') = unop f' ≫ unop f from rfl, Subobject.pullback_comp]

[Edison Xie]

Klaus Gy said:

      have : (Subobject.pullback (B ◁ unop (f ≫ f'))).obj = F ≫ F' := by
        calc
          _ = (Subobject.pullback ((B ◁ unop f) ≫ (B ◁ unop f'))).obj := sorry

I think this step is wrong

[Edison Xie]

also you don't need calculation

[Klaus Gy]

thank you a lot @Edison Xie !

[Klaus Gy]

im again stuck with maximum heartbeats error here:

import Mathlib.CategoryTheory.Subobject.Basic

open CategoryTheory Limits

variable {C : Type} [Category C] [HasPullbacks C]

def test (X Y : C) (S : Subobject Y) (f f' : X ⟶ Y) : Nat :=
    let P := (Subobject.pullback f).obj S
    have : IsPullback (Subobject.pullbackπ f' S) P.arrow S.arrow f' := sorry
    1

im a bit lost, what leads to this blowup?

EDIT: OK i see it tries to work out commuting square equations and fails at that. still weird that it doesnt give an error insteaad, but blows up in heartbeats.