Revision #1562 → #1847 · back to history
modifiedSheaf of sections of a continuous map2464fa146d0e
| Field | From #1562 | To #1847 |
|---|
| mathlib.decl | TopCat.LocalPredicate.isSection | TopCat.isSection |
| note | The local predicate `isSection p` produces the sheaf of sections of `p : T → X` via `subsheafToTypes`, but the construction is only set up for trivial fiber families and not the general `Y → X` étalé construction. | The local predicate `TopCat.isSection p` produces the sheaf of sections of `p : T → X` via `subsheafToTypes`, but the construction is only set up for trivial fiber families and not the general `Y → X` étalé construction. |
modifiedStructure sheaf and differential forms on manifoldsc76bc076e1c9
| Field | From #1562 | To #1847 |
|---|
| mathlib.module | Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace | Mathlib.Geometry.Manifold.Sheaf.Smooth |
modifiedIso/mono check via stalks21cb3976901b
| Field | From #1562 | To #1847 |
|---|
| anchor.section | Morphisms | Stalks of a sheaf |
| anchor.snippet | of sheaves on | can be tested on the stalks |
| label | Iso/monomorphism check on open sets | Iso/mono check via stalks |
| note | `isIso_iff_stalkFunctor_map_iso` and `mono_iff_stalk_mono` reduce iso/mono-ness of a sheaf morphism to stalkwise checks. | `isIso_iff_stalkFunctor_map_iso` and `mono_iff_stalk_mono` reduce iso/mono-ness of a sheaf morphism to stalkwise checks; re-anchored from the Morphisms section since the cited decls live in the stalks API. |
| provenance | ai | ai-moderated |
addedConstant sheafb66a89989f92
addedSchemes as locally ringed spaces48f39145f280
addedSheaf cohomology as derived functor of global sections9c3dd1521d58
addedPullback-pushforward adjunction9568cc09c94b