feat(topology/sheaves/Godement): define the first term of Godement resolution #16878
Conversation
jjaassoonn
commented
Oct 9, 2022
jjaassoonn
commented
jjaassoonn
added
awaiting-review
github-actions
bot
removed
the
awaiting-CI
src/topology/sheaves/Godement.lean
Outdated
| Under the isomorphism `godement_presheaf(𝓕, U) ≅ ∏ₓ skyscraper(x, 𝓕ₓ)(U)`, there is a morphism | ||
| `𝓕 ⟶ ∏ₓ skyscraper(x, 𝓕ₓ) ≅ godement_presheaf(𝓕)` | ||
| -/ | ||
| @[simps] def to_godement_presheaf : 𝓕 ⟶ godement_presheaf 𝓕 := |
There was a problem hiding this comment.
Would it be easier to work with the definition
def to_godement_presheaf : 𝓕 ⟶ godement_presheaf 𝓕 :=
pi.lift $ λ p₀, (stalk_skyscraper_presheaf_adjunction_auxs.unit p₀).app 𝓕
? I guess it depends on what you want to do with it?
There was a problem hiding this comment.
This definition is certainly more concise. All I need from this definition is this lemma, which should also hold for your definition modulo some modification. So I will use your definition instead.
There was a problem hiding this comment.
I mentioned this to you a while ago but maybe you didn't notice :)
jjaassoonn
added
awaiting-author
src/topology/sheaves/Godement.lean
Outdated
| universes u v | ||
|
|
||
| variables {X : Top.{u}} {C : Type u} [category.{u} C] | ||
| variables [has_limits C] [has_terminal C] [has_colimits C] |
There was a problem hiding this comment.
| variables [has_limits C] [has_terminal C] [has_colimits C] | |
| variables [has_limits C] [has_colimits C] |
has_limits implieshas_terminal.
There was a problem hiding this comment.
Actually, has_products suffice for this file, right? But we lack an instance from has_products to has_terminal. Maybe has_products_of_shape X + has_terminal?
We have category_theory.limits.functor_category_has_limits_of_shape but since presheaf is not a reducible def we need to manually add one more instance to topology/sheaves/limits for Lean to infer that the presheaf category also has limits of shape X.
There was a problem hiding this comment.
we still need has_colimits C for stalks
There was a problem hiding this comment.
You should only need has_filtered_colimits for that, right?
There was a problem hiding this comment.
stalk_functor assumes has_colimits, so has_colimits cannot be relaxed
There was a problem hiding this comment.
Actually,
has_productssuffice for this file, right? But we lack an instance fromhas_productstohas_terminal. Maybehas_products_of_shape X+has_terminal?We have category_theory.limits.functor_category_has_limits_of_shape but since
presheafis not a reducible def we need to manually add one more instance to topology/sheaves/limits for Lean to infer that the presheaf category also has limits of shapeX.
limit_is_sheaf requires has_limits C
jjaassoonn
added
awaiting-review
