open import Cat.Instances.Sheaves.Omega
open import Cat.Site.Grothendieck
open import Cat.Functor.Constant
open import Cat.Diagram.Sieve
open import Cat.Site.Base
open import Cat.Prelude

import Cat.Functor.Reasoning.Presheaf as PSh
import Cat.Site.Closure
import Cat.Reasoning as Cat

module Cat.Site.Instances.Atomic where

Atomic sites🔗

The atomic topology on a small category $\mathcal{C}$ is the coverage where a sieve $R$ covers an object $U$ as soon as $R$ is inhabited. If $\mathcal{C}$ is a completely arbitrary category, then the pullback of an inhabited sieve need not be inhabited; a necessary condition is that every pair of maps $f:A\to C$ and $g:B\to C$ can be completed to a commutative square

in which $X\text{,}$ $p_1$ and $p_2$ may be completely arbitrary. Following Johnstone (2002, A2.1.11(h)), we refer to this condition on $\mathcal{C}$ as the right Ore condition.

module _ {o ℓ} (C : Precategory o ℓ) where
  open Precategory C

  Squaring : ∀ {a b c} (f : Hom a c) (g : Hom b c) → Type _
  Squaring {a = a} {b} {c} f g = Σ[ d ∈ C ]
    Σ[ p1 ∈ Hom d a ] Σ[ p2 ∈ Hom d b ] (f ∘ p1 ≡ g ∘ p2)

  Right-ore : Type _
  Right-ore = ∀ {a b c} (f : Hom a c) (g : Hom b c) → ∥ Squaring f g ∥

module _ {o ℓ} (C : Precategory o ℓ) (square : Right-ore C) where
  open Cat C

Note that if this condition is satisfied, the atomic coverage is automatically a Grothendieck coverage.

  Atomic-topology : Topology C (o ⊔ ℓ)
  Atomic-topology .covering U R = ∃[ V ∈ C ] Σ[ f ∈ Hom V U ] f ∈ R
  Atomic-topology .has-is-prop = hlevel 
  Atomic-topology .stable {U} {V} f {S} = rec! λ W g hg → do
    (d , p1 , p2 , q) ← square f g
    pure (d , p1 , subst (_∈ S) (sym q) (S .closed hg p2))
  Atomic-topology .maximal r = inc (_ , _ , r)
  Atomic-topology .local = elim! λ V h pt {S} α → case α h pt of λ
    U g β → inc (_ , _ , β)

  module Atomic = Topology Atomic-topology

  open Atomic using ()
    renaming (from-topology to Atomic-coverage) public

Sheaves for the atomic topology🔗

We now want to characterise when a functor $A:\mathrm{PSh}({\mathcal{C}}^{\mathrm{op}})$ is a sheaf for the atomic topology. A morphism $f:V\to U$ is said to support a section $y:A(V)$ if maps $g,h:W\to V$ act identically on $y$ as soon as they are equal under precomposition with $f\text{.}$

  module _ {ℓ'} (A : Functor (C ^op) (Sets ℓ')) where

    is-support : ∀ {V U} (f : Hom V U) (y : A ʻ V) → Type _
    is-support {V} f y =
      ∀ {W} (g h : Hom W V)
      → f ∘ g ≡ f ∘ h
      → A ⟪ g ⟫ y ≡ A ⟪ h ⟫ y

  module _ {ℓ'} (A : Functor (C ^op) (Sets ℓ')) where
    private module A = PSh A using (collapse)

The importance of this notion is that, if a sieve $S$ is inhabited by some $f:V\to U\text{,}$ then a patch of $A$ over $S$ is precisely an element $x:A(V)$ supported by $f\text{.}$

    patch→support
      : ∀ {U V} {S : Sieve C U} {f : Hom V U} (hf : f ∈ S) (p : Patch A S)
      → is-support A f (p .part f hf)
    patch→support {S = S} {f = f} hf p g h β =
      A ⟪ g ⟫ p .part f hf ≡⟨ p .patch f hf g (S .closed hf _) ⟩≡
      p .part (f ∘ g) _    ≡⟨ app p β ⟩≡
      p .part (f ∘ h) _    ≡˘⟨ p .patch f hf h (S .closed hf _) ⟩≡˘
      A ⟪ h ⟫ p .part f hf ∎

    support→patch
      : ∀ {U V} {f : Hom V U} {x : A ʻ V}
      → is-support A f x
      → Patch {C = C} A (map→sieve f)
    support→patch {f = f} {x} supp .part g hg =
      ∥-∥-rec-set!
        (λ (h , p) → A ⟪ h ⟫ x)
        (λ (h , α) (h' , β) → supp h h' (α ∙ sym β))
        (□-tr hg)

    support→patch {f = f} {x} supp .patch = elim! λ g h p i j sq →
      A ⟪ i ⟫ (A ⟪ h ⟫ x) ≡⟨ A.collapse refl ⟩≡
      A ⟪ h ∘ i ⟫ x       ≡⟨ supp (h ∘ i) j (pulll p ∙ sym sq) ⟩≡
      A ⟪ j ⟫ x           ∎

With this correspondence, we can define a simpler notion of sheaf for the atomic topology: $A$ is a sheaf if every $y:A(V)$ supported by $f:V\to U$ admits a unique lifting $x:A(U)$ with $A(f)(x)=y\text{.}$

  is-atomic-sheaf : ∀ {ℓ'} (A : Functor (C ^op) (Sets ℓ')) → Type _
  is-atomic-sheaf A =
    ∀ {U V : ⌞ C ⌟} (y : A ʻ V) (f : Hom V U)
    → is-support A f y
    → is-contr (Σ[ x ∈ A ʻ U ] (y ≡ A ⟪ f ⟫ x))

