Docs / Semantics / Dynamic / DRT / Sheaf / Gluing

Gluing basic DRSs

import Linglib.Semantics.Dynamic.DRT.Sheaf.Gluing · namespace DRT

This file shows that basic DRSs form a sheaf and identifies the topology. A presieve on a context covers it when it is jointly surjective on literals: every literal of the context renames a literal of some member. A compatible family of local theories over any presieve has an amalgamation, the renamings of the local literals, and the amalgamation is unique iff the presieve covers; these covers form a coverage, for which basic DRSs are a sheaf.

Abramsky & Sadrzadeh 2014 glue along covers jointly surjective on referents and on the vocabulary. Along such a cover the renamings of the local literals are the least candidate: a gluing exists iff they are consistent and restrict back to every part, it is unique when the cover is jointly surjective on literals too, and it always exists when the local vocabularies are pairwise disjoint and the cover maps injective. Read on DRSs, it is then the merge of the renamed local DRSs: discourse representation theory's merge followed by unification of referents.

Main definitions

DRT.literalCoverage: the coverage of presieves jointly surjective on literals.
DRT.amalgamate: the amalgamation of a compatible family.
DRT.Cover, DRT.Cover.IsGluing: covers in the paper's sense, and gluing along them.

Main statements

DRT.isSeparatedFor_iff, DRT.isSheafFor_iff, DRT.isSheaf_literalCoverage: basic DRSs are separated, and a sheaf, for a presieve iff it is jointly surjective on literals.
DRT.Cover.exists_isGluing_iff: a gluing exists iff the renamed local literals form one.
DRT.Cover.coe_conditions_toDRS_glue: under disjoint vocabularies and injective cover maps the gluing is the merge of the renamed local DRSs.

Implementation notes

Compatibility is tested on contexts with fresh referents for the arguments of a relation, so amalgamation assumes that V has as many referents as each arity in the vocabulary; isSheaf_literalCoverage assumes V infinite, like the paper's variables.

References

Abramsky & Sadrzadeh 2014, Semantic Unification: A Sheaf Theoretic Approach to Natural Language formalized
Mac Lane & Moerdijk 1992, Sheaves in Geometry and Logic: A First Introduction to Topos Theory

Literal covers

L65–68

L70–73

Presieves jointly surjective on literals form a coverage; a literal over a pulled-back context lifts to the context of its own arguments.

def literalCoverage L80–107

(L : FirstOrder.Language) (V : Type w) [DecidableEq V] :

CategoryTheory.Coverage (Context L V)

literalCoverage L V = { toPrecoverage := literalPrecoverage L V, pullback := ⋯ }

Built from

Used by isSheaf_literalCoverage

Amalgamation

L143–156

The amalgamation of a compatible family holds the renamings of the local literals.

amalgamate L166–175

noncomputable def DRT.amalgamate {L : FirstOrder.Language} {V : Type w} {c : Context L V} {R : CategoryTheory.Presieve c} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] {x : CategoryTheory.Presieve.FamilyOfElements (presheaf L V) R} (hx : x.Compatible) (hc : ∀ r ∈ c.vocab, Nonempty (Fin r.fst ↪ V)) :

Theory c

amalgamate hx hc = { lits := {l : Literal c | ∃ (Y : Context L V) (f : Y ⟶ c) (hf : R f), ∃ m ∈ (x f hf).lits, Literal.map f m = l}, consistent := ⋯ }

Used by isAmalgamation_amalgamate

L177–183

The sheaf condition

Basic DRSs are separated for a presieve iff it is jointly surjective on literals.

theorem isSeparatedFor_iff L189–208

{L : FirstOrder.Language} {V : Type w} {c : Context L V} {R : CategoryTheory.Presieve c} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] :

CategoryTheory.Presieve.IsSeparatedFor (presheaf L V) R ↔ R ∈ (literalPrecoverage L V).coverings c

Built from

Basic DRSs are a sheaf for a presieve iff it is jointly surjective on literals.

theorem isSheafFor_iff L210–214

{L : FirstOrder.Language} {V : Type w} {c : Context L V} {R : CategoryTheory.Presieve c} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] (hc : ∀ r ∈ c.vocab, Nonempty (Fin r.fst ↪ V)) :

CategoryTheory.Presieve.IsSheafFor (presheaf L V) R ↔ R ∈ (literalPrecoverage L V).coverings c

Built from

