Quotients of First-Order Structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines prestructures and quotients of first-order structures.

Main Definitions #

If s is a setoid (equivalence relation) on M, a first_order.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 first_order.language.quotient_structure s is the resulting structure on quotient s.

source

@[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.

Instances of this typeclass

Instances of other typeclasses for first_order.language.prestructure

first_order.language.prestructure.has_sizeof_inst

source

@[protected, instance]

def first_order.language.quotient_structure {L : first_order.language} {M : Type u_3} {s : setoid M} [ps : L.prestructure s] :

L.Structure (quotient 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)}

source

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⟧

source

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

source

theorem first_order.language.term.realize_quotient_mk {L : first_order.language} {M : Type u_3} [s : setoid M] [ps : L.prestructure s] {β : Type u_4} (t : L.term β) (x : β → M) :

first_order.language.term.realize (λ (i : β), ⟦x i⟧) t = ⟦first_order.language.term.realize x t⟧