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 : FirstOrder.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 : FirstOrder.Language.Structure L M
• fun_equiv : ∀ {n : ℕ} {f : L.Functions n} (x y : Fin n → M), x ≈ y → FirstOrder.Language.Structure.funMap f x ≈ FirstOrder.Language.Structure.funMap f y
• rel_equiv : ∀ {n : ℕ} {r : L.Relations n} (x y : Fin n → M), x ≈ y → FirstOrder.Language.Structure.RelMap r x = FirstOrder.Language.Structure.RelMap r y

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

Equations

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

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

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

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