feat(topology/sheaves/*): sheaves have enough injectives under some condition #15742
Conversation
Co-authored-by: Markus Himmel <[email protected]>
Co-authored-by: Markus Himmel <[email protected]>
Co-authored-by: Markus Himmel <[email protected]>
Co-authored-by: Markus Himmel <[email protected]>
Co-authored-by: Markus Himmel <[email protected]>
Co-authored-by: Markus Himmel <[email protected]>
Co-authored-by: Markus Himmel <[email protected]>
Co-authored-by: Markus Himmel <[email protected]>
…over-community/mathlib into jjaassoonn/group_epi_mono
…jjaassoonn/equiv_Group_AddGroup
jjaassoonn
changed the title
jjaassoonn
changed the title
alreadydone
changed the title
jjaassoonn
removed
WIP
There was a problem hiding this comment.
Just some preliminary comments; will take a closer look when the diff become smaller after #15934.
| @@ -6,6 +6,7 @@ Authors: Jujian Zhang, Kevin Buzzard | |||
|
|
|||
| import algebra.homology.exact | |||
| import category_theory.types | |||
| import category_theory.functor.epi_mono | |||
There was a problem hiding this comment.
Why add this import without adding any content to this file?
|
|
||
| universes u v | ||
|
|
||
| variables {X : Top.{u}} {C : Type u} [category.{u} C] |
There was a problem hiding this comment.
Could this be relaxed to C : Type v?
| begin | ||
| have := functor.map_mono (sheaf.forget C X ⋙ stalk_functor C x) f, | ||
| exact this, | ||
| end |
There was a problem hiding this comment.
by exact should work?
|
|
||
| lemma mono_iff_stalk_mono {F G : sheaf C X} (f : F ⟶ G) : | ||
| mono f ↔ ∀ x, mono ((stalk_functor C x).map f.1) := | ||
| ⟨λ m, by { resetI, apply_instance }, λ m, by { resetI, apply_instance }⟩ |
There was a problem hiding this comment.
| ⟨λ m, by { resetI, apply_instance }, λ m, by { resetI, apply_instance }⟩ | |
| by split; { introI, apply_instance } |
(untested)
| variables (𝓕 : presheaf C X) (𝓖 : sheaf C X) | ||
|
|
||
| def godement_presheaf : presheaf C X := | ||
| ∏ (λ x, skyscraper_presheaf x (𝓕.stalk x) : X → presheaf C X) |
There was a problem hiding this comment.
Is the type ascription necessary? (Same question for injective_sheaf.)
Isn't 𝓕 ⟶ skyscraper_presheaf x (𝓕.stalk x) just the unit of the skyscraper-stalk adjunction, from which you directly get def to_godement_presheaf : 𝓕 ⟶ godement_presheaf 𝓕? It seems you didn't use the adjunction to its full force here.
By the way, your construction of the adjunction feels overly long; in my experience it's usually fastest to directly construct the unit and counit, without the need to go through hom_equiv, but I need to take a closer look before I can say for sure.
| variables [concrete_category.{u} C] [preserves_limits (forget C)] | ||
| variables [reflects_isomorphisms (forget C)] [preserves_filtered_colimits (forget C)] | ||
|
|
||
| @[simps] def sheaf_in_Type : sheaf C X ⥤ sheaf (Type u) X := |
There was a problem hiding this comment.
This should probably be done for any Grothendieck topology and moved to category_theory.sites.sheaf .
| rwa to_godement_presheaf_aux_comp_π_eq at eq1'', | ||
| end | ||
|
|
||
| example : true := trivial |
| variables {X : Top.{u}} (p₀ : X) {C : Type v} [category.{w} C] (S : C) [has_terminal C] | ||
|
|
||
| /--The topological space with on a point `{p₀}`. Hence the only open sets are ∅ and ⊤.-/ | ||
| def single_point_space : Top := ⟨({p₀} : set X), infer_instance⟩ |
There was a problem hiding this comment.
What's the reason for not simply using punit as the space?
| universes u v | ||
|
|
||
| variables {X : Top.{u}} (p₀ : X) {C : Type v} [category.{u} C] | ||
| variables [has_terminal C] -- {star : C} (ts : is_terminal star) |
There was a problem hiding this comment.
I also wondered whether we should allow the terminal object be specified ...
|
Are there plans to merge master and port this PR to Lean 4? It's listed as the first item in @joelriou 's AIM workshop statement. |
(Add)(Comm)Group#15496f b ⟶ g bis mono, then∏ f ⟶ ∏ gis mono #16180