Quotients of First-Order Structures

This file defines prestructures and quotients of first-order structures.

Main Definitions

• If s is a setoid (equivalence relation) on M, a FirstOrder.Language.Prestructure s is the data for a first-order structure on M that will still be a structure when modded out by s.
• The structure FirstOrder.Language.quotientStructure s is the resulting structure on Quotient s.

class FirstOrder.Language.Prestructure (L : Language) {M : Type u_1} (s : Setoid M) : Type (max (max u_1 u_2) u_3)

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.

• toStructure : L.Structure M
• fun_equiv {n : ℕ} {f : L.Functions n} (x y : Fin n → M) : x ≈ y → Structure.funMap f x ≈ Structure.funMap f y
• rel_equiv {n : ℕ} {r : L.Relations n} (x y : Fin n → M) : x ≈ y → Structure.RelMap r x = Structure.RelMap r y

instance FirstOrder.Language.quotientStructure {L : Language} {M : Type u_1} {s : Setoid M} [ps : L.Prestructure s] : L.Structure (Quotient s)

Equations

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

theorem FirstOrder.Language.funMap_quotient_mk' {L : Language} {M : Type u_1} (s : Setoid M) [ps : L.Prestructure s] {n : ℕ} (f : L.Functions n) (x : Fin n → M) : (Structure.funMap f fun (i : Fin n) => ⟦x i⟧) = ⟦Structure.funMap f x⟧

theorem FirstOrder.Language.relMap_quotient_mk' {L : Language} {M : Type u_1} (s : Setoid M) [ps : L.Prestructure s] {n : ℕ} (r : L.Relations n) (x : Fin n → M) : (Structure.RelMap r fun (i : Fin n) => ⟦x i⟧) ↔ Structure.RelMap r x

theorem FirstOrder.Language.Term.realize_quotient_mk' {L : Language} {M : Type u_1} (s : Setoid M) [ps : L.Prestructure s] {β : Type u_2} (t : L.Term β) (x : β → M) : realize (fun (i : β) => ⟦x i⟧) t = ⟦realize x t⟧