Exponential expansions

Lax480241.Expansions · concepts/Lax480241/Expansions.lean · lax-480241

definition

Loading review…

Natural Language Statement

Definition

An exponential expansion maps a finite ordered $L$ -structure $A$ to a structure over another vocabulary $E$ whose universe is a definable set of tagged assignments of a block of second-order variables: a tag $t$ and an assignment $\rho$ of the block form a point when the domain sentence of $t$ holds of $\rho$ , and each symbol of $E$ holds of points when its defining sentence, at their tags, holds of $A$ with one copy of the block per argument interpreted by their assignments. A block with a variable of arity $a$ has $2^{n^a}$ assignments over $n$ elements, so the expanded universe is one exponential larger; the expansion is described by first-order sentences.

Concept map

4 concepts; 8 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Order.PiLex
2	import Mathlib.Data.Prod.Lex
3	import Mathlib.Data.Fintype.EquivFin
4	import Mathlib.ModelTheory.Order
5	import Mathlib.ModelTheory.Semantics
6	import Mathlib.ModelTheory.Complexity
7	import Mathlib.Tactic.FinCases
8	import Mathlib.Logic.Equiv.Fin.Basic
9	import Mathlib.Data.Finite.Sigma
10	import Mathlib.Data.Fintype.Lattice
11	import Mathlib.Order.Lattice.Nat
12	import Mathlib.Data.Set.Card
13	import Mathlib.Data.Fintype.Pigeonhole
14	import Mathlib.Dynamics.FixedPoints.Basic
15	import Lax904597.SecondOrder
16	import Lax904597.Interpretations
17
18	/-!
19	---
20	title: Exponential expansions
21	type: definition
22	---
23	An exponential expansion maps a finite ordered $L$ -structure $A$ to a
24	structure over another vocabulary $E$ whose universe is a definable set of
25	tagged assignments of a block of second-order variables: a tag $t$ and an
26	assignment $\rho$ of the block form a point when the domain sentence of $t$
27	holds of $\rho$ , and each symbol of $E$ holds of points when its defining
28	sentence, at their tags, holds of $A$ with one copy of the block per
29	argument interpreted by their assignments. A block with a variable of arity
30	$a$ has $2^{n^a}$ assignments over $n$ elements, so the expanded universe is
31	one exponential larger; the expansion is described by first-order sentences.
32	-/
33
34	namespace Lax480241.Expansions
35
36	open Lax904597.SecondOrder
37
38	open FirstOrder
39
40	open Language Structure
41
42	namespace SOBlock
43
44	/-- `n` independent copies of a block: one relation variable per pair of a copy
45	index and a relation variable of `B`, keeping its arity. -/
46	def replicate (B : SOBlock) (n : ℕ) : SOBlock where
47	ι := Fin n × B.ι
48	arity p := B.arity p.2
49
50	/-- The assignment of the replicated block determined by one assignment per
51	copy. The index type being a plain product, this is currying and nothing
52	more. -/
53	def replicateAssign (B : SOBlock) {A : Type} {n : ℕ} (ρs : Fin n → B.Assignment A) :
54	(SOBlock.replicate B n).Assignment A :=
55	fun p => ρs p.1 p.2
56
57	end SOBlock
58
59	instance instFiniteAssignment {B : SOBlock} {A : Type} [Finite A] : Finite (B.Assignment A) :=
60	inferInstanceAs (Finite (∀ i : B.ι, (Fin (B.arity i) → A) → Prop))
61
62	variable {L : Language.{0, 0}}
63
64	section Expand
65
66	/-- The structure over `L` expanded by one copy of a block's vocabulary,
67	interpreted by an assignment. -/
68	@[reducible]
69	def SOBlock.structure₁ (B : SOBlock) {A : Type} [inst : L.Structure A]
70	(ρ : B.Assignment A) : (L.sum B.lang).Structure A :=
71	@sumStructure L B.lang A inst (B.structure ρ)
72
73	end Expand
74
75	open FirstOrder
76
77	open Language Structure
78
79	variable {L : Language.{0, 0}}
80
81	/-- An exponential expansion of `L`-structures into `E`-structures: the
82	universe is a definable set of tagged assignments of the block `B`, and each
83	relation symbol of `E` is defined, at each tuple of tags, by a first-order
84	sentence over the ordered base vocabulary expanded by one copy of the block per
85	argument. -/
86	structure ExpExpansion (L : Language.{0, 0}) : Type 1 where
87	/-- The tags: finitely many copies of the space of block assignments. -/
88	Tag : Type
89	/-- Tags are finite, so that finite structures expand to finite
90	structures. -/
91	[tagFinite : Finite Tag]
92	/-- The block whose assignments are the points of the expanded universe. -/
93	B : SOBlock
94	/-- The vocabulary of the expanded structure. -/
95	E : Language.{0, 0}
96	/-- The expanded vocabulary is relational, as every vocabulary of this
97	library. -/
98	[eRelational : E.IsRelational]
99	/-- The domain sentence of each tag: a tagged assignment `(t, ρ)` is a point
100	of the expanded universe iff `dom t` holds of `ρ`. -/
101	dom : Tag → ((L.sum Language.order).sum B.lang).Sentence
102	/-- The defining sentence of each relation symbol at each tuple of tags, over
103	as many copies of the block as the symbol has arguments. -/
104	relSentence : ∀ {n : ℕ}, E.Relations n → (Fin n → Tag) →
105	((L.sum Language.order).sum (SOBlock.replicate B n).lang).Sentence
106	/-- The definable domain is inhabited, so that nonempty structures expand to
107	nonempty structures. -/
108	dom_nonempty : ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
109	∃ (t : Tag) (ρ : B.Assignment A),
110	@Sentence.Realize _ A (SOBlock.structure₁ B (L := L.sum Language.order) ρ) (dom t)
111
112	namespace ExpExpansion
113
114	variable (X : ExpExpansion L)
115
116	attribute [instance] tagFinite eRelational
117
118	/-- A candidate point of the expanded universe: a tagged assignment of the
119	block. An `abbrev`, so that the pair structure stays visible to `rw` and to
120	instance search – only `ExpExpansion.Map` needs to be
121	opaque, to carry the expanded structure. -/
122	abbrev Point (A : Type) : Type :=
123	X.Tag × X.B.Assignment A
124
125	variable {X}
126
127	/-- The domain condition on a candidate point: its tag's domain sentence holds
128	of its assignment. -/
129	def DomHolds {A : Type} [L.Structure A] [LinearOrder A] (p : X.Point A) : Prop :=
130	@Sentence.Realize _ A (SOBlock.structure₁ X.B (L := L.sum Language.order) p.2) (X.dom p.1)
131
132	variable (X)
133
134	/-- The expanded universe: the tagged block assignments satisfying their
135	tag's domain sentence. -/
136	def Map (A : Type) [L.Structure A] [LinearOrder A] : Type :=
137	{p : X.Point A // DomHolds p}
138
139	variable {X}
140
141	/-- The point of the expanded universe carried by a tag and an assignment
142	satisfying the domain sentence. -/
143	def pt {A : Type} [L.Structure A] [LinearOrder A] (t : X.Tag) (ρ : X.B.Assignment A)
144	(h : DomHolds (X := X) (t, ρ)) : X.Map A :=
145	⟨(t, ρ), h⟩
146
147	variable (X)
148
149	/-- The expanded structure: an `n`-ary symbol holds of `n` points iff its
150	defining sentence, at their tags, holds in the base structure with the `n`
151	copies of the block interpreted by their assignments. -/
152	instance mapStructure (A : Type) [L.Structure A] [LinearOrder A] :
153	X.E.Structure (X.Map A) where
154	funMap f := isEmptyElim f
155	RelMap {n} r xs :=
156	@Sentence.Realize _ A
157	(SOBlock.structure₁ (SOBlock.replicate X.B n) (L := L.sum Language.order)
158	(SOBlock.replicateAssign X.B fun i => (xs i).1.2))
159	(X.relSentence r fun i => (xs i).1.1)
160
161	instance mapFinite (A : Type) [L.Structure A] [LinearOrder A] [Finite A] :
162	Finite (X.Map A) :=
163	inferInstanceAs (Finite {p : X.Point A // DomHolds p})
164
165	instance mapNonempty (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :
166	Nonempty (X.Map A) :=
167	let ⟨t, ρ, h⟩ := X.dom_nonempty A
168	⟨pt t ρ h⟩
169
170	end ExpExpansion
171
172	open FirstOrder
173
174	open Language Structure
175
176
177	open FirstOrder
178
179	open Language Structure
180
181	open Function (IsFixedPt)
182
183	variable {L : Language.{0, 0}}
184
185
186	end Lax480241.Expansions
187

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Exponential expansions

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments