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.
• FirstOrder.Language.Substructure.PartialEquiv is defined so that PartialEquiv L M N is the type of equivalences between substructures of M and N.

Main Results

• L.Substructure M forms a CompleteLattice.

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

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

Equations

• 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} [L.Structure M] {n : ℕ} (f : L.Functions n) : FirstOrder.Language.ClosedUnder f Set.univ

theorem FirstOrder.Language.ClosedUnder.inter {L : FirstOrder.Language} {M : Type w} [L.Structure 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} [L.Structure 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} [L.Structure 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) [L.Structure 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

theorem FirstOrder.Language.Substructure.fun_mem {L : FirstOrder.Language} {M : Type w} [L.Structure M] (self : L.Substructure M) {n : ℕ} (f : L.Functions n) : FirstOrder.Language.ClosedUnder f ↑self

instance FirstOrder.Language.Substructure.instSetLike {L : FirstOrder.Language} {M : Type w} [L.Structure M] : SetLike (L.Substructure 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} [L.Structure M] (S : L.Substructure 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} [L.Structure M] {s : L.Substructure M} {x : M} : x ∈ ↑s ↔ x ∈ s

theorem FirstOrder.Language.Substructure.ext {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {T : L.Substructure 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} [L.Structure M] (S : L.Substructure M) (s : Set M) (hs : s = ↑S) : L.Substructure M

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

Equations

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

theorem FirstOrder.Language.Term.realize_mem {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {α : Type u_3} (t : L.Term α) (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} [L.Structure M] {S : L.Substructure M} {s : Set M} (hs : s = ↑S) : ↑(S.copy s hs) = s

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

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

instance FirstOrder.Language.Substructure.instTop {L : FirstOrder.Language} {M : Type w} [L.Structure M] : Top (L.Substructure 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} [L.Structure M] : Inhabited (L.Substructure M)

Equations

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

@[simp]

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

@[simp]

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

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

The inf of two substructures is their intersection.

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

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

theorem FirstOrder.Language.Substructure.mem_iInf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {ι : Sort u_3} {S : ι → L.Substructure M} {x : M} : x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

@[simp]

theorem FirstOrder.Language.Substructure.coe_iInf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {ι : Sort u_3} {S : ι → L.Substructure M} : ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

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

Substructures of a structure form a complete lattice.

Equations

• FirstOrder.Language.Substructure.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

The L.Substructure generated by a set.

Equations

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

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.Substructure.closure_le {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure 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} [L.Structure 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} [L.Structure M] {S : L.Substructure 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} [L.Structure 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} [L.Structure 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} [L.Structure M] {s : Set M} {x : M} : x ∈ (FirstOrder.Language.Substructure.closure L).toFun s ↔ ∃ (t : L.Term ↑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} [L.Structure M] {s : Set M} : Cardinal.lift.{max u w, w} (Cardinal.mk ↥((FirstOrder.Language.Substructure.closure L).toFun s)) ≤ Cardinal.mk (L.Term ↑s)

theorem FirstOrder.Language.Substructure.lift_card_closure_le {L : FirstOrder.Language} {M : Type w} [L.Structure 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 FirstOrder.Language.Substructure.mem_closed_iff {L : FirstOrder.Language} {M : Type w} [L.Structure M] (s : Set M) : s ∈ (FirstOrder.Language.Substructure.closure L).closed ↔ ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f s

theorem FirstOrder.Language.Substructure.mem_closed_of_isRelational (L : FirstOrder.Language) {M : Type w} [L.Structure M] [L.IsRelational] (s : Set M) : s ∈ (FirstOrder.Language.Substructure.closure L).closed

@[simp]

theorem FirstOrder.Language.Substructure.closure_eq_of_isRelational (L : FirstOrder.Language) {M : Type w} [L.Structure M] [L.IsRelational] (s : Set M) : ↑((FirstOrder.Language.Substructure.closure L).toFun s) = s

@[simp]

theorem FirstOrder.Language.Substructure.mem_closure_iff_of_isRelational (L : FirstOrder.Language) {M : Type w} [L.Structure M] [L.IsRelational] (s : Set M) (m : M) : m ∈ (FirstOrder.Language.Substructure.closure L).toFun s ↔ m ∈ s

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

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

@[simp]

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

theorem FirstOrder.Language.Substructure.closure_union {L : FirstOrder.Language} {M : Type w} [L.Structure 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_iUnion {L : FirstOrder.Language} {M : Type w} [L.Structure 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)

theorem FirstOrder.Language.Substructure.closure_insert {L : FirstOrder.Language} {M : Type w} [L.Structure M] (s : Set M) (m : M) : (FirstOrder.Language.Substructure.closure L).toFun (insert m s) = (FirstOrder.Language.Substructure.closure L).toFun {m} ⊔ (FirstOrder.Language.Substructure.closure L).toFun s

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

Equations

• ⋯ = ⋯

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

theorem FirstOrder.Language.Substructure.mem_iSup_of_directed {L : FirstOrder.Language} {M : Type w} [L.Structure M] {ι : Type u_3} [hι : Nonempty ι] {S : ι → L.Substructure M} (hS : Directed (fun (x1 x2 : L.Substructure M) => x1 ≤ x2) S) {x : M} : x ∈ ⨆ (i : ι), S i ↔ ∃ (i : ι), x ∈ S i

theorem FirstOrder.Language.Substructure.mem_sSup_of_directedOn {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : Set (L.Substructure M)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : L.Substructure M) => x1 ≤ x2) S) {x : M} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

instance FirstOrder.Language.Substructure.instIsEmptySubtypeMemBotOfConstants (L : FirstOrder.Language) (M : Type w) [L.Structure M] [IsEmpty L.Constants] : IsEmpty ↥⊥

Equations

• ⋯ = ⋯

comap and map

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

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

Equations

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.Substructure.mem_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {S : L.Substructure N} {f : L.Hom M N} {x : M} : x ∈ 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} [L.Structure M] [L.Structure N] [L.Structure P] (S : L.Substructure P) (g : L.Hom N P) (f : L.Hom M N) : FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.comap g S) = FirstOrder.Language.Substructure.comap (g.comp f) S

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.Substructure.mem_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {S : L.Substructure M} {y : N} : y ∈ 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} [L.Structure M] [L.Structure N] (f : L.Hom M N) {S : L.Substructure 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} [L.Structure M] [L.Structure N] (f : L.Hom M N) (S : L.Substructure 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} [L.Structure M] [L.Structure N] [L.Structure P] (S : L.Substructure M) (g : L.Hom N P) (f : L.Hom M N) : FirstOrder.Language.Substructure.map g (FirstOrder.Language.Substructure.map f S) = FirstOrder.Language.Substructure.map (g.comp f) S

