Bundled First-Order Structures

This file bundles types together with their first-order structure.

Main Definitions

• FirstOrder.Language.Theory.ModelType is the type of nonempty models of a particular theory.
• FirstOrder.Language.equivSetoid is the isomorphism equivalence relation on bundled structures.

TODO

• Define category structures on bundled structures and models.

instance CategoryTheory.Bundled.structure {L : FirstOrder.Language} (M : CategoryTheory.Bundled L.Structure) : L.Structure ↑M

Equations

• M.structure = M.str

@[simp]

theorem Equiv.bundledInduced_str (L : FirstOrder.Language) {M : Type w} [L.Structure M] {N : Type w'} (g : M ≃ N) : (Equiv.bundledInduced L g).str = g.inducedStructure

@[simp]

theorem Equiv.bundledInduced_α (L : FirstOrder.Language) {M : Type w} [L.Structure M] {N : Type w'} (g : M ≃ N) : ↑(Equiv.bundledInduced L g) = N

def Equiv.bundledInduced (L : FirstOrder.Language) {M : Type w} [L.Structure M] {N : Type w'} (g : M ≃ N) : CategoryTheory.Bundled L.Structure

A type bundled with the structure induced by an equivalence.

Equations

• Equiv.bundledInduced L g = { α := N, str := g.inducedStructure }

def Equiv.bundledInducedEquiv (L : FirstOrder.Language) {M : Type w} [L.Structure M] {N : Type w'} (g : M ≃ N) : L.Equiv M ↑(Equiv.bundledInduced L g)

An equivalence of types as a first-order equivalence to the bundled structure on the codomain.

Equations

• Equiv.bundledInducedEquiv L g = g.inducedStructureEquiv

instance FirstOrder.Language.equivSetoid {L : FirstOrder.Language} : Setoid (CategoryTheory.Bundled L.Structure)

The equivalence relation on bundled L.Structures indicating that they are isomorphic.

Equations

• FirstOrder.Language.equivSetoid = { r := fun (M N : CategoryTheory.Bundled L.Structure) => Nonempty (L.Equiv ↑M ↑N), iseqv := ⋯ }

structure FirstOrder.Language.Theory.ModelType {L : FirstOrder.Language} (T : L.Theory) : Type (max (max u v) (w + 1))

The type of nonempty models of a first-order theory.

• Carrier : Type w
• struc : L.Structure ↑self
• is_model : ↑self ⊨ T
• nonempty' : Nonempty ↑self

theorem FirstOrder.Language.Theory.ModelType.is_model {L : FirstOrder.Language} {T : L.Theory} (self : T.ModelType) : ↑self ⊨ T

theorem FirstOrder.Language.Theory.ModelType.nonempty' {L : FirstOrder.Language} {T : L.Theory} (self : T.ModelType) : Nonempty ↑self

instance FirstOrder.Language.Theory.ModelType.instCoeSort {L : FirstOrder.Language} (T : L.Theory) : CoeSort T.ModelType (Type w)

Equations

• FirstOrder.Language.Theory.ModelType.instCoeSort T = { coe := FirstOrder.Language.Theory.ModelType.Carrier }

def FirstOrder.Language.Theory.ModelType.of {L : FirstOrder.Language} (T : L.Theory) (M : Type w) [L.Structure M] [M ⊨ T] [Nonempty M] : T.ModelType

The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses.

Equations

• FirstOrder.Language.Theory.ModelType.of T M = FirstOrder.Language.Theory.ModelType.mk M

@[simp]

theorem FirstOrder.Language.Theory.ModelType.coe_of {L : FirstOrder.Language} (T : L.Theory) (M : Type w) [L.Structure M] [M ⊨ T] [Nonempty M] : ↑(FirstOrder.Language.Theory.ModelType.of T M) = M

instance FirstOrder.Language.Theory.ModelType.instNonempty {L : FirstOrder.Language} (T : L.Theory) (M : T.ModelType) : Nonempty ↑M

Equations

• ⋯ = ⋯

instance FirstOrder.Language.Theory.ModelType.instInhabited {L : FirstOrder.Language} : Inhabited ∅.ModelType

Equations

• FirstOrder.Language.Theory.ModelType.instInhabited = { default := FirstOrder.Language.Theory.ModelType.of ∅ PUnit.{w + 1} }

def FirstOrder.Language.Theory.ModelType.equivInduced {L : FirstOrder.Language} {T : L.Theory} {M : T.ModelType} {N : Type w'} (e : ↑M ≃ N) : T.ModelType

Maps a bundled model along a bijection.

Equations

• FirstOrder.Language.Theory.ModelType.equivInduced e = FirstOrder.Language.Theory.ModelType.mk N

instance FirstOrder.Language.Theory.ModelType.of_small {L : FirstOrder.Language} {T : L.Theory} (M : Type w) [Nonempty M] [L.Structure M] [M ⊨ T] [h : Small.{w', w} M] : Small.{w', w} ↑(FirstOrder.Language.Theory.ModelType.of T M)

Equations

• ⋯ = h

noncomputable def FirstOrder.Language.Theory.ModelType.shrink {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) [Small.{w', w} ↑M] : T.ModelType

Shrinks a small model to a particular universe.

Equations

• M.shrink = FirstOrder.Language.Theory.ModelType.equivInduced (equivShrink ↑M)

def FirstOrder.Language.Theory.ModelType.ulift {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) : T.ModelType

Lifts a model to a particular universe.

Equations

• M.ulift = FirstOrder.Language.Theory.ModelType.equivInduced Equiv.ulift.symm

@[simp]

theorem FirstOrder.Language.Theory.ModelType.reduct_Carrier {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} (φ : L →ᴸ L') (M : (φ.onTheory T).ModelType) : ↑(FirstOrder.Language.Theory.ModelType.reduct φ M) = ↑M

@[simp]

theorem FirstOrder.Language.Theory.ModelType.reduct_struc {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} (φ : L →ᴸ L') (M : (φ.onTheory T).ModelType) : (FirstOrder.Language.Theory.ModelType.reduct φ M).struc = φ.reduct ↑M

def FirstOrder.Language.Theory.ModelType.reduct {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} (φ : L →ᴸ L') (M : (φ.onTheory T).ModelType) : T.ModelType

The reduct of any model of φ.onTheory T is a model of T.

Equations

• FirstOrder.Language.Theory.ModelType.reduct φ M = FirstOrder.Language.Theory.ModelType.mk ↑M

@[simp]

theorem FirstOrder.Language.Theory.ModelType.defaultExpansion_Carrier {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : φ.Injective) [(n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun (f : L.Functions n) => φ.onFunction f)] [(n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun (r : L.Relations n) => φ.onRelation r)] (M : T.ModelType) [Inhabited ↑M] : ↑(FirstOrder.Language.Theory.ModelType.defaultExpansion h M) = ↑M

@[simp]

theorem FirstOrder.Language.Theory.ModelType.defaultExpansion_struc {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : φ.Injective) [(n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun (f : L.Functions n) => φ.onFunction f)] [(n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun (r : L.Relations n) => φ.onRelation r)] (M : T.ModelType) [Inhabited ↑M] : (FirstOrder.Language.Theory.ModelType.defaultExpansion h M).struc = φ.defaultExpansion ↑M

noncomputable def FirstOrder.Language.Theory.ModelType.defaultExpansion {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : φ.Injective) [(n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun (f : L.Functions n) => φ.onFunction f)] [(n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun (r : L.Relations n) => φ.onRelation r)] (M : T.ModelType) [Inhabited ↑M] : (φ.onTheory T).ModelType

When φ is injective, defaultExpansion expands a model of T to a model of φ.onTheory T arbitrarily.

Equations

• FirstOrder.Language.Theory.ModelType.defaultExpansion h M = FirstOrder.Language.Theory.ModelType.mk ↑M

instance FirstOrder.Language.Theory.ModelType.leftStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : (L.sum L').Theory} (M : T.ModelType) : L.Structure ↑M

Equations

• M.leftStructure = FirstOrder.Language.LHom.sumInl.reduct ↑M

instance FirstOrder.Language.Theory.ModelType.rightStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : (L.sum L').Theory} (M : T.ModelType) : L'.Structure ↑M

Equations

• M.rightStructure = FirstOrder.Language.LHom.sumInr.reduct ↑M

@[simp]

theorem FirstOrder.Language.Theory.ModelType.subtheoryModel_struc {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) {T' : L.Theory} (h : T' ⊆ T) : (M.subtheoryModel h).struc = M.struc

@[simp]

theorem FirstOrder.Language.Theory.ModelType.subtheoryModel_Carrier {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) {T' : L.Theory} (h : T' ⊆ T) : ↑(M.subtheoryModel h) = ↑M

def FirstOrder.Language.Theory.ModelType.subtheoryModel {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) {T' : L.Theory} (h : T' ⊆ T) : T'.ModelType

A model of a theory is also a model of any subtheory.

Equations

• M.subtheoryModel h = FirstOrder.Language.Theory.ModelType.mk ↑M

instance FirstOrder.Language.Theory.ModelType.subtheoryModel_models {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) {T' : L.Theory} (h : T' ⊆ T) : ↑(M.subtheoryModel h) ⊨ T

Equations

• ⋯ = ⋯

def FirstOrder.Language.Theory.Model.bundled {L : FirstOrder.Language} {T : L.Theory} {M : Type w} [LM : L.Structure M] [ne : Nonempty M] (h : M ⊨ T) : T.ModelType

Bundles M ⊨ T as a T.ModelType.

Equations

• h.bundled = FirstOrder.Language.Theory.ModelType.of T M

@[simp]

theorem FirstOrder.Language.Theory.coe_of {L : FirstOrder.Language} {T : L.Theory} {M : Type w} [L.Structure M] [Nonempty M] (h : M ⊨ T) : ↑h.bundled = M

def FirstOrder.Language.ElementarilyEquivalent.toModel {L : FirstOrder.Language} (T : L.Theory) {M : T.ModelType} {N : Type u_1} [LN : L.Structure N] (h : L.ElementarilyEquivalent (↑M) N) : T.ModelType

A structure that is elementarily equivalent to a model, bundled as a model.

Equations

• FirstOrder.Language.ElementarilyEquivalent.toModel T h = FirstOrder.Language.Theory.ModelType.mk N

def FirstOrder.Language.ElementarySubstructure.toModel {L : FirstOrder.Language} (T : L.Theory) {M : T.ModelType} (S : L.ElementarySubstructure ↑M) : T.ModelType

An elementary substructure of a bundled model as a bundled model.

Equations

• FirstOrder.Language.ElementarySubstructure.toModel T S = FirstOrder.Language.ElementarilyEquivalent.toModel T ⋯

instance FirstOrder.Language.ElementarySubstructure.toModel.instSmall {L : FirstOrder.Language} (T : L.Theory) {M : T.ModelType} (S : L.ElementarySubstructure ↑M) [h : Small.{w, x} ↥S] : Small.{w, x} ↑(FirstOrder.Language.ElementarySubstructure.toModel T S)

Equations

• ⋯ = h