# mathlib3documentation

model_theory.substructures

# First-Order Substructures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines substructures of first-order structures in a similar manner to the various substructures appearing in the algebra library.

## Main Results #

def first_order.language.closed_under {L : first_order.language} {M : Type w} [L.Structure M] {n : } (f : L.functions n) (s : set M) :
Prop

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

Equations
@[simp]
theorem first_order.language.closed_under.inter {L : first_order.language} {M : Type w} [L.Structure M] {n : } {f : L.functions n} {s t : set M} (hs : s) (ht : t) :
theorem first_order.language.closed_under.inf {L : first_order.language} {M : Type w} [L.Structure M] {n : } {f : L.functions n} {s t : set M} (hs : s) (ht : t) :
theorem first_order.language.closed_under.Inf {L : first_order.language} {M : Type w} [L.Structure M] {n : } {f : L.functions n} {S : set (set M)} (hS : (s : set M), ) :

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

Instances for first_order.language.substructure
@[protected, instance]
Equations
@[simp]
@[ext]
theorem first_order.language.substructure.ext {L : first_order.language} {M : Type w} [L.Structure M] {S T : L.substructure M} (h : (x : M), x S x T) :
S = T

Two substructures are equal if they have the same elements.

@[protected]
def first_order.language.substructure.copy {L : first_order.language} {M : Type w} [L.Structure M] (S : L.substructure M) (s : set M) (hs : s = S) :

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

Equations
theorem first_order.language.term.realize_mem {L : first_order.language} {M : Type w} [L.Structure M] {S : L.substructure M} {α : Type u_1} (t : L.term α) (xs : α M) (h : (a : α), xs a S) :
@[simp]
theorem first_order.language.substructure.coe_copy {L : first_order.language} {M : Type w} [L.Structure M] {S : L.substructure M} {s : set M} (hs : s = S) :
(S.copy s hs) = s
theorem first_order.language.substructure.copy_eq {L : first_order.language} {M : Type w} [L.Structure M] {S : L.substructure M} {s : set M} (hs : s = S) :
S.copy s hs = S
@[protected, instance]

The substructure M of the structure M.

Equations
@[protected, instance]
Equations
@[protected, instance]

The inf of two substructures is their intersection.

