No zero divisors in presheaf stalks

If sections on a basis of open neighborhoods of a point have no zero divisors, the stalk has no zero divisors. This applies to semiring-valued concrete categories whose forgetful functor preserves filtered colimits; neither commutativity nor the sheaf condition is needed. The proof uses Mathlib's TopCat.Presheaf.exists_le_germ_eq to represent two germs on a common neighborhood and TopCat.Presheaf.germ_eq to witness their product vanishing locally.

theorem TopCat.Presheaf.stalk_noZeroDivisors_of_hasBasis {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {FC : C → C → Type u_1} {CC : C → Type v} [(R S : C) → FunLike (FC R S) (CC R) (CC S)] [CategoryTheory.ConcreteCategory C FC] [(R : C) → Semiring (CC R)] [∀ (R S : C), RingHomClass (FC R S) (CC R) (CC S)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {X : TopCat} (F : Presheaf C X) (x : ↑X) {ι : Type u_2} {p : ι → Prop} {U : ι → TopologicalSpace.Opens ↑X} (hB : (nhds x).HasBasis p fun (i : ι) => ↑(U i)) (hF : ∀ (i : ι), p i → NoZeroDivisors (CategoryTheory.ToType (F.obj (Opposite.op (U i))))) : NoZeroDivisors (CategoryTheory.ToType (F.stalk x))

A presheaf stalk has no zero divisors if sections on a neighborhood basis do.