## 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.

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))


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: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

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

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