Type class for an integral domain

Stream: new members

[Isak Colboubrani]

Would any of the following be the correct idiomatic formulation for an IntegralDomain type class?

class IntegralDomain₁ (P : Type*) extends CommRing P, IsCancelMulZero P, Nontrivial P
class IntegralDomain₂ (P : Type*) extends CommRing P, NoZeroDivisors P, Nontrivial P

Also, since …

example : CommRing ℤ := by infer_instance
example : IsCancelMulZero ℤ := by infer_instance
example : NoZeroDivisors ℤ := by infer_instance
example : Nontrivial ℤ := by infer_instance

… works I naïvely assumed that IntegralDomain₁ ℤ := by infer_instance and IntegralDomain₂ ℤ := by infer_instance would work too (by having Lean "combine" these existing instances), but I was mistaken. I assume that there are good reasons as to why things don't work as I naïvely assumed here. Why?

#mwe:

import Mathlib

class IntegralDomain₁ (P : Type*) extends CommRing P, IsCancelMulZero P, Nontrivial P
class IntegralDomain₂ (P : Type*) extends CommRing P, NoZeroDivisors P, Nontrivial P

example : CommRing ℤ := by infer_instance
example : IsCancelMulZero ℤ := by infer_instance
example : NoZeroDivisors ℤ := by infer_instance
example : Nontrivial ℤ := by infer_instance

-- example : IntegralDomain₁ ℤ := by infer_instance
-- example : IntegralDomain₂ ℤ := by infer_instance

[Sébastien Gouëzel]

The best solution is probably to not have a specific typeclass for integral domains, and just use [CommRing P] [IsCancelMulZero P] [Nontrivial P] whenever you need it. For instance, we don't have a typeclass for Banach spaces in mathlib, we just use [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]. And it works very well!

[Johan Commelin]

Note that [CommRing P] [IsDomain P] also works, and is slightly shorter.

[Isak Colboubrani]

Thanks! I should have mentioned that my goal in creating a type class IntegralDomain is purely for educational purposes, so I’m not proposing that it be added to Mathlib.

That said, if someone were to want an IntegralDomain class, which one of the following would be considered idiomatic? Is there a better alternative?

class IntegralDomain₁ (P : Type*) extends CommRing P, IsCancelMulZero P, Nontrivial P
class IntegralDomain₂ (P : Type*) extends CommRing P, NoZeroDivisors P, Nontrivial P
class IntegralDomain₃ (P : Type*) extends CommRing P where
  is_domain : IsDomain P

[Isak Colboubrani]

There must be an idiomatic choice among those three, right? :)

[Johan Commelin]

The idiomatic choice in mathlib is to write [CommRing R] [IsDomain R]. The practical engineering benefit of this approach is that there are fewer data-carrying classes (there are still a lot!) and we impose extra properties by adding a second typeclass assumption.