mathlib3 documentation

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 Definitions #

Main Results #

source
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
source
@[simp]
theorem first_order.language.closed_under_univ (L : first_order.language) {M : Type w} [L.Structure M] {n : ℕ} (f : L.functions n) :
first_order.language.closed_under f set.univ
source
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 : first_order.language.closed_under f s) (ht : first_order.language.closed_under f t) :
first_order.language.closed_under f (s ∩ t)
source
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 : first_order.language.closed_under f s) (ht : first_order.language.closed_under f t) :
first_order.language.closed_under f (s ⊓ t)
source
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), s ∈ S → first_order.language.closed_under f s) :
first_order.language.closed_under f (has_Inf.Inf S)
source
structure first_order.language.substructure (L : first_order.language) (M : Type w) [L.Structure M] :
Type w

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

Instances for first_order.language.substructure
source
@[protected, instance]
def first_order.language.substructure.set_like {L : first_order.language} {M : Type w} [L.Structure M] :
set_like (L.substructure M) M
Equations
source
def first_order.language.substructure.simps.coe {L : first_order.language} {M : Type w} [L.Structure M] (S : L.substructure M) :
set M

See Note [custom simps projection]

Equations
source
@[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
source
@[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.

source
@[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) :
L.substructure M

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

Equations
source
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) :
first_order.language.term.realize xs t ∈ S
source
@[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
source
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
source
theorem first_order.language.substructure.constants_mem {L : first_order.language} {M : Type w} [L.Structure M] {S : L.substructure M} (c : L.constants) :
↑c ∈ S
source
@[protected, instance]
def first_order.language.substructure.has_top {L : first_order.language} {M : Type w} [L.Structure M] :
has_top (L.substructure M)

The substructure M of the structure M.

Equations
source
@[protected, instance]
def first_order.language.substructure.inhabited {L : first_order.language} {M : Type w} [L.Structure M] :
inhabited (L.substructure M)
Equations
source
@[simp]
theorem first_order.language.substructure.mem_top {L : first_order.language} {M : Type w} [L.Structure M] (x : M) :
x ∈ ⊤
source
@[simp]
theorem first_order.language.substructure.coe_top {L : first_order.language} {M : Type w} [L.Structure M] :
↑⊤ = set.univ
source
@[protected, instance]
def first_order.language.substructure.has_inf {L : first_order.language} {M : Type w} [L.Structure M] :
has_inf (L.substructure M)

The inf of two substructures is their intersection.

Equations
source
@[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'
source
@[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'
source
@[protected, instance]
def first_order.language.substructure.has_Inf {L : first_order.language} {M : Type w} [L.Structure M] :
has_Inf (L.substructure M)
Equations
source
@[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
source
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 ∈ S → x ∈ p
source
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
source
@[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)
source
@[protected, instance]
def first_order.language.substructure.complete_lattice {L : first_order.language} {M : Type w} [L.Structure M] :
complete_lattice (L.substructure M)

Substructures of a structure form a complete lattice.

Equations
source
def first_order.language.substructure.closure (L : first_order.language) {M : Type w} [L.Structure M] :
lower_adjoint coe

The L.substructure generated by a set.

Equations
source
theorem first_order.language.substructure.mem_closure {L : first_order.language} {M : Type w} [L.Structure M] {s : set M} {x : M} :
x ∈ ⇑(first_order.language.substructure.closure L) s ↔ ∀ (S : L.substructure M), s ⊆ ↑S → x ∈ S
source
@[simp]
theorem first_order.language.substructure.subset_closure {L : first_order.language} {M : Type w} [L.Structure M] {s : set M} :
s ⊆ ↑(⇑(first_order.language.substructure.closure L) s)

The substructure generated by a set includes the set.

source
theorem first_order.language.substructure.not_mem_of_not_mem_closure {L : first_order.language} {M : Type w} [L.Structure M] {s : set M} {P : M} (hP : P ∉ ⇑(first_order.language.substructure.closure L) s) :
P ∉ s
source
@[simp]
theorem first_order.language.substructure.closed {L : first_order.language} {M : Type w} [L.Structure M] (S : L.substructure M) :
(first_order.language.substructure.closure L).closed ↑S
source
@[simp]
theorem first_order.language.substructure.closure_le {L : first_order.language} {M : Type w} [L.Structure M] {S : L.substructure M} {s : set M} :
⇑(first_order.language.substructure.closure L) s ≤ S ↔ s ⊆ ↑S

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

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

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

source
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 ≤ ⇑(first_order.language.substructure.closure L) s) :
⇑(first_order.language.substructure.closure L) s = S
source
theorem first_order.language.substructure.coe_closure_eq_range_term_realize {L : first_order.language} {M : Type w} [L.Structure M] {s : set M} :
↑(⇑(first_order.language.substructure.closure L) s) = set.range (first_order.language.term.realize coe)
source
@[protected, instance]
def first_order.language.substructure.small_closure {L : first_order.language} {M : Type w} [L.Structure M] {s : set M} [small ↥s] :
small ↥(⇑(first_order.language.substructure.closure L) s)
source
theorem first_order.language.substructure.mem_closure_iff_exists_term {L : first_order.language} {M : Type w} [L.Structure M] {s : set M} {x : M} :
x ∈ ⇑(first_order.language.substructure.closure L) s ↔ ∃ (t : L.term ↥s), first_order.language.term.realize coe t = x
source
theorem first_order.language.substructure.lift_card_closure_le_card_term {L : first_order.language} {M : Type w} [L.Structure M] {s : set M} :
(cardinal.mk ↥(⇑(first_order.language.substructure.closure L) s)).lift ≤ cardinal.mk (L.term ↥s)
source
theorem first_order.language.substructure.lift_card_closure_le {L : first_order.language} {M : Type w} [L.Structure M] {s : set M} :
(cardinal.mk ↥(⇑(first_order.language.substructure.closure L) s)).lift ≤ linear_order.max cardinal.aleph_0 ((cardinal.mk ↥s).lift + (cardinal.mk (Σ (i : ℕ), L.functions i)).lift)
source
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) :
countable ↥(⇑(first_order.language.substructure.closure L) s)
source
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 ∈ s → p 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.

source
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 ∈ s → p 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.

source
@[protected]
def first_order.language.substructure.gi (L : first_order.language) (M : Type w) [L.Structure M] :
galois_insertion ⇑(first_order.language.substructure.closure L) coe

closure forms a Galois insertion with the coercion to set.

Equations
source
@[simp]
theorem first_order.language.substructure.closure_eq {L : first_order.language} {M : Type w} [L.Structure M] (S : L.substructure M) :
⇑(first_order.language.substructure.closure L) ↑S = S

Closure of a substructure S equals S.

source
@[simp]
theorem first_order.language.substructure.closure_empty {L : first_order.language} {M : Type w} [L.Structure M] :
⇑(first_order.language.substructure.closure L) ∅ = ⊥
source
@[simp]
theorem first_order.language.substructure.closure_univ {L : first_order.language} {M : Type w} [L.Structure M] :
⇑(first_order.language.substructure.closure L) set.univ = ⊤
source
theorem first_order.language.substructure.closure_union {L : first_order.language} {M : Type w} [L.Structure M] (s t : set M) :
⇑(first_order.language.substructure.closure L) (s ∪ t) = ⇑(first_order.language.substructure.closure L) s ⊔ ⇑(first_order.language.substructure.closure L) t
source
theorem first_order.language.substructure.closure_Union {L : first_order.language} {M : Type w} [L.Structure M] {ι : Sort u_1} (s : ι → set M) :
⇑(first_order.language.substructure.closure L) (⋃ (i : ι), s i) = ⨆ (i : ι), ⇑(first_order.language.substructure.closure L) (s i)
source
@[protected, instance]
def first_order.language.substructure.small_bot {L : first_order.language} {M : Type w} [L.Structure M] :
small ↥⊥

comap and map #

source
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) :
L.substructure M

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

Equations
source
@[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) :
↑(first_order.language.substructure.comap φ S) = ⇑φ ⁻¹' ↑S
source
@[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} :
x ∈ first_order.language.substructure.comap f S ↔ ⇑f x ∈ S
source
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) :
first_order.language.substructure.comap f (first_order.language.substructure.comap g S) = first_order.language.substructure.comap (g.comp f) S
source
@[simp]
theorem first_order.language.substructure.comap_id {L : first_order.language} {P : Type u_2} [L.Structure P] (S : L.substructure P) :
first_order.language.substructure.comap (first_order.language.hom.id L P) S = S
source
@[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) :
↑(first_order.language.substructure.map φ S) = ⇑φ '' ↑S
source
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) :
L.substructure N

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

