Documentation

Mathlib.ModelTheory.LanguageMap

Language Maps #

Maps between first-order languages in the style of the Flypitch project, as well as several important maps between structures.

Main Definitions #

References #

For the Flypitch project:

structure FirstOrder.Language.LHom (L : FirstOrder.Language) (L' : FirstOrder.Language) :
Type (max (max (max u u') v) v')

A language homomorphism maps the symbols of one language to symbols of another.

Instances For

    A language homomorphism maps the symbols of one language to symbols of another.

    Instances For
      def FirstOrder.Language.LHom.mk₂ {L' : FirstOrder.Language} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} (φ₀ : cFirstOrder.Language.Constants L') (φ₁ : f₁FirstOrder.Language.Functions L' 1) (φ₂ : f₂FirstOrder.Language.Functions L' 2) (φ₁' : r₁FirstOrder.Language.Relations L' 1) (φ₂' : r₂FirstOrder.Language.Relations L' 2) :
      FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂ →ᴸ L'

      Defines a map between languages defined with Language.mk₂.

      Instances For

        Pulls a structure back along a language map.

        Instances For

          The identity language homomorphism.

          Instances For

            The inclusion of the left factor into the sum of two languages.

            Instances For

              The inclusion of the right factor into the sum of two languages.

              Instances For

                The inclusion of an empty language into any other language.

                Instances For
                  theorem FirstOrder.Language.LHom.funext {L : FirstOrder.Language} {L' : FirstOrder.Language} {F : L →ᴸ L'} {G : L →ᴸ L'} (h_fun : F.onFunction = G.onFunction) (h_rel : F.onRelation = G.onRelation) :
                  F = G

                  The composition of two language homomorphisms.

                  Instances For

                    A language map defined on two factors of a sum.

                    Instances For

                      The map between two sum-languages induced by maps on the two factors.

                      Instances For
                        @[simp]
                        theorem FirstOrder.Language.LHom.sumMap_comp_inl {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) :
                        FirstOrder.Language.LHom.comp (FirstOrder.Language.LHom.sumMap ϕ ψ) FirstOrder.Language.LHom.sumInl = FirstOrder.Language.LHom.comp FirstOrder.Language.LHom.sumInl ϕ
                        @[simp]
                        theorem FirstOrder.Language.LHom.sumMap_comp_inr {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) :
                        FirstOrder.Language.LHom.comp (FirstOrder.Language.LHom.sumMap ϕ ψ) FirstOrder.Language.LHom.sumInr = FirstOrder.Language.LHom.comp FirstOrder.Language.LHom.sumInr ψ

                        A language homomorphism is injective when all the maps between symbol types are.

                        Instances For

                          Pulls an L-structure along a language map ϕ : L →ᴸ L', and then expands it to an L'-structure arbitrarily.

                          Instances For

                            A language homomorphism is an expansion on a structure if it commutes with the interpretation of all symbols on that structure.

                            Instances
                              structure FirstOrder.Language.LEquiv (L : FirstOrder.Language) (L' : FirstOrder.Language) :
                              Type (max (max (max u_1 u_2) u_3) u_4)

                              A language equivalence maps the symbols of one language to symbols of another bijectively.

                              Instances For

                                The identity equivalence from a first-order language to itself.

                                Instances For

                                  The inverse of an equivalence of first-order languages.

                                  Instances For

                                    The composition of equivalences of first-order languages.

                                    Instances For

                                      A language with constants indexed by a type.

                                      Instances For

                                        Gives a constantsOn α structure to a type by assigning each constant a value.

                                        Instances For

                                          A map between index types induces a map between constant languages.

                                          Instances For
                                            theorem FirstOrder.Language.constantsOnMap_isExpansionOn {M : Type w} {α : Type u'} {β : Type v'} {f : αβ} {fα : αM} {fβ : βM} (h : f = ) :

                                            Extends a language with a constant for each element of a parameter set in M.

                                            Instances For

                                              Extends a language with a constant for each element of a parameter set in M.

                                              Instances For

                                                The language map adding constants.

                                                Instances For

                                                  The constant symbol indexed by a particular element.

                                                  Instances For

                                                    The language map removing an empty constant set.

                                                    Instances For

                                                      The language map extending the constant set.

                                                      Instances For
                                                        @[simp]