The easy direction is showing that this is implied by the sheaf condition. Since the sieve generated by any $f:V\to U$ is covering in the atomic topology, and we’ve already shown that supported elements correspond to patches, all we have to do is a bit of algebra.

  to-is-atomic-sheaf
    : ∀ {ℓ'} (P : Functor (C ^op) (Sets ℓ'))
    → is-sheaf Atomic-coverage P
    → is-atomic-sheaf P
  to-is-atomic-sheaf A sheaf {U} {V} y f loc = done where
    module A = PSh A

    cov : Atomic-coverage .covers U
    cov = map→sieve f , inc (V , f , inc (id , elimr refl))

    x : Patch A (map→sieve f)
    x = support→patch A loc

    rem₁ : y ≡ A ⟪ f ⟫ sheaf .whole cov x
    rem₁ = sym (sheaf .glues cov x f (inc (id , elimr refl)) ∙ A.elim refl)

    done : is-contr _
    done .centre = record { snd = rem₁ }
    done .paths (z , q) = Σ-prop-path! $ sheaf .separate cov $ elim! λ g h r →
      A ⟪ g ⟫ sheaf .whole cov x           ≡⟨ A.expand (sym r) ⟩≡
      A ⟪ h ⟫ (A ⟪ f ⟫ sheaf .whole cov x) ≡⟨ A.ap (sym rem₁) ⟩≡
      A ⟪ h ⟫ y                            ≡⟨ A.ap q ⟩≡
      A ⟪ h ⟫ (A ⟪ f ⟫ z)                  ≡⟨ A.collapse r ⟩≡
      A ⟪ g ⟫ z                            ∎

  from-is-atomic-sheaf
    : ∀ {ℓ'} (A : Functor (C ^op) (Sets ℓ'))
    → is-atomic-sheaf A → is-sheaf Atomic-coverage A
  from-is-atomic-sheaf A at = from-is-sheaf₁ λ {U} → elim! done where
    module A = PSh A

The converse direction requires slightly more work. We assume that we have a sieve $S$ covering $U\text{,}$ inhabited by some $f_0:V\to U\text{,}$ and a patch $p$ of $S\text{.}$ Since we can extract an $f_0\text{-supported}$ element $p_0$ from $p\text{,}$ by the “atomic sheaf” condition we obtain that there is a contractible space of lifts $e:A(U)$ of $p_0$ through $f_0\text{.}$

    module _ {U} (S : Sieve C U) V (f₀ : Hom V U) (hf₀ : f₀ ∈ S) (p : Patch A S) where
      p₀ : A ʻ V
      p₀ = p .part f₀ hf₀

      sec : is-contr (Σ[ x ∈ A ʻ U ] (p .part f₀ hf₀ ≡ A ⟪ f₀ ⟫ x))
      sec = at p₀ f₀ (patch→support A hf₀ p)

      open Σ (sec .centre) renaming (fst to e ; snd to q)

We must then show that $e$ agrees with $p$ at any other $f:W\to U\in S\text{.}$ To this end, suppose that we have such an $f\text{,}$ and fit it into a commutative square

using that $\mathcal{C}$ satisfies the right Ore condition.

      rem₁'
        : ∀ {W} (f : Hom W U) (hf : f ∈ S)
        → Squaring C f₀ f
        → A ⟪ f ⟫ e ≡ p .part f hf
      rem₁' {W = W} f hf (X , v , u , sq) = done where

First, a short calculation shows that $A(v)(p_0):A(X)$ is supported by $u\text{,}$ which implies that there is exactly one element in $A(W)$ on which $u$ acts to give $A(v)(p_0)\text{.}$

        cohy : is-support A u (A ⟪ v ⟫ p₀)
        cohy g h q =
          A ⟪ g ⟫ (A ⟪ v ⟫ p₀) ≡⟨ A.collapse refl ⟩≡
          A ⟪ v ∘ g ⟫ p₀       ≡⟨ patch→support A hf₀ p _ _ (pulll sq ·· pullr q ·· extendl (sym sq)) ⟩≡
          A ⟪ v ∘ h ⟫ p₀       ≡⟨ A.expand refl ⟩≡
          A ⟪ h ⟫ (A ⟪ v ⟫ p₀) ∎

        y : is-contr (Σ[ x ∈ A ʻ W ] A ⟪ v ⟫ p₀ ≡ A ⟪ u ⟫ x)
        y = at (A ⟪ v ⟫ p₀) u cohy