theorem FirstOrder.Language.Substructure.map_le_iff_le_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {S : L.Substructure M} {T : L.Substructure N} : 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} [L.Structure M] [L.Structure N] (f : L.Hom 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} [L.Structure M] [L.Structure N] (S : L.Substructure M) {T : L.Substructure N} {f : L.Hom 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} [L.Structure M] [L.Structure N] (S : L.Substructure M) {T : L.Substructure N} {f : L.Hom 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} [L.Structure M] [L.Structure N] (S : L.Substructure M) {f : L.Hom 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} [L.Structure M] [L.Structure N] {S : L.Substructure N} {f : L.Hom 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} [L.Structure M] [L.Structure N] {f : L.Hom M N} : Monotone (FirstOrder.Language.Substructure.map f)

theorem FirstOrder.Language.Substructure.monotone_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom 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} [L.Structure M] [L.Structure N] (S : L.Substructure M) {f : L.Hom 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} [L.Structure M] [L.Structure N] {S : L.Substructure N} {f : L.Hom 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} [L.Structure M] [L.Structure N] (S : L.Substructure M) (T : L.Substructure M) (f : L.Hom 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} [L.Structure M] [L.Structure N] {ι : Sort u_3} (f : L.Hom M N) (s : ι → L.Substructure M) : FirstOrder.Language.Substructure.map f (⨆ (i : ι), s i) = ⨆ (i : ι), FirstOrder.Language.Substructure.map f (s i)