Equations
source
@[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
source
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) :
⇑f x ∈ first_order.language.substructure.map f S
source
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) :
⇑f ↑x ∈ first_order.language.substructure.map f S
source
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) :
first_order.language.substructure.map g (first_order.language.substructure.map f S) = first_order.language.substructure.map (g.comp f) S
source
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} :
first_order.language.substructure.map f S ≤ T ↔ S ≤ first_order.language.substructure.comap f T
source
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) :
galois_connection (first_order.language.substructure.map f) (first_order.language.substructure.comap f)
source
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} :
S ≤ first_order.language.substructure.comap f T → first_order.language.substructure.map f S ≤ T
source
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} :
first_order.language.substructure.map f S ≤ T → S ≤ first_order.language.substructure.comap f T
source
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} :
S ≤ first_order.language.substructure.comap f (first_order.language.substructure.map f S)
source
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} :
first_order.language.substructure.map f (first_order.language.substructure.comap f S) ≤ S
source
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} :
monotone (first_order.language.substructure.map f)
source
theorem first_order.language.substructure.monotone_comap {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} :
monotone (first_order.language.substructure.comap f)
source
@[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} :
first_order.language.substructure.map f (first_order.language.substructure.comap f (first_order.language.substructure.map f S)) = first_order.language.substructure.map f S
source
@[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} :
first_order.language.substructure.comap f (first_order.language.substructure.map f (first_order.language.substructure.comap f S)) = first_order.language.substructure.comap f S
source
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) :
first_order.language.substructure.map f (S ⊔ T) = first_order.language.substructure.map f S ⊔ first_order.language.substructure.map f T
source
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) :
first_order.language.substructure.map f (supr s) = ⨆ (i : ι), first_order.language.substructure.map f (s i)
source
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) :
first_order.language.substructure.comap f (S ⊓ T) = first_order.language.substructure.comap f S ⊓ first_order.language.substructure.comap f T
source
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) :
first_order.language.substructure.comap f (infi s) = ⨅ (i : ι), first_order.language.substructure.comap f (s i)
source
@[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) :
first_order.language.substructure.map f ⊥ = ⊥
source
@[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) :
first_order.language.substructure.comap f ⊤ = ⊤
source
@[simp]
theorem first_order.language.substructure.map_id {L : first_order.language} {M : Type w} [L.Structure M] (S : L.substructure M) :
first_order.language.substructure.map (first_order.language.hom.id L M) S = S
source
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) :
first_order.language.substructure.map f (⇑(first_order.language.substructure.closure L) s) = ⇑(first_order.language.substructure.closure L) (⇑f '' s)
source
@[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) :
⇑(first_order.language.substructure.closure L) (⇑f '' s) = first_order.language.substructure.map f (⇑(first_order.language.substructure.closure L) s)
source
def first_order.language.substructure.gci_map_comap {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.injective ⇑f) :
galois_coinsertion (first_order.language.substructure.map f) (first_order.language.substructure.comap f)

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