But since $p_0$ comes from a patch of $S\text{,}$ and $f\in S\text{,}$ we can also calculate that $A(v)(p_0)$ is $p(f_{0}v)\text{,}$ which is $p(fu)$ by commutativity of the square above, and this in turn is $A(u)(pf)\text{.}$

        rem₂ : A ⟪ v ⟫ p₀ ≡ A ⟪ u ⟫ p .part f hf
        rem₂ =
          A ⟪ v ⟫ p₀             ≡⟨ p .patch f₀ hf₀ v (S .closed hf₀ v) ⟩≡
          p .part (f₀ ∘ v) _     ≡⟨ ap₂ (p .part) sq prop! ⟩≡
          p .part (f ∘ u) _      ≡˘⟨ p .patch f hf u (S .closed hf u) ⟩≡˘
          A ⟪ u ⟫ p .part f hf   ∎

On the other hand, we can also calculate that $p_0=A(f_0)(e)$ by the definition of $e\text{,}$ and that $A(v)(A(f_0)(e))=A(u)(A(f)(e))\text{,}$ so we must have $A(f)(e)=pf\text{.}$ Therefore $e$ is a section of $p\text{,}$ and we are essentially done.

        rem₃ =
          A ⟪ v ⟫ p₀           ≡⟨ A.ap q ⟩≡
          A ⟪ v ⟫ (A ⟪ f₀ ⟫ e) ≡⟨ A.weave sq ⟩≡
          A ⟪ u ⟫ (A ⟪ f ⟫ e)  ∎

        done = ap fst (is-contr→is-prop y (_ , rem₃) (_ , rem₂))

      rem₁ : ∀ {W} (f : Hom W U) (hf : f ∈ S) → A ⟪ f ⟫ e ≡ p .part f hf
      rem₁ f hf = ∥-∥-rec (hlevel ) (rem₁' f hf) (square f₀ f)

      done : is-contr (Section A p)
      done .centre = record { glues = λ g hg → rem₁ g hg }
      done .paths x = ext $ ap fst $ is-contr→is-prop sec
        (_ , q) (_ , sym (x .glues f₀ hf₀))

The most immediate consequence of this simplification is that, in the atomic topology, every constant functor is a sheaf.

  Const-is-sheaf : ∀ {ℓ'} (X : Set ℓ') → is-sheaf Atomic-coverage (Const X)
  Const-is-sheaf X = from-is-atomic-sheaf _ (λ _ _ _ → hlevel )

Atomic topoi🔗

A characteristic property of topoi of sheaves on atomic sites is that the subobject classifier sheaf is given by the constant object on the usual set of propositions. Because we know that constant presheaves are sheaves in an atomic topos, we do not need to sheafify to obtain this latter sheaf, which simplifies the calculation significantly.

module _ {ℓ} {C : Precategory ℓ ℓ} (sq : Right-ore C) where
  open Cat.Site.Closure
  open Cat C
  open _=>_

  private
    cov = Atomic-coverage C sq

    module Sh = Cat (Sheaves cov ℓ)

  ΩJ' : Sheaf cov ℓ
  ΩJ' = record
    { fst = Const (el! (Lift ℓ Ω))
    ; snd = Const-is-sheaf C sq _
    }

It’s easy to construct this isomorphism by hand. In one direction, we send a closed sieve $S$ to the proposition $\mathrm{id}\in S$ (which is equivalent to $S\equiv \top \text{);}$ In the other direction, we send a proposition $P$ to the sieve which contains any $h$ iff $P\text{.}$

  private interleaved mutual
    m1 : ΩJ cov .fst => ΩJ' .fst
    m1 .η U (S , _) = lift (S .arrows id)

    m2 : ΩJ' .fst => ΩJ cov .fst
    m2 .η x P .fst .arrows h = P .lower

    m1 .is-natural x y f = ext λ S cl → biimp
      (λ hf → cl id (inc (pullback id S , inc (y , f , subst (_∈ S) id-comm hf))))
      (λ hid → subst (_∈ S) id-comm-sym (S .closed hid f))

    m2 .η x P .fst .closed hf _ = hf
    m2 .η x P .snd h y = case Atomic.unsaturate C sq y of λ _ _ α → α
    m2 .is-natural x y f = ext λ P → Σ-prop-path! trivial!

Finally, we can show that these maps are inverses. Note that one direction is definitional, and the other is not much more complicated.

  ΩJ-is-constant : ΩJ cov Sh.≅ ΩJ'
  ΩJ-is-constant =
    let
      q = ext λ i X cl → Σ-prop-path! $ ext λ x → biimp
        (λ p → subst (_∈ X) (idl _) (X .closed p _))
        (λ p → cl id (inc (_ , inc (_ , _ , subst (_∈ X) id-comm (X .closed p id)))))
    in Sh.make-iso m1 m2 trivial! q