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

• A FirstOrder.Language.Substructure is defined so that L.Substructure M is the type of all substructures of the L-structure M.
• FirstOrder.Language.Substructure.closure is defined so that if s : Set M, closure L s is the least substructure of M containing s.
• FirstOrder.Language.Substructure.comap is defined so that s.comap f is the preimage of the substructure s under the homomorphism f, as a substructure.
• FirstOrder.Language.Substructure.map is defined so that s.map f is the image of the substructure s under the homomorphism f, as a substructure.
• FirstOrder.Language.Hom.range is defined so that f.range is the range of the homomorphism f, as a substructure.
• FirstOrder.Language.Hom.domRestrict and FirstOrder.Language.Hom.codRestrict restrict the domain and codomain respectively of first-order homomorphisms to substructures.
• FirstOrder.Language.Embedding.domRestrict and FirstOrder.Language.Embedding.codRestrict restrict the domain and codomain respectively of first-order embeddings to substructures.
• FirstOrder.Language.Substructure.inclusion is the inclusion embedding between substructures.

Main Results

• L.Substructure M forms a CompleteLattice.

def FirstOrder.Language.ClosedUnder {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {n : ℕ} (f : FirstOrder.Language.Functions L n) (s : Set M) : Prop

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

@[simp]

theorem FirstOrder.Language.closedUnder_univ (L : FirstOrder.Language) {M : Type w} [FirstOrder.Language.Structure L M] {n : ℕ} (f : FirstOrder.Language.Functions L n) : FirstOrder.Language.ClosedUnder f Set.univ

theorem FirstOrder.Language.ClosedUnder.inter {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {n : ℕ} {f : FirstOrder.Language.Functions L n} {s : Set M} {t : Set M} (hs : FirstOrder.Language.ClosedUnder f s) (ht : FirstOrder.Language.ClosedUnder f t) : FirstOrder.Language.ClosedUnder f (s ∩ t)

theorem FirstOrder.Language.ClosedUnder.inf {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {n : ℕ} {f : FirstOrder.Language.Functions L n} {s : Set M} {t : Set M} (hs : FirstOrder.Language.ClosedUnder f s) (ht : FirstOrder.Language.ClosedUnder f t) : FirstOrder.Language.ClosedUnder f (s ⊓ t)

theorem FirstOrder.Language.ClosedUnder.sInf {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {n : ℕ} {f : FirstOrder.Language.Functions L n} {S : Set (Set M)} (hS : ∀ (s : Set M), s ∈ S → FirstOrder.Language.ClosedUnder f s) : FirstOrder.Language.ClosedUnder f (sInf S)

structure FirstOrder.Language.Substructure (L : FirstOrder.Language) (M : Type w) [FirstOrder.Language.Structure L M] : Type w

• carrier : Set M
• fun_mem : ∀ {n : ℕ} (f : FirstOrder.Language.Functions L n), FirstOrder.Language.ClosedUnder f ↑s

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

instance FirstOrder.Language.Substructure.instSetLike {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] : SetLike (FirstOrder.Language.Substructure L M) M

def FirstOrder.Language.Substructure.Simps.coe {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) : Set M

See Note [custom simps projection]

@[simp]

theorem FirstOrder.Language.Substructure.mem_carrier {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {s : FirstOrder.Language.Substructure L M} {x : M} : x ∈ ↑s ↔ x ∈ s

theorem FirstOrder.Language.Substructure.ext {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.Substructure L M} {T : FirstOrder.Language.Substructure L M} (h : ∀ (x : M), x ∈ S ↔ x ∈ T) : S = T

Two substructures are equal if they have the same elements.

def FirstOrder.Language.Substructure.copy {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) (s : Set M) (hs : s = ↑S) : FirstOrder.Language.Substructure L M

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

theorem FirstOrder.Language.Term.realize_mem {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.Substructure L M} {α : Type u_3} (t : FirstOrder.Language.Term L α) (xs : α → M) (h : ∀ (a : α), xs a ∈ S) : FirstOrder.Language.Term.realize xs t ∈ S

@[simp]

theorem FirstOrder.Language.Substructure.coe_copy {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.Substructure L M} {s : Set M} (hs : s = ↑S) : ↑(FirstOrder.Language.Substructure.copy S s hs) = s

theorem FirstOrder.Language.Substructure.copy_eq {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.Substructure L M} {s : Set M} (hs : s = ↑S) : FirstOrder.Language.Substructure.copy S s hs = S

theorem FirstOrder.Language.Substructure.constants_mem {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.Substructure L M} (c : FirstOrder.Language.Constants L) : ↑c ∈ S

instance FirstOrder.Language.Substructure.instTop {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] : Top (FirstOrder.Language.Substructure L M)

The substructure M of the structure M.

instance FirstOrder.Language.Substructure.instInhabited {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] : Inhabited (FirstOrder.Language.Substructure L M)

@[simp]

theorem FirstOrder.Language.Substructure.mem_top {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (x : M) : x ∈ ⊤

@[simp]

theorem FirstOrder.Language.Substructure.coe_top {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] : ↑⊤ = Set.univ

instance FirstOrder.Language.Substructure.instInf {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] : Inf (FirstOrder.Language.Substructure L M)

The inf of two substructures is their intersection.

@[simp]

theorem FirstOrder.Language.Substructure.coe_inf {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (p : FirstOrder.Language.Substructure L M) (p' : FirstOrder.Language.Substructure L M) : ↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem FirstOrder.Language.Substructure.mem_inf {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {p : FirstOrder.Language.Substructure L M} {p' : FirstOrder.Language.Substructure L M} {x : M} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

instance FirstOrder.Language.Substructure.instInfSet {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] : InfSet (FirstOrder.Language.Substructure L M)

@[simp]

theorem FirstOrder.Language.Substructure.coe_sInf {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (S : Set (FirstOrder.Language.Substructure L M)) : ↑(sInf S) = ⋂ (s : FirstOrder.Language.Substructure L M) (_ : s ∈ S), ↑s

theorem FirstOrder.Language.Substructure.mem_sInf {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : Set (FirstOrder.Language.Substructure L M)} {x : M} : x ∈ sInf S ↔ ∀ (p : FirstOrder.Language.Substructure L M), p ∈ S → x ∈ p

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)

instance FirstOrder.Language.Substructure.instCompleteLattice {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] : CompleteLattice (FirstOrder.Language.Substructure L M)

Substructures of a structure form a complete lattice.

def FirstOrder.Language.Substructure.closure (L : FirstOrder.Language) {M : Type w} [FirstOrder.Language.Structure L M] : LowerAdjoint SetLike.coe

The L.Substructure generated by a set.

theorem FirstOrder.Language.Substructure.mem_closure {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {s : Set M} {x : M} : x ∈ LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s ↔ ∀ (S : FirstOrder.Language.Substructure L M), s ⊆ ↑S → x ∈ S

@[simp]

theorem FirstOrder.Language.Substructure.subset_closure {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {s : Set M} : s ⊆ ↑(LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s)

The substructure generated by a set includes the set.

theorem FirstOrder.Language.Substructure.not_mem_of_not_mem_closure {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {s : Set M} {P : M} (hP : ¬P ∈ LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s) : ¬P ∈ s

@[simp]

theorem FirstOrder.Language.Substructure.closed {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) : LowerAdjoint.closed (FirstOrder.Language.Substructure.closure L) ↑S

@[simp]

theorem FirstOrder.Language.Substructure.closure_le {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.Substructure L M} {s : Set M} : LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s ≤ S ↔ s ⊆ ↑S

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

theorem FirstOrder.Language.Substructure.closure_mono {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] ⦃s : Set M⦄ ⦃t : Set M⦄ (h : s ⊆ t) : LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s ≤ LowerAdjoint.toFun (FirstOrder.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.

theorem FirstOrder.Language.Substructure.closure_eq_of_le {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.Substructure L M} {s : Set M} (h₁ : s ⊆ ↑S) (h₂ : S ≤ LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s) : LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s = S

theorem FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {s : Set M} : ↑(LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s) = Set.range (FirstOrder.Language.Term.realize Subtype.val)

instance FirstOrder.Language.Substructure.small_closure {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {s : Set M} [Small.{u, w} ↑s] : Small.{u, w} { x // x ∈ LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s }

theorem FirstOrder.Language.Substructure.mem_closure_iff_exists_term {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {s : Set M} {x : M} : x ∈ LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s ↔ ∃ t, FirstOrder.Language.Term.realize Subtype.val t = x

theorem FirstOrder.Language.Substructure.lift_card_closure_le_card_term {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {s : Set M} : Cardinal.lift.{max u w, w} (Cardinal.mk { x // x ∈ LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s }) ≤ Cardinal.mk (FirstOrder.Language.Term L ↑s)

theorem FirstOrder.Language.Substructure.lift_card_closure_le {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {s : Set M} : Cardinal.lift.{u, w} (Cardinal.mk { x // x ∈ LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s }) ≤ max Cardinal.aleph0 (Cardinal.lift.{u, w} (Cardinal.mk ↑s) + Cardinal.lift.{w, u} (Cardinal.mk ((i : ℕ) × FirstOrder.Language.Functions L i)))

theorem Set.Countable.substructure_closure (L : FirstOrder.Language) {M : Type w} [FirstOrder.Language.Structure L M] {s : Set M} [Countable ((l : ℕ) × FirstOrder.Language.Functions L l)] (h : Set.Countable s) : Countable { x // x ∈ LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s }

theorem FirstOrder.Language.Substructure.closure_induction {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {s : Set M} {p : M → Prop} {x : M} (h : x ∈ LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s) (Hs : (x : M) → x ∈ s → p x) (Hfun : ∀ {n : ℕ} (f : FirstOrder.Language.Functions L n), FirstOrder.Language.ClosedUnder f (setOf 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 FirstOrder.Language.Substructure.dense_induction {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {p : M → Prop} (x : M) {s : Set M} (hs : LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s = ⊤) (Hs : (x : M) → x ∈ s → p x) (Hfun : ∀ {n : ℕ} (f : FirstOrder.Language.Functions L n), FirstOrder.Language.ClosedUnder f (setOf 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.

def FirstOrder.Language.Substructure.gi (L : FirstOrder.Language) (M : Type w) [FirstOrder.Language.Structure L M] : GaloisInsertion (FirstOrder.Language.Substructure.closure L).toFun SetLike.coe

closure forms a Galois insertion with the coercion to set.

@[simp]

theorem FirstOrder.Language.Substructure.closure_eq {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) : LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) ↑S = S

Closure of a substructure S equals S.

@[simp]

theorem FirstOrder.Language.Substructure.closure_empty {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] : LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) ∅ = ⊥

@[simp]

theorem FirstOrder.Language.Substructure.closure_univ {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] : LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) Set.univ = ⊤

theorem FirstOrder.Language.Substructure.closure_union {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (s : Set M) (t : Set M) : LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) (s ∪ t) = LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s ⊔ LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) t

theorem FirstOrder.Language.Substructure.closure_unionᵢ {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {ι : Sort u_3} (s : ι → Set M) : LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) (⋃ (i : ι), s i) = ⨆ (i : ι), LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) (s i)

instance FirstOrder.Language.Substructure.small_bot {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] : Small.{u, w} { x // x ∈ ⊥ }

comap and map

@[simp]

theorem FirstOrder.Language.Substructure.comap_coe {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.Hom L M N) (S : FirstOrder.Language.Substructure L N) : ↑(FirstOrder.Language.Substructure.comap φ S) = ↑φ ⁻¹' ↑S

def FirstOrder.Language.Substructure.comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.Hom L M N) (S : FirstOrder.Language.Substructure L N) : FirstOrder.Language.Substructure L M

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

@[simp]

theorem FirstOrder.Language.Substructure.mem_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {S : FirstOrder.Language.Substructure L N} {f : FirstOrder.Language.Hom L M N} {x : M} : x ∈ FirstOrder.Language.Substructure.comap f S ↔ ↑f x ∈ S

theorem FirstOrder.Language.Substructure.comap_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] [FirstOrder.Language.Structure L P] (S : FirstOrder.Language.Substructure L P) (g : FirstOrder.Language.Hom L N P) (f : FirstOrder.Language.Hom L M N) : FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.comap g S) = FirstOrder.Language.Substructure.comap (FirstOrder.Language.Hom.comp g f) S

@[simp]

theorem FirstOrder.Language.Substructure.comap_id {L : FirstOrder.Language} {P : Type u_2} [FirstOrder.Language.Structure L P] (S : FirstOrder.Language.Substructure L P) : FirstOrder.Language.Substructure.comap (FirstOrder.Language.Hom.id L P) S = S

@[simp]

theorem FirstOrder.Language.Substructure.map_coe {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.Hom L M N) (S : FirstOrder.Language.Substructure L M) : ↑(FirstOrder.Language.Substructure.map φ S) = ↑φ '' ↑S

def FirstOrder.Language.Substructure.map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.Hom L M N) (S : FirstOrder.Language.Substructure L M) : FirstOrder.Language.Substructure L N

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

@[simp]

theorem FirstOrder.Language.Substructure.mem_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} {S : FirstOrder.Language.Substructure L M} {y : N} : y ∈ FirstOrder.Language.Substructure.map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y

theorem FirstOrder.Language.Substructure.mem_map_of_mem {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) {S : FirstOrder.Language.Substructure L M} {x : M} (hx : x ∈ S) : ↑f x ∈ FirstOrder.Language.Substructure.map f S

theorem FirstOrder.Language.Substructure.apply_coe_mem_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) (S : FirstOrder.Language.Substructure L M) (x : { x // x ∈ S }) : ↑f ↑x ∈ FirstOrder.Language.Substructure.map f S

theorem FirstOrder.Language.Substructure.map_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] [FirstOrder.Language.Structure L P] (S : FirstOrder.Language.Substructure L M) (g : FirstOrder.Language.Hom L N P) (f : FirstOrder.Language.Hom L M N) : FirstOrder.Language.Substructure.map g (FirstOrder.Language.Substructure.map f S) = FirstOrder.Language.Substructure.map (FirstOrder.Language.Hom.comp g f) S

theorem FirstOrder.Language.Substructure.map_le_iff_le_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} {S : FirstOrder.Language.Substructure L M} {T : FirstOrder.Language.Substructure L N} : FirstOrder.Language.Substructure.map f S ≤ T ↔ S ≤ FirstOrder.Language.Substructure.comap f T

theorem FirstOrder.Language.Substructure.gc_map_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) : GaloisConnection (FirstOrder.Language.Substructure.map f) (FirstOrder.Language.Substructure.comap f)

theorem FirstOrder.Language.Substructure.map_le_of_le_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (S : FirstOrder.Language.Substructure L M) {T : FirstOrder.Language.Substructure L N} {f : FirstOrder.Language.Hom L M N} : S ≤ FirstOrder.Language.Substructure.comap f T → FirstOrder.Language.Substructure.map f S ≤ T

theorem FirstOrder.Language.Substructure.le_comap_of_map_le {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (S : FirstOrder.Language.Substructure L M) {T : FirstOrder.Language.Substructure L N} {f : FirstOrder.Language.Hom L M N} : FirstOrder.Language.Substructure.map f S ≤ T → S ≤ FirstOrder.Language.Substructure.comap f T

theorem FirstOrder.Language.Substructure.le_comap_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (S : FirstOrder.Language.Substructure L M) {f : FirstOrder.Language.Hom L M N} : S ≤ FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f S)

theorem FirstOrder.Language.Substructure.map_comap_le {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {S : FirstOrder.Language.Substructure L N} {f : FirstOrder.Language.Hom L M N} : FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S) ≤ S

theorem FirstOrder.Language.Substructure.monotone_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} : Monotone (FirstOrder.Language.Substructure.map f)

theorem FirstOrder.Language.Substructure.monotone_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} : Monotone (FirstOrder.Language.Substructure.comap f)

@[simp]

theorem FirstOrder.Language.Substructure.map_comap_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (S : FirstOrder.Language.Substructure L M) {f : FirstOrder.Language.Hom L M N} : FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f S)) = FirstOrder.Language.Substructure.map f S

@[simp]

theorem FirstOrder.Language.Substructure.comap_map_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {S : FirstOrder.Language.Substructure L N} {f : FirstOrder.Language.Hom L M N} : FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S)) = FirstOrder.Language.Substructure.comap f S

theorem FirstOrder.Language.Substructure.map_sup {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (S : FirstOrder.Language.Substructure L M) (T : FirstOrder.Language.Substructure L M) (f : FirstOrder.Language.Hom L M N) : FirstOrder.Language.Substructure.map f (S ⊔ T) = FirstOrder.Language.Substructure.map f S ⊔ FirstOrder.Language.Substructure.map f T

theorem FirstOrder.Language.Substructure.map_iSup {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {ι : Sort u_3} (f : FirstOrder.Language.Hom L M N) (s : ι → FirstOrder.Language.Substructure L M) : FirstOrder.Language.Substructure.map f (iSup s) = ⨆ (i : ι), FirstOrder.Language.Substructure.map f (s i)

theorem FirstOrder.Language.Substructure.comap_inf {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (S : FirstOrder.Language.Substructure L N) (T : FirstOrder.Language.Substructure L N) (f : FirstOrder.Language.Hom L M N) : FirstOrder.Language.Substructure.comap f (S ⊓ T) = FirstOrder.Language.Substructure.comap f S ⊓ FirstOrder.Language.Substructure.comap f T

theorem FirstOrder.Language.Substructure.comap_iInf {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {ι : Sort u_3} (f : FirstOrder.Language.Hom L M N) (s : ι → FirstOrder.Language.Substructure L N) : FirstOrder.Language.Substructure.comap f (iInf s) = ⨅ (i : ι), FirstOrder.Language.Substructure.comap f (s i)

@[simp]

theorem FirstOrder.Language.Substructure.map_bot {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) : FirstOrder.Language.Substructure.map f ⊥ = ⊥

@[simp]

theorem FirstOrder.Language.Substructure.comap_top {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) : FirstOrder.Language.Substructure.comap f ⊤ = ⊤

@[simp]

theorem FirstOrder.Language.Substructure.map_id {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) : FirstOrder.Language.Substructure.map (FirstOrder.Language.Hom.id L M) S = S

theorem FirstOrder.Language.Substructure.map_closure {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) (s : Set M) : FirstOrder.Language.Substructure.map f (LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s) = LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) (↑f '' s)

@[simp]

theorem FirstOrder.Language.Substructure.closure_image {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {s : Set M} (f : FirstOrder.Language.Hom L M N) : LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) (↑f '' s) = FirstOrder.Language.Substructure.map f (LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s)

def FirstOrder.Language.Substructure.gciMapComap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Injective ↑f) : GaloisCoinsertion (FirstOrder.Language.Substructure.map f) (FirstOrder.Language.Substructure.comap f)

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

theorem FirstOrder.Language.Substructure.comap_map_eq_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Injective ↑f) (S : FirstOrder.Language.Substructure L M) : FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f S) = S

theorem FirstOrder.Language.Substructure.comap_surjective_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Injective ↑f) : Function.Surjective (FirstOrder.Language.Substructure.comap f)

theorem FirstOrder.Language.Substructure.map_injective_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Injective ↑f) : Function.Injective (FirstOrder.Language.Substructure.map f)

theorem FirstOrder.Language.Substructure.comap_inf_map_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Injective ↑f) (S : FirstOrder.Language.Substructure L M) (T : FirstOrder.Language.Substructure L M) : FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f S ⊓ FirstOrder.Language.Substructure.map f T) = S ⊓ T

theorem FirstOrder.Language.Substructure.comap_iInf_map_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {ι : Type u_3} {f : FirstOrder.Language.Hom L M N} (hf : Function.Injective ↑f) (S : ι → FirstOrder.Language.Substructure L M) : FirstOrder.Language.Substructure.comap f (⨅ (i : ι), FirstOrder.Language.Substructure.map f (S i)) = iInf S

theorem FirstOrder.Language.Substructure.comap_sup_map_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Injective ↑f) (S : FirstOrder.Language.Substructure L M) (T : FirstOrder.Language.Substructure L M) : FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f S ⊔ FirstOrder.Language.Substructure.map f T) = S ⊔ T

theorem FirstOrder.Language.Substructure.comap_iSup_map_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {ι : Type u_3} {f : FirstOrder.Language.Hom L M N} (hf : Function.Injective ↑f) (S : ι → FirstOrder.Language.Substructure L M) : FirstOrder.Language.Substructure.comap f (⨆ (i : ι), FirstOrder.Language.Substructure.map f (S i)) = iSup S

theorem FirstOrder.Language.Substructure.map_le_map_iff_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Injective ↑f) {S : FirstOrder.Language.Substructure L M} {T : FirstOrder.Language.Substructure L M} : FirstOrder.Language.Substructure.map f S ≤ FirstOrder.Language.Substructure.map f T ↔ S ≤ T

theorem FirstOrder.Language.Substructure.map_strictMono_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Injective ↑f) : StrictMono (FirstOrder.Language.Substructure.map f)

def FirstOrder.Language.Substructure.giMapComap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Surjective ↑f) : GaloisInsertion (FirstOrder.Language.Substructure.map f) (FirstOrder.Language.Substructure.comap f)

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

theorem FirstOrder.Language.Substructure.map_comap_eq_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Surjective ↑f) (S : FirstOrder.Language.Substructure L N) : FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S) = S

