Zulip Chat Archive

Stream: general

Topic: this and that, or structure?


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:02):

I wrote

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:02):

structure open_immersion
  {α : Type*} [ : topological_space α]
  {β : Type*} [ : topological_space β]
  (f : α  β) : Prop :=
(fcont : continuous f)
(finj : function.injective f)
(fopens :  U : set α, is_open U  is_open (f '' U))

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:02):

Kenny wrote

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:04):

But I think there's an argument for putting this basic notion into mathlib

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:04):

and before I wrote the PR

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:04):

I realised I was going to have to understand better

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:05):

about the relative advantages / disadvantages between chaining "and" vs making a structure

view this post on Zulip Kenny Lau (Apr 20 2018 at 08:07):

https://github.com/kbuzzard/lean-stacks-project/commit/a3e4acc5b443f02c1decf3db32260ff28e4dd855#diff-ad019596efa140984bbb88e365b57df7

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 20 2018 at 08:07):

you wrote both definitions

view this post on Zulip Mario Carneiro (Apr 20 2018 at 08:08):

You can use pointy brackets with either definition

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:08):

You're right Kenny, thanks.

view this post on Zulip Mario Carneiro (Apr 20 2018 at 08:09):

All structure instances, in fact, can be written with pointy brackets instead of structure notation

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:10):

Were you to be getting a mathlib PR with a definition of an open immersion

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:10):

which would you prefer?

view this post on Zulip Mario Carneiro (Apr 20 2018 at 08:10):

the structure, I think

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:10):

OK thanks

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:14):

Our secret is out Kenny! Or should I say, Mr Hyde...

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 20 2018 at 08:14):

right, I'm the constructivist version of Kevin

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:14):

ha ha

view this post on Zulip 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

view this post on Zulip 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 := _}}.

view this post on Zulip Kevin Buzzard (Apr 20 2018 at 08:39):

so \and is redundant in Lean ;-)


Last updated: May 11 2021 at 13:22 UTC