module Cat.Site.Instances.Frame {o ℓ} (X : Poset o ℓ) (isf : is-frame X) where

# Frames as sites🔗

Since sites, as
categories we can define sheaves on, are meant
to axiomatise what it means for a category to have a notion of
*covering*, we should expect that *frames*, as geometric objects,
should admit the structure of a site.

This module shows that: for a frame $X,$ thought of as the opens in a space, we say that the coverings for $U:X$ are the families $f:I→X$ with $⋃f=U.$ To interpret such a family as a sieve, we say that an object $V≤U$ belongs if there exists an $i:I$ with $V≤fi;$ this is the specialisation to partial orders of the sieve generated by a family of arrows.

private Covering : ⌞ X ⌟ → Type _ Covering U = Σ[ I ∈ Type o ] Σ[ f ∈ (I → ⌞ X ⌟) ] (⋃ f ≡ U) generate : ∀ {U} → Covering U → Sieve (poset→category X) U generate (I , f , _) .arrows {V} _ = elΩ $ Σ[ i ∈ I ] V ≤ f i generate (I , f , _) .closed = rec! λ i α β → inc (i , ≤-trans β α)

For the stability property, we have to check that given a covering
$f:I→U$
and a contained
$V≤U,$
we can restrict
$f$
to a covering of
$V.$
The answer is yes, and the process is leaving the index the same, and
intersecting each part of the coverage with
$V.$
This works only *because*
$X$
is a frame: essentially, if
$⋃f=U,$
then the infinite distributive law gives us
$(i⋃ f(i)∩V)=(i⋃ f(i))∩V=U∩V,$
and this last meet, if
$V≤U,$
is just
$V;$
so
$i↦f(i)∩V$
is a covering family for
$V.$

∩-covering : ∀ {U V} → V ≤ U → Covering U → Covering V ∩-covering {U} {V} V≤U (I , f , p) = I , _ , cap-covers where abstract cap-covers : ⋃ (λ i → f i ∩ V) ≡ V cap-covers = ⋃ (λ i → f i ∩ V) ≡˘⟨ ⋃-distribr f V ⟩≡˘ ⋃ f ∩ V ≡⟨ ap₂ _∩_ p refl ⟩≡ U ∩ V ≡⟨ ∩-comm ∙ order→∩ V≤U ⟩≡ V ∎

To show that these definitions fit together to give a `Coverage`

, we must now show that,
if
$f$
is a covering family for
$U,$
then the intersection
$f∩V$
we computed above is contained in the pullback sieve
$V_{∗}(f).$
We’ll actually do one better: the intersection we computed *is*
the pullback sieve.

generate-∩ : ∀ {U V} (h : V ≤ U) (S : Covering U) → generate (∩-covering h S) ≡ pullback h (generate S) generate-∩ V≤U (I , f , p) = ext λ {W} W≤V → Ω-ua (rec! λ i W≤fi∩V → inc (i , ≤-trans W≤fi∩V ∩≤l)) (rec! λ i W≤fi → inc (i , ∩-universal _ W≤fi W≤V)) Open-coverage : Coverage (poset→category X) (lsuc o) Open-coverage .covers = Covering Open-coverage .cover = generate Open-coverage .stable {U} {V} S V≤U = inc (∩-covering V≤U S , incl) where incl : generate (∩-covering V≤U S) ⊆ pullback V≤U (generate S) incl g = subst (g ∈_) (generate-∩ V≤U S)

The open coverage on a frame enjoys the important property of being
subcanonical,
i.e. all of its covering sieves are pullback-stable colimits. This is
essentially by definition: in the open coverage, a family over
$U$
is covering if its union is
$U,$
i.e. if its *colimit* is
$U.$
Regardless, Agda will still ask that we do a bit of shuffling, and this
is where our lemma for simplifying pullbacks comes in.

Open-coverage-is-subcanonical : is-subcanonical _ Open-coverage Open-coverage-is-subcanonical {U} cov@(I , f , _) {V} V≤U = done where open make-is-colimit mk : make-is-colim (poset→category X) (generate (∩-covering V≤U cov)) mk .ψ (elem W (W≤V , _)) = W≤V

In practical terms, all we have to show is that
$V$
is the colimit of
$⋃_{i}f(i)∩V;$
This computation is implicit in the definition of `∩-covering`

, so we may reuse
that. In more details, we’re given an object
$W$
and a witness
$ε$
that, for every
$X≤V$
for which there exists an
$i:I$
with
$X≤f(i)∩V,$
we have
$X≤W,$
and we must show
$V≤W.$
Since
$ε$
has a type with pretty complex quantification, we’ll write it out
first:

mk .universal {W} ε _ = let ε' : ∀ {X} → X ≤ V → ∃[ i ∈ I ] X ≤ f i ∩ V → X ≤ W ε' {X} α β = ε (elem X (α , (tr-□ β)))

Since $V$ is equal to the join $⋃_{i}f(i)∩V,$ it has the universal property of a join: to show $V≤W,$ for any $X,$ it suffices to show that $f(i)∩V≤W$ for every $i.$ By $ε,$ we can reduce this to the two trivial conditions $f(i)∩V≤V$ and $f(i)∩V≤f(i)∩V.$ After this, we can finish the proof by transitivity.

pt : ∀ i → f i ∩ V ≤ W pt i = ε' ∩≤r (inc (i , ≤-refl)) in V =˘⟨ ∩-covering V≤U cov .snd .snd ⟩=˘ ⋃ (λ i → f i ∩ V) ≤⟨ ⋃-universal _ pt ⟩≤ W ≤∎

Commutativity, universality and uniqueness are all trivial in a
poset, so
$f∩V$
is a colim sieve, which is *almost* what we wanted. The theorem
is complete by transporting along our proof that
$f∩V=f_{∗}(V).$

mk .commutes _ = prop! mk .factors _ _ = prop! mk .unique _ _ _ _ = prop! done : is-colim (poset→category X) (pullback V≤U (generate cov)) done = subst (is-colim (poset→category X)) (generate-∩ V≤U _) (to-is-colimitp mk refl)