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
    Equations
    • FirstOrder.instDecidableEqRingFunc = FirstOrder.decEqringFunc✝

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

    Equations
    Instances For
      @[reducible, inline]

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

      Equations
      Instances For
        @[reducible, inline]

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

        Equations
        Instances For
          @[reducible, inline]

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

          Equations
          Instances For
            @[reducible, inline]

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

            Equations
            Instances For
              @[reducible, inline]

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

              Equations
              Instances For
                theorem FirstOrder.Ring.add_def (α : Type u_2) (t₁ : FirstOrder.Language.ring.Term α) (t₂ : FirstOrder.Language.ring.Term α) :
                t₁ + t₂ = FirstOrder.Ring.addFunc.apply₂ t₁ t₂
                theorem FirstOrder.Ring.mul_def (α : Type u_2) (t₁ : FirstOrder.Language.ring.Term α) (t₂ : FirstOrder.Language.ring.Term α) :
                t₁ * t₂ = FirstOrder.Ring.mulFunc.apply₂ t₁ t₂
                Equations
                • One or more equations did not get rendered due to their size.
                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.CompatibleRing.funMap_add {R : Type u_2} :
                  ∀ {inst : Add R} {inst_1 : Mul R} {inst_2 : Neg R} {inst_3 : One R} {inst_4 : Zero R} [self : FirstOrder.Ring.CompatibleRing R] (x : Fin 2R), 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

                  @[simp]
                  theorem FirstOrder.Ring.CompatibleRing.funMap_mul {R : Type u_2} :
                  ∀ {inst : Add R} {inst_1 : Mul R} {inst_2 : Neg R} {inst_3 : One R} {inst_4 : Zero R} [self : FirstOrder.Ring.CompatibleRing R] (x : Fin 2R), 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

                  @[simp]
                  theorem FirstOrder.Ring.CompatibleRing.funMap_neg {R : Type u_2} :
                  ∀ {inst : Add R} {inst_1 : Mul R} {inst_2 : Neg R} {inst_3 : One R} {inst_4 : Zero R} [self : FirstOrder.Ring.CompatibleRing R] (x : Fin 1R), 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

                  @[simp]
                  theorem FirstOrder.Ring.CompatibleRing.funMap_zero {R : Type u_2} :
                  ∀ {inst : Add R} {inst_1 : Mul R} {inst_2 : Neg R} {inst_3 : One R} {inst_4 : Zero R} [self : FirstOrder.Ring.CompatibleRing R] (x : Fin 0R), 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

                  @[simp]
                  theorem FirstOrder.Ring.CompatibleRing.funMap_one {R : Type u_2} :
                  ∀ {inst : Add R} {inst_1 : Mul R} {inst_2 : Neg R} {inst_3 : One R} {inst_4 : Zero R} [self : FirstOrder.Ring.CompatibleRing R] (x : Fin 0R), 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_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

                  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
                      @[reducible, inline]

                      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
                      Instances For
                        @[reducible, inline]

                        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
                        Instances For
                          @[reducible, inline]

                          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
                          Instances For
                            @[reducible, inline]

                            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
                              @[reducible, inline]

                              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
                                @[reducible, inline]

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