Comments (3)
Thanks! This reminded me that I'm violating the convention that isA
is usually only used when A
is a \Prop
. I'll reconsider the choice of terminology.
from hstacks.
In HoTT book it's called split essentially surjective (Definition 9.4.4), and what I proved is Lemma 9.4.5. The truncated/category version you mentioned is Lemma 9.4.7.
Problem is, I'm not sure which one is actually being used in the rest of Stacks project - or how "constructive" Algebraic Geometry is - I guess we will be mostly dealing with split essential surjectivity; I might add Lemma 9.4.7 in the future if needs be, or if someone else proves it ;)
Moreover, the definition of "surjection" in Foundation/Set.ard
also has this problem (and has an hPOV comment). Again this is not yet decided and depends on how constructive AG actually is (or can be).
About the choice of the terminology: for now I'm leaning towards reserving simpler names for the constructive/untruncated version and call the truncated version "merely surjective." This differs from HoTTbook usage but this project is still in its experimental stage, and there's intellij's refactor tool.
from hstacks.
Good points! My perspective is:
-
Algebraic geometry is very classical and you should probably assume the axiom of choice.
-
I think it would still be best not to refer to this untruncated one as "essentially surjective", but you can then prove that every surjection is split (equivalent to the axiom of choice), and hence get the result you wanted about equivalences. Aside from keeping with ordinary terminology, my reason is also that one generally thinks of surjectivity as a property, whereas the space of splittings of a surjection is not generally contractible.
Anyway, good luck with your project! It is very ambitious.
from hstacks.
Related Issues (1)
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from hstacks.