Equations
source
theorem first_order.language.substructure.comap_map_eq_of_injective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.injective ⇑f) (S : L.substructure M) :
first_order.language.substructure.comap f (first_order.language.substructure.map f S) = S
source
theorem first_order.language.substructure.comap_surjective_of_injective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.injective ⇑f) :
function.surjective (first_order.language.substructure.comap f)
source
theorem first_order.language.substructure.map_injective_of_injective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.injective ⇑f) :
function.injective (first_order.language.substructure.map f)
source
theorem first_order.language.substructure.comap_inf_map_of_injective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.injective ⇑f) (S T : L.substructure M) :
first_order.language.substructure.comap f (first_order.language.substructure.map f S ⊓ first_order.language.substructure.map f T) = S ⊓ T
source
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) :
first_order.language.substructure.comap f (⨅ (i : ι), first_order.language.substructure.map f (S i)) = infi S
source
theorem first_order.language.substructure.comap_sup_map_of_injective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.injective ⇑f) (S T : L.substructure M) :
first_order.language.substructure.comap f (first_order.language.substructure.map f S ⊔ first_order.language.substructure.map f T) = S ⊔ T
source
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) :
first_order.language.substructure.comap f (⨆ (i : ι), first_order.language.substructure.map f (S i)) = supr S
source
theorem first_order.language.substructure.map_le_map_iff_of_injective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.injective ⇑f) {S T : L.substructure M} :
first_order.language.substructure.map f S ≤ first_order.language.substructure.map f T ↔ S ≤ T
source
theorem first_order.language.substructure.map_strict_mono_of_injective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.injective ⇑f) :
strict_mono (first_order.language.substructure.map f)
source
def first_order.language.substructure.gi_map_comap {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.surjective ⇑f) :
galois_insertion (first_order.language.substructure.map f) (first_order.language.substructure.comap f)

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

