Quotients of First-Order Structures #
This file defines prestructures and quotients of first-order structures.
Main Definitions #
- If
sis a setoid (equivalence relation) onM, afirst_order.language.prestructure sis the data for a first-order structure onMthat will still be a structure when modded out bys. - The structure
first_order.language.quotient_structure sis the resulting structure onquotient s.
@[class]
structure
first_order.language.prestructure
(L : first_order.language)
{M : Type u_3}
(s : setoid M) :
Type (max u_1 u_2 u_3)
- to_structure : L.Structure M
- fun_equiv : ∀ {n : ℕ} {f : L.functions n} (x y : fin n → M), x ≈ y → first_order.language.Structure.fun_map f x ≈ first_order.language.Structure.fun_map f y
- rel_equiv : ∀ {n : ℕ} {r : L.relations n} (x y : fin n → M), x ≈ y → first_order.language.Structure.rel_map r x = first_order.language.Structure.rel_map r y
A prestructure is a first-order structure with a setoid equivalence relation on it,
such that quotienting by that equivalence relation is still a structure.
@[protected, instance]
def
first_order.language.quotient_structure
{L : first_order.language}
{M : Type u_3}
{s : setoid M}
[ps : L.prestructure s] :
Equations
- first_order.language.quotient_structure = {fun_map := λ (n : ℕ) (f : L.functions n) (x : fin n → quotient s), quotient.map (first_order.language.Structure.fun_map f) first_order.language.prestructure.fun_equiv (quotient.fin_choice x), rel_map := λ (n : ℕ) (r : L.relations n) (x : fin n → quotient s), quotient.lift (first_order.language.Structure.rel_map r) first_order.language.prestructure.rel_equiv (quotient.fin_choice x)}
theorem
first_order.language.fun_map_quotient_mk
{L : first_order.language}
{M : Type u_3}
[s : setoid M]
[ps : L.prestructure s]
{n : ℕ}
(f : L.functions n)
(x : fin n → M) :
first_order.language.Structure.fun_map f (λ (i : fin n), ⟦x i⟧) = ⟦first_order.language.Structure.fun_map f x⟧
theorem
first_order.language.rel_map_quotient_mk
{L : first_order.language}
{M : Type u_3}
[s : setoid M]
[ps : L.prestructure s]
{n : ℕ}
(r : L.relations n)
(x : fin n → M) :
first_order.language.Structure.rel_map r (λ (i : fin n), ⟦x i⟧) = first_order.language.Structure.rel_map r x
theorem
first_order.language.realize_term_quotient_mk
{L : first_order.language}
{M : Type u_3}
[s : setoid M]
[ps : L.prestructure s]
{β : Type}
(x : β → M)
(t : L.term β) :
first_order.language.realize_term (λ (i : β), ⟦x i⟧) t = ⟦first_order.language.realize_term x t⟧