-
Notifications
You must be signed in to change notification settings - Fork 299
[Merged by Bors] - feature(algebraic_geometry/Scheme): the category of schemes #3961
Conversation
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
…ib into limits_tweaks
|
||
@[ext] lemma ext {X Y : PresheafedSpace C} (α β : hom X Y) | ||
(w : α.base = β.base) (h : α.c ≫ (whisker_right (nat_trans.op (opens.map_iso _ _ w).inv) X.𝒪) = β.c) : | ||
(w : α.base = β.base) | ||
(h : α.c ≫ (whisker_right (nat_trans.op (opens.map_iso _ _ w).inv) X.presheaf) = β.c) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this the solution to the problem of equality of types?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm sorry, could you clarify your question, I'm not sure how it relates to this piece of the code.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Well, equality of types proved to be troublesome, but somehow you managed to use it without issues. (α.base = β.base
is an equality of types right)
/-- The structure sheaf of a locally ringed space. -/ | ||
def 𝒪 : sheaf CommRing X.to_Top := ⟨X.1.presheaf, X.1.sheaf_condition⟩ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why not coerce X
to a sheafed space?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I can't do exactly that, but I've replaced the RHS with X.to_SheafedSpace.sheaf
. Is that okay?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sure, but why do we not prefer coercion?
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
bors merge |
The definition of a `Scheme`, and the category of schemes as the full subcategory of locally ringed spaces. Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Ashvni <ashvni.n@gmail.com>
Pull request successfully merged into master. Build succeeded: |
The definition of a `Scheme`, and the category of schemes as the full subcategory of locally ringed spaces. Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Ashvni <ashvni.n@gmail.com>
The definition of a `Scheme`, and the category of schemes as the full subcategory of locally ringed spaces. Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Ashvni <ashvni.n@gmail.com>
The definition of a
Scheme
, and the category of schemes as the full subcategory of locally ringed spaces.Co-authored-by: Johan Commelin johan@commelin.net
Blocked
#3609,#3906,#3907