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 : L.Functions n) (s : Set M) : Prop

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

Equations

• FirstOrder.Language.ClosedUnder f s = ∀ (x : Fin n → M), (∀ (i : Fin n), x i ∈ s) → FirstOrder.Language.Structure.funMap f x ∈ s

@[simp]

theorem FirstOrder.Language.closedUnder_univ (L : FirstOrder.Language) {M : Type w} [FirstOrder.Language.Structure L M] {n : ℕ} (f : L.Functions 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 : L.Functions 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 : L.Functions 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 : L.Functions n} {S : Set (Set M)} (hS : ∀ 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

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

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

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

Equations

• FirstOrder.Language.Substructure.instSetLike = { coe := FirstOrder.Language.Substructure.carrier, coe_injective' := ⋯ }

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]

Equations

• FirstOrder.Language.Substructure.Simps.coe S = ↑S

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

Equations

• FirstOrder.Language.Substructure.copy S s hs = { carrier := s, fun_mem := ⋯ }

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.

Equations

• FirstOrder.Language.Substructure.instTop = { top := { carrier := Set.univ, fun_mem := ⋯ } }

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

Equations

• FirstOrder.Language.Substructure.instInhabited = { default := ⊤ }

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

Equations

• FirstOrder.Language.Substructure.instInf = { inf := fun (S₁ S₂ : FirstOrder.Language.Substructure L M) => { carrier := ↑S₁ ∩ ↑S₂, fun_mem := ⋯ } }

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

Equations

• FirstOrder.Language.Substructure.instInfSet = { sInf := fun (s : Set (FirstOrder.Language.Substructure L M)) => { carrier := ⋂ t ∈ s, ↑t, fun_mem := ⋯ } }

@[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 ∈ 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 ∈ 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.

Equations

• FirstOrder.Language.Substructure.instCompleteLattice = let __src := completeLatticeOfInf (FirstOrder.Language.Substructure L M) ⋯; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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.

Equations

• FirstOrder.Language.Substructure.closure L = { toFun := fun (s : Set M) => sInf {S : FirstOrder.Language.Substructure L M | s ⊆ ↑S}, gc' := ⋯ }

theorem FirstOrder.Language.Substructure.mem_closure {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {s : Set M} {x : M} : x ∈ (FirstOrder.Language.Substructure.closure L).toFun 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 ⊆ ↑((FirstOrder.Language.Substructure.closure L).toFun 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 ∉ (FirstOrder.Language.Substructure.closure L).toFun 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} : (FirstOrder.Language.Substructure.closure L).toFun 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) : (FirstOrder.Language.Substructure.closure L).toFun s ≤ (FirstOrder.Language.Substructure.closure L).toFun 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 ≤ (FirstOrder.Language.Substructure.closure L).toFun s) : (FirstOrder.Language.Substructure.closure L).toFun 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} : ↑((FirstOrder.Language.Substructure.closure L).toFun 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} ↥((FirstOrder.Language.Substructure.closure L).toFun s)

Equations

• ⋯ = ⋯

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 ∈ (FirstOrder.Language.Substructure.closure L).toFun s ↔ ∃ (t : FirstOrder.Language.Term L ↑s), 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 ↥((FirstOrder.Language.Substructure.closure L).toFun 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 ↥((FirstOrder.Language.Substructure.closure L).toFun s)) ≤ max Cardinal.aleph0 (Cardinal.lift.{u, w} (Cardinal.mk ↑s) + Cardinal.lift.{w, u} (Cardinal.mk ((i : ℕ) × L.Functions i)))

theorem Set.Countable.substructure_closure (L : FirstOrder.Language) {M : Type w} [FirstOrder.Language.Structure L M] {s : Set M} [Countable ((l : ℕ) × L.Functions l)] (h : Set.Countable s) : Countable ↥((FirstOrder.Language.Substructure.closure L).toFun 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 ∈ (FirstOrder.Language.Substructure.closure L).toFun s) (Hs : ∀ x ∈ s, p x) (Hfun : ∀ {n : ℕ} (f : L.Functions 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 : (FirstOrder.Language.Substructure.closure L).toFun s = ⊤) (Hs : ∀ x ∈ s, p x) (Hfun : ∀ {n : ℕ} (f : L.Functions 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FirstOrder.Language.Substructure.closure_eq {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) : (FirstOrder.Language.Substructure.closure L).toFun ↑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] : (FirstOrder.Language.Substructure.closure L).toFun ∅ = ⊥

@[simp]

theorem FirstOrder.Language.Substructure.closure_univ {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] : (FirstOrder.Language.Substructure.closure L).toFun 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) : (FirstOrder.Language.Substructure.closure L).toFun (s ∪ t) = (FirstOrder.Language.Substructure.closure L).toFun s ⊔ (FirstOrder.Language.Substructure.closure L).toFun t

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

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

Equations

• ⋯ = ⋯

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.

Equations

• FirstOrder.Language.Substructure.comap φ S = { carrier := ⇑φ ⁻¹' ↑S, fun_mem := ⋯ }

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

Equations

• FirstOrder.Language.Substructure.map φ S = { carrier := ⇑φ '' ↑S, fun_mem := ⋯ }

@[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 ∈ 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 : ↥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 ((FirstOrder.Language.Substructure.closure L).toFun s) = (FirstOrder.Language.Substructure.closure L).toFun (⇑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) : (FirstOrder.Language.Substructure.closure L).toFun (⇑f '' s) = FirstOrder.Language.Substructure.map f ((FirstOrder.Language.Substructure.closure L).toFun 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.

Equations

• FirstOrder.Language.Substructure.gciMapComap hf = GaloisConnection.toGaloisCoinsertion ⋯ ⋯

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.

Equations

• FirstOrder.Language.Substructure.giMapComap hf = GaloisConnection.toGaloisInsertion ⋯ ⋯

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 ↥S

Equations

• One or more equations did not get rendered due to their size.

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 (↥S) M

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

Equations

• FirstOrder.Language.Substructure.subtype S = { toEmbedding := { toFun := Subtype.val, inj' := ⋯ }, map_fun' := ⋯, map_rel' := ⋯ }

@[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 (↥⊤) M

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem FirstOrder.Language.Substructure.realize_boundedFormula_top {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {α : Type u_3} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α n} {v : α → ↥⊤} {xs : Fin n → ↥⊤} : FirstOrder.Language.BoundedFormula.Realize φ v xs ↔ FirstOrder.Language.BoundedFormula.Realize φ (Subtype.val ∘ v) (Subtype.val ∘ xs)

@[simp]

theorem FirstOrder.Language.Substructure.realize_formula_top {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {α : Type u_3} {φ : FirstOrder.Language.Formula L α} {v : α → ↥⊤} : FirstOrder.Language.Formula.Realize φ v ↔ FirstOrder.Language.Formula.Realize φ (Subtype.val ∘ v)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• FirstOrder.Language.Substructure.withConstants S h = { carrier := ↑S, fun_mem := ⋯ }

@[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 ⊆ ↑((FirstOrder.Language.Substructure.closure (FirstOrder.Language.withConstants L ↑A)).toFun 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} : (FirstOrder.Language.Substructure.closure (FirstOrder.Language.withConstants L ↑A)).toFun s = FirstOrder.Language.Substructure.withConstants ((FirstOrder.Language.Substructure.closure L).toFun (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 : ↥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 (↥p) N

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

Equations

• FirstOrder.Language.Hom.domRestrict f p = FirstOrder.Language.Hom.comp f (FirstOrder.Language.Embedding.toHom (FirstOrder.Language.Substructure.subtype p))

@[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 ↥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

• FirstOrder.Language.Hom.codRestrict p f h = { toFun := fun (c : M) => { val := f c, property := ⋯ }, map_fun' := ⋯, map_rel' := ⋯ }

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

@[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].

Equations

• FirstOrder.Language.Hom.range f = FirstOrder.Language.Substructure.copy (FirstOrder.Language.Substructure.map f ⊤) (Set.range ⇑f) ⋯

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

Equations

• FirstOrder.Language.Hom.eqLocus f g = { carrier := {x : M | f x = g x}, fun_mem := ⋯ }

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 ↑((FirstOrder.Language.Substructure.closure L).toFun 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 : (FirstOrder.Language.Substructure.closure L).toFun 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 (↥p) N

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

Equations

• FirstOrder.Language.Embedding.domRestrict f p = FirstOrder.Language.Embedding.comp f (FirstOrder.Language.Substructure.subtype p)

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

• One or more equations did not get rendered due to their size.

@[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.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 = { val := f x, property := ⋯ }

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

@[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 ↥s ↥(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.

Equations

• One or more equations did not get rendered due to their size.

@[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 : ↥p) : ↑((FirstOrder.Language.Embedding.substructureEquivMap f p) x) = f ↑x

@[simp]

theorem FirstOrder.Language.Embedding.subtype_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.Embedding.comp (FirstOrder.Language.Substructure.subtype (FirstOrder.Language.Substructure.map (FirstOrder.Language.Embedding.toHom f) s)) (FirstOrder.Language.Equiv.toEmbedding (FirstOrder.Language.Embedding.substructureEquivMap f s)) = FirstOrder.Language.Embedding.comp f (FirstOrder.Language.Substructure.subtype s)

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 ↥(FirstOrder.Language.Hom.range (FirstOrder.Language.Embedding.toHom f))

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

Equations

• One or more equations did not get rendered due to their size.

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

@[simp]

theorem FirstOrder.Language.Embedding.subtype_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.Embedding.comp (FirstOrder.Language.Substructure.subtype (FirstOrder.Language.Hom.range (FirstOrder.Language.Embedding.toHom f))) (FirstOrder.Language.Equiv.toEmbedding (FirstOrder.Language.Embedding.equivRange f)) = f

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 ↥S ↥T

The embedding associated to an inclusion of substructures.

Equations

• FirstOrder.Language.Substructure.inclusion h = FirstOrder.Language.Embedding.codRestrict T (FirstOrder.Language.Substructure.subtype S) ⋯

@[simp]

theorem FirstOrder.Language.Substructure.inclusion_self {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) : FirstOrder.Language.Substructure.inclusion ⋯ = FirstOrder.Language.Embedding.refl L ↥S

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