First Order Language of Rings

This file defines the first order language of rings, as well as defining instance of Add, Mul, etc. on terms in the language.

Main Definitions

• FirstOrder.Language.ring : the language of rings, with function symbols +, *, -, 0, 1
• FirstOrder.Ring.CompatibleRing : A class stating that a type is a Language.ring.Structure, and that this structure is the same as the structure given by the classes Add, Mul, etc. already on R.
• FirstOrder.Ring.compatibleRingOfRing : Given a type R with instances for each of the Ring operations, make a compatibleRing instance.

Implementation Notes

There are implementation difficulties with the model theory of rings caused by the fact that there are two different ways to say that R is a Ring. We can say Ring R or Language.ring.Structure R and Theory.ring.Model R (The theory of rings is not implemented yet).

The recommended way to use this library is to use the hypotheses CompatibleRing R and Ring R on any theorem that requires both a Ring instance and a Language.ring.Structure instance in order to state the theorem. To apply such a theorem to a ring R with a Ring instance, use the tactic let _ := compatibleRingOfRing R. To apply the theorem to K a Language.ring.Structure K instance and for example an instance of Theory.field.Model K, you must add local instances with definitions like ModelTheory.Field.fieldOfModelField K and FirstOrder.Ring.compatibleRingOfModelField K. (in Mathlib/ModelTheory/Algebra/Field/Basic.lean), depending on the Theory.

inductive FirstOrder.ringFunc : ℕ → Type

• add: FirstOrder.ringFunc 2
• mul: FirstOrder.ringFunc 2
• neg: FirstOrder.ringFunc 1
• zero: FirstOrder.ringFunc 0
• one: FirstOrder.ringFunc 0

The type of Ring functions, to be used in the definition of the language of rings. It contains the operations (+,*,-,0,1)

instance FirstOrder.instDecidableEqRingFunc : {a : ℕ} → DecidableEq (FirstOrder.ringFunc a)

def FirstOrder.Language.ring : FirstOrder.Language

The language of rings contains the operations (+,*,-,0,1)

instance FirstOrder.Ring.instDecidableEqFunctionsRing (n : ℕ) : DecidableEq (FirstOrder.Language.Functions FirstOrder.Language.ring n)

instance FirstOrder.Ring.instDecidableEqRelationsRing (n : ℕ) : DecidableEq (FirstOrder.Language.Relations FirstOrder.Language.ring n)

@[inline, reducible]

abbrev FirstOrder.Ring.addFunc : FirstOrder.Language.Functions FirstOrder.Language.ring 2

RingFunc.add, but with the defeq type Language.ring.Functions 2 instead of RingFunc 2

@[inline, reducible]

abbrev FirstOrder.Ring.mulFunc : FirstOrder.Language.Functions FirstOrder.Language.ring 2

RingFunc.mul, but with the defeq type Language.ring.Functions 2 instead of RingFunc 2

@[inline, reducible]

abbrev FirstOrder.Ring.negFunc : FirstOrder.Language.Functions FirstOrder.Language.ring 1

RingFunc.neg, but with the defeq type Language.ring.Functions 1 instead of RingFunc 1

@[inline, reducible]

abbrev FirstOrder.Ring.zeroFunc : FirstOrder.Language.Functions FirstOrder.Language.ring 0

RingFunc.zero, but with the defeq type Language.ring.Functions 0 instead of RingFunc 0

@[inline, reducible]

abbrev FirstOrder.Ring.oneFunc : FirstOrder.Language.Functions FirstOrder.Language.ring 0

RingFunc.one, but with the defeq type Language.ring.Functions 0 instead of RingFunc 0

instance FirstOrder.Ring.instZeroTermRing (α : Type u_2) : Zero (FirstOrder.Language.Term FirstOrder.Language.ring α)

theorem FirstOrder.Ring.zero_def (α : Type u_2) : 0 = FirstOrder.Language.Constants.term FirstOrder.Ring.zeroFunc

instance FirstOrder.Ring.instOneTermRing (α : Type u_2) : One (FirstOrder.Language.Term FirstOrder.Language.ring α)

theorem FirstOrder.Ring.one_def (α : Type u_2) : 1 = FirstOrder.Language.Constants.term FirstOrder.Ring.oneFunc

instance FirstOrder.Ring.instAddTermRing (α : Type u_2) : Add (FirstOrder.Language.Term FirstOrder.Language.ring α)

