Documentation

Mathlib.ModelTheory.Bundled

Bundled First-Order Structures #

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

Main Definitions #

TODO #

A type bundled with the structure induced by an equivalence.

Equations
@[simp]
theorem Equiv.bundledInduced_str (L : FirstOrder.Language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :
@[simp]
theorem Equiv.bundledInduced_α (L : FirstOrder.Language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :
(bundledInduced L g) = N
def Equiv.bundledInducedEquiv (L : FirstOrder.Language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :
L.Equiv M (bundledInduced L g)

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

Equations

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

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

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

  • Carrier : Type w

    The underlying type for the models

  • struc : L.Structure self
  • is_model : self T
  • nonempty' : Nonempty self

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

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

Maps a bundled model along a bijection.

Equations

Shrinks a small model to a particular universe.

Equations

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

Equations
@[simp]
theorem FirstOrder.Language.Theory.ModelType.reduct_struc {L : Language} {T : L.Theory} {L' : Language} (φ : L →ᴸ L') (M : (φ.onTheory T).ModelType) :
(reduct φ M).struc = φ.reduct M
@[simp]
theorem FirstOrder.Language.Theory.ModelType.reduct_Carrier {L : Language} {T : L.Theory} {L' : Language} (φ : L →ᴸ L') (M : (φ.onTheory T).ModelType) :
(reduct φ M) = M
noncomputable def FirstOrder.Language.Theory.ModelType.defaultExpansion {L : Language} {T : L.Theory} {L' : 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] :

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

Equations
@[simp]
theorem FirstOrder.Language.Theory.ModelType.defaultExpansion_Carrier {L : Language} {T : L.Theory} {L' : 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] :
(defaultExpansion h M) = M
@[simp]
theorem FirstOrder.Language.Theory.ModelType.defaultExpansion_struc {L : Language} {T : L.Theory} {L' : 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] :

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

Equations
@[simp]
theorem FirstOrder.Language.Theory.ModelType.subtheoryModel_Carrier {L : Language} {T : L.Theory} (M : T.ModelType) {T' : L.Theory} (h : T' T) :
(M.subtheoryModel h) = M
def FirstOrder.Language.Theory.Model.bundled {L : Language} {T : L.Theory} {M : Type w} [LM : L.Structure M] [ne : Nonempty M] (h : M T) :

Bundles M ⊨ T as a T.ModelType.

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

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

Equations