Basic DRSs are a sheaf for the topology of covers jointly surjective on literals.

theorem isSheaf_literalCoverage L216–220

{L : FirstOrder.Language} {V : Type w} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] [Infinite V] :

CategoryTheory.Presieve.IsSheaf (literalCoverage L V).toGrothendieck (presheaf L V)

Built from

Covers

A cover of a context, in Abramsky & Sadrzadeh 2014's sense, is a family of context morphisms jointly surjective on referents and on the vocabulary (⋃ Im fᵢ = X and L = ⋃ Lᵢ).

structure Cover L226–236

{L : FirstOrder.Language} {V : Type w} (c : Context L V) (ι : Type u_1) :

Type (max (max u_1 v) w)

part : ι → Context L V
The covering contexts.
map (i : ι) : self.part i ⟶ c
The covering morphisms.
exists_map_eq (x : ↥c.vars) : ∃ (i : ι) (y : ↥(self.part i).vars), (self.map i).map y = x
Every referent is the image of a referent of some part.
exists_mem_vocab (r : (n : ℕ) × L.Relations n) : r ∈ c.vocab → ∃ (i : ι), r ∈ (self.part i).vocab
Every relation symbol is in the vocabulary of some part.

Used by Cover.presieve, Cover.IsGluing, Cover.presieve_mem_literalPrecoverage_iff, Cover.eq_of_map_eq, Cover.instDecidableIsGluingPresheafOfFintype, Cover.pushforward, Cover.mem_pushforward, Cover.instDecidableMemPresieveContextSetCoveringsLiteralPrecoveragePresieve, Cover.IsGluing.pushforward_subset, Cover.exists_isGluing_iff, Cover.IsGluing.unique, Cover.glue, Cover.isGluing_glue, Cover.referents_toDRS_glue, Cover.coe_conditions_toDRS_glue

Used in Semantics/Dynamic/DRT/Sheaf/Realizers, AbramskySadrzadeh2014, ChatzikyriakidisEtAl2025

L242–243

s glues the family x over the cover when P(fᵢ)(s) = xᵢ for every i.

def Cover.IsGluing L245–248

{L : FirstOrder.Language} {V : Type w} {c : Context L V} {ι : Type u_1} (C : Cover c ι) (P : CategoryTheory.Functor (Context L V)ᵒᵖ (Type u_2)) (x : (i : ι) → P.obj (Opposite.op (C.part i))) (s : P.obj (Opposite.op c)) :

Prop

C.IsGluing P x s = ∀ (i : ι), (CategoryTheory.ConcreteCategory.hom (P.map (C.map i).op)) s = x i

Built from

Used by Cover.instDecidableIsGluingPresheafOfFintype, Cover.IsGluing.pushforward_subset, Cover.exists_isGluing_iff, Cover.IsGluing.unique, Cover.isGluing_glue

Used in AbramskySadrzadeh2014, ChatzikyriakidisEtAl2025

A family glues iff the renamings of its local literals form a gluing, which is then the least one.

theorem Cover.exists_isGluing_iff L290–300

{L : FirstOrder.Language} {V : Type w} {c : Context L V} {ι : Type u_1} {C : Cover c ι} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] {x : (i : ι) → Theory (C.part i)} [Fintype ι] :

(∃ (s : (presheaf L V).obj (Opposite.op c)), C.IsGluing (presheaf L V) x s) ↔ ∃ (h : Literal.Consistent (C.pushforward x)), C.IsGluing (presheaf L V) x { lits := C.pushforward x, consistent := h }

Built from , ,

L302–309

Disjoint vocabularies

L313–323

L328–331

L333–344

The conditions of the glued DRS are those of the renamed local DRSs, as a multiset, so the gluing is the merge of the local DRSs after unification of referents.

theorem Cover.coe_conditions_toDRS_glue L346–366

{L : FirstOrder.Language} {V : Type w} {c : Context L V} {ι : Type u_1} {C : Cover c ι} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] (x : (i : ι) → Theory (C.part i)) [Fintype ι] (hdisj : Pairwise fun (i j : ι) => Disjoint (C.part i).vocab (C.part j).vocab) (hinj : ∀ (i : ι), Function.Injective (C.map i).map) :

↑(C.glue hdisj hinj x).toDRS.conditions = ∑ i : ι, ↑(DRS.map (Context.Hom.extend (C.map i)) (x i).toDRS).conditions

Built from ,