feat(topology/sheaves/*): sheaves have enough injectives under some condition by jjaassoonn · Pull Request #15742 · leanprover-community/mathlib3

jjaassoonn · 2022-07-28T16:04:50Z

define skyscraper sheaves
skyscraper sheaves are isomorphic to pullback of a sheaf on the single point space (not actually needed for enough invectiveness, just for completeness)
calculate their stalks
skyscraper sheaves are injective if targets are injective
godement resolution
show enough injective

depends on:[Merged by Bors] - feat(category_theory/sites/{sheaf, sheafification}): monomorphisms of sheaves are precisely monomorphisms of presheaves #15932
depends on:[Merged by Bors] - feat(algebra/category/Group/epi_mono): (mono)epimorphisms and (in)surjections are the same in (Add)(Comm)Group #15496
depends on:[Merged by Bors] - feat(topology/sheaves/skyscraper): define skyscraper presheaves and calculate stalks #15934
depends on:[Merged by Bors] - feat(category_theory/preadditive/injective): Adjoint functors preserves injective objects #15935
depends on:[Merged by Bors] - feat(category_theory/limits/shapes/products): if each f b ⟶ g b is mono, then ∏ f ⟶ ∏ g is mono #16180

…i_mono

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

…over-community/mathlib into jjaassoonn/group_epi_mono

…jjaassoonn/equiv_Group_AddGroup

alreadydone

Just some preliminary comments; will take a closer look when the diff become smaller after #15934.

alreadydone · 2022-08-22T16:54:26Z

src/category_theory/preadditive/injective.lean


 import algebra.homology.exact
 import category_theory.types
+import category_theory.functor.epi_mono


Why add this import without adding any content to this file?

alreadydone · 2022-08-22T16:58:33Z

src/topology/sheaves/godement.lean

+
+universes u v
+
+variables {X : Top.{u}} {C : Type u} [category.{u} C]


Could this be relaxed to C : Type v?

alreadydone · 2022-08-22T17:03:21Z

src/topology/sheaves/stalks.lean

+begin
+  have := functor.map_mono (sheaf.forget C X ⋙ stalk_functor C x) f,
+  exact this,
+end


by exact should work?

alreadydone · 2022-08-22T17:03:58Z

src/topology/sheaves/stalks.lean

+
+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 }⟩


Suggested change

⟨λ m, by { resetI, apply_instance }, λ m, by { resetI, apply_instance }⟩

by split; { introI, apply_instance }

(untested)

alreadydone · 2022-08-22T18:59:12Z

src/topology/sheaves/godement.lean

+variables (𝓕 : presheaf C X) (𝓖 : sheaf C X)
+
+def godement_presheaf : presheaf C X :=
+∏ (λ x, skyscraper_presheaf x (𝓕.stalk x) : X → presheaf C X)


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.

alreadydone · 2022-08-22T19:21:24Z

src/topology/sheaves/godement.lean

+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 :=


This should probably be done for any Grothendieck topology and moved to category_theory.sites.sheaf .

alreadydone · 2022-08-22T19:22:44Z

src/topology/sheaves/godement.lean

+  rwa to_godement_presheaf_aux_comp_π_eq at eq1'',
+end
+
+example : true := trivial


alreadydone · 2022-08-22T19:35:19Z

src/topology/sheaves/skyscraper.lean

+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⟩


What's the reason for not simply using punit as the space?

alreadydone · 2022-08-22T19:36:49Z

src/topology/sheaves/skyscraper.lean

+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)


I also wondered whether we should allow the terminal object be specified ...

alreadydone · 2024-06-05T20:10:10Z

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.

jjaassoonn and others added 30 commits June 13, 2022 11:35

initial

5eb1c0b

finished epi

df25067

add to_additive

99553bd

add doc_string

793b87b

generalize

d80df7f

add to_addtive

9a7d5c9

remove noncomputable

5170d98

minor golf

370c5f3

minimize import

29808f5

golf

4640408

golf

697ddd9

golf

c605b39

golf

e1d1cf8

golf a little bit more

bf97e8b

Merge remote-tracking branch 'origin/master' into jjaassoonn/group_ep…

1f73f52

…i_mono

apply suggestion and fix

4b3cc16

Update src/algebra/category/Group/epi_mono.lean

f21bd67

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

Update src/algebra/category/Group/epi_mono.lean

7b39fcd

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

Update src/algebra/category/Group/epi_mono.lean

c039b7d

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

Update src/algebra/category/Group/epi_mono.lean

ef6a749

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

Update src/algebra/category/Group/epi_mono.lean

677d542

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

Update src/algebra/category/Group/epi_mono.lean

02c7601

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

Update src/algebra/category/Group/epi_mono.lean

99d2945

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

Update src/algebra/category/Group/epi_mono.lean

5fd7529

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

add noncomputable

0d8ea15

Merge branch 'jjaassoonn/group_epi_mono' of https://github.com/leanpr…

e6d4741

…over-community/mathlib into jjaassoonn/group_epi_mono

reformat

c199b07

initial

f82ff81

Merge remote-tracking branch 'origin/jjaassoonn/group_epi_mono' into …

5cdf35f

…jjaassoonn/equiv_Group_AddGroup

add missing

dab193b

jjaassoonn added 15 commits August 16, 2022 03:49

Merge remote-tracking branch 'origin/master' into jjaassoonn/sky

8b13323

fix

cf4bbe8

generalize

081ff84

minimize import

1cf1bbb

fix

67ad634

need cache

5429253

fix and add lemma about mono in sheaves

0dbcde2

fixx

729c649

commit

ffe5571

defined some auxilary isomorphism

6cfe30f

save for now

036fc2f

commit

55d4046

save

84c015d

more api

e941031

finish godement resolution

9857552

jjaassoonn changed the title ~~feat(topology/sheves/skyscraper): skyscraper sheaves are injective if the targets are injective~~ feat(topology/sheves/skyscraper): sheaves have enough injectives under some condition Aug 21, 2022

jjaassoonn changed the title ~~feat(topology/sheves/skyscraper): sheaves have enough injectives under some condition~~ feat(topology/sheves/*): sheaves have enough injectives under some condition Aug 21, 2022

cache

ef039e9

alreadydone changed the title ~~feat(topology/sheves/*): sheaves have enough injectives under some condition~~ feat(topology/sheaves/*): sheaves have enough injectives under some condition Aug 21, 2022

finish

06689d1

jjaassoonn removed WIP Work in progress awaiting-CI The author would like to see what CI has to say before doing more work. labels Aug 21, 2022

jjaassoonn added 2 commits August 21, 2022 07:59

add some more lemma

0295753

add some docs

28dc545

alreadydone reviewed Aug 23, 2022

View reviewed changes

jjaassoonn added the WIP Work in progress label Oct 9, 2022

alreadydone mentioned this pull request Oct 9, 2022

feat(topology/sheaves/Godement): define the first term of Godement resolution #16878

Draft

jjaassoonn marked this pull request as draft May 4, 2023 11:11

kim-em added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Comments

feat(topology/sheaves/*): sheaves have enough injectives under some condition#15742

feat(topology/sheaves/*): sheaves have enough injectives under some condition#15742
jjaassoonn wants to merge 95 commits intomasterfrom
jjaassoonn/sky

jjaassoonn commented Jul 28, 2022 •

edited by github-actions bot

Loading

Uh oh!

alreadydone left a comment

Uh oh!

alreadydone Aug 22, 2022

Uh oh!

alreadydone Aug 22, 2022

Uh oh!

alreadydone Aug 22, 2022

Uh oh!

alreadydone Aug 22, 2022

Uh oh!

alreadydone Aug 22, 2022

Uh oh!

alreadydone Aug 22, 2022

Uh oh!

alreadydone Aug 22, 2022

Uh oh!

alreadydone Aug 22, 2022

Uh oh!

alreadydone Aug 22, 2022

Uh oh!

alreadydone commented Jun 5, 2024 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants


		universes u v

		variables {X : Top.{u}} {C : Type u} [category.{u} C]

	⟨λ m, by { resetI, apply_instance }, λ m, by { resetI, apply_instance }⟩
	by split; { introI, apply_instance }

Comments

Conversation

jjaassoonn commented Jul 28, 2022 • edited by github-actions bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

alreadydone left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

alreadydone commented Jun 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

jjaassoonn commented Jul 28, 2022 •

edited by github-actions bot

Loading

alreadydone commented Jun 5, 2024 •

edited

Loading