Workaround `cannot find synthesization order for instance`?

Stream: new members

[Fernando Chu]

In the following code, I get cannot find synthesization order for instance. My understanding is that this is because Lean can't figure out which κ I want to reason about. Nonetheless, are there any ways around this? It is of course very painful to make this a lemma and then do (myLemma κ X).le f g instead of f ≤ g.

import Mathlib.CategoryTheory.Limits.Preorder
import Mathlib.CategoryTheory.RegularCategory.Basic
import Mathlib.CategoryTheory.Subobject.Lattice
import Mathlib.SetTheory.Cardinal.HasCardinalLT

open CategoryTheory Limits

universe u v w
namespace CategoryTheory

variable (κ : Cardinal.{w}) [Fact κ.IsRegular] (C : Type u) [Category.{v} C]

class Geometric extends Regular C where
  has_false (X : C) : HasInitial (Subobject X)
  has_joins_subobject (X : C) (I : Set κ.out) : HasCoproductsOfShape I (Subobject X)
  isJoin_isStableUnderBaseChange {Y X : C} (f : Y ⟶ X) {I : Set κ.out} (fP : I → Subobject X) :
    ∐ (fun (i : I) ↦ (Subobject.pullback f).obj (fP i)) = (Subobject.pullback f).obj (∐ fP)

attribute [instance] Geometric.has_false Geometric.has_joins_subobject

variable (κ : Cardinal.{w}) [Fact κ.IsRegular] {C : Type u} [Category.{v} C] [geo : Geometric κ C]

noncomputable instance (X : C) : OrderBot (Subobject X) :=
  Preorder.orderBotOfHasInitial (C := (Subobject X))

[Fernando Chu]

An (admittedly horrible) workaround I've found is doing:

noncomputable def orderBotSubobjectOfGeometric (X : C) : OrderBot (Subobject X) :=
  Preorder.orderBotOfHasInitial (C := (Subobject X))

instance (X : C) : OrderBot (Subobject X) :=
  sorry

Since the bot part of the structure has a universal property, it doesn't matter that it is essentially sorry. This lets me use ≤ while still knowing that that sorry is inconsequential.

[Robin Carlier]

I didn’t think about this too hard, but as you pinpointed, this is because κ is irrelevant for the instance you want, and so you might want to split off the part that is really needed for your instance and that does not depends on κ into its own type class, and have the class you really want extend it.

i.e

import Mathlib.CategoryTheory.Limits.Preorder
import Mathlib.CategoryTheory.RegularCategory.Basic
import Mathlib.CategoryTheory.Subobject.Lattice
import Mathlib.SetTheory.Cardinal.HasCardinalLT

open CategoryTheory Limits

universe u v w
namespace CategoryTheory

class HasFalses (C : Type u) [Category.{v} C] where
  hasInitial_subobject (X : C) : HasInitial (Subobject X)

attribute [instance] HasFalses.hasInitial_subobject

noncomputable instance {C: Type*} [Category* C] (X : C) [HasFalses C] : OrderBot (Subobject X) :=
  Preorder.orderBotOfHasInitial (C := (Subobject X))

variable (κ : Cardinal.{w}) [Fact κ.IsRegular] (C : Type u) [Category.{v} C]

class Geometric extends Regular C, HasFalses C where
  has_joins_subobject (X : C) (I : Set κ.out) : HasCoproductsOfShape I (Subobject X)
  isJoin_isStableUnderBaseChange {Y X : C} (f : Y ⟶ X) {I : Set κ.out} (fP : I → Subobject X) :
    ∐ (fun (i : I) ↦ (Subobject.pullback f).obj (fP i)) = (Subobject.pullback f).obj (∐ fP)

attribute [instance] Geometric.has_joins_subobject

variable (κ : Cardinal.{w}) [Fact κ.IsRegular] {C : Type u} [Category.{v} C] [geo : Geometric κ C]

variable (X : C)
#synth OrderBot (Subobject X)

[Fernando Chu]

Ohhhhh right, thank you!

[Robin Carlier]

Another option would be to have a second typeclass (say IsGeometric) asserting that the category is geometric for _some_ κ, and work with [IsGeometric] [Geometric κ C] if you really want to/need to work with the specific κ. This is essentially what is being done for locally presentable categories in mathlib (there are docs#CategoryTheory.IsCardinalLocallyPresentable and docs#CategoryTheory.IsLocallyPresentable and probably the theorem that we don’t have yet that a locally κ-presentable category is complete will run into the same kind of issues, and it will be an instance only when phrased with IsLocallyPresentable)
But I feel that splitting off the "really doesn’t depends on κ" part here is probably better (this way, you don’t infer the orderBot from something "overkill")

[Fernando Chu]

But I feel that splitting off the "really doesn’t depends on κ" part here is probably better (this way, you don’t infer the orderBot from something "overkill")

I wonder, I think in general there are many categories that HasFalses but we don't want their OrderBot instance to be defined as orderBotOfHasInitial. So HasFalses is in practice then just a wrapper to help the instance algorithm, rather than something with mathematical content.

[Robin Carlier]

What would be cases where we don’t want such an instance for a category that HasFalses? It’s true that you don’t want to put an orderBot on every preorder that HasInitial, but here this is putting the instance on a very specific terms (Subobject X) that are unlikely to have many other things putting an OrderBot on top of its already existing order. My gut feeling is that definitional equalities in Subobject X should be completely irrelevant and so that it’s a case where we shouldn’t care too much about what ⊥ is beyond the fact that there is one.

[Robin Carlier]

(For functor to types/presheaves, we have docs#CategoryTheory.Subfunctor as a replacement of Subobject (F : C ⥤ Type w) with good defeqs for the complete lattice structure, so even for these a HasFalses is "harmless" I think)

[Fernando Chu]

My gut feeling is that definitional equalities in Subobject X should be completely irrelevant

I'm now using the HasFalses instance and now I have to show foo to use stability under base change.

lemma foo (X : C) : ∐ (fun (i : (∅ : Set κ)) ↦ by aesop) = (⊥ : Subobject X)

Not too bad ofc, but I fear this happens in other cases.

[Robin Carlier]

Right, my reaction was to look at the order API but it seems there’s no typeclass for indexed supremums of a bounded cardinality, so there’s no way but to use the categorical coproduct here...
I also realized that there is already an orderBot instance on Subobject X when C has an initial object and is an InitialMonoClass (docs#CategoryTheory.Subobject.orderBot). So trying to derive an orderBot instance directly in the first place will be getting into diamonds (as there’s no way to make ⊥_ : Subobject X and ⊥_ : C defeq), so HasFalses is maybe not a good idea after all.

[Fernando Chu]

It definitely seems to me that this is a limitation on the typechecking algorthim that could be fixed, but sadly I don't know anything about it.