Zulip Chat Archive

Stream: maths

Topic: extend presheaf from basis


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

view this post on Zulip Johan Commelin (Oct 10 2018 at 09:40):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 09:43):

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

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

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

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 09:45):

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

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 09:45):

Do you have comma categories somewhere?

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 09:45):

I just want the category of opens contained in U.

view this post on Zulip Johan Commelin (Oct 10 2018 at 09:45):

Maybe you already have this somewhere...

view this post on Zulip Johan Commelin (Oct 10 2018 at 09:46):

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

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 10:06):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 10:11):

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

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

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 10:14):

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

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 10:48):

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

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 10:53):

Thanks, I added over.forget.

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

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

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 11:30):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:30):

no problem

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:31):

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 11:31):

No, presheaves aren't in mathlib

view this post on Zulip Johan Commelin (Oct 10 2018 at 11:31):

Or did you break the definition of open_set?

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:32):

Yes :-)

view this post on Zulip Johan Commelin (Oct 10 2018 at 11:32):

Aaah, ok. Hmmz.

view this post on Zulip Johan Commelin (Oct 10 2018 at 11:32):

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

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:33):

The tactic obviously doesn't even appear.

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

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:46):

try intro, then cases?

view this post on Zulip Johan Commelin (Oct 10 2018 at 11:46):

Aah cases.

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:46):

or commit something I can poke at

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:47):

remember that hom there is probably some ulift plift gadget

view this post on Zulip Scott Morrison (Oct 10 2018 at 11:48):

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

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

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 12:19):

Perhaps giving a name to full_subcategory_embedding ... will make this look nicer.

view this post on Zulip Scott Morrison (Oct 10 2018 at 12:19):

I'd be curious to see that goals after tidy on comp'.

view this post on Zulip Scott Morrison (Oct 10 2018 at 12:20):

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

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

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

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

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

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 14:07):

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

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 14:52):

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

view this post on Zulip Patrick Massot (Oct 10 2018 at 14:52):

Lots of proofs are provided in the background

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

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 18:17):

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

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 18:20):

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

view this post on Zulip Reid Barton (Oct 10 2018 at 18:29):

I've never learned these topos theory words

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 18:35):

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

view this post on Zulip Reid Barton (Oct 10 2018 at 18:37):

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 18:37):

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

view this post on Zulip Reid Barton (Oct 10 2018 at 18:38):

Which?

view this post on Zulip Johan Commelin (Oct 10 2018 at 18:38):

Kan extensions

view this post on Zulip Reid Barton (Oct 10 2018 at 18:38):

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

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

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 18:40):

The latter is good enough

view this post on Zulip Reid Barton (Oct 10 2018 at 18:41):

I see. We may want adjunctions, too.

view this post on Zulip Johan Commelin (Oct 10 2018 at 18:41):

We do

view this post on Zulip Johan Commelin (Oct 10 2018 at 18:41):

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

view this post on Zulip Reid Barton (Oct 10 2018 at 18:41):

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

view this post on Zulip Reid Barton (Oct 10 2018 at 18:42):

I guess we can define them without that though

view this post on Zulip Reid Barton (Oct 10 2018 at 18:42):

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 18:42):

Good luck!

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

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

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

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:31):

Perfectoid spaces vote for reflexive subcategories first

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

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 22:36):

Is it possible to make another lemma for the exact?

view this post on Zulip Scott Morrison (Oct 10 2018 at 22:36):

(Also, this is fabulous.)

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

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

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

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

view this post on Zulip Reid Barton (Oct 11 2018 at 04:02):

Ah, I see. I think maybe I missed the limit.pre in there, indeed

view this post on Zulip Reid Barton (Oct 11 2018 at 04:03):

I guess convert might be slightly better?

view this post on Zulip Reid Barton (Oct 11 2018 at 04:03):

change exact to convert and move it first, then see what happens?

view this post on Zulip Reid Barton (Oct 11 2018 at 04:03):

I'm a little confused how congr proved something without producing any new goals

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

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 04:04):

In some sense it was really brittle.

view this post on Zulip Reid Barton (Oct 11 2018 at 04:05):

