diff --git a/src/1Lab/Extensionality.agda b/src/1Lab/Extensionality.agda index df38f2bfd..24311dcfe 100644 --- a/src/1Lab/Extensionality.agda +++ b/src/1Lab/Extensionality.agda @@ -151,20 +151,6 @@ instance Extensional-Π'' ⦃ sb ⦄ .idsᵉ .to-path h i = sb .idsᵉ .to-path h i Extensional-Π'' ⦃ sb ⦄ .idsᵉ .to-path-over h i = sb .idsᵉ .to-path-over h i - Extensional-× - : ∀ {ℓ ℓ' ℓr ℓs} {A : Type ℓ} {B : Type ℓ'} - → ⦃ sa : Extensional A ℓr ⦄ - → ⦃ sb : Extensional B ℓs ⦄ - → Extensional (A × B) (ℓr ⊔ ℓs) - Extensional-× ⦃ sa ⦄ ⦃ sb ⦄ .Pathᵉ (x , y) (x' , y') = Pathᵉ sa x x' × Pathᵉ sb y y' - Extensional-× ⦃ sa ⦄ ⦃ sb ⦄ .reflᵉ (x , y) = reflᵉ sa x , reflᵉ sb y - Extensional-× ⦃ sa ⦄ ⦃ sb ⦄ .idsᵉ .to-path (p , q) = ap₂ _,_ - (sa .idsᵉ .to-path p) - (sb .idsᵉ .to-path q) - Extensional-× ⦃ sa ⦄ ⦃ sb ⦄ .idsᵉ .to-path-over (p , q) = Σ-pathp - (sa .idsᵉ .to-path-over p) - (sb .idsᵉ .to-path-over q) - -- Some non-confluent "reduction rules" for extensionality are those -- for functions from a type with a mapping-out property; here, we can -- immediately define instances for functions from Σ-types (equality diff --git a/src/Algebra/Group/Ab/Sum.lagda.md b/src/Algebra/Group/Ab/Sum.lagda.md index 2d88deca7..2ad419bae 100644 --- a/src/Algebra/Group/Ab/Sum.lagda.md +++ b/src/Algebra/Group/Ab/Sum.lagda.md @@ -85,5 +85,5 @@ limits][rapl]). Direct-sum-is-product .π₁∘⟨⟩ = trivial! Direct-sum-is-product .π₂∘⟨⟩ = trivial! - Direct-sum-is-product .unique p q = ext λ x → p #ₚ x , q #ₚ x + Direct-sum-is-product .unique p q = ext λ x → p #ₚ x ,ₚ q #ₚ x ``` diff --git a/src/Algebra/Ring/Module/Category.lagda.md b/src/Algebra/Ring/Module/Category.lagda.md index df9f7e9c6..130cb22b8 100644 --- a/src/Algebra/Ring/Module/Category.lagda.md +++ b/src/Algebra/Ring/Module/Category.lagda.md @@ -261,7 +261,7 @@ path-mangling, but it's nothing _too_ bad: Σ-pathp (f .preserves .linear _ _ _) (g .preserves .linear _ _ _) prod .has-is-product .π₁∘⟨⟩ = trivial! prod .has-is-product .π₂∘⟨⟩ = trivial! - prod .has-is-product .unique p q = ext λ x → p #ₚ x , q #ₚ x + prod .has-is-product .unique p q = ext λ x → p #ₚ x ,ₚ q #ₚ x ``` @@ -120,3 +123,46 @@ cocomplete→copowering colim = Copowers.Copowering λ S F → Colimit→IC _ (is-hlevel-suc 2 (S .is-tr)) F (colim _) ``` --> + +## Constant objects + +If $\cC$ has a terminal object $\star$, then the copower $S \times +\star$ is referred to as the **constant object** on $S$. By simplifying +the universal power of the copower, we obtain that constant objects +assemble into a functor left adjoint to $\cC(\star,-)$.^[This right +adjoint is often called the **global sections functor**] + + + +```agda + Constant-objects : Functor (Sets ℓ) C + Constant-objects .F₀ S = S ⊗ *C + Constant-objects .F₁ f = coprods _ _ .match λ i → coprods _ _ .ι (f i) + Constant-objects .F-id = sym $ coprods _ _ .unique _ λ i → idl _ + Constant-objects .F-∘ f g = sym $ coprods _ _ .unique _ λ i → + pullr (coprods _ _ .commute) ∙ coprods _ _ .commute + + Const⊣Γ : Constant-objects ⊣ Hom-from _ *C + Const⊣Γ = hom-iso→adjoints + (λ f x → f ∘ coprods _ _ .ι x) + (is-iso→is-equiv (iso + (λ h → coprods _ _ .match h) + (λ h → ext λ i → coprods _ _ .commute) + (λ x → sym (coprods _ _ .unique _ λ i → refl)))) + (λ g h x → ext λ y → pullr (pullr (coprods _ _ .commute))) +``` diff --git a/src/Cat/Diagram/Sieve.lagda.md b/src/Cat/Diagram/Sieve.lagda.md index e3a2b30a5..b4d2906dd 100644 --- a/src/Cat/Diagram/Sieve.lagda.md +++ b/src/Cat/Diagram/Sieve.lagda.md @@ -99,6 +99,14 @@ module _ {o ℓ : _} {C : Precategory o ℓ} where intersect {I = I} F .closed x g = inc λ i → F i .closed (□-out! x i) g ``` + + ## Representing subfunctors {defines="sieves-as-presheaves"} Let $S$ be a sieve on $\cC$. We show that it determines a presheaf diff --git a/src/Cat/Instances/OFE/Product.lagda.md b/src/Cat/Instances/OFE/Product.lagda.md index c3f0dbbfb..7c8b533e1 100644 --- a/src/Cat/Instances/OFE/Product.lagda.md +++ b/src/Cat/Instances/OFE/Product.lagda.md @@ -83,7 +83,7 @@ OFE-Product A B .has-is-product .⟨_,_⟩ f g .preserves .pres-≈ p = OFE-Product A B .has-is-product .π₁∘⟨⟩ = trivial! OFE-Product A B .has-is-product .π₂∘⟨⟩ = trivial! -OFE-Product A B .has-is-product .unique p q = ext λ x → p #ₚ x , q #ₚ x +OFE-Product A B .has-is-product .unique p q = ext λ x → p #ₚ x ,ₚ q #ₚ x ``` + +```agda +module Cat.Instances.Sheaves.Omega {ℓ} {C : Precategory ℓ ℓ} (J : Coverage C ℓ) where +``` + +# Closed sieves and the subobject classifier {defines="subobject-classifier-sheaf"} + + + +The category of [[sheaves]] $\Sh(\cC, J)$ on a small [[site]] $\cC$ 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 $\Omega_J$ explicitly, as the sheaf of **$J$-closed sieves**. + +A sieve is $J$-closed if it contains every morphism it covers. This +notion is evidently closed under pullback, so the closed sieves form a +presheaf on $\cC$. + +```agda +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) +``` + + + +```agda +Ω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|separated presheaf]]. Suppose we have two closed sieves $S$, +$T$ which agree everywhere on some $R \in J(U)$. We want to show $S = +T$, so fix some $h : V \to U$; we'll show $h \in S$ iff $h \in T$. + +```agda +ΩJ .snd = from-is-separated sep mk where +``` + +It appears that we don't know much about how $S$ and $T$ behave outside +of their agreement on $R$, 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 $R$: + +```agda + 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 → Ω-ua + (λ (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 $h \in S$, we know that the pullback $h^*(S +\cap R)$ is a covering sieve. And since $h^*(T)$ is a subsieve of +$h^*(S \cap R) = h^*(T \cap R)$, we conclude that if $h \in S$, then +$h^*(T)$ is $J$-covering; and since $T$ is closed, this implies also +that $h \in T$. + +```agda + 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. + + + +```agda + in Ω-ua (λ h∈S → cT h (rem₂' h∈S)) (λ h∈T → cS h (rem₃ h∈T)) +``` + +Now we have to show that a family $S$ of compatible closed sieves over a +$J(U)$-covering sieve $R$ can be uniquely patched to a closed sieve on +$U$. This is the sieve which is defiend to contain $g : V \to U$ +whenever, for all $f : W \to V$ in $g^*(R)$, the part $S(gf)$ is the +maximal sieve. + +```agda + 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 +``` + + + +The first thing we have to show is that this pulls back to $S$. This is, +as usual, a proof of biimplication, though in this case both directions +are painful --- and entirely mechanical --- calculations. + +```agda + restrict : ∀ {V} (f : Hom V U) (hf : f ∈ R) → pullback f S' ≡ S .part f hf .fst + restrict f hf = ext λ {V} h → Ω-ua + (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 $S'$ is closed. + +```agda + 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) +``` + + diff --git a/src/Cat/Monoidal/Instances/Day.lagda.md b/src/Cat/Monoidal/Instances/Day.lagda.md index 5976d5bbc..2317d21f1 100644 --- a/src/Cat/Monoidal/Instances/Day.lagda.md +++ b/src/Cat/Monoidal/Instances/Day.lagda.md @@ -205,8 +205,8 @@ module Day (X Y : ⌞ PSh ℓ C ⌟) where Day-diagram c .F₁ ((f⁻ , g⁻) , f⁺ , g⁺) (h , x , y) = (f⁺ ⊗₁ g⁺) ∘ h , X .F₁ f⁻ x , Y .F₁ g⁻ y - Day-diagram c .F-id = ext λ h x y → eliml (-⊗- .F-id) , X .F-id #ₚ x , Y .F-id #ₚ y - Day-diagram c .F-∘ f g = ext λ h x y → pushl (-⊗- .F-∘ _ _) , X .F-∘ _ _ #ₚ _ , Y .F-∘ _ _ #ₚ _ + Day-diagram c .F-id = ext λ h x y → eliml (-⊗- .F-id) ,ₚ X .F-id #ₚ x ,ₚ Y .F-id #ₚ y + Day-diagram c .F-∘ f g = ext λ h x y → pushl (-⊗- .F-∘ _ _) ,ₚ X .F-∘ _ _ #ₚ _ ,ₚ Y .F-∘ _ _ #ₚ _ ``` --> diff --git a/src/Cat/Site/Base.lagda.md b/src/Cat/Site/Base.lagda.md index c0a2696be..518a0a784 100644 --- a/src/Cat/Site/Base.lagda.md +++ b/src/Cat/Site/Base.lagda.md @@ -262,6 +262,12 @@ module _ {o ℓ ℓs} {C : Precategory o ℓ} {A : Functor (C ^op) (Sets ℓs)} (a .glues f hf) (b .glues f hf) i Extensional-Section ⦃ e ⦄ .idsᵉ .to-path-over p = is-prop→pathp (λ i → Pathᵉ-is-hlevel 1 e (hlevel 2)) _ _ + Section-path + : ∀ {U} {S : Sieve C U} {p : Patch A S} {s s' : Section A p} + → s .whole ≡ s' .whole + → s ≡ s' + Section-path = ext + subset→patch : ∀ {U} {S S' : Sieve C U} → S' ⊆ S @@ -443,7 +449,14 @@ as its union, then the family $(U_i \cap V) \mono (U \cap V)$ has $U @@ -468,13 +482,13 @@ for sheaves, formalisation concerns lead us to instead define an ```agda is-separated : Type _ - is-separated = ∀ {U : ⌞ C ⌟} (c : J # U) → is-separated₁ A (J .cover c) + is-separated = {U : ⌞ C ⌟} (c : J ʻ U) → is-separated₁ A ⟦ c ⟧ record is-sheaf : Type (o ⊔ ℓ ⊔ ℓs ⊔ ℓc) where no-eta-equality field - whole : ∀ {U} (S : J .covers U) (p : Patch A (J .cover S)) → A ʻ U - glues : ∀ {U} (S : J .covers U) (p : Patch A (J .cover S)) → is-section A (whole S p) p + whole : {U : ⌞ C ⌟} (S : J ʻ U) (p : Patch A ⟦ S ⟧) → A ʻ U + glues : {U : ⌞ C ⌟} (S : J ʻ U) (p : Patch A ⟦ S ⟧) → is-section A (whole S p) p separate : is-separated ``` @@ -483,7 +497,7 @@ will help us in defining [[sheafifications]] later on. We can package the first two fields as saying that each patch has a section: ```agda - split : ∀ {U} {S : J .covers U} (p : Patch A (J .cover S)) → Section A p + split : {U : ⌞ C ⌟} {S : J ʻ U} (p : Patch A ⟦ S ⟧) → Section A p split p .Section.whole = whole _ p split p .Section.glues = glues _ p diff --git a/src/Cat/Site/Closure.lagda.md b/src/Cat/Site/Closure.lagda.md index 7c626b316..a6076fd75 100644 --- a/src/Cat/Site/Closure.lagda.md +++ b/src/Cat/Site/Closure.lagda.md @@ -239,7 +239,7 @@ of $J$. This is actually a pretty simple process: ```agda data _∋_ (J : Coverage C ℓs) : {U : ⌞ C ⌟} → Sieve C U → Type (o ⊔ ℓ ⊔ ℓs) where - inc : ∀ {U} (c : J .covers U) → J ∋ J .cover c + inc : {U : ⌞ C ⌟} (c : J ʻ U) → J ∋ J .cover c max : ∀ {U} {R : Sieve C U} → id ∈ R → J ∋ R @@ -272,7 +272,19 @@ sieve belongs to the saturation in at most one way. → S ⊆ R → J ∋ S → J ∋ R incl {J = J} {S = S} sr us = local us λ f hf → subst (J ∋_) refl $ max $ sr (f ∘ id) (S .closed hf id) +``` + + +```agda Saturation : Coverage C ℓs → Coverage C (o ⊔ ℓ ⊔ ℓs) Saturation J = from-stable-property (J ∋_) λ f R s → pull f s ``` diff --git a/src/Cat/Site/Grothendieck.lagda.md b/src/Cat/Site/Grothendieck.lagda.md new file mode 100644 index 000000000..f08c8fb2d --- /dev/null +++ b/src/Cat/Site/Grothendieck.lagda.md @@ -0,0 +1,95 @@ + + +```agda +module Cat.Site.Grothendieck where +``` + +# Grothendieck sites {defines="grothendieck-site grothendieck-coverage"} + +A **grothendieck topology** $J$ on a category $\cC$ is function +assigning to each $U : \cC$ a predicate $J(U)$ on the [[sieves]] on $U$, +satisfying the [[closure properties of sites]]. Every topology generates +a topology (where the space of sieves that cover $U$ is the total space +of $J(U)$), and, conversely, every site can be [saturated] to give a +topology. + +[saturated]: Cat.Site.Closure.html#saturating-sites + +```agda +record Topology {o ℓ} (C : Precategory o ℓ) ℓs : Type (o ⊔ ℓ ⊔ lsuc ℓs) where + open Precategory C + field + covering : (U : ⌞ C ⌟) (R : Sieve C U) → Type ℓs + + _◀_ : (U : ⌞ C ⌟) (R : Sieve C U) → Type ℓs + _◀_ = covering + + field + has-is-prop : ∀ {U} {R : Sieve C U} → is-prop (U ◀ R) + + stable + : ∀ {U V} (h : Hom V U) {R : Sieve C U} (hr : U ◀ R) + → V ◀ (pullback h R) + + maximal + : ∀ {U} {R : Sieve C U} → id ∈ R → U ◀ R + + local : + ∀ {U} {R : Sieve C U} (hr : U ◀ R) {S : Sieve C U} + → (∀ {V} (f : Hom V U) (hf : f ∈ R) → V ◀ pullback f S) + → U ◀ S +``` + +The main interest in defining this notion is that if we *start* with a +topology $J$, demote it to a coverage $J_c$, and then saturate this +coverage, we obtain a topology identical to the one we started with. +Since many notions in sheaf theory speak of sieves belonging to the +saturation of a coverage, if we know that we started with a topology, +then we know that we truly haven't added any "new" coverings. + +```agda + from-topology : Coverage C _ + from-topology .covers U = ∫ₚ (U ◀_) + from-topology .cover = fst + from-topology .Site.stable (R , P) f = inc ((pullback f R , stable f P) , λ h x → x) + + unsaturate : ∀ {U} {R : Sieve C U} → from-topology ∋ R → U ◀ R + unsaturate = go where + go : ∀ {U} {R : Sieve C U} → from-topology ∋ R → U ◀ R + go (Cl.inc (_ , α)) = α + go (Cl.max x) = maximal x + go (Cl.local s p) = local (go s) λ f h → go (p f h) + go (Cl.pull h x) = stable h (go x) + go (Cl.squash x y i) = has-is-prop (go x) (go y) i +``` + + diff --git a/src/Cat/Site/Instances/Atomic.lagda.md b/src/Cat/Site/Instances/Atomic.lagda.md new file mode 100644 index 000000000..93c2fbb13 --- /dev/null +++ b/src/Cat/Site/Instances/Atomic.lagda.md @@ -0,0 +1,384 @@ + + +```agda +module Cat.Site.Instances.Atomic where +``` + +# Atomic sites + +The **atomic topology** on a small category $\cC$ is the [[coverage]] +where a [[sieve]] $R$ covers an object $U$ as soon as $R$ is +[[inhabited|propositional truncation]]. If $\cC$ 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 + +~~~{.quiver} +\[\begin{tikzcd}[ampersand replacement=\&] + X \&\& A \\ + \\ + B \&\& C + \arrow["{p_2}", from=1-1, to=1-3] + \arrow["{p_1}"', from=1-1, to=3-1] + \arrow["f", from=1-3, to=3-3] + \arrow["g"', from=3-1, to=3-3] +\end{tikzcd}\] +~~~ + +in which $X$, $p_1$ and $p_2$ may be completely arbitrary. Following +Johnstone [-@Elephant, A2.1.11(h)], we refer to this condition on $\cC$ +as the **right Ore condition**. + +```agda +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 ∥ +``` + + + +Note that if this condition is satisfied, the atomic coverage is +automatically a [[Grothendieck coverage]]. + +```agda + Atomic-topology : Topology C (o ⊔ ℓ) + Atomic-topology .covering U R = ∃[ V ∈ C ] Σ[ f ∈ Hom V U ] f ∈ R + Atomic-topology .has-is-prop = hlevel 1 + 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 (_ , _ , β) +``` + + + +## Sheaves for the atomic topology + +We now want to characterise when a functor $A : \psh(\cC\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$. + + + +```agda + 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 +``` + + + +The importance of this notion is that, if a sieve $S$ is inhabited by +some $f : V \to U$, then a [[patch]] of $A$ over $S$ is precisely an +element $x : A(V)$ supported by $f$. + +```agda + 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 ∎ +``` + +
+In the other direction, we prefer to say that any $x : A(V)$ +supported by $f : V \to U$ can be extended to a patch for the sieve +generated by $f$. + + +```agda + 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) +``` + +Note that, since we have to produce an inhabitant of $A(W)$ given only a +[[truncated|propositional truncation]] factorization of $g$ through $f$, +we must use the support property to show that we always get the *same* +inhabitant. + +```agda + 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$. + +```agda + 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. + +```agda + 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$, inhabited by some $f_0 : V \to U$, and a +patch $p$ of $S$. Since we can extract an $f_0$-supported element $p_0$ +from $p$, by the "atomic sheaf" condition we obtain that there is a +contractible space of lifts $e : A(U)$ of $p_0$ through $f_0$. + +```agda + 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$. To this end, suppose that we have such an $f$, and fit it into a +commutative square + +~~~{.quiver} +\[\begin{tikzcd}[ampersand replacement=\&] + X \&\& W \\ + \\ + V \&\& U + \arrow["u", from=1-1, to=1-3] + \arrow["v"', from=1-1, to=3-1] + \arrow["f", from=1-3, to=3-3] + \arrow["{f_0}"', from=3-1, to=3-3] +\end{tikzcd}\] +~~~ + +using that $\cC$ satisfies the right Ore condition. + +```agda + 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$, which implies that there is exactly one element in $A(W)$ on which +$u$ acts to give $A(v)(p_0)$. + +```agda + 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$, and $f \in S$, we can also +calculate that $A(v)(p_0)$ is $p(f_0v)$, which is $p(fu)$ by +commutativity of the square above, and this in turn is $A(u)(pf)$. + +```agda + 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$, and that $A(v)(A(f_0)(e)) = A(u)(A(f)(e))$, so we +must have $A(f)(e) = pf$. Therefore $e$ is a section of $p$, and we are +essentially done. + +```agda + 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 1) (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*. + +```agda + Const-is-sheaf : ∀ {ℓ'} (X : Set ℓ') → is-sheaf Atomic-coverage (Const X) + Const-is-sheaf X = from-is-atomic-sheaf _ (λ _ _ _ → hlevel 0) +``` + +## 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 +*pre*sheaves are sheaves in an atomic topos, we do not need to sheafify +to obtain this latter sheaf, which simplifies the calculation +significantly. + + + +```agda + Ω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 $\id \in S$ (which is +equivalent to $S \is \top$); In the other direction, we send a +proposition $P$ to the sieve which contains any $h$ iff $P$. + +```agda + 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 +``` + + + +Finally, we can show that these maps are inverses. Note that one +direction is definitional, and the other is not much more complicated. + +```agda + ΩJ-is-constant : ΩJ cov Sh.≅ ΩJ' + ΩJ-is-constant = + let + q = ext λ i X cl → Σ-prop-path! $ ext λ x → Ω-ua + (λ 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 (ext λ _ _ → refl) q +``` diff --git a/src/Cat/Site/Sheafification.lagda.md b/src/Cat/Site/Sheafification.lagda.md index a1087cceb..5d80acb8e 100644 --- a/src/Cat/Site/Sheafification.lagda.md +++ b/src/Cat/Site/Sheafification.lagda.md @@ -49,6 +49,8 @@ module Sheafification {o ℓ ℓc} {C : Precategory o ℓ} (J : Coverage C ℓc) open Precategory C open Functor + open Coverage J using (Membership-covers) + private module A = Functor A variable @@ -86,7 +88,7 @@ respect to $s$, living in $A^+(U)$. map : (f : Hom U V) → Sheafify₀ V → Sheafify₀ U glue - : (c : J .covers U) (p : pre.Parts C map (J .cover c)) + : (c : J ʻ U) (p : pre.Parts C map (J .cover c)) → (g : pre.is-patch C map (J .cover c) p) → Sheafify₀ U ``` @@ -109,12 +111,12 @@ a section of the given patch. ```agda sep - : ∀ {x y : Sheafify₀ U} (c : J .covers U) - → (l : ∀ {V} (f : Hom V U) (hf : f ∈ J .cover c) → map f x ≡ map f y) + : ∀ {x y : Sheafify₀ U} (c : J ʻ U) + → (l : ∀ {V} (f : Hom V U) (hf : f ∈ c) → map f x ≡ map f y) → x ≡ y glues - : (c : J .covers U) (p : pre.Parts C map (J .cover c)) + : (c : J ʻ U) (p : pre.Parts C map (J .cover c)) → (g : pre.is-patch C map (J .cover c) p) → pre.is-section C map (J .cover c) (glue c p g) p ``` @@ -185,8 +187,8 @@ restriction $A^+(f)(x)$, as long as $f \in s$. ```agda → (plocal - : ∀ {U : ⌞ C ⌟} (c : J .covers U) (x : Sheafify₀ U) - → (∀ {V} (f : Hom V U) (hf : f ∈ J .cover c) → P (map f x)) → P x) + : ∀ {U : ⌞ C ⌟} (c : J ʻ U) (x : Sheafify₀ U) + → (∀ {V} (f : Hom V U) (hf : f ∈ c) → P (map f x)) → P x) → ∀ {U} (x : Sheafify₀ U) → P x ``` @@ -236,9 +238,9 @@ $P'(p(f))$ for any $f \in s$. We want to show $P(A^+(f)(\operatorname{glue} p))$ ```agda p'glue - : ∀ {U : ⌞ C ⌟} (c : J .covers U) (p : pre.Parts C map (J .cover c)) + : ∀ {U : ⌞ C ⌟} (c : J ʻ U) (p : pre.Parts C map (J .cover c)) → (g : pre.is-patch C map (J .cover c) p) - → (∀ {V} (f : Hom V U) (hf : f ∈ J .cover c) → P' (p f hf)) + → (∀ {V} (f : Hom V U) (hf : f ∈ c) → P' (p f hf)) → P' (glue c p g) ``` diff --git a/src/Order/Instances/Pointwise.lagda.md b/src/Order/Instances/Pointwise.lagda.md index e063e61e4..4cbcf2a07 100644 --- a/src/Order/Instances/Pointwise.lagda.md +++ b/src/Order/Instances/Pointwise.lagda.md @@ -126,5 +126,5 @@ Posets-has-indexed-products F = mk where .inverses .invl → ext λ where x true → refl x false → refl - .inverses .invr → ext λ x y → refl , refl + .inverses .invr → ext λ x y → refl ,ₚ refl ``` diff --git a/src/Order/Instances/Product.lagda.md b/src/Order/Instances/Product.lagda.md index 81290aa38..a2eb4fe6f 100644 --- a/src/Order/Instances/Product.lagda.md +++ b/src/Order/Instances/Product.lagda.md @@ -48,8 +48,8 @@ P ×ᵖ Q = po module ×ᵖ where po .Poset.≤-refl = P.≤-refl , Q.≤-refl po .Poset.≤-trans (f≤g , f≤g') (g≤h , g≤h') = P.≤-trans f≤g g≤h , Q.≤-trans f≤g' g≤h' - po .Poset.≤-antisym (f≤g , f≤g') (g≤f , g≤f') = ext $ - P.≤-antisym f≤g g≤f , Q.≤-antisym f≤g' g≤f' + po .Poset.≤-antisym (f≤g , f≤g') (g≤f , g≤f') = + P.≤-antisym f≤g g≤f ,ₚ Q.≤-antisym f≤g' g≤f' {-# DISPLAY ×ᵖ.po a b = a ×ᵖ b #-} infixr 20 _×ᵖ_ @@ -91,7 +91,7 @@ Posets-has-products P Q .has-is-product .⟨_,_⟩ = pairᵖ Posets-has-products P Q .has-is-product .π₁∘⟨⟩ = trivial! Posets-has-products P Q .has-is-product .π₂∘⟨⟩ = trivial! Posets-has-products P Q .has-is-product .unique α β = - ext λ x → α #ₚ x , β #ₚ x + ext λ x → α #ₚ x ,ₚ β #ₚ x ``` As a related observation, we can show that the unique partial order on