Equations
source
theorem first_order.language.substructure.map_comap_eq_of_surjective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.surjective ⇑f) (S : L.substructure N) :
first_order.language.substructure.map f (first_order.language.substructure.comap f S) = S
source
theorem first_order.language.substructure.map_surjective_of_surjective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.surjective ⇑f) :
function.surjective (first_order.language.substructure.map f)
source
theorem first_order.language.substructure.comap_injective_of_surjective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.surjective ⇑f) :
function.injective (first_order.language.substructure.comap f)
source
theorem first_order.language.substructure.map_inf_comap_of_surjective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.surjective ⇑f) (S T : L.substructure N) :
first_order.language.substructure.map f (first_order.language.substructure.comap f S ⊓ first_order.language.substructure.comap f T) = S ⊓ T
source
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) :
first_order.language.substructure.map f (⨅ (i : ι), first_order.language.substructure.comap f (S i)) = infi S
source
theorem first_order.language.substructure.map_sup_comap_of_surjective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.surjective ⇑f) (S T : L.substructure N) :
first_order.language.substructure.map f (first_order.language.substructure.comap f S ⊔ first_order.language.substructure.comap f T) = S ⊔ T
source
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) :
first_order.language.substructure.map f (⨆ (i : ι), first_order.language.substructure.comap f (S i)) = supr S
source
theorem first_order.language.substructure.comap_le_comap_iff_of_surjective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.surjective ⇑f) {S T : L.substructure N} :
first_order.language.substructure.comap f S ≤ first_order.language.substructure.comap f T ↔ S ≤ T
source
theorem first_order.language.substructure.comap_strict_mono_of_surjective {L : first_order.language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.hom M N} (hf : function.surjective ⇑f) :
strict_mono (first_order.language.substructure.comap f)
source
@[protected, instance]
def first_order.language.substructure.induced_Structure {L : first_order.language} {M : Type w} [L.Structure M] {S : L.substructure M} :
L.Structure ↥S
Equations
source
def first_order.language.substructure.subtype {L : first_order.language} {M : Type w} [L.Structure M] (S : L.substructure M) :
L.embedding ↥S M

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

Equations
source
@[simp]
theorem first_order.language.substructure.coe_subtype {L : first_order.language} {M : Type w} [L.Structure M] (S : L.substructure M) :
⇑(S.subtype) = coe
source
def first_order.language.substructure.top_equiv {L : first_order.language} {M : Type w} [L.Structure M] :
L.equiv ↥⊤ M

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

Equations
source
@[simp]
theorem first_order.language.substructure.coe_top_equiv {L : first_order.language} {M : Type w} [L.Structure M] :
⇑first_order.language.substructure.top_equiv = coe
source
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.

source
def first_order.language.Lhom.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] :
L'.substructure M ↪o L.substructure M

Reduces the language of a substructure along a language hom.

