Gluing basic DRSs

This file defines covers of a context — jointly surjective families of context morphisms — and gluing of a family of local sections of a presheaf along a cover: a global section restricting to each local one, the indexed form of Presieve.FamilyOfElements.IsAmalgamation for Presieve.ofArrows. For the presheaf of basic DRSs the candidate gluing is the pushforward of the local literals along the cover maps: every gluing contains it, it is the unique gluing when every literal of the glued context factors through a cover map, and it glues outright when the local vocabularies are pairwise disjoint and the cover maps injective. Read on DRSs, the pushforward is the merge of the local DRSs after renaming — discourse representation theory's merge followed by unification of referents.

Main definitions

• DRT.Cover, DRT.Cover.presieve: covers and their presieves.
• DRT.Cover.IsGluing: gluing of local sections of a presheaf along a cover.
• DRT.Cover.pushforward, DRT.Cover.Factors, DRT.Cover.glue: the candidate gluing, the factorization condition, and the gluing under disjoint vocabularies.

Main statements

• DRT.Cover.IsGluing.pushforward_subset, DRT.Cover.IsGluing.unique, DRT.Cover.isSeparatedFor_of_factors: the pushforward is the least gluing and the unique one under factorization.
• DRT.Cover.isGluing_glue, DRT.Cover.coe_conditions_toDRS_glue: under disjoint vocabularies and injective maps the pushforward glues, and its DRS is the merge of the renamed local DRSs.

References

• [AS14]
• [mac-lane-moerdijk-1992]

structure DRT.Cover {L : FirstOrder.Language} {V : Type w} (c : Context L V) (ι : Type u_1) : Type (max (max u_1 v) w)

A cover of a context: a jointly surjective family of context morphisms into it (⋃ Im fᵢ = X and L = ⋃ Lᵢ).

• 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
• exists_mem_vocab (r : (n : ℕ) × L.Relations n) : r ∈ c.vocab → ∃ (i : ι), r ∈ (self.part i).vocab

@[reducible, inline]

abbrev DRT.Cover.presieve {L : FirstOrder.Language} {V : Type w} {c : Context L V} {ι : Type u_1} (C : Cover c ι) : CategoryTheory.Presieve c

The presieve of the covering morphisms.

Equations

• C.presieve = CategoryTheory.Presieve.ofArrows C.part C.map

def DRT.Cover.IsGluing {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

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

Equations

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

theorem DRT.Cover.eq_of_map_eq {L : FirstOrder.Language} {V : Type w} {c : Context L V} {ι : Type u_1} {C : Cover c ι} (hdisj : Pairwise fun (i j : ι) => Disjoint (C.part i).vocab (C.part j).vocab) {i j : ι} {m : Literal (C.part i)} {m' : Literal (C.part j)} (h : Literal.map (C.map i) m = Literal.map (C.map j) m') : i = j

@[instance_reducible]

instance DRT.Cover.instDecidableIsGluingPresheafOfFintype {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)} {s : Theory c} [Fintype ι] : Decidable (C.IsGluing (presheaf L V) x s)

Equations

• DRT.Cover.instDecidableIsGluingPresheafOfFintype = DRT.Cover.instDecidableIsGluingPresheafOfFintype._aux_1

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

The candidate gluing {±A(fᵢ(x̄)) | ±A(x̄) ∈ sᵢ}.

Equations

• C.pushforward x = Finset.univ.biUnion fun (i : ι) => Finset.image (DRT.Literal.map (C.map i)) (x i).lits

@[simp]

theorem DRT.Cover.mem_pushforward {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 ι] {l : Literal c} : l ∈ C.pushforward x ↔ ∃ (i : ι), ∃ m ∈ (x i).lits, Literal.map (C.map i) m = l

theorem DRT.Cover.IsGluing.pushforward_subset {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)} {s : Theory c} [Fintype ι] (hs : C.IsGluing (presheaf L V) x s) : C.pushforward x ⊆ s.lits

def DRT.Cover.Factors {L : FirstOrder.Language} {V : Type w} {c : Context L V} {ι : Type u_1} (C : Cover c ι) : Prop

Every literal over the glued context is the image of a literal over some part.

Equations

• C.Factors = ∀ (l : DRT.Literal c), ∃ (i : ι) (m : DRT.Literal (C.part i)), DRT.Literal.map (C.map i) m = l

@[instance_reducible]

instance DRT.Cover.instDecidableFactorsOfFintype {L : FirstOrder.Language} {V : Type w} {c : Context L V} {ι : Type u_1} {C : Cover c ι} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] [Fintype ι] : Decidable C.Factors

Equations

• DRT.Cover.instDecidableFactorsOfFintype = DRT.Cover.instDecidableFactorsOfFintype._aux_1

theorem DRT.Cover.IsGluing.lits_eq_pushforward {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)} {s : Theory c} [Fintype ι] (hC : C.Factors) (hs : C.IsGluing (presheaf L V) x s) : s.lits = C.pushforward x

theorem DRT.Cover.IsGluing.unique {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)} {s s' : Theory c} [Fintype ι] (hC : C.Factors) (hs : C.IsGluing (presheaf L V) x s) (hs' : C.IsGluing (presheaf L V) x s') : s = s'

Gluings are unique for covers through which every literal factors.

theorem DRT.Cover.isSeparatedFor_of_factors {L : FirstOrder.Language} {V : Type w} {c : Context L V} {ι : Type u_1} {C : Cover c ι} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] [Fintype ι] (hC : C.Factors) : CategoryTheory.Presieve.IsSeparatedFor (presheaf L V) C.presieve

The presheaf of basic DRSs is separated for a factoring cover.

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

With pairwise disjoint vocabularies and injective cover maps the pushforward is consistent.

Equations

• C.glue hdisj hinj x = { lits := C.pushforward x, consistent := ⋯ }

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

Under disjoint vocabularies and injective cover maps the pushforward glues: the only obstruction to gluing is consistency, and it does not arise.

theorem DRT.Cover.referents_toDRS_glue {L : FirstOrder.Language} {V : Type w} {c : Context L V} {ι : Type u_1} {C : Cover c ι} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] [Fintype ι] (hdisj : Pairwise fun (i j : ι) => Disjoint (C.part i).vocab (C.part j).vocab) (hinj : ∀ (i : ι), Function.Injective (C.map i).map) (x : (i : ι) → Theory (C.part i)) (g : ι → V → V) (hg : ∀ (i : ι) (t : ↥(C.part i).vars), g i ↑t = ↑((C.map i).map t)) : (C.glue hdisj hinj x).toDRS.referents = Finset.univ.biUnion fun (i : ι) => (DRS.map (g i) (x i).toDRS).referents

The referents of the glued DRS are those of the renamed local DRSs.

theorem DRT.Cover.coe_conditions_toDRS_glue {L : FirstOrder.Language} {V : Type w} {c : Context L V} {ι : Type u_1} {C : Cover c ι} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] [Fintype ι] (hdisj : Pairwise fun (i j : ι) => Disjoint (C.part i).vocab (C.part j).vocab) (hinj : ∀ (i : ι), Function.Injective (C.map i).map) (x : (i : ι) → Theory (C.part i)) (g : ι → V → V) (hg : ∀ (i : ι) (t : ↥(C.part i).vars), g i ↑t = ↑((C.map i).map t)) : ↑(C.glue hdisj hinj x).toDRS.conditions = ∑ i : ι, ↑(DRS.map (g i) (x i).toDRS).conditions

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