!4#5088 CategoryTheory.Monad.Monadicity

Stream: mathlib4

[Thomas Murrills]

Here there seems to be an incoming local notation "F" => leftAdjoint G (and one for "adj") which is causing problems.

I thought I'd see if I can help with the help-wanted PRs, so I'm new to this issue; it seems that so far an attempt has been made to replace it with an abbrev, but that means that some instances aren't getting synthesized when they need to in certain places. The issue with local notation is that there are many instances of e.g. F.obj, meaning we'd need to write e.g. F |>.obj for it to parse correctly instead.

Should we

1. use local notation and |>.
2. declare syntax and write a local macro/delaborator that can handle dot notation (does this exist somewhere already?)
3. manually inline leftAdjoint G in the cases that cause issues
4. do something else?

[Scott Morrison]

I mean, how bad is it to inline leftAdjoint G everywhere in that file? At first glance the notation seems not that helpful.

[Thomas Murrills]

It's not hard, but it might be a little verbose, as the "adj" local notation is for Adjunction.ofRightAdjoint G, and both are used quite a lot. I suppose we could leave a porting note and just find-replace later!

[Thomas Murrills]

(Also there are two manual-inline options, now that I think about it: use abbrev and manually inline everywhere that's necessary, or manually inline everywhere.)

[Thomas Murrills]

Separately, I'm running into the #lean4 > ✔ invalid parametric local instance error discussed in that thread in a couple of the main defs, namely

def monadicOfCreatesGSplitCoequalizers
    [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], CreatesColimit (parallelPair f g) G] :
    MonadicRightAdjoint G

def monadicOfHasPreservesReflectsGSplitCoequalizers
    [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], HasCoequalizer f g]
    [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], PreservesColimit (parallelPair f g) G]
    [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], ReflectsColimit (parallelPair f g) G] :
    MonadicRightAdjoint G

one other def with similar requirements, and

variable [∀ ⦃A B⦄ (f g : A ⟶ B) [IsReflexivePair f g], PreservesColimit (parallelPair f g) G]

The fix suggested in the linked thread would mean introducing a total of 5 classes with names like ReflectsColimitOfGSplitPair. Is this the right way to address these particular issues?

[Thomas Murrills]

(We could actually do it with 2 classes: one parametric in the property for G.IsSplitPair, e.g. OfGSplitPairs G PreservesColimit and one to handle IsReflexivePair. We could even just introduce one class OfPair which would be parametric in the kind of pair, but that seems like overkill...)

[Scott Morrison]

This PR still has a few problems, but an interesting one is:

variable [∀ ⦃A B⦄ (f g : A ⟶ B) [IsReflexivePair f g], PreservesColimit (parallelPair f g) G]

failing with:

invalid parametric local instance, parameter with type
  IsReflexivePair f g
does not have forward dependencies, type class resolution cannot use this kind of local instance because it will not be able to infer a value for this parameter.

This looks to me like a regression from Lean 3, which would have happily used this variable to generate a typeclass search for IsReflexivePair f g, when faced with PreservesColimit (parallelPair f g) G.

[Scott Morrison]

Minimisation is pretty minimal:

class P (n : Nat)
class Q (n : Nat)
variable [∀ (n : Nat) [P n], Q n] -- fails with `invalid parametric local instance`
example [P 7] : Q 7 := inferInstance -- and hence fails

while in lean 3:

class P (n : nat)
class Q (n : nat)
variable [∀ (n : nat) [P n], Q n]
example [P 7] : Q 7 := by apply_instance

Regression, not a feature, right?

[Thomas Murrills]

Is it worth trying to solve it a la the methods mentioned in the earlier thread #mathlib4 > !4#5088 CategoryTheory.Monad.Monadicity?

[Thomas Murrills]

Oh, I should link the thread which that thread links to directly—relevant prior discussion (though not with the motivation of "can we change the underlying issue"): #lean4 > ✔ invalid parametric local instance

[Notification Bot]

4 messages were moved here from #mathlib4 > CategoryTheory.Monad.Monadicity #5088 by Scott Morrison.

[Scott Morrison]

Yes, I guess Gabriel is saying here that this is by design, even if it is a regression.

[Scott Morrison]

I'm a bit unconvinced actually. With a one line patch to Lean 4 (disabling this check if the BinderInfo is .instImplicit), this example works fine.

[Scott Morrison]

lean4#2311 (as an issue), and lean4#2312 (a proposed fix).