Algebra.Category.Algebra.Basic #4504

Stream: mathlib4

[Johan Commelin]

This PR has one error left: a nasty simps error.

@[simps!] -- errors (see below)
def free : Type u ⥤ AlgebraCat.{u} R where
  obj S :=
    { carrier := FreeAlgebra R S
      isRing := Algebra.semiringToRing R }
  map f := FreeAlgebra.lift _ <| FreeAlgebra.ι _ ∘ f
  -- porting note: `apply FreeAlgebra.hom_ext` was `ext1`.
  map_id := by intro X; apply FreeAlgebra.hom_ext; simp only [FreeAlgebra.ι_comp_lift]; rfl
  map_comp := by

The error is

Error: ./Mathlib/Algebra/Category/AlgebraCat/Basic.lean:146:3: error: AlgebraCat.free_obj_isRing_nsmul.{u} Left-hand side simplifies from
  a✝¹ • a✝
to
  Quot.map₂ (fun x x_1 => x * x_1)
  (_ : ∀ (x x_1 x_2 : FreeAlgebra.Pre R S), FreeAlgebra.Rel R S x_1 x_2 → FreeAlgebra.Rel R S (x * x_1) (x * x_2))
  (_ : ∀ (x x_1 x_2 : FreeAlgebra.Pre R S), FreeAlgebra.Rel R S x x_1 → FreeAlgebra.Rel R S (x * x_2) (x_1 * x_2))
  (Nat.unaryCast a✝¹) a✝
using
  simp only [@nsmul_eq_mul, AlgebraCat.free_obj_isRing_natCast, AlgebraCat.free_obj_isRing_mul]
Try to change the left-hand side to the simplified term!

To me it seems that simps! is doing too much work. I don't think we want a lemma called AlgebraCat.free_obj_isRing_nsmul at all.
How do we instruct simps to just skip generating that lemma?

[Johan Commelin]

But maybe I'm wrong, and such a lemma is in fact a good idea?

[Scott Morrison]

yes, that's terrible, we definitely don't want lemmas like that.

You can just specify the list of lemmas you do want after the simps. I'd guess here we want map? If we want any simps to do anything with obj it should be about the coercion to type rather than anything about carrier or isRing. This suggests that AlgebraCat (and possibly all the concrete categories) is missing a initialize_simps_projections.

[Antoine Chambert-Loir]

I spent some time on that one. I gave Lean two adapted versions of what it suggested, stopping at the smulstuff.
However, once Lean has all the simps lemmas, it is able to go further, and the one it suggests doesn't compile because it requires one of the not yet compiled lemmas.

[Calvin Lee]

I disabled simp lemmas about instance projections, and I think it fixed the lint. Should be good to merge now

[Johan Commelin]

I kicked it on the queue.
Really glad that this one is now done :sweat_smile: