The First Order Theory of Fields

This file defines the first order theory of fields as a theory over the language of rings.

Main definitions

• FirstOrder.Language.Theory.field : the theory of fields
• FirstOrder.Model.fieldOfModelField : a model of the theory of fields on a type K that already has ring operations.
• FirstOrder.Model.compatibleRingOfModelField : shows that the ring operations on K given by fieldOfModelField are compatible with the ring operations on K given by the Language.ring.Structure instance.

inductive FirstOrder.Field.FieldAxiom : Type

An indexing type to name each of the field axioms. The theory of fields is defined as the range of a function FieldAxiom -> Language.ring.Sentence

• addAssoc: FirstOrder.Field.FieldAxiom
• zeroAdd: FirstOrder.Field.FieldAxiom
• negAddCancel: FirstOrder.Field.FieldAxiom
• mulAssoc: FirstOrder.Field.FieldAxiom
• mulComm: FirstOrder.Field.FieldAxiom
• oneMul: FirstOrder.Field.FieldAxiom
• existsInv: FirstOrder.Field.FieldAxiom
• leftDistrib: FirstOrder.Field.FieldAxiom
• existsPairNE: FirstOrder.Field.FieldAxiom

def FirstOrder.Field.FieldAxiom.toSentence : FirstOrder.Field.FieldAxiom → FirstOrder.Language.ring.Sentence

The first order sentence corresponding to each field axiom

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Field.FieldAxiom.zeroAdd.toSentence = ((0 + (FirstOrder.Language.var ∘ Sum.inr) 0).bdEqual ((FirstOrder.Language.var ∘ Sum.inr) 0)).all
• FirstOrder.Field.FieldAxiom.negAddCancel.toSentence = ((-(FirstOrder.Language.var ∘ Sum.inr) 0 + (FirstOrder.Language.var ∘ Sum.inr) 0).bdEqual 0).all.all
• FirstOrder.Field.FieldAxiom.oneMul.toSentence = ((1 * (FirstOrder.Language.var ∘ Sum.inr) 0).bdEqual ((FirstOrder.Language.var ∘ Sum.inr) 0)).all
• FirstOrder.Field.FieldAxiom.existsPairNE.toSentence = (((FirstOrder.Language.var ∘ Sum.inr) 0).bdEqual ((FirstOrder.Language.var ∘ Sum.inr) 1)).not.ex.ex

def FirstOrder.Field.FieldAxiom.toProp (K : Type u_2) [Add K] [Mul K] [Neg K] [Zero K] [One K] : FirstOrder.Field.FieldAxiom → Prop

The Proposition corresponding to each field axiom

Equations

• FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.addAssoc = ∀ (x y z : K), x + y + z = x + (y + z)
• FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.zeroAdd = ∀ (x : K), 0 + x = x
• FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.negAddCancel = ∀ (x : K), -x + x = 0
• FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.mulAssoc = ∀ (x y z : K), x * y * z = x * (y * z)
• FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.mulComm = ∀ (x y : K), x * y = y * x
• FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.oneMul = ∀ (x : K), 1 * x = x
• FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.existsInv = ∀ (x : K), x ≠ 0 → ∃ (y : K), x * y = 1
• FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.leftDistrib = ∀ (x y z : K), x * (y + z) = x * y + x * z
• FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.existsPairNE = ∃ (x : K) (y : K), x ≠ y

def FirstOrder.Language.Theory.field : FirstOrder.Language.ring.Theory

The first order theory of fields, as a theory over the language of rings

Equations

• FirstOrder.Language.Theory.field = Set.range FirstOrder.Field.FieldAxiom.toSentence

theorem FirstOrder.Field.FieldAxiom.realize_toSentence_iff_toProp {K : Type u_2} [Add K] [Mul K] [Neg K] [Zero K] [One K] [FirstOrder.Ring.CompatibleRing K] (ax : FirstOrder.Field.FieldAxiom) : K ⊨ ax.toSentence ↔ FirstOrder.Field.FieldAxiom.toProp K ax

theorem FirstOrder.Field.FieldAxiom.toProp_of_model {K : Type u_2} [Add K] [Mul K] [Neg K] [Zero K] [One K] [FirstOrder.Ring.CompatibleRing K] [K ⊨ FirstOrder.Language.Theory.field] (ax : FirstOrder.Field.FieldAxiom) : FirstOrder.Field.FieldAxiom.toProp K ax

@[reducible, inline]

noncomputable abbrev FirstOrder.Field.fieldOfModelField (K : Type u_2) [FirstOrder.Language.ring.Structure K] [K ⊨ FirstOrder.Language.Theory.field] : Field K

A model for the theory of fields is a field. To introduced locally on Types that don't already have instances for ring operations.

When this is used, it is almost always useful to also add locally the instance compatibleFieldOfModelField afterwards.

Equations

• FirstOrder.Field.fieldOfModelField K = Field.ofMinimalAxioms K ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

noncomputable abbrev FirstOrder.Field.compatibleRingOfModelField (K : Type u_2) [FirstOrder.Language.ring.Structure K] [K ⊨ FirstOrder.Language.Theory.field] : FirstOrder.Ring.CompatibleRing K

The instances given by fieldOfModelField are compatible with the Language.ring.Structure instance on K. This instance is to be used on models for the language of fields that do not already have the ring operations on the Type.

Always add fieldOfModelField as a local instance first before using this instance.

Equations

• FirstOrder.Field.compatibleRingOfModelField K = FirstOrder.Ring.compatibleRingOfRingStructure K

instance FirstOrder.Field.instModelField {K : Type u_1} [Field K] [FirstOrder.Ring.CompatibleRing K] : K ⊨ FirstOrder.Language.Theory.field

Equations

• ⋯ = ⋯