mathlib documentation

model_theory.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 #

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.substructure.mem_carrier {L : first_order.language} {M : Type w} [L.Structure M] {s : L.substructure M} {x : M} :
x s.carrier x s
@[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
@[simp]
theorem first_order.language.substructure.mem_top {L : first_order.language} {M : Type w} [L.Structure M] (x : M) :
@[protected, instance]

The inf of two substructures is their intersection.

Equations
@[simp]
theorem first_order.language.substructure.coe_inf {L : first_order.language} {M : Type w} [L.Structure M] (p p' : L.substructure M) :
(p p') = p p'
@[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.coe_Inf {L : first_order.language} {M : Type w} [L.Structure M] (S : set (L.substructure M)) :
(has_Inf.Inf S) = ⋂ (s : L.substructure M) (H : s S), s
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 has_Inf.Inf S ∀ (p : L.substructure M), p Sx 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
@[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.

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 (first_order.language.substructure.closure L) s) (Hs : ∀ (x : M), x sp x) (Hfun : ∀ {n : } (f : L.functions n), first_order.language.closed_under f (set_of p)) :
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 : (first_order.language.substructure.closure L) s = ) (Hs : ∀ (x : M), x sp x) (Hfun : ∀ {n : } (f : L.functions n), first_order.language.closed_under f (set_of p)) :
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.

@[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) :
@[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} :
@[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} :
y first_order.language.substructure.map f S ∃ (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.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) :
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) :
@[simp]
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) :
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) :
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) :
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) :
@[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
theorem first_order.language.substructure.closure_induction' {L : first_order.language} {M : Type w} [L.Structure M] (s : set M) {p : Π (x : M), x (first_order.language.substructure.closure L) s → Prop} (Hs : ∀ (x : M) (h : x s), p x _) (Hfun : ∀ {n : } (f : L.functions n), first_order.language.closed_under f {x : M | ∃ (hx : x (first_order.language.substructure.closure L) s), p x hx}) {x : M} (hx : x (first_order.language.substructure.closure L) s) :
p x hx

A dependent version of substructure.closure_induction.

Reduces the language of a substructure along a language hom.

Equations
@[simp]
theorem first_order.language.Lhom.mem_substructure_reduct {L : first_order.language} {M : Type w} [L.Structure M] {L' : first_order.language} [L'.Structure M] (φ : L →ᴸ L') [φ.is_expansion_on M] {x : M} {S : L'.substructure M} :

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} :
@[simp]
@[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) :
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) :
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) :
@[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.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.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 : set.eq_on f 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 : set.eq_on f 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 : (first_order.language.substructure.closure L) s = ) {f g : L.hom M N} (h : set.eq_on f g s) :
f = g
def first_order.language.embedding.dom_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 M) :

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) :
@[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) :

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) :
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