AlgebraCat.isRing isn't a Prop

Stream: mathlib4

[Kevin Buzzard]

docs#AlgebraCat looks like this:

/-- The category of R-algebras and their morphisms. -/
structure AlgebraCat where
  carrier : Type v
  [isRing : Ring carrier]
  [isAlgebra : Algebra R carrier]

Looks like @Kim Morrison wrote this in Lean 3 in 2020 (back then it looked like [is_ring : ring carrier] etc). My instinct is that is should be reserved for Props (I know that not everyone agrees) and that this field should be called toRing or ring. However it's a typeclass so this is barely relevant. The reason I noticed it was that I was reviewing #11973 which copies the style with

structure BialgebraCat extends Bundled Ring.{v} where
  [isBialgebra : Bialgebra R α]

and I was going to suggest a change but now I realise that this naming convention is following an established pattern. Are we OK with these names?

[Yaël Dillies]

Also shouldn't carrier be Carrier?

[Kevin Buzzard]

It's perhaps worth adding that after the initial boilerplate in this file, isRing shows up preciselty once in mathlib (in the same file as the definition of AlgebraCat).

[Adam Topaz]

I think such fields should be named instRing and instAlgebra. Names like toRing don't really make sense in this case IMO.

[Adam Topaz]

I think Carrier vs. carrier is more ambiguous... Imagine defining a monoid object in an arbitrary category C. Should you use Carrier : C in that case?