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.
A type bundled with the structure induced by an equivalence.
Equations
- Equiv.bundledInduced L g = { α := N, str := g.inducedStructure }
An equivalence of types as a first-order equivalence to the bundled structure on the codomain.
Equations
The equivalence relation on bundled L.Structure
s indicating that they are isomorphic.
Equations
- FirstOrder.Language.equivSetoid = { r := fun (M N : CategoryTheory.Bundled L.Structure) => Nonempty (L.Equiv ↑M ↑N), iseqv := ⋯ }
The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses.
Equations
- FirstOrder.Language.Theory.ModelType.of T M = { Carrier := M, struc := inst✝², is_model := inst✝¹, nonempty' := inst✝ }
Maps a bundled model along a bijection.
Equations
- FirstOrder.Language.Theory.ModelType.equivInduced e = { Carrier := N, struc := e.inducedStructure, is_model := ⋯, nonempty' := ⋯ }
Shrinks a small model to a particular universe.
Equations
Lifts a model to a particular universe.
The reduct of any model of φ.onTheory T
is a model of T
.
Equations
- FirstOrder.Language.Theory.ModelType.reduct φ M = { Carrier := ↑M, struc := φ.reduct ↑M, is_model := ⋯, nonempty' := ⋯ }
When φ
is injective, defaultExpansion
expands a model of T
to a model of φ.onTheory T
arbitrarily.
Equations
- FirstOrder.Language.Theory.ModelType.defaultExpansion h M = { Carrier := ↑M, struc := φ.defaultExpansion ↑M, is_model := ⋯, nonempty' := ⋯ }
A structure that is elementarily equivalent to a model, bundled as a model.
Equations
- FirstOrder.Language.ElementarilyEquivalent.toModel T h = { Carrier := N, struc := LN, is_model := ⋯, nonempty' := ⋯ }
An elementary substructure of a bundled model as a bundled model.