Question about Filter.Germ

Stream: mathlib4

[finegeometer]

If l : Filter α, Mathlib defines l.Germ as a quotient of α → β. An alternative would be to define it as a quotient of {f : PFun α β // f.Dom ∈ l}. These are equivalent unless IsEmpty (α → β) ∧ l = ⊥, in which case the existing definition says l.Germ is empty, while the alternative says it's a singleton.

Which version is standard? Which version is better? And if the answers to these questions disagree, which should Mathlib use?

[Yury G. Kudryashov]

I never needed germs along the bottom filter (and AFAIK lots of texts don't consider it to be a filter).

[Patrick Massot]

I think changing this would be a bad move. We want to keep the coercion from functions to Filter.Germ. You should probably un-#xy and tell us why you think you need PFun. The mostly likely situation is that you should stick to functions.

[David Wärn]

You would still have a coercion from functions to Filter.Germ even with the change. I don't think there can be any question that the 'alternative' definition is in fact the correct one. For example, the type of germs should be the colimit of $U \to \beta$ over $U$ in the filter. Also, the type of germs for the principal filter under $U \subseteq \alpha$ should be the type of functions $U \to \beta$ (even if $U$ is empty). Perhaps the situation is clearer if you think algebro-geometrically, where you can have lots of locally defined functions that don't extend to global functions but still define germs. I think this was discussed already many years ago, but I won't try to argue that this is an important issue or something that needs changing :-)

[Kyle Miller]

I was thinking along the same lines, but it's nice being able to take advantage of the existence of global functions (and to avoid some dependent types!)

If Filter.Germ could let you restrict the class of functions then the correct definition would definitely be correct :-)

[finegeometer]

Patrick Massot said:

You should probably un-#xy and tell us why you think you need PFun.

This wasn't, in fact, an XY problem. I don't need this for anything. I was just looking at the definition, and something seemed a bit off, so I thought I'd ask.

David Wärn said:

For example, the type of germs should be the colimit of $U \to \beta$ over $U$ in the filter. Also, the type of germs for the principal filter under $U \subseteq \alpha$ should be the type of functions $U \to \beta$ (even if $U$ is empty).

And this seems to formalize my intuition that something was slightly wrong. Thanks!

[Yury G. Kudryashov]

Generally, we try to be practical with definitions. E.g., \bot is allowed as a Filter _, because this way we have CompleteLattice (Filter _), even though many authors only work with NeBot filters. Similarly, we use globally defined functions, because this way we can avoid dependent types and proofs x ∈ f.Dom all over the place. If someone will need to deal with germs at the \bot filter and it will be important to make this type nonempty even if the codomain is empty, then we can refactor (with the one who needs it leading the effort).

[finegeometer]

That makes sense. It bugs me to have a slightly wrong definition, but you're right that it might not be worth the effort to fix.

[Yury G. Kudryashov]

If we change the definition as you suggest, then docs#Germ.ofFun will no longer be surjective, unless we assume [NeBot l] or Nonempty β. Then we'll have to either deal with these special cases in proofs, or add these assumptions in all lemmas.

[Yury G. Kudryashov]

I would prefer to avoid it unless we need to.