# mathlibdocumentation

model_theory.bundled

# Bundled First-Order Structures #

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

## Main Definitions #

• first_order.language.Theory.Model is the type of nonempty models of a particular theory.
• first_order.language.equiv_setoid is the isomorphism equivalence relation on bundled structures.

## TODO #

• Define category structures on bundled structures and models.
@[protected, instance]
Equations
@[protected, instance]

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

Equations
structure first_order.language.Theory.Model {L : first_order.language} (T : L.Theory) :
Type (max u v (w+1))

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

Instances for first_order.language.Theory.Model
@[protected, instance]
Equations
def first_order.language.Theory.Model.of {L : first_order.language} (T : L.Theory) (M : Type w) [L.Structure M] [M T] [nonempty M] :

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

Equations
@[simp]
theorem first_order.language.Theory.Model.coe_of {L : first_order.language} (T : L.Theory) (M : Type w) [L.Structure M] [M T] [nonempty M] :
@[protected, instance]
@[protected, instance]
Equations
def first_order.language.Theory.Model.equiv_induced {L : first_order.language} {T : L.Theory} {M : T.Model} {N : Type w'} (e : M N) :

Maps a bundled model along a bijection.

Equations
noncomputable def first_order.language.Theory.Model.shrink {L : first_order.language} {T : L.Theory} (M : T.Model) [small M] :

Shrinks a small model to a particular universe.

Equations

Lifts a model to a particular universe.

Equations

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

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def first_order.language.Theory.model.bundled {L : first_order.language} {T : L.Theory} {M : Type w} [LM : L.Structure M] [ne : nonempty M] (h : M T) :

Bundles M ⊨ T as a T.Model.

Equations
@[simp]
theorem first_order.language.Theory.coe_of {L : first_order.language} {T : L.Theory} {M : Type w} [L.Structure M] [nonempty M] (h : M T) :

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

Equations
Instances for ↥first_order.language.elementary_substructure.to_Model
@[protected, instance]