# Documentation

Mathlib.ModelTheory.Bundled

# 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.
@[simp]
theorem Equiv.bundledInduced_str (L : FirstOrder.Language) {M : Type w} {N : Type w'} (g : M N) :
().str =
@[simp]
theorem Equiv.bundledInduced_α (L : FirstOrder.Language) {M : Type w} {N : Type w'} (g : M N) :
↑() = N
def Equiv.bundledInduced (L : FirstOrder.Language) {M : Type w} {N : Type w'} (g : M N) :

A type bundled with the structure induced by an equivalence.

Instances For
def Equiv.bundledInducedEquiv (L : FirstOrder.Language) {M : Type w} {N : Type w'} (g : M N) :

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

Instances For

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

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

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

Instances For

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

Instances For
@[simp]

Maps a bundled model along a bijection.

Instances For

Shrinks a small model to a particular universe.

Instances For

Lifts a model to a particular universe.

Instances For

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

Instances For
@[simp]
theorem FirstOrder.Language.Theory.ModelType.defaultExpansion_Carrier {L : FirstOrder.Language} {T : } {L' : FirstOrder.Language} {φ : L →ᴸ L'} [(n : ) → (f : ) → Decidable (f Set.range fun f => )] [(n : ) → (r : ) → Decidable (r Set.range fun r => )] [] :
@[simp]
theorem FirstOrder.Language.Theory.ModelType.defaultExpansion_struc {L : FirstOrder.Language} {T : } {L' : FirstOrder.Language} {φ : L →ᴸ L'} [(n : ) → (f : ) → Decidable (f Set.range fun f => )] [(n : ) → (r : ) → Decidable (r Set.range fun r => )] [] :
noncomputable def FirstOrder.Language.Theory.ModelType.defaultExpansion {L : FirstOrder.Language} {T : } {L' : FirstOrder.Language} {φ : L →ᴸ L'} [(n : ) → (f : ) → Decidable (f Set.range fun f => )] [(n : ) → (r : ) → Decidable (r Set.range fun r => )] [] :

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

Instances For
@[simp]

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

Instances For
def FirstOrder.Language.Theory.Model.bundled {L : FirstOrder.Language} {T : } {M : Type w} [LM : ] [ne : ] (h : M T) :

Bundles M ⊨ T as a T.ModelType.

Instances For
@[simp]
theorem FirstOrder.Language.Theory.coe_of {L : FirstOrder.Language} {T : } {M : Type w} [] (h : M T) :

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

Instances For

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

Instances For