diff --git a/src/Cat/Diagram/Pullback.lagda.md b/src/Cat/Diagram/Pullback.lagda.md index cb68b0d37..703145c98 100644 --- a/src/Cat/Diagram/Pullback.lagda.md +++ b/src/Cat/Diagram/Pullback.lagda.md @@ -149,6 +149,13 @@ module _ {o ℓ} {C : Precategory o ℓ} where instance H-Level-is-pullback : ∀ {P} {p₁ : Hom P X} {f : Hom X Z} {p₂ : Hom P Y} {g : Hom Y Z} {n} → H-Level (is-pullback C p₁ f p₂ g) (suc n) H-Level-is-pullback = prop-instance is-pullback-is-prop + + subst-is-pullback + : ∀ {P} {p₁ p₁' : Hom P X} {f f' : Hom X Z} {p₂ p₂' : Hom P Y} {g g' : Hom Y Z} + → p₁ ≡ p₁' → f ≡ f' → p₂ ≡ p₂' → g ≡ g' + → is-pullback C p₁ f p₂ g + → is-pullback C p₁' f' p₂' g' + subst-is-pullback p q r s = transport (λ i → is-pullback C (p i) (q i) (r i) (s i)) ``` --> diff --git a/src/Cat/Diagram/Pullback/Along.lagda.md b/src/Cat/Diagram/Pullback/Along.lagda.md new file mode 100644 index 000000000..63ceb24f5 --- /dev/null +++ b/src/Cat/Diagram/Pullback/Along.lagda.md @@ -0,0 +1,130 @@ + + +```agda +module Cat.Diagram.Pullback.Along where +``` + + + +# Pullbacks along an indeterminate morphism + + + +This module defines the auxiliary notion of a map $p_1 : P \to X$ being +the [[pullback]] of a map $g : Y \to Z$ along a map $f : X \to Z$, by +summing over the possible maps $P \to Y$ fitting in the diagram below. + +~~~{.quiver} +\[\begin{tikzcd}[ampersand replacement=\&] + P \&\& Y \\ + \\ + X \&\& Z + \arrow[dashed, from=1-1, to=1-3] + \arrow["{p_1}"', from=1-1, to=3-1] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-3] + \arrow["g", from=1-3, to=3-3] + \arrow["f"', from=3-1, to=3-3] +\end{tikzcd}\] +~~~ + +While this is a rather artificial notion, it comes up a lot in the +context of [[elementary topos]] theory, especially in the case where $g$ +is the [[generic subobject]] $\true : \top \to \Omega$. + +```agda + record is-pullback-along {P X Y Z} (p₁ : Hom P X) (f : Hom X Z) (g : Hom Y Z) : Type (o ⊔ ℓ) where + no-eta-equality + field + top : Hom P Y + has-is-pb : is-pullback C p₁ f top g + open is-pullback has-is-pb public +``` + + + +::: warning +Despite the name `is-pullback-along`{.Agda}, nothing about the +definition guarantees that this type is a [[proposition]] after fixing +the three maps $p_1$, $f$ and $g$. However, we choose to name this +auxiliary notion as though it were always a proposition, since it will +most commonly be used when $g$ is a [[monomorphism]], and, under this +assumption, it *is* propositional: +::: + +```agda + is-monic→is-pullback-along-is-prop + : ∀ {P X Y Z} {f : Hom P X} {g : Hom X Z} {h : Hom Y Z} + → is-monic h + → is-prop (is-pullback-along C f g h) + is-monic→is-pullback-along-is-prop h-monic = Iso→is-hlevel 1 eqv λ (_ , x) (_ , y) → + Σ-prop-path! (h-monic _ _ (sym (x .square) ∙ y .square)) +``` + +Of course, the notion of being a pullback *along* a map is closed under +composition: if $k$ is the pullback of $l$ along $n$, and $h$ is the +pullback of $k$ along $m$, as in the diagram below, then $h$ is also the +pullback of $l$ along $n \circ m$. + +~~~{.quiver} +\[\begin{tikzcd}[ampersand replacement=\&] + U \&\& V \&\& W \\ + \\ + X \&\& Y \&\& Z + \arrow[dashed, from=1-1, to=1-3] + \arrow["h"', from=1-1, to=3-1] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-3] + \arrow[dashed, from=1-3, to=1-5] + \arrow["k"{description}, from=1-3, to=3-3] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=3-5] + \arrow["l", from=1-5, to=3-5] + \arrow["m"', from=3-1, to=3-3] + \arrow["n"', from=3-3, to=3-5] +\end{tikzcd}\] +~~~ + +```agda + paste-is-pullback-along + : is-pullback-along C k n l → is-pullback-along C h m k + → n ∘ m ≡ nm → is-pullback-along C h nm l + paste-is-pullback-along p q r .top = p .top ∘ q .top + paste-is-pullback-along p q r .has-is-pb = + subst-is-pullback refl r refl refl (rotate-pullback (pasting-left→outer-is-pullback + (rotate-pullback (p .has-is-pb)) + (rotate-pullback (q .has-is-pb)) + ( extendl (sym (p .is-pullback-along.square)) + ∙ pushr (sym (q .is-pullback-along.square))))) +``` diff --git a/src/Cat/Diagram/Subobject.lagda.md b/src/Cat/Diagram/Subobject.lagda.md new file mode 100644 index 000000000..61e193e5f --- /dev/null +++ b/src/Cat/Diagram/Subobject.lagda.md @@ -0,0 +1,324 @@ + + +```agda +module Cat.Diagram.Subobject where +``` + +# Subobject classifiers {defines="generic-subobject subobject-classifier"} + +In an arbitrary category $\cC$, a [[subobject]] of $X$ is, colloquially +speaking, given by a monomorphism $m : A \mono X$. Formally, though, we +must consider the object $A$ to be part of this data, since we can only +speak of morphisms if we already know their domain and codomain. The +generality in the definition means that the notion of subobject applies +to completely arbitrary $\cC$, but in completely arbitrary situations, +the notion might be _very_ badly behaved. + +There are several observations we can make about $\cC$ that "tame" the +behaviour of $\Sub_{\cC}(X)$. For example, if it has [[pullbacks]], then +$\Sub(-)$ is a [[fibration]], so that there is a universal way of +re-indexing a subobject $x : \Sub(X)$ along a morphism $f : Y \to X$, +and if it has [[images]], it's even a [[bifibration]], so that each of +these reindexings has a [[left adjoint]], giving an interpretation of +existential quantifiers. If $\cC$ is a [[regular category]], existential +quantifiers and substitution commute, restricting the behaviour of +subobjects even further. + +However, there is one assumption we can make about $\cC$ that rules them +all: it has a **generic subobject**, so that $\Sub(X)$ is equivalent to +a given $\hom$-set in $\cC$. A generic subobject is a morphism $\top : +\Omega* \to \Omega$ so that, for any a subobject $m : A \mono X$, there +is a _unique_ arrow $\name{m}$ making the square + +~~~{.quiver} +\[\begin{tikzcd}[ampersand replacement=\&] + A \&\& \Omega* \\ + \\ + X \&\& \Omega + \arrow["", from=1-1, to=1-3] + \arrow["\top", from=1-3, to=3-3] + \arrow["{\name{m}}"', from=3-1, to=3-3] + \arrow["m"', hook, from=1-1, to=3-1] +\end{tikzcd}\] +~~~ + +into a pullback. We can investigate this definition by instantiating it +in $\Sets$, which _does_ have a generic subobject. Given an +[[embedding]] $m : A \mono X$, we have a family of propositions +$\name{m} : X \to \Omega$ which maps $x : X$ to $m^*(x)$, the +`fibre`{.Agda} of $m$ over $x$. The square above _also_ computes a +fibre, this time of $\name{m}$, and saying that it is $m$ means that +$\name{m}$ assigns $\top$ to precisely those $x : X$ which are in $m$. + + + +```agda + record is-generic-subobject {Ω} (true : Subobject Ω) : Type (o ⊔ ℓ) where + field + name : ∀ {X} (m : Subobject X) → Hom X Ω + classifies + : ∀ {X} (m : Subobject X) + → is-pullback-along C (m .map) (name m) (true .map) + unique + : ∀ {X} {m : Subobject X} {nm : Hom X Ω} + → is-pullback-along C (m .map) nm (true .map) + → nm ≡ name m +``` + +::: terminology +We follow [@Elephant, A1.6] for our terminology: the morphism $\top : 1 +\to \Omega$ is called the **generic subobject**, and $\Omega$ is the +**subobject classifier**. This differs from the terminology in the +[nLab](https://ncatlab.org/nlab/show/subobject+classifier), where the +_morphism_ $\top$ is called the subobject classifier. +::: + +```agda + record Subobject-classifier : Type (o ⊔ ℓ) where + field + {Ω} : Ob + true : Subobject Ω + generic : is-generic-subobject true + open is-generic-subobject generic public +``` + +While the definition of `is-generic-subobject`{.Agda} can be stated +without assuming that $\cC$ has any limits at all, we'll need to assume +that $\cC$ has [[pullbacks]] to get anything of value done. Before we +get started, however, we'll prove a helper theorem that serves as a +"smart constructor" for `Subobject-classifier`{.Agda}, simplifying the +verification of the universal property in case $\cC$ is +[[univalent|univalent category]] and has all [[finite limits]] (in +particular, a [[terminal object]]). + + + +Assuming that we have a terminal object, we no longer need to specify +the arrow $\true$ as an arbitrary element of $\Sub(\Omega)$ --- we can +instead ask for a *point* $\true : \top \to \Omega$ instead. Since we +have pullbacks, we also have the change-of-base operation $f^*(-) : +\Sub(B) \to \Sub(A)$ for any $f : A \to B$, which allows us to +simplify the condition that "$m$ is the pullback of $n$ `along`{.Agda +ident=is-pullback-along} $f$", which requires constructing a pullback +square, to the simpler $m \cong f^*n$. The theorem is that it suffices +to ask for: + +- The point $\true : \top \to \Omega$ corresponding to the generic + subobject, +- An operation $\name{-} : \Sub(A) \to \hom(A, \Omega)$ which maps + subobjects to their names, +- A witness that, for any $m : \Sub(A)$, we have + $m \cong \name{m}^*\true$, and +- A witness that, for any $h : \hom(A, \Omega)$, we have + $h = \name{h^*\true}$. + +These two conditions amount to saying that $\name{-}$ and $(-)^*\top$ +form an [[equivalence]] between the sets $\Sub(A)$ and $\hom(A, +\Omega)$, for all $A$. Note that we do not need to assume naturality for +$\name{-}$ since it is an inverse equivalence to $(-)^*\true$, which is +already natural. + +```agda + from-classification + : ∀ {Ω} (true : Hom top Ω) + → (name : ∀ {A} (m : Subobject A) → Hom A Ω) + → (∀ {A} (m : Subobject A) → m ≅ₘ name m ^* pt true) + → (∀ {A} (h : Hom A Ω) → name (h ^* pt true) ≡ h) + → Subobject-classifier C + from-classification tru nm invl invr = done where + done : Subobject-classifier C + done .Ω = _ + done .true = pt tru + done .generic .name = nm + done .generic .classifies m = iso→is-pullback-along {m = m} {n = pt tru} (invl m) +``` + +Note that the uniqueness part of the universal property is satisfied by +the last constraint on $\name{-}$: the `is-pullback-along`{.Agda} +assumption amounts to saying that $m \is h'^*\true$, by univalence of +$\Sub(A)$; so we have $$\name{m} = \name{h'^*\true} = h'$$. + +```agda + done .generic .unique {m = m} {h'} p = + let + rem₁ : m ≡ h' ^* pt tru + rem₁ = Sub-is-category cat .to-path $ + is-pullback-along→iso {m = m} {n = pt tru} p + in sym (ap nm rem₁ ∙ invr _) +``` + + + +The prototypical category with a subobject classifier is the category of +sets. Since it is finitely complete and univalent, our helper above will +let us swiftly dispatch the construction. Our subobject classifier is +given by the type of propositions, $\Omega$, lifted to the right +universe. The name of a subobject $m : \Sub(A)$ is the family of +propositions $x \mapsto m^*(x)$. Note that we must squash this fibre +down so it fits in $\Omega$, but this squashing is benign because $m$ is +a monomorphism (hence, an embedding). + + +```agda + unbox : ∀ {A : Set ℓ} (m : Subobject A) {x} → □ (fibre (m .map) x) → fibre (m .map) x + unbox m = □-out (monic→is-embedding (hlevel 2) (λ {C} g h p → m .monic {C} g h p) _) + + mk : make-subobject-classifier _ _ + mk .make-subobject-classifier.Ω = el! (Lift _ Ω) + mk .true _ = lift ⊤Ω + mk .name m x = lift (elΩ (fibre (m .map) x)) +``` + +Showing that this `name`{.Agda} function actually works takes a bit of +fiddling, but it's nothing outrageous. + +```agda + mk .named-name m = Sub-antisym + record + { map = λ w → m .map w , lift tt , ap lift (to-is-true (inc (w , refl))) + ; sq = refl + } + record { sq = ext λ x _ p → sym (unbox m (from-is-true p) .snd )} + mk .name-named h = ext λ a → Ω-ua + (rec! λ x _ p y=a → from-is-true (ap h (sym y=a) ∙ p)) + (λ ha → inc ((a , lift tt , ap lift (to-is-true ha)) , refl)) +``` + + diff --git a/src/Cat/Displayed/Instances/Subobjects.lagda.md b/src/Cat/Displayed/Instances/Subobjects.lagda.md index 3a8d727f0..b36908db9 100644 --- a/src/Cat/Displayed/Instances/Subobjects.lagda.md +++ b/src/Cat/Displayed/Instances/Subobjects.lagda.md @@ -30,7 +30,7 @@ open Displayed ``` --> -# The fibration of subobjects {defines="poset-of-subobjects"} +# The fibration of subobjects {defines="poset-of-subobjects subobject"} Given a base category $\cB$, we can define the [[displayed category]] of _subobjects_ over $\cB$. This is, in essence, a restriction of the @@ -159,25 +159,30 @@ Now given the data in red, we verify that the dashed arrow exists, which is enough for its uniqueness. ```agda +-- The blue square: +pullback-subobject + : has-pullbacks B + → ∀ {X Y} (h : Hom X Y) (g : Subobject Y) + → Subobject X +pullback-subobject pb h g .domain = pb h (g .map) .apex +pullback-subobject pb h g .map = pb h (g .map) .p₁ +pullback-subobject pb h g .monic = is-monic→pullback-is-monic + (g .monic) (rotate-pullback (pb h (g .map) .has-is-pb)) + Subobject-fibration : has-pullbacks B → Cartesian-fibration Subobjects Subobject-fibration pb .has-lift f y' = l where - it : Pullback _ _ _ - it = pb (y' .map) f l : Cartesian-lift Subobjects f y' - -- The blue square: - l .x' .domain = it .apex - l .x' .map = it .p₂ - l .x' .monic = is-monic→pullback-is-monic (y' .monic) (it .has-is-pb) - l .lifting .map = it .p₁ - l .lifting .sq = sym (it .square) + l .x' = pullback-subobject pb f y' + l .lifting .map = pb f (y' .map) .p₂ + l .lifting .sq = pb f (y' .map) .square -- The dashed red arrow: l .cartesian .universal {u' = u'} m h' = λ where - .map → it .Pullback.universal (sym (h' .sq) ∙ sym (assoc f m (u' .map))) - .sq → sym (it .p₂∘universal) + .map → pb f (y' .map) .universal (pushr refl ∙ h' .sq) + .sq → sym (pb f (y' .map) .p₁∘universal) l .cartesian .commutes _ _ = prop! l .cartesian .unique _ _ = prop! ``` diff --git a/src/Cat/Displayed/Instances/Subobjects/Reasoning.lagda.md b/src/Cat/Displayed/Instances/Subobjects/Reasoning.lagda.md new file mode 100644 index 000000000..c17523c72 --- /dev/null +++ b/src/Cat/Displayed/Instances/Subobjects/Reasoning.lagda.md @@ -0,0 +1,153 @@ + + +```agda +module Cat.Displayed.Instances.Subobjects.Reasoning + {o ℓ} {C : Precategory o ℓ} (pb : has-pullbacks C) where +``` + + + +# Subobjects in a cartesian category + +```agda +_^*_ : (f : Hom X Y) (m : Subobject Y) → Subobject X +f ^* m = pullback-subobject pb f m + +^*-univ : ≤-over f m n → m ≤ₘ f ^* n +^*-univ = Cartesian-fibration.has-lift.universalv (Subobject-fibration pb) _ _ + +infixr 35 _^*_ + +^*-id : id ^* m ≅ₘ m +^*-id .to = Ix.^*-id-to +^*-id .from = Ix.^*-id-from +^*-id .inverses = record { invl = prop! ; invr = prop! } + +^*-assoc : f ^* (g ^* m) ≅ₘ (g ∘ f) ^* m +^*-assoc .to = Ix.^*-comp-from +^*-assoc .from = Ix.^*-comp-to +^*-assoc .inverses = record { invl = prop! ; invr = prop! } + +⊤ₘ : Subobject X +⊤ₘ .domain = _ +⊤ₘ .map = id +⊤ₘ .monic = id-monic + +opaque + !ₘ : m ≤ₘ ⊤ₘ + !ₘ {m = m} = record { map = m .map ; sq = refl } + +opaque + _∩ₘ_ : Subobject X → Subobject X → Subobject X + m ∩ₘ n = Sub-products pb m n .Product.apex + + infixr 30 _∩ₘ_ + +opaque + unfolding _∩ₘ_ + + ∩ₘ≤l : m ∩ₘ n ≤ₘ m + ∩ₘ≤l = Sub-products pb _ _ .Product.π₁ + + ∩ₘ≤r : m ∩ₘ n ≤ₘ n + ∩ₘ≤r = Sub-products pb _ _ .Product.π₂ + + ∩ₘ-univ : ∀ {p} → p ≤ₘ m → p ≤ₘ n → p ≤ₘ m ∩ₘ n + ∩ₘ-univ = Sub-products pb _ _ .Product.⟨_,_⟩ + +opaque + ∩ₘ-idl : ⊤ₘ ∩ₘ m ≅ₘ m + ∩ₘ-idl = Sub-antisym ∩ₘ≤r (∩ₘ-univ !ₘ Sub.id) + + ∩ₘ-idr : m ∩ₘ ⊤ₘ ≅ₘ m + ∩ₘ-idr = Sub-antisym ∩ₘ≤l (∩ₘ-univ Sub.id !ₘ) + + ∩ₘ-assoc : l ∩ₘ m ∩ₘ n ≅ₘ (l ∩ₘ m) ∩ₘ n + ∩ₘ-assoc = Sub-antisym + (∩ₘ-univ (∩ₘ-univ ∩ₘ≤l (∩ₘ≤l Sub.∘ ∩ₘ≤r)) (∩ₘ≤r Sub.∘ ∩ₘ≤r)) + (∩ₘ-univ (∩ₘ≤l Sub.∘ ∩ₘ≤l) (∩ₘ-univ (∩ₘ≤r Sub.∘ ∩ₘ≤l) ∩ₘ≤r)) + +opaque + unfolding _∩ₘ_ + + ^*-∩ₘ : f ^* (m ∩ₘ n) ≅ₘ f ^* m ∩ₘ f ^* n + ^*-∩ₘ {f = f} {m = m} {n = n} = Sub-antisym + (∩ₘ-univ + (^*-univ record { sq = pb _ _ .square ∙ pullr refl }) + (^*-univ record { sq = pb _ _ .square ∙ pullr refl ∙ extendl (pb _ _ .square) })) + record + { map = pb _ _ .universal + {p₁' = pb _ _ .p₁ ∘ pb _ _ .p₁} + {p₂' = pb _ _ .universal {p₁' = pb _ _ .p₂ ∘ pb _ _ .p₁} {p₂' = pb _ _ .p₂ ∘ pb _ _ .p₂} + (pulll (sym (pb _ _ .square)) ∙ pullr (pb _ _ .square) ∙ extendl (pb _ _ .square))} + (sym (pullr (pb _ _ .p₁∘universal) ∙ extendl (sym (pb _ _ .square)))) + ; sq = sym (pb _ _ .p₁∘universal ∙ introl refl) + } + + ^*-⊤ₘ : f ^* ⊤ₘ ≅ₘ ⊤ₘ + ^*-⊤ₘ {f = f} = Sub-antisym !ₘ record + { map = pb _ _ .universal {p₁' = id} {p₂' = f} id-comm + ; sq = sym (pb _ _ .p₁∘universal ∙ introl refl) + } + +opaque + is-pullback-along→iso : is-pullback-along C (m .map) h (n .map) → m ≅ₘ h ^* n + is-pullback-along→iso pba = Sub-antisym + record { map = pb _ _ .universal (pba .square) ; sq = sym (pb _ _ .p₁∘universal ∙ introl refl) } + record { map = pba .universal (pb _ _ .square) ; sq = sym (pba .p₁∘universal ∙ introl refl) } + + iso→is-pullback-along : m ≅ₘ h ^* n → is-pullback-along C (m .map) h (n .map) + iso→is-pullback-along _ .top = _ + iso→is-pullback-along {h = h} {n = n} m .has-is-pb = subst-is-pullback + (sym (m .Sub.to .sq) ∙ idl _) refl refl refl + (is-pullback-iso + record + { to = m .Sub.from .map + ; from = m .Sub.to .map + ; inverses = record + { invl = ap ≤-over.map (m .Sub.invr) + ; invr = ap ≤-over.map (m .Sub.invl) + } + } + (pb h (n .map) .has-is-pb)) +``` diff --git a/src/Cat/Morphism.lagda.md b/src/Cat/Morphism.lagda.md index d1ad6efc2..ae573d5fd 100644 --- a/src/Cat/Morphism.lagda.md +++ b/src/Cat/Morphism.lagda.md @@ -49,6 +49,8 @@ open _↪_ public @@ -498,6 +500,18 @@ inverses→invertible : ∀ {f : Hom a b} {g : Hom b a} → Inverses f g → is- inverses→invertible x .is-invertible.inv = _ inverses→invertible x .is-invertible.inverses = x +_≅⟨_⟩_ : ∀ (x : Ob) {y z} → x ≅ y → y ≅ z → x ≅ z +x ≅⟨ p ⟩ q = p ∘Iso q + +_≅˘⟨_⟩_ : ∀ (x : Ob) {y z} → y ≅ x → y ≅ z → x ≅ z +x ≅˘⟨ p ⟩ q = (p Iso⁻¹) ∘Iso q + +_≅∎ : (x : Ob) → x ≅ x +x ≅∎ = id-iso + +infixr 2 _≅⟨_⟩_ _≅˘⟨_⟩_ +infix 3 _≅∎ + invertible→iso : (f : Hom a b) → is-invertible f → a ≅ b invertible→iso f x = record diff --git a/src/Cat/Topos/Elementary.lagda.md b/src/Cat/Topos/Elementary.lagda.md new file mode 100644 index 000000000..8cff583f3 --- /dev/null +++ b/src/Cat/Topos/Elementary.lagda.md @@ -0,0 +1,11 @@ + + +```agda +module Cat.Topos.Elementary where +``` + +# Elementary topoi {defines="elementary-topos elementary-topoi"} diff --git a/src/preamble.tex b/src/preamble.tex index 318c08561..27a8a679a 100644 --- a/src/preamble.tex +++ b/src/preamble.tex @@ -160,6 +160,9 @@ \DeclareMathOperator{\glue}{glue} \DeclareMathOperator{\unglue}{unglue} +\newcommand{\true}{\mathtt{true}} +\newcommand{\name}[1]{\ulcorner #1 \urcorner} + \renewcommand{\day}[1]{\operatorname{day}(#1)} \newcommand{\loc}[1]{[{#1}\inv]}