# Documentation

Mathlib.ModelTheory.Algebra.Ring.Basic

# 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.

• mul:
• neg:
• zero:
• one:

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

Instances For

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

Instances For
@[inline, reducible]

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

Instances For
@[inline, reducible]

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

Instances For
@[inline, reducible]

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

Instances For
@[inline, reducible]

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

Instances For
@[inline, reducible]

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

Instances For
theorem FirstOrder.Ring.one_def (α : Type u_2) :
theorem FirstOrder.Ring.add_def (α : Type u_2) :
theorem FirstOrder.Ring.mul_def (α : Type u_2) :
@[simp]
class FirstOrder.Ring.CompatibleRing (R : Type u_2) [Add R] [Mul R] [Neg R] [One R] [Zero R] extends :
Type u_2
• funMap : {n : } → (Fin nR) → R
• RelMap : {n : } → (Fin nR) → Prop
• funMap_add : ∀ (x : Fin 2R),

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

• funMap_mul : ∀ (x : Fin 2R),

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

• funMap_neg : ∀ (x : Fin 1R),

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

• funMap_zero : ∀ (x : Fin 0R),

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

• funMap_one : ∀ (x : Fin 0R),

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

Instances
@[simp]
theorem FirstOrder.Ring.realize_add {α : Type u_1} {R : Type u_2} [Add R] [Mul R] [Neg R] [One R] [Zero R] (v : αR) :
@[simp]
theorem FirstOrder.Ring.realize_mul {α : Type u_1} {R : Type u_2} [Add R] [Mul R] [Neg R] [One R] [Zero R] (v : αR) :
@[simp]
theorem FirstOrder.Ring.realize_neg {α : Type u_1} {R : Type u_2} [Add R] [Mul R] [Neg R] [One R] [Zero R] (v : αR) :
@[simp]
theorem FirstOrder.Ring.realize_zero {α : Type u_1} {R : Type u_2} [Add R] [Mul R] [Neg R] [One R] [Zero R] (v : αR) :
@[simp]
theorem FirstOrder.Ring.realize_one {α : Type u_1} {R : Type u_2} [Add R] [Mul R] [Neg R] [One R] [Zero R] (v : αR) :
def FirstOrder.Ring.compatibleRingOfRing (R : Type u_2) [Add R] [Mul R] [Neg R] [One R] [Zero 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

Instances For
def FirstOrder.Ring.languageEquivEquivRingEquiv {R : Type u_2} {S : Type u_3} [] [] :

An isomorphism in the language of rings is a ring isomorphism

Instances For
@[reducible]

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

Instances For
@[reducible]

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

Instances For
@[reducible]

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

Instances For
@[reducible]

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

Instances For
@[reducible]

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

Instances For
@[reducible]

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.

Instances For