# Zulip Chat Archive

## Stream: maths

### Topic: extend presheaf from basis

#### Johan Commelin (Oct 10 2018 at 09:39):

@Scott Morrison Somehow this is not doing what I hoped:

import category_theory.presheaves import category_theory.sheaves import category_theory.limits open category_theory open category_theory.examples open category_theory.limits universes u v w variables {X : Top.{u}} variables {V : Type v} [𝒱 : category.{v w} V] [has_limits.{v w} V] include 𝒱 def extend {B : set (set X)} (h : topological_space.is_topological_basis B) (F : presheaf B V) : presheaf (open_set X) V := { obj := λ U, limit ((full_subcategory_embedding (λ U' : B, U'.1 ⊆ U)) ⋙ F), map' := sorry }

#### Johan Commelin (Oct 10 2018 at 09:40):

The embedding is complaining about universes. I don't get why.

#### Scott Morrison (Oct 10 2018 at 09:43):

@Johan Commelin, I'm just guessing here, but there are universe constraints in taking limits.

#### Kevin Buzzard (Oct 10 2018 at 09:44):

I don't know anything about your errors but even seeing that you're daring to write this sort of code -- "extending a presheaf from a basis might be possible" -- makes me quite excited for the future.

#### Scott Morrison (Oct 10 2018 at 09:44):

In particular, the index category is meant to be a category.{v v}, and the target category is meant to be a category.{u v}.

#### Scott Morrison (Oct 10 2018 at 09:44):

If you don't satisfy those constraints to begin with, you're going to have to ulift.

#### Scott Morrison (Oct 10 2018 at 09:45):

Me too, by the way --- I'm very excited to see things like this work!

#### Johan Commelin (Oct 10 2018 at 09:45):

But it is looking for some `Type w`

. I really don't know where it is getting that from?

#### Johan Commelin (Oct 10 2018 at 09:45):

Do you have comma categories somewhere?

#### Kevin Buzzard (Oct 10 2018 at 09:45):

One thing which might be obvious to everyone already is that of course when you extend, you don't literally "extend", you define a new object on all open sets, and its values on basic open sets are isomorphic to, but not defeq to, the values taken by the old object.

#### Johan Commelin (Oct 10 2018 at 09:45):

I just want the category of opens contained in `U`

.

#### Johan Commelin (Oct 10 2018 at 09:45):

Maybe you already have this somewhere...

#### Johan Commelin (Oct 10 2018 at 09:46):

@Kevin Buzzard Do you want me to include the scare-quotes in the definition :lol: ?

#### Kevin Buzzard (Oct 10 2018 at 09:47):

I am just being reminded of the nightmares I had when doing sheaves by hand in the schemes project.

#### Scott Morrison (Oct 10 2018 at 10:06):

Sorry, I will try to look at this soon. I'm working on installation instructions, still. :-)

#### Scott Morrison (Oct 10 2018 at 10:11):

@Johan Commelin , is that code available somewhere? I'd like to look at the universe issue.

#### Scott Morrison (Oct 10 2018 at 10:13):

(universes scare the bejeebus out of me, and I'm perpetually terrified that someone is going to discover I've still got them wrong in the category theory library)

#### Reid Barton (Oct 10 2018 at 10:13):

You have made V a category.{v w} which means you can only form limits of size w

#### Scott Morrison (Oct 10 2018 at 10:14):

(phew, that's Reid agreeing with me... my heart rate is dropping again. :-)

#### Johan Commelin (Oct 10 2018 at 10:41):

Hmmm, let me take another look.

@Scott Morrison All the code I have is what I posted above.

#### Johan Commelin (Oct 10 2018 at 10:48):

@Reid Barton I still don't get what is wrong with my code.

#### Johan Commelin (Oct 10 2018 at 10:50):

@Scott Morrison Here is a snippet that is probably useful for `over.lean`

:

section over variables {C : Type u} [𝒞 : category.{u v} C] include 𝒞 def over.forget (Z : C) : over Z ⥤ C := { obj := λ X, X.1, map' := λ X Y f, f.1 } end over

#### Scott Morrison (Oct 10 2018 at 10:53):

Thanks, I added `over.forget`

.

#### Johan Commelin (Oct 10 2018 at 11:03):

@Scott Morrison Ok, so I should take `X : Top.{w}`

. It is important that I don't take `Top.{u}`

. Can you explain why?

#### Scott Morrison (Oct 10 2018 at 11:04):

Reid Barton: You have made V a category.{v w} which means you can only form limits of size w

#### Johan Commelin (Oct 10 2018 at 11:06):

Ok... I don't think I care too much. It is a bit tricky to get right. I wouldn't mind if Lean just scaled everything into the right universe. But I guess that brings some tradeoff in foundations that I don't understand.

#### Johan Commelin (Oct 10 2018 at 11:30):

@Scott Morrison May we *please* have presheaves be contravariant. My head is breaking without the `op`

s.

#### Scott Morrison (Oct 10 2018 at 11:30):

no problem

#### Scott Morrison (Oct 10 2018 at 11:31):

We need to make a PR to mathlib to fix this, right?

#### Johan Commelin (Oct 10 2018 at 11:31):

No, presheaves aren't in mathlib

#### Johan Commelin (Oct 10 2018 at 11:31):

Or did you break the definition of `open_set`

?

#### Scott Morrison (Oct 10 2018 at 11:32):

Yes :-)

#### Johan Commelin (Oct 10 2018 at 11:32):

Aaah, ok. Hmmz.

#### Johan Commelin (Oct 10 2018 at 11:32):

Well... yes. Then we need a PR.

#### Scott Morrison (Oct 10 2018 at 11:33):

Regarding automating the copy-and-paste: I really doubt this can work in most of my cases here, where the rewrites are occurring in auto_params for structure fields.

#### Scott Morrison (Oct 10 2018 at 11:33):

The tactic `obviously`

doesn't even appear.

#### Johan Commelin (Oct 10 2018 at 11:45):

@Scott Morrison I'm stuck on

⊢ (U₁ ⟶ U₂) → U₂.s ⊆ U₁.s

After that we have extended presheaves.

#### Johan Commelin (Oct 10 2018 at 11:45):

That goal looks like very trivial. But I don't know how to extract the inclusion from the hom.

#### Scott Morrison (Oct 10 2018 at 11:46):

try `intro`

, then `cases`

?

#### Johan Commelin (Oct 10 2018 at 11:46):

Aah `cases`

.

#### Scott Morrison (Oct 10 2018 at 11:46):

or commit something I can poke at

#### Scott Morrison (Oct 10 2018 at 11:47):

remember that hom there is probably some ulift plift gadget

#### Scott Morrison (Oct 10 2018 at 11:48):

to turn a Prop into a Type at whatever universe you're living in

#### Johan Commelin (Oct 10 2018 at 11:48):

Right, it's working now. Except that it couldn't figure out `comp'`

on its own :sad:

#### Johan Commelin (Oct 10 2018 at 11:49):

import category_theory.presheaves import category_theory.sheaves import category_theory.limits open category_theory open category_theory.examples open category_theory.limits universes u v w section extend variables {X : Top.{w}} variables {V : Type v} [𝒱 : category.{v w} V] [has_limits.{v w} V] include 𝒱 variables {B : set (open_set X)} (h : topological_space.is_topological_basis ((λ U : open_set X, U.s) '' B)) def extend (F : presheaf B V) : presheaf (open_set X) V := { obj := λ U, limit ((full_subcategory_embedding (λ U' : B, U'.1 ⊆ U)) ⋙ F), map' := λ U₁ U₂ ι, limit.lift (full_subcategory_embedding (λ (U' : ↥B), U'.val ⊆ U₂) ⋙ F) { X := limit (full_subcategory_embedding (λ (U' : ↥B), U'.val ⊆ U₁) ⋙ F), π := λ U, begin dsimp, refine limit.π _ ⟨U.1, set.subset.trans U.2 _⟩ ≫ _, { cases ι, cases ι, exact ι }, { exact 𝟙 _ } end } } end extend

#### Scott Morrison (Oct 10 2018 at 12:19):

Perhaps giving a name to `full_subcategory_embedding ...`

will make this look nicer.

#### Scott Morrison (Oct 10 2018 at 12:19):

I'd be curious to see that goals after `tidy`

on `comp'`

.

#### Scott Morrison (Oct 10 2018 at 12:20):

I wonder if we need some extra help for posets here.

#### Johan Commelin (Oct 10 2018 at 12:32):

@Scott Morrison Here is what I have now:

import category_theory.presheaves import category_theory.sheaves import category_theory.limits open category_theory open category_theory.examples open category_theory.limits universes u v w section under_set variables {X : Top.{v}} def under_set (B : set (open_set X)) (U : open_set X) : set B := (λ U' : B, U'.1 ⊆ U) variables {B : set (open_set X)} {U U₁ U₂ : open_set X} instance : category (under_set B U) := by unfold under_set; apply_instance variables (B) (U) def under_set.map (ι : U₁ ⟶ U₂) : under_set B U₂ ⥤ under_set B U₁ := { obj := λ U, ⟨U.1, set.subset.trans U.2 ι.1.1⟩, map' := λ U U' f, f } def under_set.embedding : under_set B U ⥤ B := full_subcategory_embedding (under_set B U) end under_set section extend variables {X : Top.{v}} variables {V : Type u} [𝒱 : category.{u v} V] [has_limits.{u v} V] include 𝒱 variables (B : set (open_set X)) (h : topological_space.is_topological_basis ((λ U : open_set X, U.s) '' B)) def extend (F : presheaf B V) : presheaf (open_set X) V := { obj := λ U, limit ((under_set.embedding B U) ⋙ F), map' := λ U₁ U₂ ι, limit.lift ((under_set.embedding B U₂) ⋙ F) { X := limit ((under_set.embedding B U₁) ⋙ F), π := λ U, limit.π _ ⟨U.1, set.subset.trans U.2 ι.1.1⟩ ≫ (𝟙 _) } } end extend

#### Johan Commelin (Oct 10 2018 at 12:32):

Goal is:

tactic failed, there are unsolved goals state: X : Top, V : Type u, 𝒱 : category V, _inst_1 : has_limits V, B : set (open_set X), F : presheaf {x // x ∈ B} V, U₁ U₂ : open_set X, ι : U₁ ≤ U₂, j_val_val : open_set X, j_val_property : j_val_val ∈ B, j_property : ⟨j_val_val, j_val_property⟩ ∈ under_set B U₂, j'_val_val : open_set X, j'_val_property : j'_val_val ∈ B, j'_property : ⟨j'_val_val, j'_val_property⟩ ∈ under_set B U₂, f : j_val_val ≤ j'_val_val ⊢ limit.π (under_set.embedding B U₁ ⋙ F) ⟨⟨j_val_val, j_val_property⟩, _⟩ ≫ functor.map F (functor.map (under_set.embedding B U₂) {down := {down := f}}) = limit.π (under_set.embedding B U₁ ⋙ F) ⟨⟨j'_val_val, j'_val_property⟩, _⟩

#### Johan Commelin (Oct 10 2018 at 13:54):

Here is a version where the auto_param gets the job done:

def extend (F : presheaf B V) : presheaf (open_set X) V := { obj := λ U, limit ((under_set.embedding B U) ⋙ F), map' := λ U₁ U₂ ι, begin rw show limit (under_set.embedding B U₂ ⋙ F) = limit (under_set.map B ι ⋙ under_set.embedding B U₁ ⋙ F), by congr, exact limit.pre ((under_set.embedding B U₁) ⋙ F) (under_set.map B ι), end }

#### Johan Commelin (Oct 10 2018 at 13:55):

I still don't like the `rw show`

, but I don't know how to get rid of it.

#### Patrick Massot (Oct 10 2018 at 13:57):

Don't we have a gentleman agreement that any use of Scott's category theory must begin with a local notation reintroducing the proper composition symbol everywhere?

#### Johan Commelin (Oct 10 2018 at 14:07):

:lol: I didn't think about it. Sorry...

#### Johan Commelin (Oct 10 2018 at 14:51):

And we now have:

def Γ {C : Type w₁} [category.{w₁ w₂} C] (U : C) (F : presheaf C V) : V := F.obj U lemma extend_val {F : presheaf B V} (U : open_set X) : Γ U (extend F) = limit ((under_set.embedding B U) ⋙ F) := rfl lemma extend_val_basic_open {F : presheaf B V} (U : B) : Γ U.1 (extend F) ≅ Γ U F := by rw extend_val; exact { hom := limit.π (under_set.embedding B (U.val) ⋙ F) ⟨U, set.subset.refl _⟩, inv := limit.lift (under_set.embedding B (U.val) ⋙ F) { X := Γ U F, π := λ U', F.map (ulift.up (plift.up U'.2)) } }

#### Johan Commelin (Oct 10 2018 at 14:52):

That latter thing is really slow )-; But I don't see how to speed it up.

#### Patrick Massot (Oct 10 2018 at 14:52):

Lots of proofs are provided in the background

#### Johan Commelin (Oct 10 2018 at 14:54):

elaboration: tactic execution took 16.8s

num. allocated objects: 146

num. allocated closures: 146

16762ms 100.0% tactic.seq

16762ms 100.0% tactic.step

16762ms 100.0% tactic.istep._lambda_1

16762ms 100.0% tactic.istep

16762ms 100.0% scope_trace

16762ms 100.0% interaction_monad.monad._lambda_9

16759ms 100.0% all_goals_core

16759ms 100.0% tactic.interactive.exact

16759ms 100.0% _private.3346078393.all_goals_core._main._lambda_2

16759ms 100.0% tactic.all_goals

16756ms 100.0% tactic.to_expr

3ms 0.0% rw_core

3ms 0.0% tactic.exact

3ms 0.0% _private.3200700535.rw_goal._lambda_4

3ms 0.0% _private.3200700535.rw_goal._lambda_2

3ms 0.0% interaction_monad.orelse'

3ms 0.0% tactic.rewrite_target

3ms 0.0% interactive.loc.apply

3ms 0.0% tactic.interactive.propagate_tags

3ms 0.0% _interaction._lambda_2

2ms 0.0% tactic.rewrite

2ms 0.0% tactic.rewrite_core

1ms 0.0% tactic.replace_target

1ms 0.0% tactic.mk_eq_mpr

#### Johan Commelin (Oct 10 2018 at 18:16):

The next step would be to define sheaves on a basis, and show that their extensions are sheaves on the space.

#### Johan Commelin (Oct 10 2018 at 18:17):

I have the vague feeling that maybe we just want a general statement about sites.

#### Johan Commelin (Oct 10 2018 at 18:19):

@Reid Barton Do you know if the inclusion of a basis `B`

into `open_set X`

is some sort of geometric morphism?

#### Johan Commelin (Oct 10 2018 at 18:20):

If so, then I'dd rather just start attacking the general case...

#### Reid Barton (Oct 10 2018 at 18:29):

I've never learned these topos theory words

#### Johan Commelin (Oct 10 2018 at 18:31):

It seems that the answer might be yes... so now we want topos theory in mathlib :lol:

#### Johan Commelin (Oct 10 2018 at 18:35):

@Reid Barton Did you ever do things with Kan extensions in your library?

#### Reid Barton (Oct 10 2018 at 18:37):

Nope, near the top of my list for post-colimits.

#### Johan Commelin (Oct 10 2018 at 18:37):

Ok... cool. How close do you think this is to being mathlib-ready?

#### Reid Barton (Oct 10 2018 at 18:38):

Which?

#### Johan Commelin (Oct 10 2018 at 18:38):

Kan extensions

#### Reid Barton (Oct 10 2018 at 18:38):

Oh, I haven't actually started on them at all yet.

#### Johan Commelin (Oct 10 2018 at 18:39):

If Scott's limit and colimit stuff is in mathlib. Would that be a follow-up PR? Or would you need other stuff before that?

#### Reid Barton (Oct 10 2018 at 18:40):

Are you going to need general Kan extensions? Or just extending a functor on C to presheaves on C

#### Johan Commelin (Oct 10 2018 at 18:40):

The latter is good enough

#### Reid Barton (Oct 10 2018 at 18:41):

I see. We may want adjunctions, too.

#### Johan Commelin (Oct 10 2018 at 18:41):

We do

#### Johan Commelin (Oct 10 2018 at 18:41):

But I guess that will be the third PR that Scott has on his list (-;

#### Reid Barton (Oct 10 2018 at 18:41):

In order to state the characterization of Kan extension as left adjoint to restriction

#### Reid Barton (Oct 10 2018 at 18:42):

I guess we can define them without that though

#### Reid Barton (Oct 10 2018 at 18:42):

:plane: but should be back online in not too long

#### Johan Commelin (Oct 10 2018 at 18:42):

Good luck!

#### Patrick Massot (Oct 10 2018 at 19:03):

Nope, near the top of my list for post-colimits.

What about formalizing what you told us about reflective subcategory?

#### Johan Commelin (Oct 10 2018 at 19:11):

@Reid Barton Hmmm, a topological basis doesn't give a site. You don't have intersections = products. So the generalisation doesn't apply. Too bad.

#### Reid Barton (Oct 10 2018 at 19:27):

Reflective subcategories are in the same bulleted list in my notes. I forget which one is listed first :)

#### Patrick Massot (Oct 10 2018 at 19:31):

Perfectoid spaces vote for reflexive subcategories first

#### Kevin Buzzard (Oct 10 2018 at 20:54):

Aah

`cases`

.

You needed that for that `option`

question yesterday too. It works for any inductive type.

#### Scott Morrison (Oct 10 2018 at 22:35):

Hmm, your profiling output is not very helpful, because everything is hidden behind the `to_expr`

that `exact`

is calling.

#### Scott Morrison (Oct 10 2018 at 22:36):

Is it possible to make another lemma for the `exact`

?

#### Scott Morrison (Oct 10 2018 at 22:36):

(Also, this is fabulous.)

#### Kevin Buzzard (Oct 10 2018 at 22:44):

I've been really busy over the last couple of days -- but have you (@Johan Commelin ) just extended a presheaf from a basis and then shown that the restriction back to the basis is isomorphic to the original presheaf, in about 10 lines? Heh, I guess you should really have shown that the restriction was isomorphic as a presheaf on the basis to F ;-) But still -- who cares if it's slow, it's a small number of lines and that feels right to a mathematician.

#### Reid Barton (Oct 11 2018 at 03:24):

@Johan Commelin I finally looked at your actual code (too many missing Unicode characters on my phone to be practical) and I think you can use something called `limit.pre`

or similar to simplify your `extend`

even further.

If you have a diagram `X : J -> C`

and a functor `F : I -> J`

then you get an induced map `lim_I X -> lim_J (X \o F)`

and this map is called `limit.pre`

.

If you have a map `a -> b`

in `C`

then you get a functor `C/a -> C/b`

and I think your `extend`

is `limit.pre`

of this functor.

#### Johan Commelin (Oct 11 2018 at 04:00):

@Reid Barton I'm sorry, I think you have been looking at old code. The new code already uses `limit.pre`

: https://github.com/jcommelin/lean-perfectoid-spaces/blob/huber_tate/src/for_mathlib/presheaves.lean

#### Johan Commelin (Oct 11 2018 at 04:01):

It isn't as nice as I wish. I would like to get rid of the ugly `rw, congr, exact`

.

#### Reid Barton (Oct 11 2018 at 04:02):

Ah, I see. I think maybe I missed the `limit.pre`

in there, indeed

#### Reid Barton (Oct 11 2018 at 04:03):

I guess `convert`

might be slightly better?

#### Reid Barton (Oct 11 2018 at 04:03):

change `exact`

to `convert`

and move it first, then see what happens?

#### Reid Barton (Oct 11 2018 at 04:03):

I'm a little confused how `congr`

proved something without producing any new goals

#### Johan Commelin (Oct 11 2018 at 04:03):

@Kevin Buzzard Yes, I did. Isn't it delightful? But proving that the extension of a sheaf is a sheaf will be a lot harder.

#### Johan Commelin (Oct 11 2018 at 04:04):

change

`exact`

to`convert`

and move it first, then see what happens?

I think that didn't work: deterministic timeout or something.

#### Johan Commelin (Oct 11 2018 at 04:04):

In some sense it was really brittle.

#### Reid Barton (Oct 11 2018 at 04:05):

Odd

#### Johan Commelin (Oct 11 2018 at 04:05):

That file doens't need anything from the perfectoid project. So if you want to hack on it, you can just copy-paste it.

#### Johan Commelin (Oct 11 2018 at 04:10):

Of course you need Scott's libs

#### Reid Barton (Oct 11 2018 at 16:21):

@Johan Commelin I was able to replace the whole `map'`

field by

map' := λ U₁ U₂ ι, limit.pre ((under_set.embedding B U₁) ⋙ F) (under_set.map B ι)

Everything is quite slow in the editor, I believe because there are errors in the imports (stuff under `category_theory.limits`

)

#### Johan Commelin (Oct 11 2018 at 19:11):

Cool! Thanks a lot. Somehow I think I got deterministic timeouts when I tried that. Maybe it is related to the errors in the imports that you mentioned.

#### Reid Barton (Oct 11 2018 at 19:13):

My understanding is that `lean --make`

doesn't write out `.olean`

files when the build was unsuccessful, which means if your imports have errors then lean in the editor will be much slower.

#### Reid Barton (Oct 11 2018 at 19:14):

It looks like the errors are rather trivial in this case (some tactics failed because there were no goals remaining) but I didn't try to just fix them because they are in lean-category-theory

#### Johan Commelin (Oct 12 2018 at 07:18):

Ok, now it worked for me as well.

#### Johan Commelin (Oct 15 2018 at 07:27):

I think the following is pretty ugly:

variables {B : set (open_set X)} variables (h : topological_space.is_topological_basis ((λ U : open_set X, U.s) '' B))

Does this mean that I should define `is_basis`

for `B`

directly? It feels like duplicating a lot of stuff. Is this the curse of bundling?

#### Mario Carneiro (Oct 15 2018 at 07:41):

I don't understand what you are trying to do

#### Johan Commelin (Oct 15 2018 at 07:41):

I'm trying to say that a collection of open sets is a basis. But the open sets are bundled.

#### Mario Carneiro (Oct 15 2018 at 07:46):

I guess you can write `open_set.s`

instead of the lambda

#### Johan Commelin (Oct 15 2018 at 07:47):

Ok, and would that be the *morally correct* way? Or should I "develop the theory of a basis of bundled open sets"?

#### Mario Carneiro (Oct 15 2018 at 07:48):

I'm not sure if you want the forward image or preimage yet, but I think this is what you want

#### Johan Commelin (Oct 15 2018 at 07:52):

Well, you could redefine `is_basis`

for a set of opens, right? Something like

\forall U : open_set X, x : X, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ⊆ U

#### Mario Carneiro (Oct 15 2018 at 07:56):

I would define `open_set.is_basis`

using the image formulation, and then prove that version as a theorem

#### Johan Commelin (Oct 15 2018 at 07:56):

Ok, thanks.

#### Mario Carneiro (Oct 15 2018 at 07:57):

also that's not the right condition

#### Mario Carneiro (Oct 15 2018 at 07:57):

the exists is satisfied by `U`

#### Johan Commelin (Oct 15 2018 at 07:58):

No, `U`

is not `∈ B`

. (In general.)

#### Mario Carneiro (Oct 15 2018 at 07:58):

oh... but what about intersections?

#### Johan Commelin (Oct 15 2018 at 07:58):

What's with them?

#### Mario Carneiro (Oct 15 2018 at 07:59):

a basis should be closed under intersection (ish)

#### Johan Commelin (Oct 15 2018 at 07:59):

Oooo... maybe. I'll see when I start proving things (-;

#### Mario Carneiro (Oct 15 2018 at 08:00):

This just says B covers the space

#### Johan Commelin (Oct 15 2018 at 08:00):

It says that `B`

covers every open.

#### Mario Carneiro (Oct 15 2018 at 08:01):

oh, actually I think you have the intersection property then

#### Mario Carneiro (Oct 15 2018 at 08:02):

if $U, V \in B$ and $x \in U \cap V$, then $U\cap V$ is open so you can find $x\in W\in B$ with $W\subseteq U\cap V$

#### Johan Commelin (Oct 15 2018 at 08:03):

That looks good, right?

#### Mario Carneiro (Oct 15 2018 at 08:12):

yeah

#### Mario Carneiro (Oct 15 2018 at 08:13):

actually now I recall Kevin saying that this was the obvious definition and he was confused by mathlib's

#### Johan Commelin (Oct 15 2018 at 12:09):

@Mario Carneiro Proving that the two definitions are equivalent is a major headache. I feel like we are missing an induction principle for generated topologies. But maybe it is *me* who is missing it.

#### Johan Commelin (Oct 15 2018 at 12:21):

-- set.lean @[reducible] def sUnion (s : set (set α)) : set α := {t | ∃ a ∈ s, t ∈ a} prefix `⋃₀`:110 := sUnion

Does this mean that we can't use `⋃₀`

to take the union of `Us : set (open_set X)`

? Or can/should I overload notation?

#### Johan Commelin (Oct 15 2018 at 12:36):

I would expect that this notation is meaningful for every type that has a union-operator.

#### Kenny Lau (Oct 15 2018 at 12:51):

try it wthout 0?

#### Johan Commelin (Oct 15 2018 at 12:53):

That gives a weird error: `invalid expression starting at 27:51`

#### Johan Commelin (Oct 15 2018 at 12:57):

@Kenny Lau How is this supposed to work? I tried

lemma is_basis_iff₁ {B : set (open_set X)} : is_basis B ↔ ∀ {U : open_set X}, ∃ Us ⊆ set B, U = ⋃ U' ∈ Us, U' := sorry

Clearly this is not what Lean wants to see...

#### Kenny Lau (Oct 15 2018 at 12:58):

you need : not \in

#### Kenny Lau (Oct 15 2018 at 12:58):

and it’s called bUnion

#### Johan Commelin (Oct 15 2018 at 13:03):

Right, so for this we need a lattice structure on `open_set`

. Which we will need at some point anyway.

#### Johan Commelin (Oct 15 2018 at 15:03):

@Scott Morrison I know you are busy. Just posting this in case you have a couple of minutes where you are bored :stuck_out_tongue_wink:

import category_theory.examples.topological_spaces import order.lattice import category_theory.tactics.obviously universes u v open category_theory open category_theory.examples namespace open_set open topological_space lattice variables {X : Top.{v}} local attribute [back] topological_space.is_open_inter local attribute [back] is_open_union local attribute [back] open_set.is_open instance : has_inter (open_set X) := { inter := λ U V, ⟨ U.s ∩ V.s, by obviously ⟩ } instance : has_union (open_set X) := { union := λ U V, ⟨ U.s ∪ V.s, by obviously ⟩ } instance : lattice (open_set X) := by refine { sup := open_set.has_union.union, inf := open_set.has_inter.inter, le_antisymm := λ U₁ U₂ _ _, by cases U₁; cases U₂; tidy, le_sup_left := begin intros U₁ U₂, cases U₁; cases U₂, tidy, end, le_sup_right := sorry, sup_le := sorry, inf_le_left := sorry, inf_le_right := sorry, le_inf := sorry, ..open_set.preorder }; tidy

What incantations do I need to get `tidy`

up to speed?

#### Johannes Hölzl (Oct 15 2018 at 15:07):

I guess you need the rules how `union`

and `intersection`

behave under `subset`

, like `set.subset_union_left`

. So try add this as `back`

.

#### Mario Carneiro (Oct 15 2018 at 15:31):

hey @Kenny Lau, I see a galois insertion...

#### Reid Barton (Oct 15 2018 at 15:35):

Do we have an emoji for galois insertion

#### Johan Commelin (Oct 15 2018 at 15:43):

Thanks, I'll try that tomorrow.

#### Kevin Buzzard (Oct 15 2018 at 16:21):

Do we have an emoji for galois insertion

So we need to choose one, right? People should vote on Reid's question.

#### Johan Commelin (Oct 16 2018 at 06:45):

@Scott Morrison I implemented Johannes suggestion. Now I have the following bunch of code:

import category_theory.examples.topological_spaces import order.lattice import category_theory.tactics.obviously universes u v open category_theory open category_theory.examples namespace open_set open topological_space lattice variables {X : Top.{v}} local attribute [back] topological_space.is_open_inter local attribute [back] is_open_union local attribute [back] open_set.is_open local attribute [back] set.subset_union_left local attribute [back] set.subset_union_right instance : has_inter (open_set X) := { inter := λ U V, ⟨ U.s ∩ V.s, by obviously ⟩ } instance : has_union (open_set X) := { union := λ U V, ⟨ U.s ∪ V.s, by obviously ⟩ } #print prefix open_set.has_union local attribute [simp] open_set.has_union.equations._eqn_1 instance : lattice (open_set X) := by refine { sup := open_set.has_union.union, inf := open_set.has_inter.inter, le_antisymm := λ U₁ U₂ _ _, by cases U₁; cases U₂; tidy, le_sup_left := begin tidy, end, le_sup_right := begin intros U₁ U₂, cases U₁; cases U₂, tidy, end, sup_le := sorry, inf_le_left := sorry, inf_le_right := sorry, le_inf := sorry, ..open_set.preorder }; tidy

#### Johan Commelin (Oct 16 2018 at 06:46):

The `tidy`

in the proof of `le_sup_left`

leaves me with the following goal:

X : Top, a b : open_set X, a_1 : X.α, a_2 : a_1 ∈ a.s ⊢ a_1 ∈ a.s ∨ a_1 ∈ b.s

#### Johan Commelin (Oct 16 2018 at 06:47):

Ooh wait! Does this mean that I have to mark `or.inl`

with `[back!]`

or something like that?

#### Kevin Buzzard (Oct 16 2018 at 06:47):

Does `@[simp] instance : has_union (open_set X)`

do the same as `attribute [simp] open_set.has_union.equations._eqn_1`

?

#### Mario Carneiro (Oct 16 2018 at 06:49):

or.inl is not a good `back!`

lemma

#### Johan Commelin (Oct 16 2018 at 06:49):

Hmmm, why not?

#### Mario Carneiro (Oct 16 2018 at 06:50):

because it will try to prove everything by the left disjunct

#### Johan Commelin (Oct 16 2018 at 06:50):

Only if the assumptions are satisfied, right?

#### Mario Carneiro (Oct 16 2018 at 06:50):

not with the `!`

#### Mario Carneiro (Oct 16 2018 at 06:50):

I think `simp`

should work

#### Mario Carneiro (Oct 16 2018 at 06:51):

because it will turn the goal into `true \/ ...`

and then `true`

#### Johan Commelin (Oct 16 2018 at 06:51):

Well, it doesn't. Because `tidy`

would try that.

#### Mario Carneiro (Oct 16 2018 at 06:51):

did you see if `simp * at *`

works by hand?

#### Mario Carneiro (Oct 16 2018 at 06:51):

what about `simp *`

?

#### Johan Commelin (Oct 16 2018 at 06:53):

Ok, that works. Is that a bug in `tidy`

?

#### Mario Carneiro (Oct 16 2018 at 06:55):

or a bug in `simp * at *`

#### Mario Carneiro (Oct 16 2018 at 06:56):

wait, which is "that"

#### Kevin Buzzard (Oct 16 2018 at 06:57):

I have a very unclear idea about what all these things like `tidy`

and `obviously`

and `backwards_reasoning`

do. It seems to me that they "all do the same thing" -- they just "try a bunch of stuff like simp and split and stuff". Does `tidy`

have a sufficiently formal specification that one can ask if there is a "bug" in it? Do you actually mean "let's make `tidy`

try more stuff"?

#### Mario Carneiro (Oct 16 2018 at 06:58):

`back`

has a "spec", but you are right about the others

#### Mario Carneiro (Oct 16 2018 at 06:58):

`obviously`

is `tidy`

+ `rewrite_search`

#### Mario Carneiro (Oct 16 2018 at 06:58):

which is that graph thing that Keeley Hoek did

#### Johan Commelin (Oct 16 2018 at 06:59):

`simp *`

worked. I would imagine that `tidy`

should try that as well. Of course it is not a bug in the strict sense; but I meant a "bug" in the sense that it would be a nice feature to add to `tidy`

.

#### Mario Carneiro (Oct 16 2018 at 06:59):

`tidy`

is just a kitchen sink tactic right now, although I understand it is loosely based on the Gowers-Ganesalingam prover

#### Johan Commelin (Oct 16 2018 at 07:05):

I'm struggling with finding a statement that type checks. I just proved that `open_set X`

has a lattice structure. Now I want to take a union of a bunch of opens. What should I tell Lean to make sense of this?

lemma is_basis_iff₁ {B : set (open_set X)} : is_basis B ↔ ∀ {U : open_set X}, ∃ Us ⊆ set B, U = ⋃ U' : Us, U' := sorry

#### Johan Commelin (Oct 16 2018 at 07:05):

Currently it doesn't like the `⋃`

symbol.

#### Mario Carneiro (Oct 16 2018 at 07:07):

use the sup symbol

#### Kevin Buzzard (Oct 16 2018 at 07:07):

Isn't there `union`

and `Union`

and `bUnion`

and `sUnion`

or something? Usage depends on whether you're taking a union of two things, or a set of things, or a type of things etc. One of them is that big union symbol -- aren't there other notations too though? I can never remember which is which here.

#### Mario Carneiro (Oct 16 2018 at 07:08):

most of the union/inter notation is specific to `set`

#### Mario Carneiro (Oct 16 2018 at 07:08):

the generic version is `Sup`

and `Inf`

#### Johan Commelin (Oct 16 2018 at 07:08):

Ok, I see. So for everything else we want to use lattice notation?

#### Mario Carneiro (Oct 16 2018 at 07:08):

yes

#### Johan Commelin (Oct 16 2018 at 07:09):

And turning something into a lattice doesn't automatically give you a `has_Sup`

. Is that on purpose?

I don't know anything about lattices.

#### Mario Carneiro (Oct 16 2018 at 07:09):

`∃ Us ⊆ set B,`

what should this mean?

#### Mario Carneiro (Oct 16 2018 at 07:09):

a complete lattice, not a lattice

#### Johan Commelin (Oct 16 2018 at 07:09):

That there is a bunch of basic opens such that...

#### Mario Carneiro (Oct 16 2018 at 07:09):

lattice just gives you binary sup

#### Johan Commelin (Oct 16 2018 at 07:09):

Ok, so I should prove that `open_set`

is a complete lattice.

#### Mario Carneiro (Oct 16 2018 at 07:10):

yes

#### Mario Carneiro (Oct 16 2018 at 07:10):

again, galois insertion should make it easy

#### Johan Commelin (Oct 16 2018 at 07:12):

I propose :return: for galois connections and adjunctions. I don't understand the :basketball: symbol. Maybe it's because I'm Dutch :lol:

#### Johan Commelin (Oct 16 2018 at 07:13):

Ok, I have no idea what boilerplate I should write for that Galois insertion. What is the best way to find this out?

#### Mario Carneiro (Oct 16 2018 at 07:16):

you need a pair of functions with a galois connection, from the complete lattice to the type you want a complete lattice structure on, and one round trip should be the identity

#### Kevin Buzzard (Oct 16 2018 at 07:21):

The basketball was the only emoji I found which looked like anything being inserted into anything, that's all

#### Kevin Buzzard (Oct 16 2018 at 07:22):

I didn't even look for an emoji of something being connected to something

#### Johan Commelin (Oct 16 2018 at 07:23):

Ok, so one of the maps is `open_set.s`

and the other is ?? the interior? Or the smallest open containing some set `S`

?

#### Mario Carneiro (Oct 16 2018 at 07:23):

interior, certainly

#### Johan Commelin (Oct 16 2018 at 07:23):

Brainfart, that doesn't even make sense. So it should be the interior.

#### Mario Carneiro (Oct 16 2018 at 07:25):

actually I'm a bit worried you will end up the wrong way around, i.e. you will get the `u`

function being injective instead of the `l`

function

#### Mario Carneiro (Oct 16 2018 at 07:25):

@Johannes Hölzl How do you want to do galois coinsertions?

#### Johan Commelin (Oct 16 2018 at 07:37):

Ok, so `l = interior`

and `u = open_set.s`

. Is this good or bad news for our complete_lattice?

#### Mario Carneiro (Oct 16 2018 at 07:39):

try to prove galois insertion?

#### Johan Commelin (Oct 16 2018 at 07:44):

Oops, I switched `l`

and `u`

. I still find those names confusing... Ok, so it is going to be a `coinsertion`

.

#### Johan Commelin (Oct 16 2018 at 07:50):

@Mario Carneiro Is the Galois connection enough to get the complete lattice structure? Or do I need to work out `galois_coinsertion`

first? I really don't know the maths here.

#### Mario Carneiro (Oct 16 2018 at 07:50):

the insertion is important

#### Mario Carneiro (Oct 16 2018 at 07:50):

it is basically making an order embedding

#### Mario Carneiro (Oct 16 2018 at 07:50):

and you pull the relation back along that

#### Johan Commelin (Oct 16 2018 at 07:50):

You mean coinsertion?

#### Mario Carneiro (Oct 16 2018 at 07:51):

that too

#### Johan Commelin (Oct 16 2018 at 07:51):

Hmmm, I will try to dualize all the stuff about `insertion`

s.

#### Mario Carneiro (Oct 16 2018 at 07:51):

it should work just as well, it will just pull a lattice from left to right instead of right to left

#### Mario Carneiro (Oct 16 2018 at 07:51):

or vice versa

#### Mario Carneiro (Oct 16 2018 at 07:51):

you know, just put co everywhere

#### Johannes Hölzl (Oct 16 2018 at 07:52):

look into how it is done for `filter`

. Here I use `dual_order`

to get the other way round

#### Mario Carneiro (Oct 16 2018 at 07:53):

I was just about to suggest that

#### Johannes Hölzl (Oct 16 2018 at 07:53):

def gi_generate (α : Type*) : @galois_insertion (set (set α)) (order_dual (filter α)) _ _ filter.generate filter.sets

#### Mario Carneiro (Oct 16 2018 at 07:53):

but filter is dualized on only one side

#### Mario Carneiro (Oct 16 2018 at 07:54):

I guess a coinsertion is dualized on both sides

#### Johannes Hölzl (Oct 16 2018 at 07:54):

is it enough to add `order_dual`

on both sides?

#### Mario Carneiro (Oct 16 2018 at 07:54):

I wonder whether we want a separate definition though since otherwise the names will be even more confusing than they already are

#### Mario Carneiro (Oct 16 2018 at 07:55):

plus `galois_coinsertion`

should extend `galois_connection`

with no duals

#### Mario Carneiro (Oct 16 2018 at 07:56):

do we know that `galois_connection`

is self-dual?

#### Johannes Hölzl (Oct 16 2018 at 07:56):

to its symmetric form:

protected lemma dual [pα : preorder α] [pβ : preorder β] (l : α → β) (u : β → α) (gc : galois_connection l u) : @galois_connection (order_dual β) (order_dual α) _ _ u l := assume a b, (gc _ _).symm

#### Johannes Hölzl (Oct 16 2018 at 07:56):

in https://github.com/leanprover/mathlib/blob/master/order/galois_connection.lean#L160

#### Kevin Buzzard (Oct 16 2018 at 08:01):

then it should just be called `galois_nnection`

#### Kevin Buzzard (Oct 16 2018 at 08:02):

it's shorter

#### Johan Commelin (Oct 16 2018 at 08:03):

Aaahrg, all those design decisions. Is there a choice procedure for such design decisions?

I think we should make the same choice as for the `limit`

vs `colimit`

story in category theory.

#### Johan Commelin (Oct 16 2018 at 08:04):

So we just copy-paste all the code and dualize it. Right?

#### Kevin Buzzard (Oct 16 2018 at 08:04):

[or write a tactic which generates the code for you...]

#### Johannes Hölzl (Oct 16 2018 at 08:05):

usually you copy all statements from the Galois insertion anyway. I don't see a problem to use a Galois insertion and `dual_order`

twice. You only want to use it to get the complete lattice, afterwards you don't care anymore.

#### Johan Commelin (Oct 16 2018 at 09:06):

Ok, now I've got

def interior (s : set X) : open_set X := { s := interior s, is_open := is_open_interior } def gc : galois_connection (@open_set.s X) interior := λ U s, ⟨λ h, interior_maximal h U.is_open, λ h, le_trans h interior_subset⟩ def gco : galois_coinsertion (@open_set.s X) interior := { choice := λ s _, interior s, gc := gc, u_l_le := λ _, interior_subset, choice_eq := λ _ _, rfl } instance : partial_order (open_set X) := { le_antisymm := λ U₁ U₂ _ _, by cases U₁; cases U₂; tidy, .. open_set.preorder } instance : complete_lattice (open_set X) := galois_coinsertion.lift_complete_lattice gco def univ : open_set X := { s := set.univ, is_open := is_open_univ }

I guess that this definition of `univ`

is not correct? Should it be a theorem about `⊤`

somehow?

#### Johan Commelin (Oct 16 2018 at 11:38):

@Johannes Hölzl Those `order_dual`

s are completely blowing up my brain. Does this look good or am I missing something?

def interior (s : set X) : open_set X := { s := interior s, is_open := is_open_interior } def gc : galois_connection (@open_set.s X) interior := λ U s, ⟨λ h, interior_maximal h U.is_open, λ h, le_trans h interior_subset⟩ def gi : @galois_insertion (order_dual _) (order_dual _) _ _ interior (@open_set.s X) := { choice := λ s _, interior s, gc := galois_connection.dual _ _ gc, le_l_u := λ _, interior_subset, choice_eq := λ _ _, rfl } instance : partial_order (open_set X) := { le_antisymm := λ U₁ U₂ _ _, by cases U₁; cases U₂; tidy, .. open_set.preorder } instance : complete_lattice (open_set X) := @galois_insertion.lift_complete_lattice (order_dual _) (order_dual _) _ interior (@open_set.s X) _ gi

#### Johannes Hölzl (Oct 16 2018 at 11:45):

looks good to me. Is there something wrong?

#### Johan Commelin (Oct 16 2018 at 11:52):

Yes, I'm getting the dual order.

#### Johan Commelin (Oct 16 2018 at 11:53):

So now I need a function that takes an order, and flips it around.

#### Johan Commelin (Oct 16 2018 at 11:58):

@Johannes Hölzl Is there a way to unfold something only once?

#### Johannes Hölzl (Oct 16 2018 at 12:01):

hm, `rw [h] {occs := occurrences.pos [1]}`

is the only thing I know

#### Johannes Hölzl (Oct 16 2018 at 12:03):

for the dual, lets take a look at filters again:

private def original_complete_lattice : complete_lattice (filter α) := @order_dual.lattice.complete_lattice _ (gi_generate α).lift_complete_lattice

#### Johan Commelin (Oct 16 2018 at 12:03):

I hacked around it like this:

instance open_set.lattice.complete_lattice.order_dual : complete_lattice (order_dual (open_set X)) := @galois_insertion.lift_complete_lattice (order_dual _) (order_dual _) _ interior (@open_set.s X) _ gi lemma order_dual_order_dual {α : Type*} : order_dual (order_dual α) = α := rfl instance : complete_lattice (open_set X) := begin have foo : complete_lattice (order_dual (order_dual (open_set X))), by apply_instance, rw order_dual_order_dual at foo, exact foo end

@Johannes Hölzl I am not so sure that the coinsertions are useless. This is causing me quite some pain...

#### Johannes Hölzl (Oct 16 2018 at 12:04):

`order_dual.lattice.complete_lattice`

does what you want

#### Johannes Hölzl (Oct 16 2018 at 12:04):

and it doesn't have the `rw`

problem

#### Johan Commelin (Oct 16 2018 at 12:06):

@Johannes Hölzl I don't see how to apply it. It can only put orders on `order_dual _`

, it can't go the other way.

#### Johannes Hölzl (Oct 16 2018 at 12:09):

you are sure it doesn't work? `preorder (order_dual (order_dual A)) = preorder A`

should be (in your case) by definition

#### Johannes Hölzl (Oct 16 2018 at 12:09):

can you put your theory on a gist?

#### Johan Commelin (Oct 16 2018 at 12:17):

@Johannes Hölzl Voila: https://gist.github.com/jcommelin/c9d04b7770f89a0fadc11aae5ca90d87

This is what I have so far.

#### Johannes Hölzl (Oct 16 2018 at 12:27):

instance : partial_order (open_set X) := { le_antisymm := λ U₁ U₂ _ _, by cases U₁; cases U₂; tidy, .. open_set.preorder } instance : complete_lattice (open_set X) := @order_dual.lattice.complete_lattice _ (@galois_insertion.lift_complete_lattice (order_dual _) (order_dual _) _ interior (@open_set.s X) _ gi)

now you have the dual

#### Johannes Hölzl (Oct 16 2018 at 12:27):

is this what you want?

#### Johan Commelin (Oct 16 2018 at 12:27):

I think it is. Let me try.

#### Johan Commelin (Oct 16 2018 at 12:29):

But this still isn't proved by `rfl`

:

@[simp] lemma Lub_s {Us : set (open_set X)} : (⨆ U ∈ Us, U).s = ⋃₀ (open_set.s '' Us) :=

And I think that with coinsertions it could have been `rfl`

, right?

#### Johannes Hölzl (Oct 16 2018 at 12:30):

only if you setup `choice`

correctly

#### Johannes Hölzl (Oct 16 2018 at 12:31):

and this is also with insertion a `rfl`

#### Johannes Hölzl (Oct 16 2018 at 12:32):

so, no `coinsertion`

doesn't give you a rfl by default. It will only be a `rfl`

when you use the proof in `choice`

to construct `rfl`

data. And since `insertion`

and `coinsertion`

are just dual, it works also with insertion.

#### Johannes Hölzl (Oct 16 2018 at 12:33):

So what you need to do:

def gi : @galois_insertion (order_dual (set X)) (order_dual (open_set X)) _ _ interior (@open_set.s X) := { choice := λ s _, interior s, gc := galois_connection.dual _ _ gc, le_l_u := λ U, interior_subset, choice_eq := λ _ _, rfl }

Instead of `choice := λ s _, interior s,`

you need to write something like:

`choice := λ s _, (s, proof that s is open),`

#### Johan Commelin (Oct 16 2018 at 12:35):

Huuh, but `s`

isn't open.

#### Johannes Hölzl (Oct 16 2018 at 12:35):

yes it is, the `_`

is actually a proof from which you can show that it is open

#### Johannes Hölzl (Oct 16 2018 at 12:36):

it says: `interior s = s`

#### Johannes Hölzl (Oct 16 2018 at 12:37):

then you also need to adapt your `choice_eq`

proof accordingly

#### Johan Commelin (Oct 16 2018 at 12:38):

Ok, I see. I'll try to do this.

#### Johan Commelin (Oct 16 2018 at 12:47):

@Johannes Hölzl Sorry, but the following still doesn't work:

have foo : (Sup Us).s = Sup (open_set.s '' Us) := rfl

#### Johannes Hölzl (Oct 16 2018 at 12:59):

you should get:

have foo : (Sup Us).s = (⨆a∈Us, a.s) := rfl

#### Johan Commelin (Oct 16 2018 at 13:05):

@Johannes Hölzl That gives me

invalid field notation, type is not of the form (C ...) where C is a constant a has type ?m_1

I now have the following ugly proof myself:

@[simp] lemma Sup_s {Us : set (open_set X)} : (Sup Us).s = ⋃₀ (open_set.s '' Us) := by rw [@galois_connection.l_Sup _ _ _ _ (@open_set.s X) interior (gc) Us, set.sUnion_image]

#### Johannes Hölzl (Oct 16 2018 at 13:05):

what about `have foo : (Sup Us).s = (⨆a∈Us, open_set.s a) := rfl`

#### Johan Commelin (Oct 16 2018 at 13:10):

Still fails:

invalid type ascription, term has type ?m_2 = ?m_2 but is expected to have type (Sup Us).s = ⨆ (a : open_set X) (H : a ∈ Us), a.s

#### Johannes Hölzl (Oct 16 2018 at 13:16):

how does your `gi`

look like?

#### Johan Commelin (Oct 16 2018 at 13:17):

def gi : @galois_insertion (order_dual (set X)) (order_dual (open_set X)) _ _ interior (@open_set.s X) := { choice := λ s hs, { s := s, is_open := interior_eq_iff_open.mp $ le_antisymm interior_subset hs }, gc := galois_connection.dual _ _ gc, le_l_u := λ _, interior_subset, choice_eq := λ s hs, le_antisymm interior_subset hs }

#### Johannes Hölzl (Oct 16 2018 at 13:36):

hm

set_option pp.all true #print open_set.lattice.complete_lattice

somewhere `set`

gets unfolded and the `pi`

instance is used. Then we get different `Sup`

and `Inf`

.

#### Reid Barton (Oct 16 2018 at 13:36):

Kudos to the individual who came up with :gun: for Galois insertion btw

#### Johan Commelin (Oct 16 2018 at 13:38):

@Johannes Hölzl Hmmm... I think I'm giving up on debugging this. It is too annoying. If you feel like debugging it, I haven't made much progress since my gist.

#### Johannes Hölzl (Oct 16 2018 at 13:40):

instance : complete_lattice (open_set X) := @order_dual.lattice.complete_lattice _ (@galois_insertion.lift_complete_lattice (order_dual (set X)) (order_dual (open_set X)) _ interior (@open_set.s X) _ gi) lemma Sup_s {Us : set (open_set X)} : (Sup Us).s = ⨆s∈Us, open_set.s s := rfl

this works

#### Johannes Hölzl (Oct 16 2018 at 13:46):

`(order_dual (set _))`

is already enough. Then the elaborator finds the right instance, instead of the instance for `X -> Prop`

#### Johan Commelin (Oct 16 2018 at 13:48):

Ok, so my instance is wrong... hmmzzz. Thanks for finding this bug!

#### Alex J. Best (Oct 16 2018 at 15:25):

@Reid Barton Thanks, after trying to teach myself some lean on the side and lurking here a lot without doing anything I'm glad someone found my first "contribution" as funny as I did

#### David Michael Roberts (Oct 17 2018 at 08:49):

then it should just be called

`galois_nnection`

or a cogalois-nnection (sorry)

Last updated: May 19 2021 at 02:10 UTC