Any finite integral domain is a field, etc. (ring theory)

Stream: new members

[Isak Colboubrani]

For demonstration purposes, I have translated some elementary textbook definitions and results from ring theory into corresponding Mathlib example:s. The goal is to illustrate for fellow mathematics undergraduates how familiar pen-and-paper concepts can be expressed using Mathlib.

The idea is to closely follow Dummit & Foote's ring theory chapter, essentially replicating it one-to-one.

Are there any obvious errors in the content below? What improvements would you suggest? Is the choice of tactics sound? All suggestions are welcome.

#mwe

import Mathlib

-- A ring R with identity 1 is a set together with two binary operations
-- + and * (called addition and multiplication) satisfying the following
-- axioms:
--
-- 1. (R, +) is an abelian group:
example (R : Type) [Ring R] : ∀ a : R, a + (-a) = 0 ∧ (-a) + a = 0 := by
  simp
example (R : Type) [Ring R] : ∀ a : R, a + 0 = a ∧ 0 + a = a := by
  simp
example (R : Type) [Ring R] : ∀ a b c : R, a + (b + c) = (a + b) + c := by
  intro a b c
  rw [@AddSemigroup.add_assoc]
-- 2. * is associative:
example (R : Type) [Ring R] : ∀  a b c : R, (a * b) * c = a * (b * c) := by
  intro a b c
  exact mul_assoc a b c
-- 3. the distributive laws hold in R:
example (R : Type) [Ring R] : ∀ a b c : R, (a + b) * c = a * c + b * c ∧ a * (b + c) = a * b + a * c := by
  aesop
-- 4. there is an element 1 ∈ R with 1 * a = a * 1 = a ∀ a ∈ R:
example (R : Type) [Ring R] : ∀ a : R, 1 * a = a ∧ a * 1 = a := by
  simp

-- The ring R is commutative if multiplication is commutative.
example (R : Type) [CommRing R] : ∀ a b : R, a * b = b * a := by
  intro a b
  exact CommMonoid.mul_comm a b

-- A ring with identity 1, where 1 ≠ 0, is called a division ring
-- (or skew field) if every nonzero element a ∈ R has a multiplicative
-- inverse.
example (R : Type) [DivisionRing R] : ∃ x y : R, x ≠ y := by
  exact exists_pair_ne R
example (R : Type) [DivisionRing R] : ∀ (a : R), a ≠ 0 → a * a⁻¹ = 1 := by
  aesop

-- A commutative division ring is called a field.
example (R : Type) [CommRing R] [DivisionRing R] : IsField R := by sorry

-- A commutative ring with identity 1 ≠ 0 is called an integral domain
-- if it has no zero divisors.
class IntegralDomain (P : Type) extends CommRing P, IsDomain P
example (R : Type) [IntegralDomain R] : ∀ a b c : R, a ≠ 0 → a * b = a * c → b = c ∧ b ≠ 0 → a * b = c * b → a = c := by
  simp_all

-- Any finite integral domain is a field.
example (R : Type) [IntegralDomain R] [Finite R] : IsField R := by
  exact Finite.isField_of_domain R

[Kevin Buzzard]

rw [@AddSemigroup.add_assoc] should just be rw [add_assoc] and exact CommMonoid.mul_comm a b should be exact mul_comm a b (these are more idiomatic).

[Kevin Buzzard]

example (R : Type) [CommRing R] [DivisionRing R] : IsField R := by sorry

This is not provable. Both CommRing and DivisionRing are data, so they put e.g. two different additions and multiplications on R.

[Isak Colboubrani]

Thanks! My mental model here was clearly off, and I realize I have some reading to do. (If you have any recommendations for a resource that thoroughly explains the difference between data-carrying and non-data-carrying structures, I'd really appreciate it—I've struggled with this concept before.)

When I read (R : Type) [CommRing R] [DivisionRing R] : IsField RI naively think that assuming a type R that satisfies the contracts of both a CommRing and a DivisionRing, we claim that is can be show that R fulfills the contract of a Field.

