Docs / Semantics / Dynamic / DRT / Sheaf / Realizers
import Linglib.Semantics.Dynamic.DRT.Sheaf.Realizers · namespace DRT
A basic DRS is true under an assignment of its context's referents when each literal holds, and its realizers, the assignments that make it true, are the verifying embeddings of the DRS. Assignments form a presheaf on contexts that is a sheaf for a presieve exactly when it is jointly surjective on referents, the first of Abramsky and Sadrzadeh's two conditions on covers. An assignment realizes the least gluing of a family along a cover exactly when its restrictions realize the local theories, so the realizers of the gluing are the compatible families of local realizers.
Abramsky and Sadrzadeh leave a sheaf-theoretic semantics of DRSs to future work; this file only shows that truth is compatible with their gluing.
l.Holds g says that the assignment g makes l true, its atom holding when l is
positive and failing when it is negative.
Used by Literal.holds_map, Literal.holds_comp_val_iff, Literal.realizers, Literal.mem_realizers
The realizers of a set of literals are the assignments of the context's referents that make each of them true.
Built from
Used by Literal.mem_realizers, Literal.realizers_iUnion, Literal.realizers_image_map, Literal.comp_val_mem_realizers_iff, Theory.verifies_toDRS_iff, Theory.comp_mem_realizers_restrict, Cover.realizers_pushforward, Cover.realizersEquiv
An embedding verifies the DRS of a theory exactly when its restriction to the context's referents realizes the theory.
Built from
Assignments of values to the referents of contexts form a presheaf, restricting by precomposition.
The definition is too large to print here; read it in the source.
Used by assignments_map, compatible_assignments_iff, arrows_compatible_assignments_iff, isSheafFor_assignments, isSheafFor_assignments_iff, isSheaf_referentCoverage, Cover.realizersEquiv
A presieve belongs to the referent precoverage when every referent of the context is the image of a referent of some member.
Used by mem_referentPrecoverage_iff, isSheafFor_assignments, isSheafFor_assignments_iff, referentCoverage, Cover.presieve_mem_referentPrecoverage
A family of assignments is compatible when its members agree wherever the presieve identifies referents.
Built from
Built from
Assignments glue uniquely along a presieve jointly surjective on referents.
Built from ,
Assignments to a nontrivial structure are a sheaf for a presieve iff it is jointly surjective on referents.
Built from ,
Presieves jointly surjective on referents form a coverage; a referent of a pulled-back context lifts to a context of its own.
Built from
Used by isSheaf_referentCoverage
Assignments are a sheaf for the topology of covers jointly surjective on referents.
Built from ,
An assignment makes the renamed local literals of a family true exactly when its restriction along every cover morphism realizes the local theory.
Built from
The realizers of the renamed local literals of a family, its least gluing when it has one, are the compatible families of local realizers.
Built from ,