Commit 2024-11-25 09:33 5f457536

refactor(Algebra/Category): turn homs in AlgebraCat into a structure (#19065) In the current design of concrete categories in mathlib, there are two sources of erws:

• Def-Eq abuse of A ⟶ B and A →ₐ [R] B: The type of A ⟶ B is by definition A →ₐ[R] B, but not at reducible transparency. So it happens that one rw lemma transforms a term in a form, where the next rw expects A →ₐ B. By supplying explicit show lines (copying the output of the pretty-printer), Lean correctly re-synthesizes the type to be A →ₐ B and the rw succeeds. This def-eq abuse hence always causes issues in the case where a lemma from the non-category theoretic part of the library should be applied. An insightful example is the following proof excerpt from current master (proof of AlgebraCat.adj):

import Mathlib.Algebra.Category.AlgebraCat.Basic
open CategoryTheory AlgebraCat
variable {R : Type u} [CommRing R]
set_option pp.analyze true
example : free.{u} R ⊣ forget (AlgebraCat.{u} R) :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun _ _ => (FreeAlgebra.lift _).symm
      homEquiv_naturality_left_symm := by
        intro X Y Z f g
        apply FreeAlgebra.hom_ext
        ext x
        simp only [Equiv.symm_symm, Function.comp_apply, free_map]
        /- Eq (α := Z)
             (((FreeAlgebra.lift R) (f ≫ g) :
               Prefunctor.obj (Functor.toPrefunctor (free R)) X ⟶ Z) (FreeAlgebra.ι R x) : ↑Z) _
        -/
        erw [FreeAlgebra.lift_ι_apply]
        sorry
      homEquiv_naturality_right := sorry }

The simp lemma FreeAlgebra.lift_ι_apply expects an AlgHom, but as the pp.analyze shows, the type is synthesized as a ⟶. With a show line before the erw, Lean correctly synthesizes the type as an AlgHom again and the rw succeeds. The solution is to strictly distinguish between A ⟶ B and A →ₐ[R] B: We define a new AlgebraCat.Hom structure with a single field hom : A →ₐ[R] B. The above proof is mostly solved by ext; simp then, except for the ext lemma FreeAlgebra.hom_ext not applying. This is because now the type is AlgebraCat.of R (FreeAlgebra R X) →ₐ[R] _ and Lean can't see through the AlgebraCat.of at reducible transparency. Hence the solution is to make AlgebraCat.of an abbrev. Finally, the proof is by ext; simp or even by aesop.

• FunLike: An intermediate design adapted the changes from the first point, but with keeping a FunLike and an AlgHomClass instance on A ⟶ B. This lead to many additional coe lemmas for composition of morphisms, where it mattered which of the three appearing terms of AlgebraCat where of the form AlgebraCat.of R A. Eric Wieser suggested to replace the FunLike by a CoeFun which is inlined, so an invocation of f x turns into f.hom x. This has then worked very smoothly. So the key points are:
• Homs in concrete categories should be one-field structures to maintain a strict type distinction.
• Use CoeFun instead of FunLike, since the latter is automatically inlined.
• Make .of constructors an abbrev to obtain the def-eq ↑(AlgebraCat.of R A) = A at reducible transparency. For more details, see the Zulip discussion.