# 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 : ) :
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 :
• fun_equiv : ∀ {n : } {f : L.Functions n} (x y : Fin nM),
• rel_equiv : ∀ {n : } {r : L.Relations n} (x y : Fin nM),
Instances
instance FirstOrder.Language.quotientStructure {L : FirstOrder.Language} {M : Type u_1} {s : } [ps : ] :
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 : ) [ps : ] {n : } (f : L.Functions n) (x : Fin nM) :
(FirstOrder.Language.Structure.funMap f fun (i : Fin n) => x i) =
theorem FirstOrder.Language.relMap_quotient_mk' {L : FirstOrder.Language} {M : Type u_1} (s : ) [ps : ] {n : } (r : L.Relations n) (x : Fin nM) :
(FirstOrder.Language.Structure.RelMap r fun (i : Fin n) => x i)
theorem FirstOrder.Language.Term.realize_quotient_mk' {L : FirstOrder.Language} {M : Type u_1} (s : ) [ps : ] {β : Type u_2} (t : ) (x : βM) :
FirstOrder.Language.Term.realize (fun (i : β) => x i) t =