Who started using filters like we do

Stream: general

[Anatole Dedecker]

Just out of curiosity, does anyone know who started doing filters the way we do (e.g include the $\bot$ filter and do most things algebraically using pushforward, pullbacks and the complete lattices operations) ?

[Eric Rodriguez]

I think the answer is likely bourbaki

[Anatole Dedecker]

No, Bourbaki says that our $\bot$ is not a filter

[Anatole Dedecker]

See the docstring of https://leanprover-community.github.io/mathlib_docs/order/filter/basic.html

[Kevin Buzzard]

I asked this question in about 2018 and Johannes Hoelzl pointed me to some short paper from the 1960s or so which observed that if filters were defined our way then you could push them forward and pull them back; I will have a try at digging up the reference but I'm busy right now...

[Anatole Dedecker]

Thanks Kevin ! No hurry of course

[Mauricio Collares]

I think page number 10 (17th page in the PDF) of https://kilthub.cmu.edu/articles/A_survey_of_top_categories/6476729/files/11908172.pdf says this, but I am not sure.

[Johan Commelin]

See https://mathoverflow.net/questions/325218/reference-request-filter-tends-to-filter-along-map (question by Kevin, probably the one he wanted to dig up)

[Anatole Dedecker]

Thanks !

[Kevin Buzzard]

Thanks Johan -- I was looking through old emails and messages and I'd misremembered that it was Johannes (although perhaps he told me the same thing but couldn't remember the reference for the paper?) -- but I didn't try MO. This was definitely what I was inaccurately referring to above.