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 (FirstOrder.Language.Structure L)) : FirstOrder.Language.Structure L ↑M

Equations

• CategoryTheory.Bundled.structure M = M.str

@[simp]

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

@[simp]

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

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

A type bundled with the structure induced by an equivalence.

Equations

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

def Equiv.bundledInducedEquiv (L : FirstOrder.Language) {M : Type w} [FirstOrder.Language.Structure L M] {N : Type w'} (g : M ≃ N) : FirstOrder.Language.Equiv L 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 = Equiv.inducedStructureEquiv g

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

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

Equations

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

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

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

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

instance FirstOrder.Language.Theory.ModelType.instCoeSort {L : FirstOrder.Language} (T : FirstOrder.Language.Theory L) : CoeSort (FirstOrder.Language.Theory.ModelType T) (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 : FirstOrder.Language.Theory L) (M : Type w) [FirstOrder.Language.Structure L M] [M ⊨ T] [Nonempty M] : FirstOrder.Language.Theory.ModelType T

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 : FirstOrder.Language.Theory L) (M : Type w) [FirstOrder.Language.Structure L M] [M ⊨ T] [Nonempty M] : ↑(FirstOrder.Language.Theory.ModelType.of T M) = M

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

Equations

• ⋯ = ⋯

instance FirstOrder.Language.Theory.ModelType.instInhabited {L : FirstOrder.Language} : Inhabited (FirstOrder.Language.Theory.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 : FirstOrder.Language.Theory L} {M : FirstOrder.Language.Theory.ModelType T} {N : Type w'} (e : ↑M ≃ N) : FirstOrder.Language.Theory.ModelType T

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 : FirstOrder.Language.Theory L} (M : Type w) [Nonempty M] [FirstOrder.Language.Structure L 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 : FirstOrder.Language.Theory L} (M : FirstOrder.Language.Theory.ModelType T) [Small.{w', w} ↑M] : FirstOrder.Language.Theory.ModelType T

Shrinks a small model to a particular universe.

Equations

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

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

Lifts a model to a particular universe.

Equations

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

@[simp]

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

@[simp]

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

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

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 : FirstOrder.Language.Theory L} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : FirstOrder.Language.LHom.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 : FirstOrder.Language.Theory.ModelType T) [Inhabited ↑M] : ↑(FirstOrder.Language.Theory.ModelType.defaultExpansion h M) = ↑M

@[simp]

theorem FirstOrder.Language.Theory.ModelType.defaultExpansion_struc {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : FirstOrder.Language.LHom.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 : FirstOrder.Language.Theory.ModelType T) [Inhabited ↑M] : (FirstOrder.Language.Theory.ModelType.defaultExpansion h M).struc = FirstOrder.Language.LHom.defaultExpansion φ ↑M

noncomputable def FirstOrder.Language.Theory.ModelType.defaultExpansion {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : FirstOrder.Language.LHom.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 : FirstOrder.Language.Theory.ModelType T) [Inhabited ↑M] : FirstOrder.Language.Theory.ModelType (FirstOrder.Language.LHom.onTheory φ T)

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 : FirstOrder.Language.Theory (FirstOrder.Language.sum L L')} (M : FirstOrder.Language.Theory.ModelType T) : FirstOrder.Language.Structure L ↑M

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Bundles M ⊨ T as a T.ModelType.

Equations

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

@[simp]

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

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

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 : FirstOrder.Language.Theory L) {M : FirstOrder.Language.Theory.ModelType T} (S : FirstOrder.Language.ElementarySubstructure L ↑M) : FirstOrder.Language.Theory.ModelType T

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 : FirstOrder.Language.Theory L) {M : FirstOrder.Language.Theory.ModelType T} (S : FirstOrder.Language.ElementarySubstructure L ↑M) [h : Small.{u_2, u_1} ↥S] : Small.{u_2, u_1} ↑(FirstOrder.Language.ElementarySubstructure.toModel T S)

Equations

• ⋯ = h