Odd

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 04:10):

Of course you need Scott's libs

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

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

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

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

view this post on Zulip Johan Commelin (Oct 12 2018 at 07:18):

Ok, now it worked for me as well.

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

view this post on Zulip Mario Carneiro (Oct 15 2018 at 07:41):

I don't understand what you are trying to do

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

view this post on Zulip Mario Carneiro (Oct 15 2018 at 07:46):

I guess you can write open_set.s instead of the lambda

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

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

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

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

view this post on Zulip Johan Commelin (Oct 15 2018 at 07:56):

Ok, thanks.

view this post on Zulip Mario Carneiro (Oct 15 2018 at 07:57):

also that's not the right condition

view this post on Zulip Mario Carneiro (Oct 15 2018 at 07:57):

the exists is satisfied by U

view this post on Zulip Johan Commelin (Oct 15 2018 at 07:58):

No, U is not ∈ B. (In general.)

view this post on Zulip Mario Carneiro (Oct 15 2018 at 07:58):

oh... but what about intersections?

view this post on Zulip Johan Commelin (Oct 15 2018 at 07:58):

What's with them?

view this post on Zulip Mario Carneiro (Oct 15 2018 at 07:59):

a basis should be closed under intersection (ish)

view this post on Zulip Johan Commelin (Oct 15 2018 at 07:59):

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

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:00):

This just says B covers the space

view this post on Zulip Johan Commelin (Oct 15 2018 at 08:00):

It says that B covers every open.

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:01):

oh, actually I think you have the intersection property then

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:02):

if U,VBU, V \in B and xUVx \in U \cap V, then UVU\cap V is open so you can find xWBx\in W\in B with WUVW\subseteq U\cap V

view this post on Zulip Johan Commelin (Oct 15 2018 at 08:03):

That looks good, right?

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:12):

yeah

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

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

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

view this post on Zulip Johan Commelin (Oct 15 2018 at 12:36):

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

view this post on Zulip Kenny Lau (Oct 15 2018 at 12:51):

try it wthout 0?

view this post on Zulip Johan Commelin (Oct 15 2018 at 12:53):

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

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

view this post on Zulip Kenny Lau (Oct 15 2018 at 12:58):

you need : not \in

view this post on Zulip Kenny Lau (Oct 15 2018 at 12:58):

and it’s called bUnion

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

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

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

view this post on Zulip Mario Carneiro (Oct 15 2018 at 15:31):

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

view this post on Zulip Reid Barton (Oct 15 2018 at 15:35):

Do we have an emoji for galois insertion

view this post on Zulip Johan Commelin (Oct 15 2018 at 15:43):

Thanks, I'll try that tomorrow.

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

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

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

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

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 06:49):

or.inl is not a good back! lemma

view this post on Zulip Johan Commelin (Oct 16 2018 at 06:49):

Hmmm, why not?

view this post on Zulip Mario Carneiro (Oct 16 2018 at 06:50):

because it will try to prove everything by the left disjunct

view this post on Zulip Johan Commelin (Oct 16 2018 at 06:50):

Only if the assumptions are satisfied, right?

view this post on Zulip Mario Carneiro (Oct 16 2018 at 06:50):

not with the !

view this post on Zulip Mario Carneiro (Oct 16 2018 at 06:50):

I think simp should work

view this post on Zulip Mario Carneiro (Oct 16 2018 at 06:51):

because it will turn the goal into true \/ ... and then true

view this post on Zulip Johan Commelin (Oct 16 2018 at 06:51):

Well, it doesn't. Because tidy would try that.

view this post on Zulip Mario Carneiro (Oct 16 2018 at 06:51):

did you see if simp * at * works by hand?

view this post on Zulip Mario Carneiro (Oct 16 2018 at 06:51):

what about simp *?

view this post on Zulip Johan Commelin (Oct 16 2018 at 06:53):

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 06:55):

or a bug in simp * at *

view this post on Zulip Mario Carneiro (Oct 16 2018 at 06:56):

wait, which is "that"

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 06:58):

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 06:58):

