Refactoring adjunctions

Stream: mathlib4

[Dagur Asgeirsson]

In #16317, I redefine adjunction so that the only data contained in an adjunction is that of the unit and counit. Then homEquiv is defined in terms of the unit and counit.

The constructor mkOfHomEquiv to to create an adjunction from a natural hom set equivalence remains, and a new constructor Adjunction.mk' which is the old definition of an adjunction, containing the data of a unit, counit and hom set equivalence, together with proofs of the equalities homEquiv_unit and homEquiv_counit relating them.

This change makes the lemmas homEquiv_unit and homEquiv_counit definitional equalities, which seems to make it slightly easier for automation to apply them.

It's not a huge improvement, but I think it's a more natural definition. I'm not entirely convinved it's a good change and I'd be happy to hear others' opinion about this, arguments against this change and what was the original motivation for the current definition of Adjunction in mathlib

[Kim Morrison]

Seems like a good win in terms of reducing use of erw and change.

I think @Johan Commelin may have originally introduced this definition, so hopefully can comment if we're missing something.

[Johan Commelin]

The original design was because my intuition told me that we would care about getting good defeqs for homEquiv.

[Johan Commelin]

You've dropped homEquiv in a number of places. In other places you used Adjunction.mk'. How did you choose which option to use?

[Johan Commelin]

The reduction of erw make me happy :grinning:

[Dagur Asgeirsson]

Johan Commelin said:

The original design was because my intuition told me that we would care about getting good defeqs for homEquiv.

Indeed, the regressions I'm seeing is that some lemmas about homEquivs that were proved by rfl before now have more complicated proofs. But you always the propeqs.

[Dagur Asgeirsson]

Johan Commelin said:

You've dropped homEquiv in a number of places. In other places you used Adjunction.mk'. How did you choose which option to use?

I just dropped homEquiv if it didn't break anything. Using Adjunction.mk' makes the old proofs work. But I'm sure some of them could be refactored if desired.

[Johan Commelin]

Part of me wants to keep the homEquiv's around, if we have them anyway. And I guess you an still get rid of the erws even if you keep them.

[Johan Commelin]

But I also understand the desire to have diffs that drop code :smiley:

[Dagur Asgeirsson]

Johan Commelin said:

And I guess you an still get rid of the erws even if you keep them.

Not all of them, like in the mysterious file Adjunction.Opposites. But I'm sure I can get rid of many without this change

[Johan Commelin]

Maybe wasn't clear: I meant that you change the definition, like you do in the PR. But you use Adjunction.mk' in all places where homEquiv used to be part of the defn.

[Johan Commelin]

If you do that, you should still be able to get rid of all erw's, right?

[Johan Commelin]

If not, then that is a good reason to drop the homEquiv's

[Dagur Asgeirsson]

Ah, I see! I'll try it

[Dagur Asgeirsson]

I added back all the homEquivs, except one in Topology.Sheaves.Skyscraper. There the previous definition relied on defeqs of homEquivs, so I refactored the whole file using the new definition (removing a few more erws in the process).

@Junyan Xu and @Jujian Zhang are listed as authors and might have opinons about this change

[Johan Commelin]

Sorry for the delay. I just kicked this on the queue

[Yuma Mizuno]

I noticed the following, which is somewhat related to this PR, but perhaps should be discussed elsewhere.

/-- Composition of adjunctions.

See <https://stacks.math.columbia.edu/tag/0DV0>.
-/
def comp : F ⋙ H ⊣ I ⋙ G :=
  mk' {
    homEquiv := fun _ _ ↦ Equiv.trans (adj₂.homEquiv _ _) (adj₁.homEquiv _ _)
    unit := adj₁.unit ≫ (whiskerLeft F <| whiskerRight adj₂.unit G) ≫ (Functor.associator _ _ _).inv
    counit :=
      (Functor.associator _ _ _).hom ≫ (whiskerLeft I <| whiskerRight adj₁.counit H) ≫ adj₂.counit }

It looks the last (Functor.associator _ _ _).inv in the unit expression is put to avoid defeq abuse, but actually it fails to do that.

The expected type here is F ⋙ (H ⋙ I) ⋙ G ⟶ (F ⋙ H) ⋙ I ⋙ G, but the type of (Functor.associator _ _ _).inv (actually (Functor.associator F (H ⋙ I) G).inv) is F ⋙ (H ⋙ I) ⋙ G ⟶ (F ⋙ H ⋙ I) ⋙ G. The correct expression with the expected type is slightly more involved like whiskerLeft F (Functor.associator H I G).hom ≫ (Functor.associator F H (I ⋙ G)).inv.

[Junyan Xu]

Is this still a concern (causing slowdown)? If not we should feel free to remove the associators.