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

@[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.

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.

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.

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

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

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

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

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.

@[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

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

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.

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)

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.

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.

@[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.

@[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 : FirstOrder.Language.Functions L' n) → Decidable (f ∈ Set.range fun f => FirstOrder.Language.LHom.onFunction φ f)] [(n : ℕ) → (r : FirstOrder.Language.Relations L' n) → Decidable (r ∈ Set.range fun r => FirstOrder.Language.LHom.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 : FirstOrder.Language.Functions L' n) → Decidable (f ∈ Set.range fun f => FirstOrder.Language.LHom.onFunction φ f)] [(n : ℕ) → (r : FirstOrder.Language.Relations L' n) → Decidable (r ∈ Set.range fun r => FirstOrder.Language.LHom.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 : FirstOrder.Language.Functions L' n) → Decidable (f ∈ Set.range fun f => FirstOrder.Language.LHom.onFunction φ f)] [(n : ℕ) → (r : FirstOrder.Language.Relations L' n) → Decidable (r ∈ Set.range fun r => FirstOrder.Language.LHom.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.

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

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

@[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.

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

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.

@[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.

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.

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} { x // x ∈ S }] : Small.{u_2, u_1} ↑(FirstOrder.Language.ElementarySubstructure.toModel T S)