Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Subobject classifiers #802

Closed
wants to merge 5 commits into from
Closed

Subobject classifiers #802

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
738a7eb
Add pullbacks in large precategories
maybemabeline Sep 28, 2023
753b8ed
Add missing file
maybemabeline Sep 28, 2023
8f2b187
Update src/category-theory/pullbacks-in-large-precategories.lagda.md
maybemabeline Sep 28, 2023
92031c9
Deindex variables and unnest module
maybemabeline Sep 29, 2023
bff8acd
Reformat path algebra
maybemabeline Sep 29, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions src/category-theory.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,13 +112,15 @@ open import category-theory.pregroupoids public
open import category-theory.presheaf-categories public
open import category-theory.products-in-precategories public
open import category-theory.products-of-precategories public
open import category-theory.pullbacks-in-large-precategories public
open import category-theory.pullbacks-in-precategories public
open import category-theory.representable-functors-categories public
open import category-theory.representable-functors-large-precategories public
open import category-theory.representable-functors-precategories public
open import category-theory.representing-arrow-category public
open import category-theory.sieves-in-categories public
open import category-theory.slice-precategories public
open import category-theory.subobject-classifier-in-large-precategories public
open import category-theory.subprecategories public
open import category-theory.terminal-objects-precategories public
open import category-theory.yoneda-lemma-categories public
Expand Down
28 changes: 28 additions & 0 deletions src/category-theory/monomorphisms-in-large-precategories.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ open import category-theory.isomorphisms-in-large-precategories
open import category-theory.large-precategories

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.identity-types
Expand Down Expand Up @@ -51,6 +52,33 @@ module _
is-prop-type-Prop is-mono-prop-Large-Precategory
```

## The type of monomorphisms in a large precategory

```agda
module _
{α : Level → Level} {β : Level → Level → Level}
(C : Large-Precategory α β) {l1 l2 : Level} (l3 : Level)
(X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2)
where

mono-Large-Precategory : UU (α l3 ⊔ β l3 l1 ⊔ β l3 l2 ⊔ β l1 l2)
mono-Large-Precategory =
Σ
( hom-Large-Precategory C X Y)
( is-mono-Large-Precategory C l3 X Y)

module _
(f : mono-Large-Precategory)
where
maybemabeline marked this conversation as resolved.
Show resolved Hide resolved

hom-mono-Large-Precategory : hom-Large-Precategory C X Y
hom-mono-Large-Precategory = pr1 f

is-mono-mono-Large-Precategory :
is-mono-Large-Precategory C l3 X Y hom-mono-Large-Precategory
is-mono-mono-Large-Precategory = pr2 f
```

## Properties

### Isomorphisms are monomorphisms
Expand Down
186 changes: 186 additions & 0 deletions src/category-theory/pullbacks-in-large-precategories.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,186 @@
# Pullbacks in large precategories

```agda
module category-theory.pullbacks-in-large-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.large-precategories

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.unique-existence
open import foundation.universe-levels
```

</details>

## Idea

A pullback of two morphisms `f : hom y x` and `g : hom z x` in a category `C`
Copy link
Collaborator

@fredrik-bakke fredrik-bakke Sep 28, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
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.

consists of:

- an object `w`
- morphisms `p₁ : hom w y` and `p₂ : hom w z` such that
- `f ∘ p₁ = g ∘ p₂` together with the universal property that for every object
`w'` and pair of morphisms `p₁' : hom w' y` and `p₂' : hom w' z` such that
`f ∘ p₁' = g ∘ p₂'` there exists a unique morphism `h : hom w' w` such that
- `p₁ ∘ h = p₁'`
- `p₂ ∘ h = p₂'`.
maybemabeline marked this conversation as resolved.
Show resolved Hide resolved

We say that `C` has all pullbacks if there is a choice of a pullback for each
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
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

object `x` and pair of morphisms into `x` in `C`.

## Definition