Equations
@[simp]
@[simp]
theorem first_order.language.substructure.mem_inf {L : first_order.language} {M : Type w} [L.Structure M] {p p' : L.substructure M} {x : M} :
x p p' x p x p'
@[protected, instance]
Equations
@[simp, norm_cast]
theorem first_order.language.substructure.mem_Inf {L : first_order.language} {M : Type w} [L.Structure M] {S : set (L.substructure M)} {x : M} :
x (p : L.substructure M), p S x p
theorem first_order.language.substructure.mem_infi {L : first_order.language} {M : Type w} [L.Structure M] {ι : Sort u_1} {S : ι L.substructure M} {x : M} :
(x (i : ι), S i) (i : ι), x S i
@[simp, norm_cast]
theorem first_order.language.substructure.coe_infi {L : first_order.language} {M : Type w} [L.Structure M] {ι : Sort u_1} {S : ι L.substructure M} :
( (i : ι), S i) = (i : ι), (S i)
@[protected, instance]

Substructures of a structure form a complete lattice.

Equations

The L.substructure generated by a set.

Equations
theorem first_order.language.substructure.mem_closure {L : first_order.language} {M : Type w} [L.Structure M] {s : set M} {x : M} :
(S : L.substructure M), s S x S
@[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.

theorem first_order.language.substructure.closure_mono {L : first_order.language} {M : Type w} [L.Structure M] ⦃s t : set M⦄ (h : s t) :

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

theorem first_order.language.substructure.closure_eq_of_le {L : first_order.language} {M : Type w} [L.Structure M] {S : L.substructure M} {s : set M} (h₁ : s S) (h₂ : S ) :
@[protected, instance]
theorem set.countable.substructure_closure (L : first_order.language) {M : Type w} [L.Structure M] {s : set M} [countable (Σ (l : ), L.functions l)] (h : s.countable) :
theorem first_order.language.substructure.closure_induction {L : first_order.language} {M : Type w} [L.Structure M] {s : set M} {p : M Prop} {x : M} (h : x ) (Hs : (x : M), x s p x) (Hfun : {n : } (f : L.functions n), ) :
p x

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.

theorem first_order.language.substructure.dense_induction {L : first_order.language} {M : Type w} [L.Structure M] {p : M Prop} (x : M) {s : set M} (hs : = ) (Hs : (x : M), x s p x) (Hfun : {n : } (f : L.functions n), ) :
p x

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.

@[protected]

closure forms a Galois insertion with the coercion to set.

Equations
@[simp]

Closure of a substructure S equals S.

theorem first_order.language.substructure.closure_Union {L : first_order.language} {M : Type w} [L.Structure M] {ι : Sort u_1} (s : ι set M) :
( (i : ι), s i) = (i : ι),
@[protected, instance]

### comap and map#

def first_order.language.substructure.comap {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (φ : L.hom M N) (S : L.substructure N) :

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

Equations
@[simp]
theorem first_order.language.substructure.comap_coe {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (φ : L.hom M N) (S : L.substructure N) :
@[simp]
theorem first_order.language.substructure.mem_comap {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {S : L.substructure N} {f : L.hom M N} {x : M} :
f x S
theorem first_order.language.substructure.comap_comap {L : first_order.language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (S : L.substructure P) (g : L.hom N P) (f : L.hom M N) :
@[simp]
theorem first_order.language.substructure.map_coe {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (φ : L.hom M N) (S : L.substructure M) :
def first_order.language.substructure.map {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (φ : L.hom M N) (S : L.substructure M) :

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

Equations
@[simp]
theorem first_order.language.substructure.mem_map {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} {S : L.substructure M} {y : N} :
(x : M) (H : x S), f x = y
theorem first_order.language.substructure.mem_map_of_mem {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.hom M N) {S : L.substructure M} {x : M} (hx : x S) :
theorem first_order.language.substructure.apply_coe_mem_map {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.hom M N) (S : L.substructure M) (x : S) :
theorem first_order.language.substructure.map_map {L : first_order.language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (S : L.substructure M) (g : L.hom N P) (f : L.hom M N) :
theorem first_order.language.substructure.map_le_iff_le_comap {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} {S : L.substructure M} {T : L.substructure N} :
theorem first_order.language.substructure.gc_map_comap {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.hom M N) :
theorem first_order.language.substructure.map_le_of_le_comap {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.substructure M) {T : L.substructure N} {f : L.hom M N} :
theorem first_order.language.substructure.le_comap_of_map_le {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.substructure M) {T : L.substructure N} {f : L.hom M N} :
theorem first_order.language.substructure.le_comap_map {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.substructure M) {f : L.hom M N} :
theorem first_order.language.substructure.map_comap_le {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {S : L.substructure N} {f : L.hom M N} :
theorem first_order.language.substructure.monotone_map {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} :
@[simp]
theorem first_order.language.substructure.map_comap_map {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.substructure M) {f : L.hom M N} :
@[simp]
theorem first_order.language.substructure.comap_map_comap {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {S : L.substructure N} {f : L.hom M N} :
theorem first_order.language.substructure.map_sup {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S T : L.substructure M) (f : L.hom M N) :
theorem first_order.language.substructure.map_supr {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Sort u_2} (f : L.hom M N) (s : ι L.substructure M) :
= (i : ι),
theorem first_order.language.substructure.comap_inf {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S T : L.substructure N) (f : L.hom M N) :
theorem first_order.language.substructure.comap_infi {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Sort u_2} (f : L.hom M N) (s : ι L.substructure N) :
= (i : ι),
@[simp]
theorem first_order.language.substructure.map_bot {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.hom M N) :
@[simp]
theorem first_order.language.substructure.comap_top {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.hom M N) :
theorem first_order.language.substructure.map_closure {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.hom M N) (s : set M) :
@[simp]
theorem first_order.language.substructure.closure_image {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {s : set M} (f : L.hom M N) :

map f and comap f form a galois_coinsertion when f is injective.

Equations
theorem first_order.language.substructure.comap_infi_map_of_injective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.hom M N} (hf : function.injective f) (S : ι L.substructure M) :
( (i : ι), = infi S
theorem first_order.language.substructure.comap_supr_map_of_injective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.hom M N} (hf : function.injective f) (S : ι L.substructure M) :
( (i : ι), = supr S

map f and comap f form a galois_insertion when f is surjective.

Equations
theorem first_order.language.substructure.map_infi_comap_of_surjective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.hom M N} (hf : function.surjective f) (S : ι L.substructure N) :
( (i : ι), = infi S
theorem first_order.language.substructure.map_supr_comap_of_surjective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.hom M N} (hf : function.surjective f) (S : ι L.substructure N) :
( (i : ι), = supr S
@[protected, instance]
Equations

The natural embedding of an L.substructure of M into M.

Equations

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

Equations
@[simp]
theorem first_order.language.substructure.closure_induction' {L : first_order.language} {M : Type w} [L.Structure M] (s : set M) {p : Π (x : M), Prop} (Hs : (x : M) (h : x s), p x _) (Hfun : {n : } (f : L.functions n), {x : M | (hx : , p x hx}) {x : M} (hx : x ) :
p x hx

A dependent version of substructure.closure_induction.

Reduces the language of a substructure along a language hom.

Equations

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

Equations
@[simp]
theorem first_order.language.substructure.mem_with_constants {L : first_order.language} {M : Type w} [L.Structure M] {S : L.substructure M} {A : set M} (h : A S) {x : M} :
x x S
@[simp]
theorem first_order.language.hom.dom_restrict_to_fun {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.hom M N) (p : L.substructure M) (ᾰ : p) :
(f.dom_restrict p) = f
def first_order.language.hom.dom_restrict {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.hom M N) (p : L.substructure M) :
L.hom p N

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

Equations
@[simp]
theorem first_order.language.hom.cod_restrict_to_fun_coe {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.substructure N) (f : L.hom M N) (h : (c : M), f c p) (c : M) :
c) = f c
def first_order.language.hom.cod_restrict {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.substructure N) (f : L.hom M N) (h : (c : M), f c p) :
L.hom M p

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

Equations
@[simp]
theorem first_order.language.hom.comp_cod_restrict {L : first_order.language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (f : L.hom M N) (g : L.hom N P) (p : L.substructure P) (h : (b : N), g b p) :
=
@[simp]
theorem first_order.language.hom.subtype_comp_cod_restrict {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.hom M N) (p : L.substructure N) (h : (b : M), f b p) :
= f
def first_order.language.hom.range {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.hom M N) :

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

Equations
theorem first_order.language.hom.range_coe {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.hom M N) :
(f.range) =
@[simp]
theorem first_order.language.hom.mem_range {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} {x : N} :
x f.range (y : M), f y = x
theorem first_order.language.hom.range_eq_map {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.hom M N) :
theorem first_order.language.hom.mem_range_self {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.hom M N) (x : M) :
theorem first_order.language.hom.range_comp {L : first_order.language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (f : L.hom M N) (g : L.hom N P) :
theorem first_order.language.hom.range_comp_le_range {L : first_order.language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (f : L.hom M N) (g : L.hom N P) :
theorem first_order.language.hom.range_eq_top {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} :
theorem first_order.language.hom.range_le_iff_comap {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} {p : L.substructure N} :
theorem first_order.language.hom.map_le_range {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} {p : L.substructure M} :
def first_order.language.hom.eq_locus {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f g : L.hom M N) :

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

Equations
theorem first_order.language.hom.eq_on_closure {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f g : L.hom M N} {s : set M} (h : g s) :

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

theorem first_order.language.hom.eq_of_eq_on_top {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f g : L.hom M N} (h : g ) :
f = g
theorem first_order.language.hom.eq_of_eq_on_dense {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {s : set M} (hs : = ) {f g : L.hom M N} (h : g s) :
f = g

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

Equations
@[simp]
theorem first_order.language.embedding.dom_restrict_apply {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.embedding M N) (p : L.substructure M) (x : p) :
def first_order.language.embedding.cod_restrict {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.substructure N) (f : L.embedding M N) (h : (c : M), f c p) :

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

Equations
@[simp]
theorem first_order.language.embedding.cod_restrict_apply {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.substructure N) (f : L.embedding M N) {h : (c : M), f c p} (x : M) :
x) = f x
@[simp]
theorem first_order.language.embedding.comp_cod_restrict {L : first_order.language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (f : L.embedding M N) (g : L.embedding N P) (p : L.substructure P) (h : (b : N), g b p) :
@[simp]
theorem first_order.language.embedding.subtype_comp_cod_restrict {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.embedding M N) (p : L.substructure N) (h : (b : M), f b p) :
noncomputable def first_order.language.embedding.substructure_equiv_map {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.embedding M N) (s : L.substructure M) :

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

Equations
@[simp]
theorem first_order.language.embedding.substructure_equiv_map_apply {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.embedding M N) (p : L.substructure M) (x : p) :
( x) = f x
noncomputable def first_order.language.embedding.equiv_range {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.embedding M N) :

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

Equations
@[simp]
theorem first_order.language.embedding.equiv_range_apply {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.embedding M N) (x : M) :
theorem first_order.language.equiv.to_hom_range {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.equiv M N) :

The embedding associated to an inclusion of substructures.

Equations
@[simp]