Mathlib.Algebra.Field.IsField

Module docstring

{"# IsField predicate

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. "}

IsField structure

(R : Type u) [Semiring R]

Full source

/-- A predicate to express that a (semi)ring is a (semi)field.

This is mainly useful because such a predicate does not contain data,
and can therefore be easily transported along ring isomorphisms.
Additionally, this is useful when trying to prove that
a particular ring structure extends to a (semi)field. -/
structure IsField (R : Type u) [Semiring R] : Prop where
  /-- For a semiring to be a field, it must have two distinct elements. -/
  exists_pair_ne : ∃ x y : R, x ≠ y
  /-- Fields are commutative. -/
  mul_comm : ∀ x y : R, x * y = y * x
  /-- Nonzero elements have multiplicative inverses. -/
  mul_inv_cancel : ∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1

(Semi)Field Predicate

Informal description

A predicate on a (semi)ring $R$ stating that it is a (semi)field, meaning that the multiplication is commutative, there exists more than one element, and every nonzero element has a multiplicative inverse. Unlike the structure `Field`, which includes an explicit inverse function, this predicate only asserts the existence of inverses, making it more flexible for transferring properties along ring isomorphisms or proving extensions to (semi)fields.

Semifield.toIsField theorem

(R : Type u) [Semifield R] : IsField R

Full source

/-- Transferring from `Semifield` to `IsField`. -/
theorem Semifield.toIsField (R : Type u) [Semifield R] : IsField R where
  __ := ‹Semifield R›
  mul_inv_cancel {a} ha := ⟨a⁻¹, mul_inv_cancel₀ ha⟩

Semifields are IsField structures

Informal description

Every semifield $R$ satisfies the `IsField` predicate, meaning that $R$ has commutative multiplication, contains more than one element, and every nonzero element has a multiplicative inverse.

Field.toIsField theorem

(R : Type u) [Field R] : IsField R

Full source

/-- Transferring from `Field` to `IsField`. -/
theorem Field.toIsField (R : Type u) [Field R] : IsField R :=
  Semifield.toIsField _

Fields satisfy the IsField predicate

Informal description

Every field $R$ satisfies the `IsField` predicate, meaning that $R$ has commutative multiplication, contains more than one element, and every nonzero element has a multiplicative inverse.

IsField.nontrivial theorem

{R : Type u} [Semiring R] (h : IsField R) : Nontrivial R

Full source

@[simp]
theorem IsField.nontrivial {R : Type u} [Semiring R] (h : IsField R) : Nontrivial R :=
  ⟨h.exists_pair_ne⟩

Nontriviality of Semifields

Informal description

If a semiring $R$ satisfies the `IsField` predicate (i.e., it is a semifield), then $R$ is nontrivial (contains at least two distinct elements).

not_isField_of_subsingleton theorem

(R : Type u) [Semiring R] [Subsingleton R] : ¬IsField R

Full source

@[simp]
theorem not_isField_of_subsingleton (R : Type u) [Semiring R] [Subsingleton R] : ¬IsField R :=
  fun h =>
  let ⟨_, _, h⟩ := h.exists_pair_ne
  h (Subsingleton.elim _ _)

Subsingleton Semirings Are Not Fields

Informal description

If a semiring $R$ is a subsingleton (i.e., has at most one element), then $R$ does not satisfy the `IsField` predicate.

IsField.toSemifield definition

{R : Type u} [Semiring R] (h : IsField R) : Semifield R

Full source

/-- Transferring from `IsField` to `Semifield`. -/
noncomputable def IsField.toSemifield {R : Type u} [Semiring R] (h : IsField R) : Semifield R where
  __ := ‹Semiring R›
  __ := h
  inv a := if ha : a = 0 then 0 else Classical.choose (h.mul_inv_cancel ha)
  inv_zero := dif_pos rfl
  mul_inv_cancel a ha := by convert Classical.choose_spec (h.mul_inv_cancel ha); exact dif_neg ha
  nnqsmul := _
  nnqsmul_def _ _ := rfl

Semifield structure from IsField predicate

Informal description

Given a semiring $ R $ that satisfies the `IsField` predicate (i.e., $ R $ is a semifield), this definition constructs a `Semifield` structure on $ R $. The multiplicative inverse function is defined as follows: for any $ a \in R $, if $ a = 0 $, then the inverse is $ 0 $; otherwise, the inverse is the unique element $ y $ such that $ a \cdot y = 1 $, whose existence is guaranteed by the `IsField` predicate. The definition also ensures that the inverse of zero is zero and that the inverse satisfies the multiplicative inverse property for nonzero elements.

IsField.toField definition

{R : Type u} [Ring R] (h : IsField R) : Field R

Full source

/-- Transferring from `IsField` to `Field`. -/
noncomputable def IsField.toField {R : Type u} [Ring R] (h : IsField R) : Field R where
  __ := (‹Ring R›:) -- this also works without the `( :)`, but it's slow
  __ := h.toSemifield
  qsmul := _
  qsmul_def := fun _ _ => rfl

Field structure from IsField predicate

Informal description

Given a ring $ R $ that satisfies the `IsField` predicate (i.e., $ R $ is a field), this definition constructs a `Field` structure on $ R $. The multiplicative inverse function is defined as follows: for any $ a \in R $, if $ a = 0 $, then the inverse is $ 0 $; otherwise, the inverse is the unique element $ y $ such that $ a \cdot y = 1 $, whose existence is guaranteed by the `IsField` predicate. The definition also ensures that the inverse of zero is zero and that the inverse satisfies the multiplicative inverse property for nonzero elements.

uniq_inv_of_isField theorem

(R : Type u) [Ring R] (hf : IsField R) : ∀ x : R, x ≠ 0 → ∃! y : R, x * y = 1

Full source

/-- For each field, and for each nonzero element of said field, there is a unique inverse.
Since `IsField` doesn't remember the data of an `inv` function and as such,
a lemma that there is a unique inverse could be useful.
-/
theorem uniq_inv_of_isField (R : Type u) [Ring R] (hf : IsField R) :
    ∀ x : R, x ≠ 0 → ∃! y : R, x * y = 1 := by
  intro x hx
  apply existsUnique_of_exists_of_unique
  · exact hf.mul_inv_cancel hx
  · intro y z hxy hxz
    calc
      y = y * (x * z) := by rw [hxz, mul_one]
      _ = x * y * z := by rw [← mul_assoc, hf.mul_comm y x]
      _ = z := by rw [hxy, one_mul]

Unique Existence of Multiplicative Inverse in a Field

Informal description

For any ring $R$ that satisfies the `IsField` predicate and any nonzero element $x \in R$, there exists a unique element $y \in R$ such that $x \cdot y = 1$.