Zulip Chat Archive
Stream: general
Topic: this and that, or structure?
Kevin Buzzard (Apr 20 2018 at 08:02):
I notice that in our schemes work, Kenny and I independently defined the concept of an open immersion between topological spaces.
Kevin Buzzard (Apr 20 2018 at 08:02):
I wrote
Kevin Buzzard (Apr 20 2018 at 08:02):
structure open_immersion {α : Type*} [Tα : topological_space α] {β : Type*} [Tβ : topological_space β] (f : α → β) : Prop := (fcont : continuous f) (finj : function.injective f) (fopens : ∀ U : set α, is_open U ↔ is_open (f '' U))
Kevin Buzzard (Apr 20 2018 at 08:02):
Kenny wrote
Kevin Buzzard (Apr 20 2018 at 08:02):
def topological_space.open_immersion {X Y : Type} [tX : topological_space X] [tY : topological_space Y] (φ : X → Y) := continuous φ ∧ function.injective φ ∧ ∀ U : set X, tX.is_open U → tY.is_open (set.image φ U)
Kevin Buzzard (Apr 20 2018 at 08:04):
I don't think it would be too taxing to check that these two props were equivalent.
Kevin Buzzard (Apr 20 2018 at 08:04):
But I think there's an argument for putting this basic notion into mathlib
Kevin Buzzard (Apr 20 2018 at 08:04):
and before I wrote the PR
Kevin Buzzard (Apr 20 2018 at 08:04):
I realised I was going to have to understand better
Kevin Buzzard (Apr 20 2018 at 08:05):
about the relative advantages / disadvantages between chaining "and" vs making a structure
Kenny Lau (Apr 20 2018 at 08:07):
Kevin Buzzard (Apr 20 2018 at 08:07):
They're both props, the structure version has the feature that it demands that you spell out which term is doing which of the three jobs that need doing, which may or may not be a good thing, and the "and" approach lets you write more compact code, constructing instances with pointy brackets, which may or may not be a good thing
Kenny Lau (Apr 20 2018 at 08:07):
you wrote both definitions
Mario Carneiro (Apr 20 2018 at 08:08):
You can use pointy brackets with either definition
Kevin Buzzard (Apr 20 2018 at 08:08):
You're right Kenny, thanks.
Mario Carneiro (Apr 20 2018 at 08:09):
All structure instances, in fact, can be written with pointy brackets instead of structure notation
Mario Carneiro (Apr 20 2018 at 08:09):
it's just that this is harder to read when there are many properties since order matters
Kevin Buzzard (Apr 20 2018 at 08:10):
Were you to be getting a mathlib PR with a definition of an open immersion
Kevin Buzzard (Apr 20 2018 at 08:10):
which would you prefer?
Mario Carneiro (Apr 20 2018 at 08:10):
the structure, I think
Kevin Buzzard (Apr 20 2018 at 08:10):
OK thanks
Kevin Buzzard (Apr 20 2018 at 08:11):
Sorry Kenny, I could see that you had done the hard work in that tag (supplying the proof of the result below) so just assumed you'd written the definition.
Patrick Massot (Apr 20 2018 at 08:13):
you wrote both definitions
Ooohh, I never realized Kenny is only one schizophrenic identity of Kevin. That explains soo much...
Kevin Buzzard (Apr 20 2018 at 08:14):
Our secret is out Kenny! Or should I say, Mr Hyde...
Kevin Buzzard (Apr 20 2018 at 08:14):
In fact the far more mundane truth is that I write code, forget, and then write code again.
Kenny Lau (Apr 20 2018 at 08:14):
right, I'm the constructivist version of Kevin
Kevin Buzzard (Apr 20 2018 at 08:14):
ha ha
Patrick Massot (Apr 20 2018 at 08:18):
Yeah, the story of a first year working in scheme theory was sort of believable, but the constructivism stuff I should have realize this was completely impossible
Gabriel Ebner (Apr 20 2018 at 08:21):
You can use pointy brackets with either definition
OTOH, curly braces work much more nicely with the structure. That is, you can write {fcont := _, finj := _, fopens := _}. While with ∧, you'd need {left := _, right := {left := _, right := _}}.
Kevin Buzzard (Apr 20 2018 at 08:39):
so \and is redundant in Lean ;-)
Last updated: Dec 20 2023 at 11:08 UTC