theorem FirstOrder.Language.Substructure.map_surjective_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Surjective ↑f) : Function.Surjective (FirstOrder.Language.Substructure.map f)

theorem FirstOrder.Language.Substructure.comap_injective_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Surjective ↑f) : Function.Injective (FirstOrder.Language.Substructure.comap f)

theorem FirstOrder.Language.Substructure.map_inf_comap_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Surjective ↑f) (S : FirstOrder.Language.Substructure L N) (T : FirstOrder.Language.Substructure L N) : FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S ⊓ FirstOrder.Language.Substructure.comap f T) = S ⊓ T

theorem FirstOrder.Language.Substructure.map_iInf_comap_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {ι : Type u_3} {f : FirstOrder.Language.Hom L M N} (hf : Function.Surjective ↑f) (S : ι → FirstOrder.Language.Substructure L N) : FirstOrder.Language.Substructure.map f (⨅ (i : ι), FirstOrder.Language.Substructure.comap f (S i)) = iInf S

theorem FirstOrder.Language.Substructure.map_sup_comap_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Surjective ↑f) (S : FirstOrder.Language.Substructure L N) (T : FirstOrder.Language.Substructure L N) : FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S ⊔ FirstOrder.Language.Substructure.comap f T) = S ⊔ T

theorem FirstOrder.Language.Substructure.map_iSup_comap_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {ι : Type u_3} {f : FirstOrder.Language.Hom L M N} (hf : Function.Surjective ↑f) (S : ι → FirstOrder.Language.Substructure L N) : FirstOrder.Language.Substructure.map f (⨆ (i : ι), FirstOrder.Language.Substructure.comap f (S i)) = iSup S

