Skip to content

Commit 42f80cb

Browse files
ChrisHughes24ChrisHughes24
committed
feat(ModelTheory): the language of rings (#7185)
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
1 parent fb84a08 commit 42f80cb

File tree

2 files changed

+323
-0
lines changed

2 files changed

+323
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2514,6 +2514,7 @@ import Mathlib.MeasureTheory.Measure.VectorMeasure
25142514
import Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure
25152515
import Mathlib.MeasureTheory.PiSystem
25162516
import Mathlib.MeasureTheory.Tactic
2517+
import Mathlib.ModelTheory.Algebra.Ring.Basic
25172518
import Mathlib.ModelTheory.Basic
25182519
import Mathlib.ModelTheory.Bundled
25192520
import Mathlib.ModelTheory.Definability

‎Mathlib/ModelTheory/Algebra/Ring/Basic.lean‎

Lines changed: 322 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,322 @@
1+
/-
2+
Copyright (c) 2023 Chris Hughes. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Chris Hughes
5+
-/
6+
7+
import Mathlib.ModelTheory.Syntax
8+
import Mathlib.ModelTheory.Semantics
9+
import Mathlib.Algebra.Ring.Equiv
10+
11+
/-!
12+
13+
# First Order Language of Rings
14+
15+
This file defines the first order language of rings, as well as defining instance of `Add`, `Mul`,
16+
etc. on terms in the language.
17+
18+
## Main Definitions
19+
20+
* `FirstOrder.Language.ring` : the language of rings, with function symbols `+`, `*`, `-`, `0`, `1`
21+
* `FirstOrder.Ring.CompatibleRing` : A class stating that a type is a `Language.ring.Structure`, and
22+
that this structure is the same as the structure given by the classes `Add`, `Mul`, etc. already on
23+
`R`.
24+
* `FirstOrder.Ring.compatibleRingOfRing` : Given a type `R` with instances for each of the `Ring`
25+
operations, make a `compatibleRing` instance.
26+
27+
## Implementation Notes
28+
29+
There are implementation difficulties with the model theory of rings caused by the fact that there
30+
are two different ways to say that `R` is a `Ring`. We can say `Ring R` or
31+
`Language.ring.Structure R` and `Theory.ring.Model R` (The theory of rings is not implemented yet).
32+
33+
The recommended way to use this library is to use the hypotheses `CompatibleRing R` and `Ring R`
34+
on any theorem that requires both a `Ring` instance and a `Language.ring.Structure` instance
35+
in order to state the theorem. To apply such a theorem to a ring `R` with a `Ring` instance,
36+
use the tactic `let _ := compatibleRingOfRing R`. To apply the theorem to `K`
37+
a `Language.ring.Structure K` instance and for example an instance of `Theory.field.Model K`,
38+
you must add local instances with definitions like `ModelTheory.Field.fieldOfModelField K` and
39+
`FirstOrder.Ring.compatibleRingOfModelField K`.
40+
(in `Mathlib/ModelTheory/Algebra/Field/Basic.lean`), depending on the Theory.
41+
42+
-/
43+
44+
variable {α : Type*}
45+
46+
namespace FirstOrder
47+
48+
open FirstOrder
49+
50+
/-- The type of Ring functions, to be used in the definition of the language of rings.
51+
It contains the operations (+,*,-,0,1) -/
52+
inductive ringFunc : ℕ → Type
53+
| add : ringFunc 2
54+
| mul : ringFunc 2
55+
| neg : ringFunc 1
56+
| zero : ringFunc 0
57+
| one : ringFunc 0
58+
deriving DecidableEq
59+
60+
/-- The language of rings contains the operations (+,*,-,0,1) -/
61+
def Language.ring : Language :=
62+
{ Functions := ringFunc
63+
Relations := fun _ => Empty }
64+
65+
namespace Ring
66+
67+
open ringFunc Language
68+
69+
instance (n : ℕ) : DecidableEq (Language.ring.Functions n) := by
70+
dsimp [Language.ring]; infer_instance
71+
72+
instance (n : ℕ) : DecidableEq (Language.ring.Relations n) := by
73+
dsimp [Language.ring]; infer_instance
74+
75+
/-- `RingFunc.add`, but with the defeq type `Language.ring.Functions 2` instead
76+
of `RingFunc 2` -/
77+
abbrev addFunc : Language.ring.Functions 2 := add
78+
79+
/-- `RingFunc.mul`, but with the defeq type `Language.ring.Functions 2` instead
80+
of `RingFunc 2` -/
81+
abbrev mulFunc : Language.ring.Functions 2 := mul
82+
83+
/-- `RingFunc.neg`, but with the defeq type `Language.ring.Functions 1` instead
84+
of `RingFunc 1` -/
85+
abbrev negFunc : Language.ring.Functions 1 := neg
86+
87+
/-- `RingFunc.zero`, but with the defeq type `Language.ring.Functions 0` instead
88+
of `RingFunc 0` -/
89+
abbrev zeroFunc : Language.ring.Functions 0 := zero
90+
91+
/-- `RingFunc.one`, but with the defeq type `Language.ring.Functions 0` instead
92+
of `RingFunc 0` -/
93+
abbrev oneFunc : Language.ring.Functions 0 := one
94+
95+
instance (α : Type*) : Zero (Language.ring.Term α) :=
96+
{ zero := Constants.term zeroFunc }
97+
98+
theorem zero_def (α : Type*) : (0 : Language.ring.Term α) = Constants.term zeroFunc := rfl
99+
100+
instance (α : Type*) : One (Language.ring.Term α) :=
101+
{ one := Constants.term oneFunc }
102+
103+
theorem one_def (α : Type*) : (1 : Language.ring.Term α) = Constants.term oneFunc := rfl
104+
105+
instance (α : Type*) : Add (Language.ring.Term α) :=
106+
{ add := addFunc.apply₂ }
107+
108+
theorem add_def (α : Type*) (t₁ t₂ : Language.ring.Term α) :
109+
t₁ + t₂ = addFunc.apply₂ t₁ t₂ := rfl
110+
111+
instance (α : Type*) : Mul (Language.ring.Term α) :=
112+
{ mul := mulFunc.apply₂ }
113+
114+
theorem mul_def (α : Type*) (t₁ t₂ : Language.ring.Term α) :
115+
t₁ * t₂ = mulFunc.apply₂ t₁ t₂ := rfl
116+
117+
instance (α : Type*) : Neg (Language.ring.Term α) :=
118+
{ neg := negFunc.apply₁ }
119+
120+
theorem neg_def (α : Type*) (t : Language.ring.Term α) :
121+
-t = negFunc.apply₁ t := rfl
122+
123+
instance : Fintype Language.ring.Symbols :=
124+
⟨⟨Multiset.ofList
125+
[Sum.inl ⟨2, .add⟩,
126+
Sum.inl ⟨2, .mul⟩,
127+
Sum.inl ⟨1, .neg⟩,
128+
Sum.inl ⟨0, .zero⟩,
129+
Sum.inl ⟨0, .one⟩], by
130+
dsimp [Language.Symbols]; decide⟩, by
131+
intro x
132+
dsimp [Language.Symbols]
133+
rcases x with ⟨_, f⟩ | ⟨_, f⟩
134+
· cases f <;> decide
135+
· cases f ⟩
136+
137+
@[simp]
138+
theorem card_ring : card Language.ring = 5 := by
139+
have : Fintype.card Language.ring.Symbols = 5 := rfl
140+
simp [Language.card, this]
141+
142+
open Language ring Structure
143+
144+
/-- A Type `R` is a `CompatibleRing` if it is a structure for the language of rings and this
145+
structure is the same as the structure already given on `R` by the classes `Add`, `Mul` etc.
146+
147+
It is recommended to use this type class as a hypothesis to any theorem whose statement
148+
requires a type to have be both a `Ring` (or `Field` etc.) and a
149+
`Language.ring.Structure` -/
150+
/- This class does not extend `Add` etc, because this way it can be used in
151+
combination with a `Ring`, or `Field` instance without having multiple different
152+
`Add` structures on the Type. -/
153+
class CompatibleRing (R : Type*) [Add R] [Mul R] [Neg R] [One R] [Zero R]
154+
extends Language.ring.Structure R where
155+
/-- Addition in the `Language.ring.Structure` is the same as the addition given by the
156+
`Add` instance -/
157+
( funMap_add : ∀ x, funMap addFunc x = x 0 + x 1 )
158+
/-- Multiplication in the `Language.ring.Structure` is the same as the multiplication given by the
159+
`Mul` instance -/
160+
( funMap_mul : ∀ x, funMap mulFunc x = x 0 * x 1 )
161+
/-- Negation in the `Language.ring.Structure` is the same as the negation given by the
162+
`Neg` instance -/
163+
( funMap_neg : ∀ x, funMap negFunc x = -x 0 )
164+
/-- The constant `0` in the `Language.ring.Structure` is the same as the constant given by the
165+
`Zero` instance -/
166+
( funMap_zero : ∀ x, funMap (zeroFunc : Language.ring.Constants) x = 0 )
167+
/-- The constant `1` in the `Language.ring.Structure` is the same as the constant given by the
168+
`One` instance -/
169+
( funMap_one : ∀ x, funMap (oneFunc : Language.ring.Constants) x = 1 )
170+
171+
open CompatibleRing
172+
173+
attribute [simp] funMap_add funMap_mul funMap_neg funMap_zero funMap_one
174+
175+
section
176+
177+
variable {R : Type*} [Add R] [Mul R] [Neg R] [One R] [Zero R] [CompatibleRing R]
178+
179+
@[simp]
180+
theorem realize_add (x y : ring.Term α) (v : α → R) :
181+
Term.realize v (x + y) = Term.realize v x + Term.realize v y := by
182+
simp [add_def, funMap_add]
183+
184+
@[simp]
185+
theorem realize_mul (x y : ring.Term α) (v : α → R) :
186+
Term.realize v (x * y) = Term.realize v x * Term.realize v y := by
187+
simp [mul_def, funMap_mul]
188+
189+
@[simp]
190+
theorem realize_neg (x : ring.Term α) (v : α → R) :
191+
Term.realize v (-x) = -Term.realize v x := by
192+
simp [neg_def, funMap_neg]
193+
194+
@[simp]
195+
theorem realize_zero (v : α → R) : Term.realize v (0 : ring.Term α) = 0 := by
196+
simp [zero_def, funMap_zero, constantMap]
197+
198+
@[simp]
199+
theorem realize_one (v : α → R) : Term.realize v (1 : ring.Term α) = 1 := by
200+
simp [one_def, funMap_one, constantMap]
201+
202+
end
203+
204+
/-- Given a Type `R` with instances for each of the `Ring` operations, make a
205+
`Language.ring.Structure R` instance, along with a proof that the operations given
206+
by the `Language.ring.Structure` are the same as those given by the `Add` or `Mul` etc.
207+
instances.
208+
209+
This definition can be used when applying a theorem about the model theory of rings
210+
to a literal ring `R`, by writing `let _ := compatibleRingOfRing R`. After this, if,
211+
for example, `R` is a field, then Lean will be able to find the instance for
212+
`Theory.field.Model R`, and it will be possible to apply theorems about the model theory
213+
of fields.
214+
215+
This is a `def` and not an `instance`, because the path
216+
`Ring` => `Language.ring.Structure` => `Ring` cannot be made to
217+
commute by definition
218+
-/
219+
def compatibleRingOfRing (R : Type*) [Add R] [Mul R] [Neg R] [One R] [Zero R] :
220+
CompatibleRing R :=
221+
{ funMap := fun {n} f =>
222+
match n, f with
223+
| _, .add => fun x => x 0 + x 1
224+
| _, .mul => fun x => x 0 * x 1
225+
| _, .neg => fun x => -x 0
226+
| _, .zero => fun _ => 0
227+
| _, .one => fun _ => 1
228+
RelMap := Empty.elim,
229+
funMap_add := fun _ => rfl,
230+
funMap_mul := fun _ => rfl,
231+
funMap_neg := fun _ => rfl,
232+
funMap_zero := fun _ => rfl,
233+
funMap_one := fun _ => rfl }
234+
235+
/-- An isomorphism in the language of rings is a ring isomorphism -/
236+
def languageEquivEquivRingEquiv {R S : Type*}
237+
[NonAssocRing R] [NonAssocRing S]
238+
[CompatibleRing R] [CompatibleRing S] :
239+
(Language.ring.Equiv R S) ≃ (R ≃+* S) :=
240+
{ toFun := fun f =>
241+
{ f with
242+
map_add' := by
243+
intro x y
244+
simpa using f.map_fun addFunc ![x, y]
245+
map_mul' := by
246+
intro x y
247+
simpa using f.map_fun mulFunc ![x, y] }
248+
invFun := fun f =>
249+
{ f with
250+
map_fun' := fun {n} f => by
251+
cases f <;> simp
252+
map_rel' := fun {n} f => by cases f },
253+
left_inv := fun f => by ext; rfl
254+
right_inv := fun f => by ext; rfl }
255+
256+
variable (R : Type*) [Language.ring.Structure R]
257+
258+
/-- A def to put an `Add` instance on a type with a `Language.ring.Structure` instance.
259+
260+
To be used sparingly, usually only when defining a more useful definition like,
261+
`[Language.ring.Structure K] -> [Theory.field.Model K] -> Field K` -/
262+
@[reducible] def addOfRingStructure : Add R :=
263+
{ add := fun x y => funMap addFunc ![x, y] }
264+
265+
/-- A def to put an `Mul` instance on a type with a `Language.ring.Structure` instance.
266+
267+
To be used sparingly, usually only when defining a more useful definition like,
268+
`[Language.ring.Structure K] -> [Theory.field.Model K] -> Field K` -/
269+
@[reducible] def mulOfRingStructure : Mul R :=
270+
{ mul := fun x y => funMap mulFunc ![x, y] }
271+
272+
/-- A def to put an `Neg` instance on a type with a `Language.ring.Structure` instance.
273+
274+
To be used sparingly, usually only when defining a more useful definition like,
275+
`[Language.ring.Structure K] -> [Theory.field.Model K] -> Field K` -/
276+
@[reducible] def negOfRingStructure : Neg R :=
277+
{ neg := fun x => funMap negFunc ![x] }
278+
279+
/-- A def to put an `Zero` instance on a type with a `Language.ring.Structure` instance.
280+
281+
To be used sparingly, usually only when defining a more useful definition like,
282+
`[Language.ring.Structure K] -> [Theory.field.Model K] -> Field K` -/
283+
@[reducible] def zeroOfRingStructure : Zero R :=
284+
{ zero := funMap zeroFunc ![] }
285+
286+
/-- A def to put an `One` instance on a type with a `Language.ring.Structure` instance.
287+
288+
To be used sparingly, usually only when defining a more useful definition like,
289+
`[Language.ring.Structure K] -> [Theory.field.Model K] -> Field K` -/
290+
@[reducible] def oneOfRingStructure : One R :=
291+
{ one := funMap oneFunc ![] }
292+
293+
attribute [local instance] addOfRingStructure mulOfRingStructure negOfRingStructure
294+
zeroOfRingStructure oneOfRingStructure
295+
296+
/--
297+
Given a Type `R` with a `Language.ring.Structure R`, the instance given by
298+
`addOfRingStructure` etc are compatible with the `Language.ring.Structure` instance on `R`.
299+
300+
This definition is only to be used when `addOfRingStructure`, `mulOfRingStructure` etc
301+
are local instances.
302+
-/
303+
@[reducible] def compatibleRingOfRingStructure : CompatibleRing R :=
304+
{ funMap_add := by
305+
simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi];
306+
intros; rfl
307+
funMap_mul := by
308+
simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi];
309+
intros; rfl
310+
funMap_neg := by
311+
simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi];
312+
intros; rfl
313+
funMap_zero := by
314+
simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi];
315+
intros; rfl
316+
funMap_one := by
317+
simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi];
318+
intros; rfl }
319+
320+
end Ring
321+
322+
end FirstOrder

0 commit comments

Comments
 (0)