Documentation

Mathlib.ModelTheory.Bundled

Bundled First-Order Structures #

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

Main Definitions #

TODO #

instance CategoryTheory.Bundled.structure {L : FirstOrder.Language} (M : CategoryTheory.Bundled L.Structure) :
L.Structure M
Equations
  • M.structure = M.str
@[simp]
theorem Equiv.bundledInduced_str (L : FirstOrder.Language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :
(Equiv.bundledInduced L g).str = g.inducedStructure
@[simp]
theorem Equiv.bundledInduced_α (L : FirstOrder.Language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :
def Equiv.bundledInduced (L : FirstOrder.Language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :

A type bundled with the structure induced by an equivalence.

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

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

    Equations
    Instances For

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

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

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

      • Carrier : Type w
      • struc : L.Structure self
      • is_model : self T
      • nonempty' : Nonempty self
      Instances For
        theorem FirstOrder.Language.Theory.ModelType.is_model {L : FirstOrder.Language} {T : L.Theory} (self : T.ModelType) :
        self T
        theorem FirstOrder.Language.Theory.ModelType.nonempty' {L : FirstOrder.Language} {T : L.Theory} (self : T.ModelType) :
        Nonempty self
        Equations
        def FirstOrder.Language.Theory.ModelType.of {L : FirstOrder.Language} (T : L.Theory) (M : Type w) [L.Structure M] [M T] [Nonempty M] :
        T.ModelType

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

        Equations
        Instances For
          @[simp]
          theorem FirstOrder.Language.Theory.ModelType.coe_of {L : FirstOrder.Language} (T : L.Theory) (M : Type w) [L.Structure M] [M T] [Nonempty M] :
          instance FirstOrder.Language.Theory.ModelType.instNonempty {L : FirstOrder.Language} (T : L.Theory) (M : T.ModelType) :
          Equations
          • =
          Equations
          def FirstOrder.Language.Theory.ModelType.equivInduced {L : FirstOrder.Language} {T : L.Theory} {M : T.ModelType} {N : Type w'} (e : M N) :
          T.ModelType

          Maps a bundled model along a bijection.

          Equations
          Instances For
            Equations
            • = h
            noncomputable def FirstOrder.Language.Theory.ModelType.shrink {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) [Small.{w', w} M] :
            T.ModelType

            Shrinks a small model to a particular universe.

            Equations
            Instances For
              def FirstOrder.Language.Theory.ModelType.ulift {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) :
              T.ModelType

              Lifts a model to a particular universe.

              Equations
              Instances For
                @[simp]
                theorem FirstOrder.Language.Theory.ModelType.reduct_Carrier {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} (φ : L →ᴸ L') (M : (φ.onTheory T).ModelType) :
                @[simp]
                theorem FirstOrder.Language.Theory.ModelType.reduct_struc {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} (φ : L →ᴸ L') (M : (φ.onTheory T).ModelType) :
                def FirstOrder.Language.Theory.ModelType.reduct {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} (φ : L →ᴸ L') (M : (φ.onTheory T).ModelType) :
                T.ModelType

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

                Equations
                Instances For
                  @[simp]
                  theorem FirstOrder.Language.Theory.ModelType.defaultExpansion_Carrier {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : φ.Injective) [(n : ) → (f : L'.Functions n) → Decidable (f Set.range fun (f : L.Functions n) => φ.onFunction f)] [(n : ) → (r : L'.Relations n) → Decidable (r Set.range fun (r : L.Relations n) => φ.onRelation r)] (M : T.ModelType) [Inhabited M] :
                  @[simp]
                  theorem FirstOrder.Language.Theory.ModelType.defaultExpansion_struc {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : φ.Injective) [(n : ) → (f : L'.Functions n) → Decidable (f Set.range fun (f : L.Functions n) => φ.onFunction f)] [(n : ) → (r : L'.Relations n) → Decidable (r Set.range fun (r : L.Relations n) => φ.onRelation r)] (M : T.ModelType) [Inhabited M] :
                  (FirstOrder.Language.Theory.ModelType.defaultExpansion h M).struc = φ.defaultExpansion M
                  noncomputable def FirstOrder.Language.Theory.ModelType.defaultExpansion {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : φ.Injective) [(n : ) → (f : L'.Functions n) → Decidable (f Set.range fun (f : L.Functions n) => φ.onFunction f)] [(n : ) → (r : L'.Relations n) → Decidable (r Set.range fun (r : L.Relations n) => φ.onRelation r)] (M : T.ModelType) [Inhabited M] :
                  (φ.onTheory T).ModelType

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

                  Equations
                  Instances For
                    instance FirstOrder.Language.Theory.ModelType.leftStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : (L.sum L').Theory} (M : T.ModelType) :
                    L.Structure M
                    Equations
                    • M.leftStructure = FirstOrder.Language.LHom.sumInl.reduct M
                    instance FirstOrder.Language.Theory.ModelType.rightStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : (L.sum L').Theory} (M : T.ModelType) :
                    L'.Structure M
                    Equations
                    • M.rightStructure = FirstOrder.Language.LHom.sumInr.reduct M
                    @[simp]
                    theorem FirstOrder.Language.Theory.ModelType.subtheoryModel_struc {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) {T' : L.Theory} (h : T' T) :
                    (M.subtheoryModel h).struc = M.struc
                    @[simp]
                    theorem FirstOrder.Language.Theory.ModelType.subtheoryModel_Carrier {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) {T' : L.Theory} (h : T' T) :
                    (M.subtheoryModel h) = M
                    def FirstOrder.Language.Theory.ModelType.subtheoryModel {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) {T' : L.Theory} (h : T' T) :
                    T'.ModelType

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

                    Equations
                    Instances For
                      instance FirstOrder.Language.Theory.ModelType.subtheoryModel_models {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) {T' : L.Theory} (h : T' T) :
                      (M.subtheoryModel h) T
                      Equations
                      • =
                      def FirstOrder.Language.Theory.Model.bundled {L : FirstOrder.Language} {T : L.Theory} {M : Type w} [LM : L.Structure M] [ne : Nonempty M] (h : M T) :
                      T.ModelType

                      Bundles M ⊨ T as a T.ModelType.

                      Equations
                      Instances For
                        @[simp]
                        theorem FirstOrder.Language.Theory.coe_of {L : FirstOrder.Language} {T : L.Theory} {M : Type w} [L.Structure M] [Nonempty M] (h : M T) :
                        h.bundled = M
                        def FirstOrder.Language.ElementarilyEquivalent.toModel {L : FirstOrder.Language} (T : L.Theory) {M : T.ModelType} {N : Type u_1} [LN : L.Structure N] (h : L.ElementarilyEquivalent (↑M) N) :
                        T.ModelType

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

                        Equations
                        Instances For
                          def FirstOrder.Language.ElementarySubstructure.toModel {L : FirstOrder.Language} (T : L.Theory) {M : T.ModelType} (S : L.ElementarySubstructure M) :
                          T.ModelType

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

                          Equations
                          Instances For
                            instance FirstOrder.Language.ElementarySubstructure.toModel.instSmall {L : FirstOrder.Language} (T : L.Theory) {M : T.ModelType} (S : L.ElementarySubstructure M) [h : Small.{w, x} S] :
                            Equations
                            • = h