theorem FirstOrder.Language.Substructure.comap_le_comap_iff_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Surjective ↑f) {S : FirstOrder.Language.Substructure L N} {T : FirstOrder.Language.Substructure L N} : FirstOrder.Language.Substructure.comap f S ≤ FirstOrder.Language.Substructure.comap f T ↔ S ≤ T

theorem FirstOrder.Language.Substructure.comap_strictMono_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} (hf : Function.Surjective ↑f) : StrictMono (FirstOrder.Language.Substructure.comap f)

instance FirstOrder.Language.Substructure.inducedStructure {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.Substructure L M} : FirstOrder.Language.Structure L { x // x ∈ S }

def FirstOrder.Language.Substructure.subtype {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) : FirstOrder.Language.Embedding L { x // x ∈ S } M

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

@[simp]

theorem FirstOrder.Language.Substructure.coeSubtype {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) : ↑(FirstOrder.Language.Substructure.subtype S) = Subtype.val

def FirstOrder.Language.Substructure.topEquiv {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] : FirstOrder.Language.Equiv L { x // x ∈ ⊤ } M

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

@[simp]

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

theorem FirstOrder.Language.Substructure.closure_induction' {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (s : Set M) {p : (x : M) → x ∈ LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s → Prop} (Hs : (x : M) → (h : x ∈ s) → p x (_ : x ∈ ↑(LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s))) (Hfun : ∀ {n : ℕ} (f : FirstOrder.Language.Functions L n), FirstOrder.Language.ClosedUnder f {x | ∃ hx, p x hx}) {x : M} (hx : x ∈ LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s) : p x hx

A dependent version of Substructure.closure_induction.

def FirstOrder.Language.LHom.substructureReduct {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {L' : FirstOrder.Language} [FirstOrder.Language.Structure L' M] (φ : L →ᴸ L') [FirstOrder.Language.LHom.IsExpansionOn φ M] : FirstOrder.Language.Substructure L' M ↪o FirstOrder.Language.Substructure L M

Reduces the language of a substructure along a language hom.

@[simp]

theorem FirstOrder.Language.LHom.mem_substructureReduct {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {L' : FirstOrder.Language} [FirstOrder.Language.Structure L' M] (φ : L →ᴸ L') [FirstOrder.Language.LHom.IsExpansionOn φ M] {x : M} {S : FirstOrder.Language.Substructure L' M} : x ∈ ↑(FirstOrder.Language.LHom.substructureReduct φ) S ↔ x ∈ S

@[simp]

theorem FirstOrder.Language.LHom.coe_substructureReduct {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {L' : FirstOrder.Language} [FirstOrder.Language.Structure L' M] (φ : L →ᴸ L') [FirstOrder.Language.LHom.IsExpansionOn φ M] {S : FirstOrder.Language.Substructure L' M} : ↑(↑(FirstOrder.Language.LHom.substructureReduct φ) S) = ↑S

def FirstOrder.Language.Substructure.withConstants {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) {A : Set M} (h : A ⊆ ↑S) : FirstOrder.Language.Substructure (FirstOrder.Language.withConstants L ↑A) M

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

@[simp]

theorem FirstOrder.Language.Substructure.mem_withConstants {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.Substructure L M} {A : Set M} (h : A ⊆ ↑S) {x : M} : x ∈ FirstOrder.Language.Substructure.withConstants S h ↔ x ∈ S

@[simp]

theorem FirstOrder.Language.Substructure.coe_withConstants {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.Substructure L M} {A : Set M} (h : A ⊆ ↑S) : ↑(FirstOrder.Language.Substructure.withConstants S h) = ↑S

@[simp]

theorem FirstOrder.Language.Substructure.reduct_withConstants {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.Substructure L M} {A : Set M} (h : A ⊆ ↑S) : ↑(FirstOrder.Language.LHom.substructureReduct (FirstOrder.Language.lhomWithConstants L ↑A)) (FirstOrder.Language.Substructure.withConstants S h) = S

theorem FirstOrder.Language.Substructure.subset_closure_withConstants {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {s : Set M} : A ⊆ ↑(LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure (FirstOrder.Language.withConstants L ↑A)) s)

theorem FirstOrder.Language.Substructure.closure_withConstants_eq {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {s : Set M} : LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure (FirstOrder.Language.withConstants L ↑A)) s = FirstOrder.Language.Substructure.withConstants (LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) (A ∪ s)) (_ : A ⊆ ↑(LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) (A ∪ s)))

@[simp]

theorem FirstOrder.Language.Hom.domRestrict_toFun {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) (p : FirstOrder.Language.Substructure L M) : ∀ (a : { x // x ∈ p }), ↑(FirstOrder.Language.Hom.domRestrict f p) a = ↑f ↑a

def FirstOrder.Language.Hom.domRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) (p : FirstOrder.Language.Substructure L M) : FirstOrder.Language.Hom L { x // x ∈ p } N

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

@[simp]

theorem FirstOrder.Language.Hom.codRestrict_toFun_coe {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (p : FirstOrder.Language.Substructure L N) (f : FirstOrder.Language.Hom L M N) (h : ∀ (c : M), ↑f c ∈ p) (c : M) : ↑(↑(FirstOrder.Language.Hom.codRestrict p f h) c) = ↑f c

def FirstOrder.Language.Hom.codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (p : FirstOrder.Language.Substructure L N) (f : FirstOrder.Language.Hom L M N) (h : ∀ (c : M), ↑f c ∈ p) : FirstOrder.Language.Hom L M { x // x ∈ p }

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

@[simp]

theorem FirstOrder.Language.Hom.comp_codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] [FirstOrder.Language.Structure L P] (f : FirstOrder.Language.Hom L M N) (g : FirstOrder.Language.Hom L N P) (p : FirstOrder.Language.Substructure L P) (h : ∀ (b : N), ↑g b ∈ p) : FirstOrder.Language.Hom.comp (FirstOrder.Language.Hom.codRestrict p g h) f = FirstOrder.Language.Hom.codRestrict p (FirstOrder.Language.Hom.comp g f) fun x => h (↑f x)

@[simp]

theorem FirstOrder.Language.Hom.subtype_comp_codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) (p : FirstOrder.Language.Substructure L N) (h : ∀ (b : M), ↑f b ∈ p) : FirstOrder.Language.Hom.comp (FirstOrder.Language.Embedding.toHom (FirstOrder.Language.Substructure.subtype p)) (FirstOrder.Language.Hom.codRestrict p f h) = f

def FirstOrder.Language.Hom.range {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) : FirstOrder.Language.Substructure L N

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

theorem FirstOrder.Language.Hom.range_coe {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) : ↑(FirstOrder.Language.Hom.range f) = Set.range ↑f

@[simp]

theorem FirstOrder.Language.Hom.mem_range {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} {x : N} : x ∈ FirstOrder.Language.Hom.range f ↔ ∃ y, ↑f y = x

theorem FirstOrder.Language.Hom.range_eq_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) : FirstOrder.Language.Hom.range f = FirstOrder.Language.Substructure.map f ⊤

theorem FirstOrder.Language.Hom.mem_range_self {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) (x : M) : ↑f x ∈ FirstOrder.Language.Hom.range f

@[simp]

theorem FirstOrder.Language.Hom.range_id {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] : FirstOrder.Language.Hom.range (FirstOrder.Language.Hom.id L M) = ⊤

theorem FirstOrder.Language.Hom.range_comp {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] [FirstOrder.Language.Structure L P] (f : FirstOrder.Language.Hom L M N) (g : FirstOrder.Language.Hom L N P) : FirstOrder.Language.Hom.range (FirstOrder.Language.Hom.comp g f) = FirstOrder.Language.Substructure.map g (FirstOrder.Language.Hom.range f)

theorem FirstOrder.Language.Hom.range_comp_le_range {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] [FirstOrder.Language.Structure L P] (f : FirstOrder.Language.Hom L M N) (g : FirstOrder.Language.Hom L N P) : FirstOrder.Language.Hom.range (FirstOrder.Language.Hom.comp g f) ≤ FirstOrder.Language.Hom.range g

theorem FirstOrder.Language.Hom.range_eq_top {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} : FirstOrder.Language.Hom.range f = ⊤ ↔ Function.Surjective ↑f

theorem FirstOrder.Language.Hom.range_le_iff_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} {p : FirstOrder.Language.Substructure L N} : FirstOrder.Language.Hom.range f ≤ p ↔ FirstOrder.Language.Substructure.comap f p = ⊤

theorem FirstOrder.Language.Hom.map_le_range {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} {p : FirstOrder.Language.Substructure L M} : FirstOrder.Language.Substructure.map f p ≤ FirstOrder.Language.Hom.range f

def FirstOrder.Language.Hom.eqLocus {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) (g : FirstOrder.Language.Hom L M N) : FirstOrder.Language.Substructure L M

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

theorem FirstOrder.Language.Hom.eqOn_closure {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} {g : FirstOrder.Language.Hom L M N} {s : Set M} (h : Set.EqOn (↑f) (↑g) s) : Set.EqOn ↑f ↑g ↑(LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s)

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

theorem FirstOrder.Language.Hom.eq_of_eqOn_top {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} {g : FirstOrder.Language.Hom L M N} (h : Set.EqOn ↑f ↑g ↑⊤) : f = g

theorem FirstOrder.Language.Hom.eq_of_eqOn_dense {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {s : Set M} (hs : LowerAdjoint.toFun (FirstOrder.Language.Substructure.closure L) s = ⊤) {f : FirstOrder.Language.Hom L M N} {g : FirstOrder.Language.Hom L M N} (h : Set.EqOn (↑f) (↑g) s) : f = g

def FirstOrder.Language.Embedding.domRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) (p : FirstOrder.Language.Substructure L M) : FirstOrder.Language.Embedding L { x // x ∈ p } N

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

@[simp]

theorem FirstOrder.Language.Embedding.domRestrict_apply {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) (p : FirstOrder.Language.Substructure L M) (x : { x // x ∈ p }) : ↑(FirstOrder.Language.Embedding.domRestrict f p) x = ↑f ↑x

def FirstOrder.Language.Embedding.codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (p : FirstOrder.Language.Substructure L N) (f : FirstOrder.Language.Embedding L M N) (h : ∀ (c : M), ↑f c ∈ p) : FirstOrder.Language.Embedding L M { x // x ∈ p }

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

@[simp]

theorem FirstOrder.Language.Embedding.codRestrict_apply {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (p : FirstOrder.Language.Substructure L N) (f : FirstOrder.Language.Embedding L M N) {h : ∀ (c : M), ↑f c ∈ p} (x : M) : ↑(↑(FirstOrder.Language.Embedding.codRestrict p f h) x) = ↑f x

@[simp]

theorem FirstOrder.Language.Embedding.comp_codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] [FirstOrder.Language.Structure L P] (f : FirstOrder.Language.Embedding L M N) (g : FirstOrder.Language.Embedding L N P) (p : FirstOrder.Language.Substructure L P) (h : ∀ (b : N), ↑g b ∈ p) : FirstOrder.Language.Embedding.comp (FirstOrder.Language.Embedding.codRestrict p g h) f = FirstOrder.Language.Embedding.codRestrict p (FirstOrder.Language.Embedding.comp g f) fun x => h (↑f x)

@[simp]

theorem FirstOrder.Language.Embedding.subtype_comp_codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) (p : FirstOrder.Language.Substructure L N) (h : ∀ (b : M), ↑f b ∈ p) : FirstOrder.Language.Embedding.comp (FirstOrder.Language.Substructure.subtype p) (FirstOrder.Language.Embedding.codRestrict p f h) = f

noncomputable def FirstOrder.Language.Embedding.substructureEquivMap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) (s : FirstOrder.Language.Substructure L M) : FirstOrder.Language.Equiv L { x // x ∈ s } { x // x ∈ FirstOrder.Language.Substructure.map (FirstOrder.Language.Embedding.toHom f) s }

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

@[simp]

theorem FirstOrder.Language.Embedding.substructureEquivMap_apply {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) (p : FirstOrder.Language.Substructure L M) (x : { x // x ∈ p }) : ↑(↑(FirstOrder.Language.Embedding.substructureEquivMap f p) x) = ↑f ↑x

noncomputable def FirstOrder.Language.Embedding.equivRange {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) : FirstOrder.Language.Equiv L M { x // x ∈ FirstOrder.Language.Hom.range (FirstOrder.Language.Embedding.toHom f) }

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

@[simp]

theorem FirstOrder.Language.Embedding.equivRange_apply {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) (x : M) : ↑(↑(FirstOrder.Language.Embedding.equivRange f) x) = ↑f x

theorem FirstOrder.Language.Equiv.toHom_range {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Equiv L M N) : FirstOrder.Language.Hom.range (FirstOrder.Language.Equiv.toHom f) = ⊤

def FirstOrder.Language.Substructure.inclusion {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.Substructure L M} {T : FirstOrder.Language.Substructure L M} (h : S ≤ T) : FirstOrder.Language.Embedding L { x // x ∈ S } { x // x ∈ T }

The embedding associated to an inclusion of substructures.

@[simp]

theorem FirstOrder.Language.Substructure.coe_inclusion {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.Substructure L M} {T : FirstOrder.Language.Substructure L M} (h : S ≤ T) : ↑(FirstOrder.Language.Substructure.inclusion h) = Set.inclusion h

theorem FirstOrder.Language.Substructure.range_subtype {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) : FirstOrder.Language.Hom.range (FirstOrder.Language.Embedding.toHom (FirstOrder.Language.Substructure.subtype S)) = S