extend presheaf from basis

Stream: maths

[Johan Commelin]

@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]

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

[Scott Morrison]

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

[Kevin Buzzard]

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]

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]

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

[Scott Morrison]

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

[Johan Commelin]

But it is looking for some Type w. I really don't know where it is getting that from?

[Johan Commelin]

Do you have comma categories somewhere?

[Kevin Buzzard]

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]

I just want the category of opens contained in U.

[Johan Commelin]

Maybe you already have this somewhere...

[Johan Commelin]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

(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]

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

[Scott Morrison]

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

[Johan Commelin]

Hmmm, let me take another look.
@Scott Morrison All the code I have is what I posted above.

[Johan Commelin]

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

[Johan Commelin]

@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]

Thanks, I added over.forget.

[Johan Commelin]

@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]

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

[Johan Commelin]

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]

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

[Scott Morrison]

no problem

[Scott Morrison]

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

[Johan Commelin]

No, presheaves aren't in mathlib

[Johan Commelin]

Or did you break the definition of open_set?

[Scott Morrison]

Yes :-)

[Johan Commelin]

Aaah, ok. Hmmz.

[Johan Commelin]

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

[Scott Morrison]

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]

The tactic obviously doesn't even appear.

[Johan Commelin]

@Scott Morrison I'm stuck on

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

After that we have extended presheaves.

[Johan Commelin]

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

[Scott Morrison]

try intro, then cases?

[Johan Commelin]

Aah cases.

[Scott Morrison]

or commit something I can poke at

[Scott Morrison]

remember that hom there is probably some ulift plift gadget

[Scott Morrison]

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

[Johan Commelin]

Right, it's working now. Except that it couldn't figure out comp' on its own :sad:

[Johan Commelin]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

@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]

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]

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]

I still don't like the rw show, but I don't know how to get rid of it.

[Patrick Massot]

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]

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

[Johan Commelin]

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]

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

[Patrick Massot]

Lots of proofs are provided in the background

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

@Reid Barton Do you know if the inclusion of a basis B into open_set X is some sort of geometric morphism?

[Johan Commelin]

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

[Reid Barton]

I've never learned these topos theory words

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

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

[Reid Barton]

Which?

[Johan Commelin]

Kan extensions

[Reid Barton]

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

[Johan Commelin]

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]

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

[Johan Commelin]

The latter is good enough

[Reid Barton]

I see. We may want adjunctions, too.

[Johan Commelin]

We do

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

I guess we can define them without that though

[Reid Barton]

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

[Johan Commelin]

Good luck!

[Patrick Massot]

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

What about formalizing what you told us about reflective subcategory?

[Johan Commelin]

@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]

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

[Patrick Massot]

Perfectoid spaces vote for reflexive subcategories first

[Kevin Buzzard]

Aah cases.

You needed that for that option question yesterday too. It works for any inductive type.

[Scott Morrison]

Hmm, your profiling output is not very helpful, because everything is hidden behind the to_expr that exact is calling.

[Scott Morrison]

Is it possible to make another lemma for the exact?

[Scott Morrison]

(Also, this is fabulous.)

[Kevin Buzzard]

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]

@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]

@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]

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

[Reid Barton]

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

[Reid Barton]

I guess convert might be slightly better?

[Reid Barton]

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

[Reid Barton]

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

[Johan Commelin]

@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]

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

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

[Johan Commelin]

In some sense it was really brittle.

[Reid Barton]

Odd

[Johan Commelin]

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]

Of course you need Scott's libs

[Reid Barton]

@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]

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]

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]

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]

Ok, now it worked for me as well.

[Johan Commelin]

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]

I don't understand what you are trying to do

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

I would define open_set.is_basis using the image formulation, and then prove that version as a theorem

[Johan Commelin]

Ok, thanks.

[Mario Carneiro]

also that's not the right condition

[Mario Carneiro]

the exists is satisfied by U

[Johan Commelin]

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

[Mario Carneiro]

oh... but what about intersections?

[Johan Commelin]

What's with them?

[Mario Carneiro]

a basis should be closed under intersection (ish)

[Johan Commelin]

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

[Mario Carneiro]

This just says B covers the space

[Johan Commelin]

It says that B covers every open.

[Mario Carneiro]

oh, actually I think you have the intersection property then

[Mario Carneiro]

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]

That looks good, right?

[Mario Carneiro]

yeah

[Mario Carneiro]

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

[Johan Commelin]

@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]

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

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

[Kenny Lau]

try it wthout 0?

[Johan Commelin]

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

[Johan Commelin]

@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]

you need : not \in

[Kenny Lau]

and it’s called bUnion

[Johan Commelin]

Right, so for this we need a lattice structure on open_set. Which we will need at some point anyway.

[Johan Commelin]

@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]

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]

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

[Reid Barton]

Do we have an emoji for galois insertion

[Johan Commelin]

Thanks, I'll try that tomorrow.

