mathlib3 documentation

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 #

TODO #

source
@[protected, instance]
def category_theory.bundled.Structure {L : first_order.language} (M : category_theory.bundled L.Structure) :
L.Structure ↥M
Equations
source
def equiv.bundled_induced (L : first_order.language) {M : Type w} [L.Structure M] {N : Type w'} (g : M ≃ N) :
category_theory.bundled L.Structure

A type bundled with the structure induced by an equivalence.

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

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

Equations
source
@[protected, instance]
def first_order.language.equiv_setoid {L : first_order.language} :
setoid (category_theory.bundled L.Structure)

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

Equations
source
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
source
@[protected, instance]
def first_order.language.Theory.Model.has_coe_to_sort {L : first_order.language} (T : L.Theory) :
has_coe_to_sort T.Model (Type w)
Equations
source
@[simp]
theorem first_order.language.Theory.Model.carrier_eq_coe {L : first_order.language} (T : L.Theory) (M : T.Model) :
M.carrier = ↥M
source
def first_order.language.Theory.Model.of {L : first_order.language} (T : L.Theory) (M : Type w) [L.Structure M] [M ⊨ T] [nonempty M] :
T.Model

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
source
@[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] :
↥(first_order.language.Theory.Model.of T M) = M
source
@[protected, instance]
def first_order.language.Theory.Model.nonempty {L : first_order.language} (T : L.Theory) (M : T.Model) :
nonempty ↥M
source
@[protected, instance]
def first_order.language.Theory.Model.inhabited {L : first_order.language} :
inhabited ∅.Model
Equations
source
def first_order.language.Theory.Model.equiv_induced {L : first_order.language} {T : L.Theory} {M : T.Model} {N : Type w'} (e : ↥M ≃ N) :
T.Model

Maps a bundled model along a bijection.

Equations
source
@[protected, instance]
def first_order.language.Theory.Model.of_small {L : first_order.language} {T : L.Theory} (M : Type w) [nonempty M] [L.Structure M] [M ⊨ T] [h : small M] :
small ↥(first_order.language.Theory.Model.of T M)
source
noncomputable def first_order.language.Theory.Model.shrink {L : first_order.language} {T : L.Theory} (M : T.Model) [small ↥M] :
T.Model

Shrinks a small model to a particular universe.

Equations
source
def first_order.language.Theory.Model.ulift {L : first_order.language} {T : L.Theory} (M : T.Model) :
T.Model

Lifts a model to a particular universe.

Equations
source
def first_order.language.Theory.Model.reduct {L : first_order.language} {T : L.Theory} {L' : first_order.language} (φ : L →ᴸ L') (M : (φ.on_Theory T).Model) :
T.Model

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

Equations
source
@[simp]
theorem first_order.language.Theory.Model.reduct_struc {L : first_order.language} {T : L.Theory} {L' : first_order.language} (φ : L →ᴸ L') (M : (φ.on_Theory T).Model) :
(first_order.language.Theory.Model.reduct φ M).struc = φ.reduct ↥M
source
@[simp]
theorem first_order.language.Theory.Model.reduct_carrier {L : first_order.language} {T : L.Theory} {L' : first_order.language} (φ : L →ᴸ L') (M : (φ.on_Theory T).Model) :
↥(first_order.language.Theory.Model.reduct φ M) = ↥M
source
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] :
(φ.on_Theory T).Model

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

Equations
source
@[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] :
↥(first_order.language.Theory.Model.default_expansion h M) = ↥M
source
@[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] :
(first_order.language.Theory.Model.default_expansion h M).struc = φ.default_expansion ↥M
source
@[protected, instance]
def first_order.language.Theory.Model.left_Structure {L : first_order.language} {L' : first_order.language} {T : (L.sum L').Theory} (M : T.Model) :
L.Structure ↥M
Equations
source
@[protected, instance]
def first_order.language.Theory.Model.right_Structure {L : first_order.language} {L' : first_order.language} {T : (L.sum L').Theory} (M : T.Model) :
L'.Structure ↥M
Equations
source
@[simp]
theorem first_order.language.Theory.Model.subtheory_Model_carrier {L : first_order.language} {T : L.Theory} (M : T.Model) {T' : L.Theory} (h : T' ⊆ T) :
↥(M.subtheory_Model h) = ↥M
source
@[simp]
theorem first_order.language.Theory.Model.subtheory_Model_struc {L : first_order.language} {T : L.Theory} (M : T.Model) {T' : L.Theory} (h : T' ⊆ T) :
(M.subtheory_Model h).struc = M.struc
source
def first_order.language.Theory.Model.subtheory_Model {L : first_order.language} {T : L.Theory} (M : T.Model) {T' : L.Theory} (h : T' ⊆ T) :
T'.Model

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

Equations
Instances for ↥first_order.language.Theory.Model.subtheory_Model
source
@[protected, instance]
def first_order.language.Theory.Model.subtheory_Model_models {L : first_order.language} {T : L.Theory} (M : T.Model) {T' : L.Theory} (h : T' ⊆ T) :
↥(M.subtheory_Model h) ⊨ T
source
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) :
T.Model

Bundles M ⊨ T as a T.Model.

Equations
source
@[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) :
↥(h.bundled) = M
source
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 : L.elementarily_equivalent ↥M N) :
T.Model

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

Equations
source
def first_order.language.elementary_substructure.to_Model {L : first_order.language} (T : L.Theory) {M : T.Model} (S : L.elementary_substructure ↥M) :
T.Model

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

Equations
Instances for ↥first_order.language.elementary_substructure.to_Model
source
@[protected, instance]
def first_order.language.to_Model.small {L : first_order.language} (T : L.Theory) {M : T.Model} (S : L.elementary_substructure ↥M) [h : small ↥S] :
small ↥(first_order.language.elementary_substructure.to_Model T S)