# mathlib3documentation

model_theory.bundled

# Bundled First-Order Structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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
def equiv.bundled_induced (L : first_order.language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :

A type bundled with the structure induced by an equivalence.

Equations
@[simp]
theorem equiv.bundled_induced_str (L : first_order.language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :
@[simp]
theorem equiv.bundled_induced_α (L : first_order.language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :
= N
@[simp]
def equiv.bundled_induced_equiv (L : first_order.language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :

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

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

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

Equations
Instances for ↥first_order.language.Theory.Model.of
@[simp]
@[protected, instance]
@[protected, instance]
Equations

Maps a bundled model along a bijection.

Equations
@[protected, instance]
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
noncomputable def first_order.language.Theory.Model.default_expansion {L : first_order.language} {T : L.Theory} {L' : first_order.language} {φ : L →ᴸ L'} (h : φ.injective) [Π (n : ) (f : L'.functions n), decidable (f set.range (λ (f : L.functions n), φ.on_function f))] [Π (n : ) (r : L'.relations n), decidable (r set.range (λ (r : L.relations n), φ.on_relation r))] (M : T.Model) [inhabited M] :

When φ is injective, default_expansion expands a model of T to a model of φ.on_Theory T arbitrarily.

Equations
@[simp]
theorem first_order.language.Theory.Model.default_expansion_carrier {L : first_order.language} {T : L.Theory} {L' : first_order.language} {φ : L →ᴸ L'} (h : φ.injective) [Π (n : ) (f : L'.functions n), decidable (f set.range (λ (f : L.functions n), φ.on_function f))] [Π (n : ) (r : L'.relations n), decidable (r set.range (λ (r : L.relations n), φ.on_relation r))] (M : T.Model) [inhabited M] :
@[simp]
theorem first_order.language.Theory.Model.default_expansion_struc {L : first_order.language} {T : L.Theory} {L' : first_order.language} {φ : L →ᴸ L'} (h : φ.injective) [Π (n : ) (f : L'.functions n), decidable (f set.range (λ (f : L.functions n), φ.on_function f))] [Π (n : ) (r : L'.relations n), decidable (r set.range (λ (r : L.relations n), φ.on_relation r))] (M : T.Model) [inhabited M] :
@[protected, instance]
Equations
@[protected, instance]
Equations

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

Equations
Instances for ↥first_order.language.Theory.Model.subtheory_Model
@[protected, instance]
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) :
def first_order.language.elementarily_equivalent.to_Model {L : first_order.language} (T : L.Theory) {M : T.Model} {N : Type u_2} [LN : L.Structure N] (h : N) :

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

Equations

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

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