Mathlib.Algebra.Field.Defs

Module docstring

{"# Division (semi)rings and (semi)fields

This file introduces fields and division rings (also known as skewfields) and proves some basic statements about them. For a more extensive theory of fields, see the FieldTheory folder.

Main definitions

DivisionSemiring: Nontrivial semiring with multiplicative inverses for nonzero elements.
DivisionRing: Nontrivial ring with multiplicative inverses for nonzero elements.
Semifield: Commutative division semiring.
Field: Commutative division ring.
IsField: Predicate on a (semi)ring that it is a (semi)field, i.e. that the multiplication is commutative, that it has more than one element and that all non-zero elements have a multiplicative inverse. In contrast to Field, which contains the data of a function associating to an element of the field its multiplicative inverse, this predicate only assumes the existence and can therefore more easily be used to e.g. transfer along ring isomorphisms.

Implementation details

By convention 0⁻¹ = 0 in a field or division ring. This is due to the fact that working with total functions has the advantage of not constantly having to check that x ≠ 0 when writing x⁻¹. With this convention in place, some statements like (a + b) * c⁻¹ = a * c⁻¹ + b * c⁻¹ still remain true, while others like the defining property a * a⁻¹ = 1 need the assumption a ≠ 0. If you are a beginner in using Lean and are confused by that, you can read more about why this convention is taken in Kevin Buzzard's blogpost

A division ring or field is an example of a GroupWithZero. If you cannot find a division ring / field lemma that does not involve +, you can try looking for a GroupWithZero lemma instead.

Tags

field, division ring, skew field, skew-field, skewfield "}

NNRat.castRec definition

[NatCast K] [Div K] (q : ℚ≥0) : K

Full source

/-- The default definition of the coercion `ℚ≥0 → K` for a division semiring `K`.

`↑q : K` is defined as `(q.num : K) / (q.den : K)`.

Do not use this directly (instances of `DivisionSemiring` are allowed to override that default for
better definitional properties). Instead, use the coercion. -/
def NNRat.castRec [NatCast K] [Div K] (q : ℚ≥0) : K := q.num / q.den

Canonical map from nonnegative rationals to a division semiring

Informal description

The default definition of the canonical map from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ to a division semiring $K$, where a nonnegative rational number $q$ is mapped to $(\text{num } q) / (\text{den } q)$ in $K$, with $\text{num } q$ and $\text{den } q$ being the numerator and denominator of $q$ respectively. Here, the division is performed in $K$.

Rat.castRec definition

[NatCast K] [IntCast K] [Div K] (q : ℚ) : K

Full source

/-- The default definition of the coercion `ℚ → K` for a division ring `K`.

`↑q : K` is defined as `(q.num : K) / (q.den : K)`.

Do not use this directly (instances of `DivisionRing` are allowed to override that default for
better definitional properties). Instead, use the coercion. -/
def Rat.castRec [NatCast K] [IntCast K] [Div K] (q : ℚ) : K := q.num / q.den

Canonical map from rationals to a division ring

Informal description

The default definition of the canonical map from the rational numbers $\mathbb{Q}$ to a division ring $K$, where a rational number $q$ is mapped to $(\text{num } q) / (\text{den } q)$ in $K$, with $\text{num } q$ and $\text{den } q$ being the numerator and denominator of $q$ respectively. Here, the division is performed in $K$.

DivisionSemiring structure

(K : Type*) extends Semiring K, GroupWithZero K, NNRatCast K

Full source

/-- A `DivisionSemiring` is a `Semiring` with multiplicative inverses for nonzero elements.

An instance of `DivisionSemiring K` includes maps `nnratCast : ℚ≥0 → K` and `nnqsmul : ℚ≥0 → K → K`.
Those two fields are needed to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance since we
need to control the specific definitions for some special cases of `K` (in particular `K = ℚ≥0`
itself). See also note [forgetful inheritance].

If the division semiring has positive characteristic `p`, our division by zero convention forces
`nnratCast (1 / p) = 1 / 0 = 0`. -/
class DivisionSemiring (K : Type*) extends Semiring K, GroupWithZero K, NNRatCast K where
  protected nnratCast := NNRat.castRec
  /-- However `NNRat.cast` is defined, it must be propositionally equal to `a / b`.

  Do not use this lemma directly. Use `NNRat.cast_def` instead. -/
  protected nnratCast_def (q : ℚ≥0) : (NNRat.cast q : K) = q.num / q.den := by intros; rfl
  /-- Scalar multiplication by a nonnegative rational number.

  Unless there is a risk of a `Module ℚ≥0 _` instance diamond, write `nnqsmul := _`. This will set
  `nnqsmul` to `(NNRat.cast · * ·)` thanks to unification in the default proof of `nnqsmul_def`.

  Do not use directly. Instead use the `•` notation. -/
  protected nnqsmul : ℚ≥0 → K → K
  /-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.

  Do not use this lemma directly. Use `NNRat.smul_def` instead. -/
  protected nnqsmul_def (q : ℚ≥0) (a : K) : nnqsmul q a = NNRat.cast q * a := by intros; rfl

Division Semiring

Informal description

A division semiring is a semiring $ K $ equipped with multiplicative inverses for all nonzero elements. It extends the structure of a semiring and a group with zero, and includes a canonical map from the nonnegative rationals $ \mathbb{Q}_{\geq 0} $ to $ K $. The division by zero convention is $ 0^{-1} = 0 $.

DivisionRing structure

(K : Type*)
  extends Ring K, DivInvMonoid K, Nontrivial K, NNRatCast K, RatCast K

Full source

/-- A `DivisionRing` is a `Ring` with multiplicative inverses for nonzero elements.

An instance of `DivisionRing K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance]. Similarly, there are maps `nnratCast ℚ≥0 → K` and
`nnqsmul : ℚ≥0 → K → K` to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance.

If the division ring has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`. -/
class DivisionRing (K : Type*)
  extends Ring K, DivInvMonoid K, Nontrivial K, NNRatCast K, RatCast K where
  /-- For a nonzero `a`, `a⁻¹` is a right multiplicative inverse. -/
  protected mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1
  /-- The inverse of `0` is `0` by convention. -/
  protected inv_zero : (0 : K)⁻¹ = 0
  protected nnratCast := NNRat.castRec
  /-- However `NNRat.cast` is defined, it must be equal to `a / b`.

  Do not use this lemma directly. Use `NNRat.cast_def` instead. -/
  protected nnratCast_def (q : ℚ≥0) : (NNRat.cast q : K) = q.num / q.den := by intros; rfl
  /-- Scalar multiplication by a nonnegative rational number.

  Unless there is a risk of a `Module ℚ≥0 _` instance diamond, write `nnqsmul := _`. This will set
  `nnqsmul` to `(NNRat.cast · * ·)` thanks to unification in the default proof of `nnqsmul_def`.

  Do not use directly. Instead use the `•` notation. -/
  protected nnqsmul : ℚ≥0 → K → K
  /-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.

  Do not use this lemma directly. Use `NNRat.smul_def` instead. -/
  protected nnqsmul_def (q : ℚ≥0) (a : K) : nnqsmul q a = NNRat.cast q * a := by intros; rfl
  protected ratCast := Rat.castRec
  /-- However `Rat.cast q` is defined, it must be propositionally equal to `q.num / q.den`.

  Do not use this lemma directly. Use `Rat.cast_def` instead. -/
  protected ratCast_def (q : ℚ) : (Rat.cast q : K) = q.num / q.den := by intros; rfl
  /-- Scalar multiplication by a rational number.

  Unless there is a risk of a `Module ℚ _` instance diamond, write `qsmul := _`. This will set
  `qsmul` to `(Rat.cast · * ·)` thanks to unification in the default proof of `qsmul_def`.

  Do not use directly. Instead use the `•` notation. -/
  protected qsmul : ℚ → K → K
  /-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.

  Do not use this lemma directly. Use `Rat.cast_def` instead. -/
  protected qsmul_def (a : ℚ) (x : K) : qsmul a x = Rat.cast a * x := by intros; rfl

Division Ring

Informal description

A division ring is a ring $ K $ with multiplicative inverses for all nonzero elements, i.e., for every $ x \in K $ with $ x \neq 0 $, there exists $ x^{-1} \in K $ such that $ x \cdot x^{-1} = 1 $. Additionally, it includes the structure to handle rational number casting and scalar multiplication by rational numbers, and it is required to be nontrivial (i.e., it has at least two distinct elements).

DivisionRing.toDivisionSemiring instance

[DivisionRing K] : DivisionSemiring K

Full source

instance (priority := 100) DivisionRing.toDivisionSemiring [DivisionRing K] : DivisionSemiring K :=
  { ‹DivisionRing K› with }

Division Rings as Division Semirings

Informal description

Every division ring is a division semiring.

Semifield structure

(K : Type*) extends CommSemiring K, DivisionSemiring K, CommGroupWithZero K

Full source

/-- A `Semifield` is a `CommSemiring` with multiplicative inverses for nonzero elements.

An instance of `Semifield K` includes maps `nnratCast : ℚ≥0 → K` and `nnqsmul : ℚ≥0 → K → K`.
Those two fields are needed to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance since we
need to control the specific definitions for some special cases of `K` (in particular `K = ℚ≥0`
itself). See also note [forgetful inheritance].

If the semifield has positive characteristic `p`, our division by zero convention forces
`nnratCast (1 / p) = 1 / 0 = 0`. -/
class Semifield (K : Type*) extends CommSemiring K, DivisionSemiring K, CommGroupWithZero K

Semifield

Informal description

A semifield is a commutative semiring $ K $ equipped with multiplicative inverses for all nonzero elements. This structure includes maps $ \mathbb{Q}_{\geq 0} \to K $ and $ \mathbb{Q}_{\geq 0} \times K \to K $ to handle the inheritance of algebraic structures. If $ K $ has positive characteristic $ p $, the division by zero convention implies $ (1/p) = 0 $.

Field structure

(K : Type u) extends CommRing K, DivisionRing K

Full source

/-- A `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`. -/
@[stacks 09FD "first part"]
class Field (K : Type u) extends CommRing K, DivisionRing K

Field

Informal description

A field is a commutative ring $ K $ equipped with multiplicative inverses for all nonzero elements. The structure includes maps $ \mathbb{Q} \to K $ and $ \mathbb{Q} \times K \to K $ to handle the inheritance of algebraic structures. By convention, $ 0^{-1} = 0 $. If $ K $ has positive characteristic $ p $, this convention implies $ (1/p) = 0 $.

Field.toSemifield instance

[Field K] : Semifield K

Full source

instance (priority := 100) Field.toSemifield [Field K] : Semifield K := { ‹Field K› with }

Fields are Semifields

Informal description

Every field $K$ is a semifield.

NNRat.smulDivisionSemiring instance

: SMul ℚ≥0 K

Full source

instance (priority := 100) smulDivisionSemiring : SMul ℚ≥0 K := ⟨DivisionSemiring.nnqsmul⟩

Scalar Multiplication of Nonnegative Rationals on Division Semirings

Informal description

For any division semiring $K$, there is a scalar multiplication operation $\mathbb{Q}_{\geq 0} \times K \to K$ defined by $q \cdot a = q * a$, where $q$ is a nonnegative rational number and $a$ is an element of $K$.

NNRat.cast_def theorem

(q : ℚ≥0) : (q : K) = q.num / q.den

Full source

lemma cast_def (q : ℚ≥0) : (q : K) = q.num / q.den := DivisionSemiring.nnratCast_def _

Embedding of Nonnegative Rationals via Numerator and Denominator

Informal description

For any nonnegative rational number $q$ in a division semiring $K$, the canonical embedding of $q$ into $K$ is equal to the quotient of its numerator and denominator, i.e., $q = \frac{\text{num}(q)}{\text{den}(q)}$.

NNRat.smul_def theorem

(q : ℚ≥0) (a : K) : q • a = q * a

Full source

lemma smul_def (q : ℚ≥0) (a : K) : q • a = q * a := DivisionSemiring.nnqsmul_def q a

Scalar Multiplication by Nonnegative Rationals in Division Semirings

Informal description

For any nonnegative rational number $q$ and any element $a$ in a division semiring $K$, the scalar multiplication $q \cdot a$ is equal to the product $q * a$.

NNRat.smul_one_eq_cast theorem

(q : ℚ≥0) : q • (1 : K) = q

Full source

@[simp] lemma smul_one_eq_cast (q : ℚ≥0) : q • (1 : K) = q := by rw [NNRat.smul_def, mul_one]

Scalar Multiplication of Identity by Nonnegative Rationals Equals Canonical Embedding

Informal description

For any nonnegative rational number $q$ and any division semiring $K$, the scalar multiplication of $q$ with the multiplicative identity $1_K$ equals the canonical embedding of $q$ into $K$, i.e., $q \cdot 1_K = q$.

Rat.cast_def theorem

(q : ℚ) : (q : K) = q.num / q.den

Full source

lemma cast_def (q : ℚ) : (q : K) = q.num / q.den := DivisionRing.ratCast_def _

Rational Number Cast as Fraction in Division Ring

Informal description

For any rational number $q$ and any division ring $K$, the canonical map from $\mathbb{Q}$ to $K$ satisfies $(q : K) = \frac{\text{num}(q)}{\text{den}(q)}$, where $\text{num}(q)$ and $\text{den}(q)$ are the numerator and denominator of $q$ respectively.

Rat.cast_mk' theorem

(a b h1 h2) : ((⟨a, b, h1, h2⟩ : ℚ) : K) = a / b

Full source

lemma cast_mk' (a b h1 h2) : ((⟨a, b, h1, h2⟩ : ℚ) : K) = a / b := cast_def _

Rational Cast as Fraction in Division Ring

Informal description

For any integers $a$ and $b$ with $b \neq 0$ and $\gcd(a,b) = 1$, the canonical map from the rational number $\frac{a}{b}$ to a division ring $K$ satisfies $\left(\frac{a}{b} : K\right) = \frac{a}{b}$.

Rat.smulDivisionRing instance

: SMul ℚ K

Full source

instance (priority := 100) smulDivisionRing : SMul ℚ K :=
  ⟨DivisionRing.qsmul⟩

Scalar Multiplication by Rational Numbers on a Division Ring

Informal description

For any division ring $K$, there is a scalar multiplication operation $\mathbb{Q} \times K \to K$ defined by $q \cdot x = qx$, where $qx$ is the product of the rational number $q$ interpreted as an element of $K$ and $x$.

Rat.smul_def theorem

(a : ℚ) (x : K) : a • x = ↑a * x

Full source

theorem smul_def (a : ℚ) (x : K) : a • x = ↑a * x := DivisionRing.qsmul_def a x

Scalar Multiplication by Rationals in a Division Ring Equals Cast Multiplication

Informal description

For any rational number $a$ and any element $x$ in a division ring $K$, the scalar multiplication $a \cdot x$ is equal to the product of the canonical embedding of $a$ into $K$ and $x$, i.e., $a \cdot x = a * x$.

Rat.smul_one_eq_cast theorem

(A : Type*) [DivisionRing A] (m : ℚ) : m • (1 : A) = ↑m

Full source

@[simp]
theorem smul_one_eq_cast (A : Type*) [DivisionRing A] (m : ℚ) : m • (1 : A) = ↑m := by
  rw [Rat.smul_def, mul_one]

Scalar Multiplication of Identity in Division Ring Equals Rational Cast: $m \cdot 1_A = m_A$

Informal description

For any division ring $A$ and any rational number $m$, the scalar multiplication of $m$ with the multiplicative identity $1 \in A$ equals the canonical embedding of $m$ into $A$, i.e., $m \cdot 1_A = m_A$.

Rat.ofScientific_eq_ofScientific theorem

(m : ℕ) (s : Bool) (e : ℕ) : Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) = OfScientific.ofScientific m s e

Full source

/-- `OfScientific.ofScientific` is the simp-normal form. -/
@[simp]
theorem Rat.ofScientific_eq_ofScientific (m : ℕ) (s : Bool) (e : ℕ) :
    Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) = OfScientific.ofScientific m s e := rfl

Equality of Rational Number Constructions via `Rat.ofScientific` and `OfScientific.ofScientific`

Informal description

For any natural numbers $m$ and $e$, and boolean $s$, the rational number constructed from $m$, $s$, and $e$ via `Rat.ofScientific` applied to `OfNat.ofNat` instances equals the rational number constructed via `OfScientific.ofScientific` with the same parameters.