theorem FirstOrder.Language.Substructure.comap_inf {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.Substructure N) (T : L.Substructure N) (f : L.Hom 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} [L.Structure M] [L.Structure N] {ι : Sort u_3} (f : L.Hom M N) (s : ι → L.Substructure N) : FirstOrder.Language.Substructure.comap f (⨅ (i : ι), s i) = ⨅ (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} [L.Structure M] [L.Structure N] (f : L.Hom M N) : FirstOrder.Language.Substructure.map f ⊥ = ⊥

@[simp]

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

@[simp]

theorem FirstOrder.Language.Substructure.map_id {L : FirstOrder.Language} {M : Type w} [L.Structure M] (S : L.Substructure 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} [L.Structure M] [L.Structure N] (f : L.Hom 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} [L.Structure M] [L.Structure N] {s : Set M} (f : L.Hom 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} [L.Structure M] [L.Structure N] {f : L.Hom 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 = ⋯.toGaloisCoinsertion ⋯

theorem FirstOrder.Language.Substructure.comap_map_eq_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective ⇑f) (S : L.Substructure M) : 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} [L.Structure M] [L.Structure N] {f : L.Hom 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} [L.Structure M] [L.Structure N] {f : L.Hom 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} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective ⇑f) (S : L.Substructure M) (T : L.Substructure 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} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.Hom M N} (hf : Function.Injective ⇑f) (S : ι → L.Substructure M) : FirstOrder.Language.Substructure.comap f (⨅ (i : ι), FirstOrder.Language.Substructure.map f (S i)) = ⨅ (i : ι), S i

theorem FirstOrder.Language.Substructure.comap_sup_map_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective ⇑f) (S : L.Substructure M) (T : L.Substructure 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} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.Hom M N} (hf : Function.Injective ⇑f) (S : ι → L.Substructure M) : FirstOrder.Language.Substructure.comap f (⨆ (i : ι), FirstOrder.Language.Substructure.map f (S i)) = ⨆ (i : ι), S i

theorem FirstOrder.Language.Substructure.map_le_map_iff_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective ⇑f) {S : L.Substructure M} {T : L.Substructure 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} [L.Structure M] [L.Structure N] {f : L.Hom 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} [L.Structure M] [L.Structure N] {f : L.Hom 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 = ⋯.toGaloisInsertion ⋯

theorem FirstOrder.Language.Substructure.map_comap_eq_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective ⇑f) (S : L.Substructure N) : 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} [L.Structure M] [L.Structure N] {f : L.Hom 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} [L.Structure M] [L.Structure N] {f : L.Hom 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} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective ⇑f) (S : L.Substructure N) (T : L.Substructure 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} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.Hom M N} (hf : Function.Surjective ⇑f) (S : ι → L.Substructure N) : FirstOrder.Language.Substructure.map f (⨅ (i : ι), FirstOrder.Language.Substructure.comap f (S i)) = ⨅ (i : ι), S i

theorem FirstOrder.Language.Substructure.map_sup_comap_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective ⇑f) (S : L.Substructure N) (T : L.Substructure 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} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.Hom M N} (hf : Function.Surjective ⇑f) (S : ι → L.Substructure N) : FirstOrder.Language.Substructure.map f (⨆ (i : ι), FirstOrder.Language.Substructure.comap f (S i)) = ⨆ (i : ι), S i

theorem FirstOrder.Language.Substructure.comap_le_comap_iff_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective ⇑f) {S : L.Substructure N} {T : L.Substructure 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} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective ⇑f) : StrictMono (FirstOrder.Language.Substructure.comap f)

