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

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

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

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

Equations

• FirstOrder.instDecidableEqRingFunc = FirstOrder.decEqringFunc✝

def FirstOrder.Language.ring : FirstOrder.Language

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

Equations

• FirstOrder.Language.ring = { Functions := FirstOrder.ringFunc, Relations := fun (x : ℕ) => Empty }

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

Equations

• FirstOrder.Ring.instDecidableEqFunctionsRing n = id inferInstance

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

Equations

• FirstOrder.Ring.instDecidableEqRelationsRing n = id inferInstance

@[inline, reducible]

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

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

Equations

• FirstOrder.Ring.addFunc = FirstOrder.ringFunc.add

@[inline, reducible]

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

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

Equations

• FirstOrder.Ring.mulFunc = FirstOrder.ringFunc.mul

@[inline, reducible]

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

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

Equations

• FirstOrder.Ring.negFunc = FirstOrder.ringFunc.neg

@[inline, reducible]

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

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

Equations

• FirstOrder.Ring.zeroFunc = FirstOrder.ringFunc.zero

@[inline, reducible]

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

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

Equations

• FirstOrder.Ring.oneFunc = FirstOrder.ringFunc.one

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

Equations

• FirstOrder.Ring.instZeroTermRing α = { zero := FirstOrder.Language.Constants.term FirstOrder.Ring.zeroFunc }

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 α)

Equations

• FirstOrder.Ring.instOneTermRing α = { one := FirstOrder.Language.Constants.term FirstOrder.Ring.oneFunc }

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 α)

Equations

• FirstOrder.Ring.instAddTermRing α = { add := FirstOrder.Language.Functions.apply₂ FirstOrder.Ring.addFunc }

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 α)

Equations

• FirstOrder.Ring.instMulTermRing α = { mul := FirstOrder.Language.Functions.apply₂ FirstOrder.Ring.mulFunc }

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 α)

Equations

• FirstOrder.Ring.instNegTermRing α = { neg := FirstOrder.Language.Functions.apply₁ FirstOrder.Ring.negFunc }

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)

Equations

• One or more equations did not get rendered due to their size.

@[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

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

• funMap : {n : ℕ} → FirstOrder.Language.ring.Functions n → (Fin n → R) → R
• RelMap : {n : ℕ} → FirstOrder.Language.ring.Relations 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

@[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

Equations

• FirstOrder.Ring.compatibleRingOfRing R = FirstOrder.Ring.CompatibleRing.mk ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• One or more equations did not get rendered due to their size.

@[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

Equations

• FirstOrder.Ring.addOfRingStructure R = { add := fun (x y : R) => FirstOrder.Language.Structure.funMap FirstOrder.Ring.addFunc ![x, y] }

@[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

Equations

• FirstOrder.Ring.mulOfRingStructure R = { mul := fun (x y : R) => FirstOrder.Language.Structure.funMap FirstOrder.Ring.mulFunc ![x, y] }

@[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

Equations

• FirstOrder.Ring.negOfRingStructure R = { neg := fun (x : R) => FirstOrder.Language.Structure.funMap FirstOrder.Ring.negFunc ![x] }

@[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

Equations

• FirstOrder.Ring.zeroOfRingStructure R = { zero := FirstOrder.Language.Structure.funMap FirstOrder.Ring.zeroFunc ![] }

@[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

Equations

• FirstOrder.Ring.oneOfRingStructure R = { one := FirstOrder.Language.Structure.funMap FirstOrder.Ring.oneFunc ![] }

@[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.

Equations

• FirstOrder.Ring.compatibleRingOfRingStructure R = FirstOrder.Ring.CompatibleRing.mk ⋯ ⋯ ⋯ ⋯ ⋯