[Kevin Buzzard]

Do we have an emoji for galois insertion

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

[Johan Commelin]

@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]

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]

Ooh wait! Does this mean that I have to mark or.inl with [back!] or something like that?

[Kevin Buzzard]

Does @[simp] instance : has_union (open_set X) do the same as attribute [simp] open_set.has_union.equations._eqn_1?

[Mario Carneiro]

or.inl is not a good back! lemma

[Johan Commelin]

Hmmm, why not?

[Mario Carneiro]

because it will try to prove everything by the left disjunct

[Johan Commelin]

Only if the assumptions are satisfied, right?

[Mario Carneiro]

not with the !

[Mario Carneiro]

I think simp should work

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

what about simp *?

[Johan Commelin]

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

[Mario Carneiro]

or a bug in simp * at *

[Mario Carneiro]

wait, which is "that"

[Kevin Buzzard]

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]

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

[Mario Carneiro]

obviously is tidy + rewrite_search

[Mario Carneiro]

which is that graph thing that Keeley Hoek did

[Johan Commelin]

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]

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

[Johan Commelin]

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]

Currently it doesn't like the ⋃ symbol.

[Mario Carneiro]

use the sup symbol

[Kevin Buzzard]

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]

most of the union/inter notation is specific to set

[Mario Carneiro]

the generic version is Sup and Inf

[Johan Commelin]

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

[Mario Carneiro]

yes

[Johan Commelin]

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]

∃ Us ⊆ set B,

what should this mean?

[Mario Carneiro]

a complete lattice, not a lattice

[Johan Commelin]

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

[Mario Carneiro]

lattice just gives you binary sup

[Johan Commelin]

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

[Mario Carneiro]

yes

[Mario Carneiro]

again, galois insertion should make it easy

[Johan Commelin]

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]

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]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

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]

interior, certainly

[Johan Commelin]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

Ok, so l = interior and u = open_set.s. Is this good or bad news for our complete_lattice?

[Mario Carneiro]

try to prove galois insertion?

[Johan Commelin]

Oops, I switched l and u. I still find those names confusing... Ok, so it is going to be a coinsertion.

[Johan Commelin]

@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]

the insertion is important

[Mario Carneiro]

it is basically making an order embedding

[Mario Carneiro]

and you pull the relation back along that

[Johan Commelin]

You mean coinsertion?

[Mario Carneiro]

that too

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

or vice versa

[Mario Carneiro]

you know, just put co everywhere

[Johannes Hölzl]

look into how it is done for filter. Here I use dual_order to get the other way round

[Mario Carneiro]

I was just about to suggest that

[Johannes Hölzl]

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

[Mario Carneiro]

but filter is dualized on only one side

[Mario Carneiro]

I guess a coinsertion is dualized on both sides

[Johannes Hölzl]

is it enough to add order_dual on both sides?

[Mario Carneiro]

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

[Mario Carneiro]

plus galois_coinsertion should extend galois_connection with no duals

[Mario Carneiro]

do we know that galois_connection is self-dual?

[Johannes Hölzl]

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]

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

[Kevin Buzzard]

then it should just be called galois_nnection

[Kevin Buzzard]

it's shorter

[Johan Commelin]

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]

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

[Kevin Buzzard]

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

[Johannes Hölzl]

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]

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]

@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

[Johannes Hölzl]

looks good to me. Is there something wrong?

[Johan Commelin]

Yes, I'm getting the dual order.

[Johan Commelin]

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

[Johan Commelin]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

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]

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]

order_dual.lattice.complete_lattice does what you want

[Johannes Hölzl]

and it doesn't have the rw problem

[Johan Commelin]

@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]

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]

can you put your theory on a gist?

[Johan Commelin]

@Johannes Hölzl Voila: https://gist.github.com/jcommelin/c9d04b7770f89a0fadc11aae5ca90d87
This is what I have so far.

[Johannes Hölzl]

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]

is this what you want?

[Johan Commelin]

I think it is. Let me try.

[Johan Commelin]

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]

only if you setup choice correctly

[Johannes Hölzl]

and this is also with insertion a rfl

[Johannes Hölzl]

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]

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]

Huuh, but s isn't open.

[Johannes Hölzl]

yes it is, the _ is actually a proof from which you can show that it is open

[Johannes Hölzl]

it says: interior s = s

[Johannes Hölzl]

then you also need to adapt your choice_eq proof accordingly

[Johan Commelin]

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

[Johan Commelin]

@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]

you should get:

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

[Johan Commelin]

@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]

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

[Johan Commelin]

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]

how does your gi look like?

[Johan Commelin]

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]

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]

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

[Johan Commelin]

@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]

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]

(order_dual (set _)) is already enough. Then the elaborator finds the right instance, instead of the instance for X -> Prop

[Johan Commelin]

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

[Alex J. Best]

@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]

then it should just be called galois_nnection

or a cogalois-nnection (sorry)