instance FirstOrder.Language.Substructure.inducedStructure {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} : L.Structure ↥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} [L.Structure M] (S : L.Substructure M) : L.Embedding (↥S) M

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

Equations

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

@[simp]

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

def FirstOrder.Language.Substructure.topEquiv {L : FirstOrder.Language} {M : Type w} [L.Structure M] : L.Equiv (↥⊤) M

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

Equations

• FirstOrder.Language.Substructure.topEquiv = { toFun := ⇑⊤.subtype, invFun := fun (m : M) => ⟨m, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_fun' := ⋯, map_rel' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

theorem FirstOrder.Language.Substructure.closure_induction' {L : FirstOrder.Language} {M : Type w} [L.Structure 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} [L.Structure M] {L' : FirstOrder.Language} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] : L'.Substructure M ↪o L.Substructure M

Reduces the language of a substructure along a language hom.

Equations

• φ.substructureReduct = { toFun := fun (S : L'.Substructure M) => { carrier := ↑S, fun_mem := ⋯ }, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

Equations

• f.domRestrict p = f.comp p.subtype.toHom

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

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

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

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

Equations

• f.eqLocus 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} [L.Structure M] [L.Structure N] {f : L.Hom M N} {g : L.Hom 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} [L.Structure M] [L.Structure N] {f : L.Hom M N} {g : L.Hom 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} [L.Structure M] [L.Structure N] {s : Set M} (hs : (FirstOrder.Language.Substructure.closure L).toFun s = ⊤) {f : L.Hom M N} {g : L.Hom 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} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (p : L.Substructure M) : L.Embedding (↥p) N

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

Equations

• f.domRestrict p = f.comp p.subtype

@[simp]

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

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

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

Equations

• FirstOrder.Language.Embedding.codRestrict p f h = { toFun := ⇑(FirstOrder.Language.Hom.codRestrict p f.toHom h), inj' := ⋯, map_fun' := ⋯, map_rel' := ⋯ }

@[simp]

theorem FirstOrder.Language.Embedding.codRestrict_apply {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.Substructure N) (f : L.Embedding M N) {h : ∀ (c : M), f c ∈ p} (x : M) : ↑((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} [L.Structure M] [L.Structure N] (p : L.Substructure N) (f : L.Embedding 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} [L.Structure M] [L.Structure N] [L.Structure P] (f : L.Embedding M N) (g : L.Embedding N P) (p : L.Substructure P) (h : ∀ (b : N), g b ∈ p) : (FirstOrder.Language.Embedding.codRestrict p g h).comp f = FirstOrder.Language.Embedding.codRestrict p (g.comp f) ⋯

@[simp]

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

noncomputable def FirstOrder.Language.Embedding.substructureEquivMap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (s : L.Substructure M) : L.Equiv ↥s ↥(FirstOrder.Language.Substructure.map f.toHom 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} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (p : L.Substructure M) (x : ↥p) : ↑((f.substructureEquivMap p) x) = f ↑x

@[simp]

theorem FirstOrder.Language.Embedding.subtype_substructureEquivMap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (s : L.Substructure M) : (FirstOrder.Language.Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding = f.comp s.subtype

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

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_toEquiv_apply {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (a : M) : f.equivRange.toEquiv a = (FirstOrder.Language.Embedding.codRestrict f.toHom.range f ⋯) a

@[simp]

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

@[simp]

theorem FirstOrder.Language.Embedding.subtype_equivRange {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) : f.toHom.range.subtype.comp f.equivRange.toEmbedding = f

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

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

The embedding associated to an inclusion of substructures.

Equations

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem FirstOrder.Language.Substructure.subtype_comp_inclusion {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {T : L.Substructure M} (h : S ≤ T) : T.subtype.comp (FirstOrder.Language.Substructure.inclusion h) = S.subtype