PID, UFD, GCD domain, etc. in Mathlib

Stream: new members

[Isak Colboubrani]

Is the following a correct summary on how these structures are expressed/obtained using Mathlib?

• Algebraically closed field: [Field P] [IsAlgClosed P]
• Principal ideal domain: [CommRing P] [IsDomain P] [IsPrincipalIdealRing P]
• Unique factorization domain: [CommRing P] [IsDomain P] [UniqueFactorizationMonoid P]
• GCD domain: [CommRing P] [IsDomain P] [GCDMonoid P]
• Integrally closed domain: [CommRing P] [IsDomain P] [IsIntegrallyClosed P]
• Integral domain: [CommRing P] [IsDomain P]

[Kevin Buzzard]

My course exercises agree with you on Principal Ideal Domain and Unique Factorization Domain :-)

[Isak Colboubrani]

Thanks @Kevin Buzzard!

The Mathlib source code documentation seems to agree on integral domain.

@Ruben Van de Velde seems to agree on UFD, GCD domain and integrally closed domain.

That leaves us with algebraically closed fields. My interpretation of this snippet of Mathlib source code is that an algebraically closed field is obtained in Mathlib by [Field P] [IsAlgClosed P].

[Kevin Buzzard]

Yeah they're all fine :-)

[Kevin Buzzard]

Remember though that all of these classes are data-carrying, so if you wanted to state something like "an integrally closed principal ideal domain is a unique factorization domain" then you can't say example (R : Type) [IntegrallyClosedDomain R] [PrincipalIdealDomain R] : UniqueFactorizationDomain R because that means "define a multiplication on R making it into an integrally closed domain, and then define a completely unrelated second multiplication on R making it into a principal ideal domain" and then you get errors everywhere because Lean doesn't know which of the two functions * means. There is a reason we do it the way we do it.