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 #

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)

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

                Instances
                  @[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) :
                  @[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) :

                  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

                    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