Documentation

Mathlib.ModelTheory.Substructures

First-Order Substructures #

This file defines substructures of first-order structures in a similar manner to the various substructures appearing in the algebra library.

Main Definitions #

Main Results #

Indicates that a set in a given structure is a closed under a function symbol.

Instances For

    A substructure of a structure M is a set closed under application of function symbols.

    Instances For

      Two substructures are equal if they have the same elements.

      Copy a substructure replacing carrier with a set that is equal to it.

      Instances For

        The inf of two substructures is their intersection.

        theorem FirstOrder.Language.Substructure.mem_iInf {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {ι : Sort u_3} {S : ιFirstOrder.Language.Substructure L M} {x : M} :
        x ⨅ (i : ι), S i ∀ (i : ι), x S i
        @[simp]
        theorem FirstOrder.Language.Substructure.coe_iInf {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {ι : Sort u_3} {S : ιFirstOrder.Language.Substructure L M} :
        ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
        @[simp]

        The substructure generated by a set includes the set.

        @[simp]

        A substructure S includes closure L s if and only if it includes s.

        Substructure closure of a set is monotone in its argument: if s ⊆ t, then closure L s ≤ closure L t.

        An induction principle for closure membership. If p holds for all elements of s, and is preserved under function symbols, then p holds for all elements of the closure of s.

        If s is a dense set in a structure M, Substructure.closure L s = ⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s, and verify that p is preserved under function symbols.

        closure forms a Galois insertion with the coercion to set.

        Instances For

          comap and map #

          The preimage of a substructure along a homomorphism is a substructure.

          Instances For

            The image of a substructure along a homomorphism is a substructure.

            Instances For

              The equivalence between the maximal substructure of a structure and the structure itself.

              Instances For
                @[simp]
                theorem FirstOrder.Language.Substructure.coe_topEquiv {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] :
                FirstOrder.Language.Substructure.topEquiv = Subtype.val

                Turns any substructure containing a constant set A into a L[[A]]-substructure.

                Instances For

                  The restriction of a first-order hom to a substructure s ⊆ M gives a hom s → N.

                  Instances For

                    A first-order hom f : M → N whose values lie in a substructure p ⊆ N can be restricted to a hom M → p.

                    Instances For

                      The range of a first-order hom f : M → N is a submodule of N. See Note [range copy pattern].

                      Instances For

                        The substructure of elements x : M such that f x = g x

                        Instances For

                          If two L.Homs are equal on a set, then they are equal on its substructure closure.

                          The restriction of a first-order embedding to a substructure s ⊆ M gives an embedding s → N.

                          Instances For

                            A first-order embedding f : M → N whose values lie in a substructure p ⊆ N can be restricted to an embedding M → p.

                            Instances For

                              The equivalence between a substructure s and its image s.map f.toHom, where f is an embedding.

                              Instances For

                                The equivalence between the domain and the range of an embedding f.

                                Instances For

                                  The embedding associated to an inclusion of substructures.

                                  Instances For