I now understand where my reasoning goes wrong: Lean treats these as two separate structures, meaning the two additions and two multiplications (of CommRing and DivisionRing respectively) may not coincide.

To force them to coincide, the correct approach is to bundle the structures into a single, unified structure?

My naive attempt might be:

class CommDivisionRing (R : Type) extends CommRing R, DivisionRing R
example (R : Type) [CommDivisionRing R] : IsField R := by sorry

Would this avoid the problem?

What would be a better, more idiomatic way to do it?

Essentially, I want to demonstrate that a commutative ring that also functions as a division ring is, in fact, a field. (I guess one alternative approach could be to show the source code definitions of Field, CommRing, and DivisionRing side by side. However, I believe it would be more approachable to illustrate this using example blocks instead.)

[Isak Colboubrani]

I think part of the confusion is that sometimes my flawed mental model of this ends up giving the right result (unfortunately).

Consider these two examples:

example (R : Type) [CommRing R] [IsDomain R] [Finite R] : IsField R := by exact Finite.isField_of_domain R
example (R : Type) [CommRing R] [DivisionRing R] : IsField R := by sorry

The first example is correct, but the second one is not? Is this because DivisionRing is a data-carrying structure while IsDomain and Finite are not?

Is there a naming convention that indicates when a structure is non-data-carrying—I would guess at least everything prefixed Is is not data-carrying? Or more generally, how do I know is a structure is data-carrying or not?

[Damiano Testa]

In your CommDivisionRing case, you can use

example (R : Type) [CommDivisionRing R] : IsField R :=
  @Field.toIsField _ {__ := (inferInstance : CommDivisionRing R)}

though this is just an obscure way of saying: CommDivisionRing and Field have the same properties.

[Isak Colboubrani]

@Damiano Testa hint suggests exact IsArtinianRing.isField_of_isDomain R.

That was not what I expected! :)

import Mathlib
class CommDivisionRing (R : Type) extends CommRing R, DivisionRing R
example (R : Type) [CommDivisionRing R] : IsField R := by
  exact IsArtinianRing.isField_of_isDomain R

Is the introduction of a new class CommDivisionRing a sane way to do this (to demonstrate with an example that a commutative ring that also functions as a division ring is, in fact, a field), or is there an alternative method that would be more idiomatic?

[Damiano Testa]

If you are trying to show what implications there are among the various typeclasses, I would say that this is a good way to show how things work.

[Damiano Testa]

If you were building a mathematical library, I would suggest thinking really hard about whether there is any advantage to introducing a new typeclass that is "the same" as an existing one.

[Damiano Testa]

Wrt the proof that I suggested and the one found by hint, I think that there is pedagogical value in both.

[Damiano Testa]

The one that I suggested basically tells you that the fields of Field are all contained among the fields of CommDivisionRing.

[Damiano Testa]

The one found by hint leverages the typeclass system to find a proof and actually has some mathematical content, since the implication (Artinian + domain => Field) is not just moving around axioms (inasmuch as some tautologies are less obvious than others).

[Isak Colboubrani]

@Damiano Testa Yes, to clarify: these examples are solely for demonstration purposes. I consider them analogous to the summaries a student might jot down during a lecture, but written in Lean using Mathlib instead of on paper, to illustrate how concepts might look when formalized.

[Kevin Buzzard]

Don't we have something like docs#Commute ?

You can tell if something is data-carrying by hovering over it and seeing if it's a Type or a Prop. If I had my way you'd also be able to tell by seeing if the name begins with Is or not, but this is less reliable right now.

[Kevin Buzzard]

Oh hmm, Commute is not a typeclass. I would just go for DivisionRing and then add the hypothesis that \forall a b, a * b = b * a.

[Ruben Van de Velde]

Isn't that a field?

[Ruben Van de Velde]

Oh, that's what you're showing