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 fieldsFirstOrder.Model.fieldOfModelField
: a model of the theory of fields on a typeK
that already has ring operations.FirstOrder.Model.compatibleRingOfModelField
: shows that the ring operations onK
given byfieldOfModelField
are compatible with the ring operations onK
given by theLanguage.ring.Structure
instance.
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
Instances For
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
Instances For
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
Instances For
The first order theory of fields, as a theory over the language of rings
Instances For
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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
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.