obviously is tidy + rewrite_search

view this post on Zulip Mario Carneiro (Oct 16 2018 at 06:58):

which is that graph thing that Keeley Hoek did

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

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

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

view this post on Zulip Johan Commelin (Oct 16 2018 at 07:05):

Currently it doesn't like the symbol.

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:07):

use the sup symbol

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:08):

most of the union/inter notation is specific to set

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:08):

the generic version is Sup and Inf

view this post on Zulip Johan Commelin (Oct 16 2018 at 07:08):

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:08):

yes

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:09):

∃ Us ⊆ set B,

what should this mean?

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:09):

a complete lattice, not a lattice

view this post on Zulip Johan Commelin (Oct 16 2018 at 07:09):

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:09):

lattice just gives you binary sup

view this post on Zulip Johan Commelin (Oct 16 2018 at 07:09):

Ok, so I should prove that open_set is a complete lattice.

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:10):

yes

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:10):

again, galois insertion should make it easy

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

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

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

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 07:22):

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

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:23):

interior, certainly

view this post on Zulip Johan Commelin (Oct 16 2018 at 07:23):

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

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:25):

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

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:39):

try to prove galois insertion?

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

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:50):

the insertion is important

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:50):

it is basically making an order embedding

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:50):

and you pull the relation back along that

view this post on Zulip Johan Commelin (Oct 16 2018 at 07:50):

You mean coinsertion?

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:51):

that too

view this post on Zulip Johan Commelin (Oct 16 2018 at 07:51):

Hmmm, I will try to dualize all the stuff about insertions.

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:51):

or vice versa

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:51):

you know, just put co everywhere

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:53):

I was just about to suggest that

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 07:53):

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:53):

but filter is dualized on only one side

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:54):

I guess a coinsertion is dualized on both sides

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 07:54):

is it enough to add order_dual on both sides?

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:55):

plus galois_coinsertion should extend galois_connection with no duals

view this post on Zulip Mario Carneiro (Oct 16 2018 at 07:56):

do we know that galois_connection is self-dual?

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 07:56):

to its symmetric form:

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

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 07:56):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 08:01):

then it should just be called galois_nnection

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 08:02):

it's shorter

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

view this post on Zulip Johan Commelin (Oct 16 2018 at 08:04):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 08:04):

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

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

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

view this post on Zulip Johan Commelin (Oct 16 2018 at 11:38):

@Johannes Hölzl Those order_duals 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

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 11:45):

looks good to me. Is there something wrong?

view this post on Zulip Johan Commelin (Oct 16 2018 at 11:52):

Yes, I'm getting the dual order.

view this post on Zulip Johan Commelin (Oct 16 2018 at 11:53):

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

view this post on Zulip Johan Commelin (Oct 16 2018 at 11:58):

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

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 12:01):

hm, rw [h] {occs := occurrences.pos [1]} is the only thing I know

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

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

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 12:04):

order_dual.lattice.complete_lattice does what you want

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 12:04):

and it doesn't have the rw problem

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

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

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 12:09):

can you put your theory on a gist?

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

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

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 12:27):

is this what you want?

view this post on Zulip Johan Commelin (Oct 16 2018 at 12:27):

I think it is. Let me try.

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

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 12:30):

only if you setup choice correctly

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 12:31):

and this is also with insertion a rfl

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

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

view this post on Zulip Johan Commelin (Oct 16 2018 at 12:35):

Huuh, but s isn't open.

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

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 12:36):

it says: interior s = s

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 12:37):

then you also need to adapt your choice_eq proof accordingly

view this post on Zulip Johan Commelin (Oct 16 2018 at 12:38):

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

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

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 12:59):

you should get:

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

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

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 13:05):

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

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

view this post on Zulip Johannes Hölzl (Oct 16 2018 at 13:16):

how does your gi look like?

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

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

view this post on Zulip Reid Barton (Oct 16 2018 at 13:36):

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

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

view this post on Zulip 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 = sUs, open_set.s s :=
rfl

this works

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

view this post on Zulip Johan Commelin (Oct 16 2018 at 13:48):

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

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

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