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 aLanguage.ring.Structure
, and that this structure is the same as the structure given by the classesAdd
,Mul
, etc. already onR
.FirstOrder.Ring.compatibleRingOfRing
: Given a typeR
with instances for each of theRing
operations, make acompatibleRing
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.
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
Instances For
Equations
- FirstOrder.instDecidableEqRingFunc = FirstOrder.decEqringFunc✝
The language of rings contains the operations (+,*,-,0,1)
Equations
- FirstOrder.Language.ring = { Functions := FirstOrder.ringFunc, Relations := fun (x : ℕ) => Empty }
Instances For
RingFunc.add
, but with the defeq type Language.ring.Functions 2
instead
of RingFunc 2
Instances For
RingFunc.mul
, but with the defeq type Language.ring.Functions 2
instead
of RingFunc 2
Instances For
RingFunc.neg
, but with the defeq type Language.ring.Functions 1
instead
of RingFunc 1
Instances For
RingFunc.zero
, but with the defeq type Language.ring.Functions 0
instead
of RingFunc 0
Instances For
RingFunc.one
, but with the defeq type Language.ring.Functions 0
instead
of RingFunc 0
Instances For
Equations
Equations
Equations
- FirstOrder.Ring.instAddTermRing α = { add := FirstOrder.Ring.addFunc.apply₂ }
Equations
- FirstOrder.Ring.instMulTermRing α = { mul := FirstOrder.Ring.mulFunc.apply₂ }
Equations
- FirstOrder.Ring.instNegTermRing α = { neg := FirstOrder.Ring.negFunc.apply₁ }
Equations
- One or more equations did not get rendered due to their size.
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 theAdd
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 theMul
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 theNeg
instance - funMap_zero : ∀ (x : Fin 0 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.zeroFunc x = 0
The constant
0
in theLanguage.ring.Structure
is the same as the constant given by theZero
instance - funMap_one : ∀ (x : Fin 0 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.oneFunc x = 1
The constant
1
in theLanguage.ring.Structure
is the same as the constant given by theOne
instance
Instances
Addition in the Language.ring.Structure
is the same as the addition given by the
Add
instance
Multiplication in the Language.ring.Structure
is the same as the multiplication given by the
Mul
instance
Negation in the Language.ring.Structure
is the same as the negation given by the
Neg
instance
The constant 0
in the Language.ring.Structure
is the same as the constant given by the
Zero
instance
The constant 1
in the Language.ring.Structure
is the same as the constant given by the
One
instance
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
Instances For
An isomorphism in the language of rings is a ring isomorphism
Equations
- One or more equations did not get rendered due to their size.
Instances For
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] }
Instances For
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] }
Instances For
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] }
Instances For
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
Instances For
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
Instances For
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.