theorem FirstOrder.Ring.add_def (α : Type u_2) (t₁ : FirstOrder.Language.Term FirstOrder.Language.ring α) (t₂ : FirstOrder.Language.Term FirstOrder.Language.ring α) : t₁ + t₂ = FirstOrder.Language.Functions.apply₂ FirstOrder.Ring.addFunc t₁ t₂

instance FirstOrder.Ring.instMulTermRing (α : Type u_2) : Mul (FirstOrder.Language.Term FirstOrder.Language.ring α)

theorem FirstOrder.Ring.mul_def (α : Type u_2) (t₁ : FirstOrder.Language.Term FirstOrder.Language.ring α) (t₂ : FirstOrder.Language.Term FirstOrder.Language.ring α) : t₁ * t₂ = FirstOrder.Language.Functions.apply₂ FirstOrder.Ring.mulFunc t₁ t₂

instance FirstOrder.Ring.instNegTermRing (α : Type u_2) : Neg (FirstOrder.Language.Term FirstOrder.Language.ring α)

theorem FirstOrder.Ring.neg_def (α : Type u_2) (t : FirstOrder.Language.Term FirstOrder.Language.ring α) : -t = FirstOrder.Language.Functions.apply₁ FirstOrder.Ring.negFunc t

instance FirstOrder.Ring.instFintypeSymbolsRing : Fintype (FirstOrder.Language.Symbols FirstOrder.Language.ring)

@[simp]

theorem FirstOrder.Ring.card_ring : FirstOrder.Language.card FirstOrder.Language.ring = 5

class FirstOrder.Ring.CompatibleRing (R : Type u_2) [Add R] [Mul R] [Neg R] [One R] [Zero R] extends FirstOrder.Language.Structure : Type u_2