```agda
module _
{α : Level → Level} {β : Level → Level → Level}
(C : Large-Precategory α β) {l1 l2 l3 l4 : Level}
where

is-pullback-Large-Precategory :
(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) →
maybemabeline marked this conversation as resolved.
Show resolved Hide resolved
(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₂ →
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) →
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

w' must be able to live at any universe level

Copy link
Collaborator

@fredrik-bakke fredrik-bakke Sep 28, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this should mirror the definition of universal-property-pullback in foundation-core.universal-property-pullbacks

Copy link
Collaborator

@fredrik-bakke fredrik-bakke Sep 28, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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₂' →
∃!
Copy link
Collaborator

@fredrik-bakke fredrik-bakke Sep 28, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, yes, my bad, you're right!

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

( hom-Large-Precategory C w' w)
( λ h →
( comp-hom-Large-Precategory C p₁ h ＝ p₁') ×
( comp-hom-Large-Precategory C p₂ h ＝ p₂'))

pullback-Large-Precategory :
(x : obj-Large-Precategory C l1) →
(y : obj-Large-Precategory C l2) →
(z : obj-Large-Precategory C l3) →
hom-Large-Precategory C y x →
hom-Large-Precategory C z x →
UU (α l1 ⊔ α l4 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔
β l1 l4 ⊔ β l4 l1 ⊔ β l4 l2 ⊔ β l4 l3)
pullback-Large-Precategory x y z f g =
Σ (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₂ α
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The proper formatting for this is

Suggested change
Σ (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)


has-all-pullbacks-Large-Precategory :
UU (α l1 ⊔ α l2 ⊔ α l3 ⊔ α l4 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔
β l1 l4 ⊔ β l2 l1 ⊔ β l3 l1 ⊔ β l4 l1 ⊔ β l4 l2 ⊔ β l4 l3)
has-all-pullbacks-Large-Precategory =
(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) →
pullback-Large-Precategory x y z f g

module _
{α : Level → Level} {β : Level → Level → Level}
(C : Large-Precategory α β) {l1 l2 : Level}
(t : has-all-pullbacks-Large-Precategory C)
(x y z : obj-Large-Precategory C l1)
(f : hom-Large-Precategory C y x)
(g : hom-Large-Precategory C z x)
where

object-pullback-Large-Precategory : obj-Large-Precategory C l2
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

obj-pullback-...

object-pullback-Large-Precategory = pr1 (t x y z f g)

pr1-pullback-Large-Precategory :
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

hom-Large-Precategory C object-pullback-Large-Precategory y
pr1-pullback-Large-Precategory = pr1 (pr2 (t x y z f g))

pr2-pullback-Large-Precategory :
hom-Large-Precategory C object-pullback-Large-Precategory z
pr2-pullback-Large-Precategory = pr1 (pr2 (pr2 (t x y z f g)))

pullback-square-Large-Precategory-comm :
comp-hom-Large-Precategory C f pr1-pullback-Large-Precategory ＝
comp-hom-Large-Precategory C g pr2-pullback-Large-Precategory
pullback-square-Large-Precategory-comm = pr1 (pr2 (pr2 (pr2 (t x y z f g))))

module _
(w' : obj-Large-Precategory C l1)
(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₂')
where

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₂' α))
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


morphism-into-pullback-comm-pr1-Large-Precategory :
comp-hom-Large-Precategory C
pr1-pullback-Large-Precategory
morphism-into-pullback-Large-Precategory ＝
p₁'
morphism-into-pullback-comm-pr1-Large-Precategory =
pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)))

morphism-into-pullback-comm-pr2-Large-Precategory :
comp-hom-Large-Precategory C
pr2-pullback-Large-Precategory
morphism-into-pullback-Large-Precategory ＝
p₂'
morphism-into-pullback-comm-pr2-Large-Precategory =
pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)))

is-unique-morphism-into-pullback-Large-Precategory :
(h' : hom-Large-Precategory C w' object-pullback-Large-Precategory) →
comp-hom-Large-Precategory C pr1-pullback-Large-Precategory h' ＝ p₁' →
comp-hom-Large-Precategory C pr2-pullback-Large-Precategory h' ＝ p₂' →
morphism-into-pullback-Large-Precategory ＝ h'
is-unique-morphism-into-pullback-Large-Precategory h' α₁ α₂ =
ap
( pr1)
( pr2 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α) (h' , α₁ , α₂))

module _
{α : Level → Level} {β : Level → Level → Level}
{l1 l2 l3 l4 : Level} (C : Large-Precategory α β)
(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)
Comment on lines +164 to +169
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You probably want x y z and w to be implicit arguments here, unless Agda is unable to infer them generally

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point! I'll change this in the other file too.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, when they are implicit, I would place w right after z instead

(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₂)
where

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)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note that we are changing is-prop-Π³ to a general is-prop-iterated-Π 3 with #797 😁


is-pullback-prop-Large-Precategory :
Prop (α l1 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔ β l1 l4)
pr1 is-pullback-prop-Large-Precategory =
is-pullback-Large-Precategory C x y z f g w p₁ p₂ α₁
pr2 is-pullback-prop-Large-Precategory =
is-prop-is-pullback-Large-Precategory
```
14 changes: 7 additions & 7 deletions src/category-theory/pullbacks-in-precategories.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,16 +76,16 @@ module _
Σ (comp-hom-Precategory C f p₁ ＝ comp-hom-Precategory C g p₂) λ α →
is-pullback-Precategory x y z f g w p₁ p₂ α

has-all-pullback-Precategory : UU (l1 ⊔ l2)
has-all-pullback-Precategory =
has-all-pullbacks-Precategory : UU (l1 ⊔ l2)
has-all-pullbacks-Precategory =
(x y z : obj-Precategory C) →
(f : hom-Precategory C y x) →
(g : hom-Precategory C z x) →
pullback-Precategory x y z f g

module _
{l1 l2 : Level} (C : Precategory l1 l2)
(t : has-all-pullback-Precategory C)
(t : has-all-pullbacks-Precategory C)
(x y z : obj-Precategory C)
(f : hom-Precategory C y x)
(g : hom-Precategory C z x)
Expand Down Expand Up @@ -119,20 +119,20 @@ module _
morphism-into-pullback-Precategory =
pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))

morphism-into-pullback-comm-pr1 :
morphism-into-pullback-comm-pr1-Precategory :
comp-hom-Precategory C
pr1-pullback-Precategory
morphism-into-pullback-Precategory ＝
p₁'
morphism-into-pullback-comm-pr1 =
morphism-into-pullback-comm-pr1-Precategory =
pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)))

morphism-into-pullback-comm-pr2 :
morphism-into-pullback-comm-pr2-Precategory :
comp-hom-Precategory C
pr2-pullback-Precategory
morphism-into-pullback-Precategory ＝
p₂'
morphism-into-pullback-comm-pr2 =
morphism-into-pullback-comm-pr2-Precategory =
pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)))

is-unique-morphism-into-pullback-Precategory :
Expand Down
Loading