IsIntegralDomain and IsUniqueFactorizationDomain

Stream: new members

[Isak Colboubrani]

Would the following be the correct and idiomatic definitions for IsIntegralDomain and IsUniqueFactorizationDomain?

What can be improved?

def IsIntegralDomain (α : Type) [CommRing α] : Prop :=
  IsDomain α
def IsUniqueFactorizationDomain (α : Type) [CommRing α] [CancelCommMonoidWithZero α] : Prop :=
  IsDomain α ∧ UniqueFactorizationMonoid α

Example:

example : IsIntegralDomain ℤ := by
  unfold IsIntegralDomain
  infer_instance
example : IsUniqueFactorizationDomain ℤ := by
  unfold IsUniqueFactorizationDomain
  constructor
  infer_instance
  infer_instance

[Ruben Van de Velde]

No, I'm pretty sure combining [CommRing α] [CancelCommMonoidWithZero α] will cause trouble

[Ruben Van de Velde]

Maybe def IsUniqueFactorizationDomain (α : Type) [CommRing α] [NoZeroDivisors α]

[Isak Colboubrani]

New try:

import Mathlib

-- An integral domain is a commutative ring without zero divisors.
structure IntegralDomain (α : Type) [CommRing α] [IsDomain α]
-- ℤ is an integral domain.
example : IntegralDomain ℤ := by constructor

-- A unique factorization domain is an integral domain where every element can be written as a product of prime elements.
structure UniqueFactorizationDomain (α : Type) [CommRing α] [IsDomain α] [UniqueFactorizationMonoid α]
-- ℤ is a unique factorization domain.
example : UniqueFactorizationDomain ℤ := by constructor

Is it correct, and idiomatic?

[Isak Colboubrani]

Can be contrasted with:

class IsAlgClosed : Prop where…
class Field (K : Type u) extends CommRing K, DivisionRing K…
class EuclideanDomain (R : Type u) extends CommRing R, Nontrivial R where…
class IsPrincipalIdealRing (R : Type u) [Semiring R] : Prop where…
class UniqueFactorizationMonoid (α : Type*) [CancelCommMonoidWithZero α] extends…
class IsDomain (α : Type u) [Semiring α] extends IsCancelMulZero α, Nontrivial α : Prop…
class CommRing (α : Type u) extends Ring α, CommMonoid α…
class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R…
class NonUnitalRing (α : Type*) extends NonUnitalNonAssocRing α, NonUnitalSemiring α…

[Isak Colboubrani]

Upon further reflection, I think my inquiry is twofold:

1. If IntegralDomain were defined in Mathlib, what would its structure and implementation be? For example, would it take the form: class IntegralDomain (α : Type) [CommRing α] [IsDomain α]?

2. Should such a structure exist in Mathlib (as a separate class), and if so, what are the reasons for or against its inclusion?

[Kevin Buzzard]

class IntegralDomain (α : Type*) extends CommRing α, IsDomain α

We don't really need it, because instead of saying [IntegralDomain R] we can just say [CommRing R] [IsDomain R], so in some sense it's just clogging the typeclass system up and the system is already extremely large and unwieldy. An argument for it is better readability for mathematicians, but there might be other ways to achieve this.

[Isak Colboubrani]

Ah, thanks! I understand.

When you mention clogging up the typeclass system, are you referring strictly to performance issues, where having too many type classes slows down processing? Or are you also talking about usability concerns, where an excess of type classes makes the code more difficult to handle for Mathlib users or developers?

A naïve undergraduate (like myself) just starting with Lean and Mathlib would likely assume the following naming conventions and use grep accordingly:

Name in undergraduate literature	Expected name in Mathlib	Actual name in Mathlib (IIUC)
algebraically closed fields	AlgebraicallyClosedField	IsAlgClosed
fields	Field	Field
Euclidean domains	EuclideanDomain	EuclideanDomain
principal ideal domains	PrincipalIdealDomain	IsDomain + IsPrincipalIdealRing
unique factorization domains	UniqueFactorizationDomain	IsDomain + CommRing + UniqueFactorizationMonoid
GCD domains	GCDDomain	IsDomain + CommRing + GCDMonoid
integrally closed domains	IntegrallyClosedDomain	IsDomain + IsIntegrallyClosed
integral domains	IntegralDomain	IsDomain + CommRing
commutative rings	CommutativeRing	CommRing
rings	Ring	Ring
rngs, non-unital rings	NonUnitalRing	NonUnitalRing

Fortunately, most of the entries in the hierarchy align with the expectations of a naïve beginner, but some do not—specifically the non-Euclidean integral domains. (To be completely honest, I'm not entirely sure I got the Mathlib column for all the non-Euclidean integral domains correct above... Please let me know if any of them are wrong!)

Does Lean support some kind of "type aliases" that would allow for aliases like the following without affecting performance?

• [PrincipalIdealDomain P] as an alias for [IsDomain P] [IsPrincipalIdealRing P]
• [UniqueFactorizationDomain P] as an alias for [IsDomain P] [CommRing P] [UniqueFactorizationMonoid P]
• [GCDDomain P] as an alias for [IsDomain P] [CommRing P] [GCDMonoid P]
• [IntegrallyClosedDomain P] as an alias for [IsDomain P] [IsIntegrallyClosed P]
• [IntegralDomain P] as an alias for [IsDomain P] [CommRing P]

Another question out of curiosity: why is it class IsAlgClosed instead of the more grep-friendly and predictable class AlgebraicallyClosedField?