Equations
source
@[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} :
x ∈ ⇑(φ.substructure_reduct) S ↔ x ∈ S
source
@[simp]
theorem first_order.language.Lhom.coe_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] {S : L'.substructure M} :
↑(⇑(φ.substructure_reduct) S) = ↑S
source
def first_order.language.substructure.with_constants {L : first_order.language} {M : Type w} [L.Structure M] (S : L.substructure M) {A : set M} (h : A ⊆ ↑S) :
(L.with_constants ↥A).substructure M

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

Equations
source
@[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 ∈ S.with_constants h ↔ x ∈ S
source
@[simp]
theorem first_order.language.substructure.coe_with_constants {L : first_order.language} {M : Type w} [L.Structure M] {S : L.substructure M} {A : set M} (h : A ⊆ ↑S) :
↑(S.with_constants h) = ↑S
source
@[simp]
theorem first_order.language.substructure.reduct_with_constants {L : first_order.language} {M : Type w} [L.Structure M] {S : L.substructure M} {A : set M} (h : A ⊆ ↑S) :
⇑((L.Lhom_with_constants ↥A).substructure_reduct) (S.with_constants h) = S
source
theorem first_order.language.substructure.subset_closure_with_constants {L : first_order.language} {M : Type w} [L.Structure M] {A s : set M} :
A ⊆ ↑(⇑(first_order.language.substructure.closure (L.with_constants ↥A)) s)
source
theorem first_order.language.substructure.closure_with_constants_eq {L : first_order.language} {M : Type w} [L.Structure M] {A s : set M} :
⇑(first_order.language.substructure.closure (L.with_constants ↥A)) s = (⇑(first_order.language.substructure.closure L) (A ∪ s)).with_constants _
source
@[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 ↑ᾰ
source
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
source
@[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) :
↑(⇑(first_order.language.hom.cod_restrict p f h) c) = ⇑f c
source
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
source
@[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) :
(first_order.language.hom.cod_restrict p g h).comp f = first_order.language.hom.cod_restrict p (g.comp f) _
source
@[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) :
p.subtype.to_hom.comp (first_order.language.hom.cod_restrict p f h) = f
source
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) :
L.substructure N

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

Equations
source
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) = set.range ⇑f
source
@[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
source
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) :
f.range = first_order.language.substructure.map f ⊤
source
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) :
⇑f x ∈ f.range
source
@[simp]
theorem first_order.language.hom.range_id {L : first_order.language} {M : Type w} [L.Structure M] :
(first_order.language.hom.id L M).range = ⊤
source
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) :
(g.comp f).range = first_order.language.substructure.map g f.range
source
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) :
(g.comp f).range ≤ g.range
source
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} :
f.range = ⊤ ↔ function.surjective ⇑f
source
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} :
f.range ≤ p ↔ first_order.language.substructure.comap f p = ⊤
source
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} :
first_order.language.substructure.map f p ≤ f.range
source
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) :
L.substructure M

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

Equations
source
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) :
set.eq_on ⇑f ⇑g ↑(⇑(first_order.language.substructure.closure L) s)

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

source
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
source
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
source
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) :
L.embedding ↥p N

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

Equations
source
@[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) :
⇑(f.dom_restrict p) x = ⇑f ↑x
source
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) :
L.embedding M ↥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
source
@[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) :
↑(⇑(first_order.language.embedding.cod_restrict p f h) x) = ⇑f x
source
@[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) :
(first_order.language.embedding.cod_restrict p g h).comp f = first_order.language.embedding.cod_restrict p (g.comp f) _
source
@[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) :
p.subtype.comp (first_order.language.embedding.cod_restrict p f h) = f
source
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) :
L.equiv ↥s ↥(first_order.language.substructure.map f.to_hom s)

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

Equations
source
@[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) :
↑(⇑(f.substructure_equiv_map p) x) = ⇑f ↑x
source
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) :
L.equiv M ↥(f.to_hom.range)

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

Equations
source
@[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) :
↑(⇑(f.equiv_range) x) = ⇑f x
source
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) :
f.to_hom.range = ⊤
source
def first_order.language.substructure.inclusion {L : first_order.language} {M : Type w} [L.Structure M] {S T : L.substructure M} (h : S ≤ T) :
L.embedding ↥S ↥T

The embedding associated to an inclusion of substructures.

Equations
source
@[simp]
theorem first_order.language.substructure.coe_inclusion {L : first_order.language} {M : Type w} [L.Structure M] {S T : L.substructure M} (h : S ≤ T) :
⇑(first_order.language.substructure.inclusion h) = set.inclusion h
source
theorem first_order.language.substructure.range_subtype {L : first_order.language} {M : Type w} [L.Structure M] (S : L.substructure M) :
S.subtype.to_hom.range = S