TopCat.Presheaf.ext

theorem TopCat.Presheaf.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} {P Q : TopCat.Presheaf C X} {f g : P ⟶ Q}, (∀ (U : TopologicalSpace.Opens ↑X), f.app (Opposite.op U) = g.app (Opposite.op U)) → f = g

The theorem `TopCat.Presheaf.ext` states that for any category `C`, any topological space `X`, and any two `C`-valued presheaves `P` and `Q` on `X`, if two natural transformations `f` and `g` from `P` to `Q` have the property that for every open set `U` in `X`, the application of `f` to the opposite of `U` equals the application of `g` to the opposite of `U`, then `f` and `g` are the same natural transformation. In other words, two natural transformations between presheaves are equal if and only if their corresponding applications are equal for each open set.

More concisely: For any category `C`, topological space `X`, and `C`-valued presheaves `P` and `Q` on `X`, if two natural transformations `f` and `g` from `P` to `Q` satisfy `f(U) = g(U)` for all open sets `U` in `X`, then `f` is equal to `g`.