module Cat.Instances.Sheaves.Omega {ℓ} {C : Precategory ℓ ℓ} (J : Coverage C ℓ) where
Closed sieves and the subobject classifier🔗
The category of sheaves on a small site is a topos, which means that — in addition to finite limits and exponential objects — it has a subobject classifier, a sheaf which plays the role of the “universe of propositions”. We can construct the sheaf explicitly, as the sheaf of sieves.
A sieve is if it contains every morphism it covers. This notion is evidently closed under pullback, so the closed sieves form a presheaf on
is-closed : ∀ {U} → Sieve C U → Type ℓ is-closed {U} S = ∀ {V} (h : Hom V U) → J ∋ pullback h S → h ∈ S abstract is-closed-pullback : ∀ {U V} (f : Hom V U) (S : Sieve C U) → is-closed S → is-closed (pullback f S) is-closed-pullback f S c h p = c (f ∘ h) (subst (J ∋_) (sym pullback-∘) p)
private instance Extensional-closed-sieve : ∀ {ℓr U} ⦃ _ : Extensional (Sieve C U) ℓr ⦄ → Extensional (Σ[ R ∈ Sieve C U ] is-closed R) ℓr Extensional-closed-sieve ⦃ e ⦄ = injection→extensional! Σ-prop-path! e
ΩJ : Sheaf J ℓ ΩJ .fst = pre where pre : Functor (C ^op) (Sets ℓ) pre .F₀ U = el! (Σ[ R ∈ Sieve C U ] is-closed R) pre .F₁ f (R , c) = pullback f R , is-closed-pullback f R c pre .F-id = funext λ _ → Σ-prop-path! pullback-id pre .F-∘ f g = funext λ _ → Σ-prop-path! pullback-∘
It remains to show that this is a sheaf. We start by showing that it is separated. Suppose we have two closed sieves which agree everywhere on some We want to show so fix some we’ll show iff
ΩJ .snd = from-is-separated sep mk where
It appears that we don’t know much about how and behave outside of their agreement on but knowing that they’re closed will be enough to show that they agree everywhere. First, let’s codify that they actually agree on their intersection with
sep : is-separated J (ΩJ .fst) sep {U} R {S , cS} {T , cT} α = ext λ {V} h → let rem₁ : S ∩S ⟦ R ⟧ ≡ T ∩S ⟦ R ⟧ rem₁ = ext λ {V} h → biimp (λ (h∈S , h∈R) → cT h (subst (J ∋_) (ap fst (α h h∈R)) (max (S .closed h∈S id))) , h∈R) (λ (h∈T , h∈R) → cS h (subst (J ∋_) (ap fst (sym (α h h∈R))) (max (T .closed h∈T id))) , h∈R)
Then, assuming w.l.o.g. that we know that the pullback is a covering sieve. And since is a subsieve of we conclude that if then is and since is closed, this implies also that
rem₂ : h ∈ S → J ∋ pullback h (S ∩S ⟦ R ⟧) rem₂ h∈S = local (pull h (inc R)) λ f hf∈R → max ( S .closed h∈S (f ∘ id) , subst (_∈ R) (ap (h ∘_) (intror refl)) hf∈R ) rem₂' : h ∈ S → J ∋ pullback h T rem₂' h∈S = incl (λ _ → fst) (subst (J ∋_) (ap (pullback h) rem₁) (rem₂ h∈S))
We omit the symmetric converse for brevity.
rem₃ : h ∈ T → J ∋ pullback h S rem₃ ht = incl (λ _ → fst) (subst (J ∋_) (ap (pullback h) (sym rem₁)) (local (pull h (inc R)) λ f rfh → max (T .closed ht (f ∘ id) , subst (_∈ R) (ap (h ∘_) (intror refl)) rfh)))
in biimp (λ h∈S → cT h (rem₂' h∈S)) (λ h∈T → cS h (rem₃ h∈T))
Now we have to show that a family of compatible closed sieves over a sieve can be uniquely patched to a closed sieve on This is the sieve which is defined to contain whenever, for all in the part is the maximal sieve.
module _ {U : ⌞ C ⌟} (R : J ʻ U) (S : Patch (ΩJ .fst) ⟦ R ⟧) where S' : Sieve C U S' .arrows {V} g = elΩ $ ∀ {W} (f : Hom W V) (hf : f ∈ pullback g ⟦ R ⟧) → ∀ {V'} (i : Hom V' W) → i ∈ S .part (g ∘ f) hf .fst S' .closed = elim! λ α h → inc λ {W} g hf → subst (λ e → ∀ (h : e ∈ R) {V'} (i : Hom V' W) → i ∈ S .part e h .fst) (assoc _ _ _) (α (h ∘ g)) hf
module _ {V W W'} (f : Hom V U) (hf : f ∈ ⟦ R ⟧) (g : Hom W V) (hfg : f ∘ g ∈ ⟦ R ⟧) {h : Hom W' W} where lemma : h ∈ S .part (f ∘ g) hfg .fst ≡ (g ∘ h) ∈ S .part f hf .fst lemma = sym (ap (λ e → ⌞ e .fst .arrows h ⌟) (S .patch f hf g hfg)) module lemma = Equiv (path→equiv lemma)
The first thing we have to show is that this pulls back to This is, as usual, a proof of biimplication, though in this case both directions are painful — and entirely mechanical — calculations.
restrict : ∀ {V} (f : Hom V U) (hf : f ∈ R) → pullback f S' ≡ S .part f hf .fst restrict f hf = ext λ {V} h → biimp (rec! λ α → let step₁ : id ∈ S .part (f ∘ h ∘ id) (⟦ R ⟧ .closed hf (h ∘ id)) .fst step₁ = subst₂ (λ e e' → id ∈ S .part e e' .fst) (pullr refl) (to-pathp⁻ refl) (α id _ id) step₂ : ((h ∘ id) ∘ id) ∈ S .part f hf .fst step₂ = lemma.to f hf (h ∘ id) (⟦ R ⟧ .closed hf (h ∘ id)) {id} step₁ in subst (λ e → ⌞ S .part f hf .fst .arrows e ⌟) (cancelr (idr _)) step₂) (λ hh → inc λ {W} g hg {V'} i → S .part ((f ∘ h) ∘ g) hg .snd i (max let s1 : i ∈ S .part (f ∘ h ∘ g) _ .fst s1 = lemma.from f hf (h ∘ g) _ (subst (_∈ S .part f hf .fst) (assoc _ _ _) (S .part f hf .fst .closed hh (g ∘ i))) q : PathP (λ i → assoc f h g i ∈ R) _ hg q = to-pathp⁻ refl in transport (λ j → ⌞ S .part (assoc f h g j) (q j) .fst .arrows (idr i (~ j)) ⌟) s1))
Finally, we can use this to show that is closed.
abstract S'-closed : is-closed S' S'-closed {V} h hb = inc λ {W} f hf {V'} i → S .part (h ∘ f) hf .snd i $ let p = pullback (f ∘ i) (pullback h S') ≡˘⟨ pullback-∘ ⟩≡˘ pullback (h ∘ f ∘ i) S' ≡⟨ restrict (h ∘ f ∘ i) (subst (_∈ R) (sym (assoc h f i)) (⟦ R ⟧ .closed hf i)) ⟩≡ S .part (h ∘ f ∘ i) _ .fst ≡⟨ ap₂ (λ e e' → S .part e e' .fst) (assoc h f i) (to-pathp⁻ refl) ⟩≡ S .part ((h ∘ f) ∘ i) _ .fst ≡˘⟨ ap fst (S .patch (h ∘ f) hf i (⟦ R ⟧ .closed hf i)) ⟩≡˘ pullback i (S .part (h ∘ f) hf .fst) ∎ in subst (J ∋_) p (pull (f ∘ i) hb)