Elementary topos nonsense #411
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
New pages
Changed pages
|
|
oh, she's alive! |
|
What needs to be done to take this out of draft status? Working on injective objects right now, and I'd like to show that every subobject classifier is injective 🙂 |
|
I guess what's here is mostly done, there's just not a lot of it |
plt-amy
force-pushed
the
aliao/elementary-topoi
branch
3 times, most recently
from
9fdee2c to
106ce8c
Compare
plt-amy
force-pushed
the
aliao/elementary-topoi
branch
from
23a1e6c to
1c9be5c
Compare
plt-amy
force-pushed
the
aliao/elementary-topoi
branch
from
297f881 to
376903d
Compare
TOTBWF
requested changes
Mar 7, 2025
| $\name{A} : A \to \Omega$ into the presheaf of sieves on $\cC$ is valued | ||
| in closed sieves. | ||
|
|
||
| First, suppose that the domain of $A' \mono A$ is indeed a sheaf. First, |
There was a problem hiding this comment.
why after you're done assuming the other thing is the new first thing to do!
| We can then compute, in $\psh(\cC)$, the name of $A'$, resulting in a | ||
| natural transformation $\name{A'} : A \to \Omega$. It remains to show | ||
| that this transformation is actually valued in $\Omega_J$, i.e. that | ||
| each of the resulting sieves is closed. To this end, susppose we have |
There was a problem hiding this comment.
Suggested change
| each of the resulting sieves is closed. To this end, susppose we have | |
| each of the resulting sieves is closed. To this end, suppose we have |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
watch this space but not too closely