Subobject classifiers #802
Conversation
src/category-theory/monomorphisms-in-large-precategories.lagda.md
Outdated
Show resolved
Hide resolved
|
|
||
| ## Idea | ||
|
|
||
| A pullback of two morphisms `f : hom y x` and `g : hom z x` in a category `C` |
There was a problem hiding this comment.
| A pullback of two morphisms `f : hom y x` and `g : hom z x` in a category `C` | |
| A **pullback** of two morphisms `f : hom y x` and `g : hom z x` in a [category](category-theory.categories.md) `C` |
We write terms in boldface when defining them, and add links when mentioning terms for the first time in a file that are defined elsewhere.
| - `p₁ ∘ h = p₁'` | ||
| - `p₂ ∘ h = p₂'`. | ||
|
|
||
| We say that `C` has all pullbacks if there is a choice of a pullback for each |
There was a problem hiding this comment.
| We say that `C` has all pullbacks if there is a choice of a pullback for each | |
| We say that `C` **has all pullbacks** if there is a choice of a pullback for each |
| (x : obj-Large-Precategory C l1) | ||
| (y : obj-Large-Precategory C l2) | ||
| (z : obj-Large-Precategory C l3) | ||
| (f : hom-Large-Precategory C y x) | ||
| (g : hom-Large-Precategory C z x) | ||
| (w : obj-Large-Precategory C l4) |
There was a problem hiding this comment.
You probably want x y z and w to be implicit arguments here, unless Agda is unable to infer them generally
There was a problem hiding this comment.
Good point! I'll change this in the other file too.
There was a problem hiding this comment.
Also, when they are implicit, I would place w right after z instead
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
| Σ (obj-Large-Precategory C l4) λ w → | ||
| Σ (hom-Large-Precategory C w y) λ p₁ → | ||
| Σ (hom-Large-Precategory C w z) λ p₂ → | ||
| Σ (comp-hom-Large-Precategory C f p₁ | ||
| ＝ comp-hom-Large-Precategory C g p₂) λ α → | ||
| is-pullback-Large-Precategory x y z f g w p₁ p₂ α |
There was a problem hiding this comment.
The proper formatting for this is
| Σ (obj-Large-Precategory C l4) λ w → | |
| Σ (hom-Large-Precategory C w y) λ p₁ → | |
| Σ (hom-Large-Precategory C w z) λ p₂ → | |
| Σ (comp-hom-Large-Precategory C f p₁ | |
| ＝ comp-hom-Large-Precategory C g p₂) λ α → | |
| is-pullback-Large-Precategory x y z f g w p₁ p₂ α | |
| Σ ( obj-Large-Precategory C l4) | |
| ( λ w → | |
| Σ ( hom-Large-Precategory C w y) | |
| ( λ p → | |
| Σ ( hom-Large-Precategory C w z) | |
| ( λ q → | |
| Σ ( comp-hom-Large-Precategory C f p ＝ | |
| comp-hom-Large-Precategory C g q) | |
| ( is-pullback-Large-Precategory x y z f g w p q)))) |
(if that stays within the 80-character limit)
| morphism-into-pullback-Large-Precategory : | ||
| hom-Large-Precategory C w' object-pullback-Large-Precategory | ||
| morphism-into-pullback-Large-Precategory = | ||
| pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)) |
There was a problem hiding this comment.
You will want to define named projections for things like this instead of using cryptic composites of pr1 and pr2. Maybe a good reference for how to do this is to look at how we define projections of (small) precategories.
| (g : hom-Large-Precategory C z x) | ||
| where | ||
|
|
||
| object-pullback-Large-Precategory : obj-Large-Precategory C l2 |
| object-pullback-Large-Precategory : obj-Large-Precategory C l2 | ||
| object-pullback-Large-Precategory = pr1 (t x y z f g) | ||
|
|
||
| pr1-pullback-Large-Precategory : |
There was a problem hiding this comment.
Usually, I would want to say that you should take a look at foundation.pullbacks for how to name these. Sadly, that file is in need of refactoring as well. But you can have a look at foundation.cones-over-cospans for how to name these.
| comp-hom-Large-Precategory C f p₁ ＝ comp-hom-Large-Precategory C g p₂ → | ||
| UU (α l1 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔ β l1 l4) | ||
| is-pullback-Large-Precategory x y z f g w p₁ p₂ _ = | ||
| (w' : obj-Large-Precategory C l1) → |
There was a problem hiding this comment.
w' must be able to live at any universe level
There was a problem hiding this comment.
this should mirror the definition of universal-property-pullback in foundation-core.universal-property-pullbacks
There was a problem hiding this comment.
Just to confirm your question earlier, using the above reference, x, y, z, and w should indeed all be able to have different universe levels.
| (p₁' : hom-Large-Precategory C w' y) → | ||
| (p₂' : hom-Large-Precategory C w' z) → | ||
| comp-hom-Large-Precategory C f p₁' ＝ comp-hom-Large-Precategory C g p₂' → | ||
| ∃! |
There was a problem hiding this comment.
Instead of using unique existence, we prefer to define universal properties in terms of certain evaluation maps being equivalences. Here, that unfolds to requiring that the map that sends a morphism w' -> w, where w is the pullback, to the cone constructed by postcomposing with f and g being an iso in the (large) span precategory with fixed codomains y and z. Maybe Egbert has a different opinion on this, but that is what I would say this definition should be at the moment.
There was a problem hiding this comment.
Maybe to expand a little on the above remark. Notice how this definition makes itself more readily available for use with univalence down the line.
There was a problem hiding this comment.
I'm not sure I understand how this would be an isomorphism in the category of spans. Do you mean that postcomposition with f and g forms equivalence between the slice category C/w and the category of spans with codomains y and z?
There was a problem hiding this comment.
Ah, yes, my bad, you're right!
There was a problem hiding this comment.
Also, I shouldn't have said span category. It's the cone category over the cospan of f and g. And the cone is constructed by postcomposing with p and q, not f and g.
| is-prop-is-pullback-Large-Precategory : | ||
| is-prop (is-pullback-Large-Precategory C x y z f g w p₁ p₂ α₁) | ||
| is-prop-is-pullback-Large-Precategory = | ||
| is-prop-Π³ (λ w' p₁' p₂' → is-prop-function-type is-property-is-contr) |
There was a problem hiding this comment.
Note that we are changing is-prop-Π³ to a general is-prop-iterated-Π 3 with #797 😁
|
Do let me know if you have any questions about my comments! |
|
If this helps, they are currently working on formalizing elementary topoi over at 1lab. See in particular here for the subobject classifier: https://github.com/plt-amy/1lab/blob/e2c7a58fcf534c0611dd8bdea7d054f1eb80bd28/src/Cat/Diagram/Subobject.lagda.md, and note that they take a fibrational approach. Are you planning on taking a similar path? If so, that would be super neat! I was hoping to do some basic work on fibrations of categories at some point, but I don't currently know when/if I will take the time to do that. |
|
Hi @maybemabeline! How is this PR going? |
|
That's too bad! Do get in touch if you want to coordinate on working towards formalizing this in the future, @maybemabeline. A little bit of topos theory wouldn't hurt the library :) I also did refactor pullbacks in types a bit in one of my recent PRs (#839), so that should give a better starting point now. |
|
No pressure though, there's an endless supply of cool things to formalize. 😄 |
I plan to implement subobject classifiers, construct them in the category of presheaves and prove some adjacent results.
To start off I realized I need pullbacks in large precategories, so I tried enlarging the file. The object w' in line 123 is forced to be at level l1 by the following functions though and I can't seem to tell why. I also added the type of all monomorphisms in a large precategory.