• funMap : {n : ℕ} → FirstOrder.Language.Functions FirstOrder.Language.ring n → (Fin n → R) → R
• RelMap : {n : ℕ} → FirstOrder.Language.Relations FirstOrder.Language.ring n → (Fin n → R) → Prop
• funMap_add : ∀ (x : Fin 2 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.addFunc x = x 0 + x 1

  Addition in the Language.ring.Structure is the same as the addition given by the Add instance

• funMap_mul : ∀ (x : Fin 2 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.mulFunc x = x 0 * x 1

  Multiplication in the Language.ring.Structure is the same as the multiplication given by the Mul instance

• funMap_neg : ∀ (x : Fin 1 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.negFunc x = -x 0

  Negation in the Language.ring.Structure is the same as the negation given by the Neg instance

• funMap_zero : ∀ (x : Fin 0 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.zeroFunc x = 0

  The constant 0 in the Language.ring.Structure is the same as the constant given by the Zero instance

• funMap_one : ∀ (x : Fin 0 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.oneFunc x = 1

  The constant 1 in the Language.ring.Structure is the same as the constant given by the One instance

A Type R is a CompatibleRing if it is a structure for the language of rings and this structure is the same as the structure already given on R by the classes Add, Mul etc.

It is recommended to use this type class as a hypothesis to any theorem whose statement requires a type to have be both a Ring (or Field etc.) and a Language.ring.Structure

@[simp]

theorem FirstOrder.Ring.realize_add {α : Type u_1} {R : Type u_2} [Add R] [Mul R] [Neg R] [One R] [Zero R] [FirstOrder.Ring.CompatibleRing R] (x : FirstOrder.Language.Term FirstOrder.Language.ring α) (y : FirstOrder.Language.Term FirstOrder.Language.ring α) (v : α → R) : FirstOrder.Language.Term.realize v (x + y) = FirstOrder.Language.Term.realize v x + FirstOrder.Language.Term.realize v y

@[simp]

theorem FirstOrder.Ring.realize_mul {α : Type u_1} {R : Type u_2} [Add R] [Mul R] [Neg R] [One R] [Zero R] [FirstOrder.Ring.CompatibleRing R] (x : FirstOrder.Language.Term FirstOrder.Language.ring α) (y : FirstOrder.Language.Term FirstOrder.Language.ring α) (v : α → R) : FirstOrder.Language.Term.realize v (x * y) = FirstOrder.Language.Term.realize v x * FirstOrder.Language.Term.realize v y

@[simp]

theorem FirstOrder.Ring.realize_neg {α : Type u_1} {R : Type u_2} [Add R] [Mul R] [Neg R] [One R] [Zero R] [FirstOrder.Ring.CompatibleRing R] (x : FirstOrder.Language.Term FirstOrder.Language.ring α) (v : α → R) : FirstOrder.Language.Term.realize v (-x) = -FirstOrder.Language.Term.realize v x

@[simp]

theorem FirstOrder.Ring.realize_zero {α : Type u_1} {R : Type u_2} [Add R] [Mul R] [Neg R] [One R] [Zero R] [FirstOrder.Ring.CompatibleRing R] (v : α → R) : FirstOrder.Language.Term.realize v 0 = 0

@[simp]

theorem FirstOrder.Ring.realize_one {α : Type u_1} {R : Type u_2} [Add R] [Mul R] [Neg R] [One R] [Zero R] [FirstOrder.Ring.CompatibleRing R] (v : α → R) : FirstOrder.Language.Term.realize v 1 = 1

def FirstOrder.Ring.compatibleRingOfRing (R : Type u_2) [Add R] [Mul R] [Neg R] [One R] [Zero R] : FirstOrder.Ring.CompatibleRing R

Given a Type R with instances for each of the Ring operations, make a Language.ring.Structure R instance, along with a proof that the operations given by the Language.ring.Structure are the same as those given by the Add or Mul etc. instances.

This definition can be used when applying a theorem about the model theory of rings to a literal ring R, by writing let _ := compatibleRingOfRing R. After this, if, for example, R is a field, then Lean will be able to find the instance for Theory.field.Model R, and it will be possible to apply theorems about the model theory of fields.

This is a def and not an instance, because the path Ring => Language.ring.Structure => Ring cannot be made to commute by definition

def FirstOrder.Ring.languageEquivEquivRingEquiv {R : Type u_2} {S : Type u_3} [NonAssocRing R] [NonAssocRing S] [FirstOrder.Ring.CompatibleRing R] [FirstOrder.Ring.CompatibleRing S] : FirstOrder.Language.Equiv FirstOrder.Language.ring R S ≃ (R ≃+* S)

An isomorphism in the language of rings is a ring isomorphism

@[reducible]

def FirstOrder.Ring.addOfRingStructure (R : Type u_2) [FirstOrder.Language.Structure FirstOrder.Language.ring R] : Add R

A def to put an Add instance on a type with a Language.ring.Structure instance.

To be used sparingly, usually only when defining a more useful definition like, [Language.ring.Structure K] -> [Theory.field.Model K] -> Field K

@[reducible]

def FirstOrder.Ring.mulOfRingStructure (R : Type u_2) [FirstOrder.Language.Structure FirstOrder.Language.ring R] : Mul R

A def to put an Mul instance on a type with a Language.ring.Structure instance.

To be used sparingly, usually only when defining a more useful definition like, [Language.ring.Structure K] -> [Theory.field.Model K] -> Field K

@[reducible]

def FirstOrder.Ring.negOfRingStructure (R : Type u_2) [FirstOrder.Language.Structure FirstOrder.Language.ring R] : Neg R

A def to put an Neg instance on a type with a Language.ring.Structure instance.

To be used sparingly, usually only when defining a more useful definition like, [Language.ring.Structure K] -> [Theory.field.Model K] -> Field K

@[reducible]

def FirstOrder.Ring.zeroOfRingStructure (R : Type u_2) [FirstOrder.Language.Structure FirstOrder.Language.ring R] : Zero R

A def to put an Zero instance on a type with a Language.ring.Structure instance.

To be used sparingly, usually only when defining a more useful definition like, [Language.ring.Structure K] -> [Theory.field.Model K] -> Field K

@[reducible]

def FirstOrder.Ring.oneOfRingStructure (R : Type u_2) [FirstOrder.Language.Structure FirstOrder.Language.ring R] : One R

A def to put an One instance on a type with a Language.ring.Structure instance.

To be used sparingly, usually only when defining a more useful definition like, [Language.ring.Structure K] -> [Theory.field.Model K] -> Field K

@[reducible]

def FirstOrder.Ring.compatibleRingOfRingStructure (R : Type u_2) [FirstOrder.Language.Structure FirstOrder.Language.ring R] : FirstOrder.Ring.CompatibleRing R

Given a Type R with a Language.ring.Structure R, the instance given by addOfRingStructure etc are compatible with the Language.ring.Structure instance on R.

This definition is only to be used when addOfRingStructure, mulOfRingStructure etc are local instances.