dependent argument hell

Stream: general

[Scott Morrison]

I seem to have backed myself into a corner, and I don't understand how to escape. I would really appreciate some help, as it feels like this problem is an instance of one that will become more and more severe as we do more advanced maths.

[Scott Morrison]

I've been working on morphisms of presheaves.

[Scott Morrison]

These are "bundled" presheaves, so they consist of a topological space, along with a functor from the category of open sets (morphisms are subsets) to some other category.

[Scott Morrison]

A morphism of presheaves (X, O_X) \hom (Y, O_Y) consists of a pair: a function f : X \hom Y, which is just a continuous map, and

[Scott Morrison]

a "comorphism", which is a natural transformation from O_Y \to f_* O_X.

[Scott Morrison]

The point here is that you can push forward a presheaf on X to presheaf on Y, along a continuous map (take an open set of Y, pull it back via f, then evaluate the presheaf on it).

[Scott Morrison]

Now, I want to define the identity presheaf morphism, and I want to define compositions of presheaf morphisms, and check they satisfy the right properties.

[Scott Morrison]

Yesterday I managed to do this, but both the constructions and the proofs were very ugly.

[Scott Morrison]

Today I've made another attempt, where the constructions are quite a bit better, and the proofs look like they should be easy but get stuck at the last hurdle, when we should just be cancelling off identity morphisms and saying we're done.

[Scott Morrison]

The code is at <https://github.com/semorrison/lean-category-theory/blob/master/src/category_theory/V_pre.lean>.

[Scott Morrison]

The particular problem I reach is the proof of comp_id' in constructing instance : category (Presheaf.{u v} C) := ....

[Scott Morrison]

Just before the sorry, the goal is

C : Type u,
𝒞 : category C,
X Y : Presheaf C,
f : Presheaf_hom X Y,
X_1 : open_set ((Y.X).α)
⊢ functor.map (Y.𝒪) (𝟙 X_1) ≫
      ⇑(f.c) (⇑(map_open_set (𝟙 (Y.X))) X_1) ≫
        functor.map (X.𝒪) (functor.map (map_open_set (f.f)) (𝟙 (⇑(map_open_set (𝟙 (Y.X))) X_1))) =
    ⇑(f.c) X_1

[Scott Morrison]

And this should be perfectly manageable. The left hand side is a composition of three morphisms, and we should begin by observing the first and third are actually identity morphisms, since they are explicitly some functor applied to some identity morphism.

[Scott Morrison]

In particular we should be able to rewrite functor.map (Y.𝒪) (𝟙 X_1) into 𝟙 (Y.𝒪 X_1)

[Scott Morrison]

However simp fails.

[Reid Barton]

Yeah I've had this happen too. In that case the problem was some implicit argument was not X_1 but only something defeq to it, and simp didn't like that.

[Reid Barton]

In my case dsimp, simp worked, but it doesn't look like that will help you judging from the two preceding lines

[Scott Morrison]

Trying the rewrite by hand, with increasing desperation:

rw [category_theory.functor.map_id]
rw [category_theory.functor.map_id Y.𝒪 X_1]

[Scott Morrison]

rw [category_theory.functor.map_id Y.𝒪 X_1] {md:=semireducible}

[Scott Morrison]

all fail.

[Reid Barton]

erw?

[Scott Morrison]

erw is just the same as {md:=semireducible}

[Scott Morrison]

(I'd usually use erw but didn't want to scare anyone. :-)

[Scott Morrison]

Reid is exactly right that the problem is an implicit argument.

[Scott Morrison]

Let's look at that, turning on set_option pp.implict true and inspecting the goal again.

[Scott Morrison]

The whole thing is a bit long, but the bit that corresponds to functor.map (Y.𝒪) (𝟙 X_1) is

@functor.map
        (@open_set (@bundled.α topological_space (@Presheaf.X C 𝒞 Y))
           (examples.topological_space (@Presheaf.X C 𝒞 Y)))
        (@open_set.open_sets (@bundled.α topological_space (@Presheaf.X C 𝒞 Y))
           (examples.topological_space (@Presheaf.X C 𝒞 Y)))
        C
        𝒞
        (@Presheaf.𝒪 C 𝒞 Y)
        X_1
        (⇑(@map_open_set (@Presheaf.X C 𝒞 Y) (@Presheaf.X C 𝒞 Y) (𝟙 (@Presheaf.X C 𝒞 Y))) X_1)
        (𝟙 X_1)

[Scott Morrison]

We can see the problem at the end there: the last three arguments are meant to consist of two objects, and a hom between them.

[Scott Morrison]

However we've got X_1, (⇑(@map_open_set (@Presheaf.X C 𝒞 Y) (@Presheaf.X C 𝒞 Y) (𝟙 (@Presheaf.X C 𝒞 Y))) X_1), and (𝟙 X_1).

[Reid Barton]

Something like id ⁻¹' X_1, I guess?

[Scott Morrison]

We really want that second object to just be X_1 again.

[Reid Barton]

is what that long thing is

[Scott Morrison]

If we dsimp [map_open_set] we see:

[Scott Morrison]

(@open_set.mk (@bundled.α topological_space (@Presheaf.X C 𝒞 Y)) (examples.topological_space (@Presheaf.X C 𝒞 Y)) (@subtype.val (@bundled.α topological_space (@Presheaf.X C 𝒞 Y) → @bundled.α topological_space (@Presheaf.X C 𝒞 Y)) (@continuous (@bundled.α topological_space (@Presheaf.X C 𝒞 Y)) (@bundled.α topological_space (@Presheaf.X C 𝒞 Y)) (@bundled.str topological_space (@Presheaf.X C 𝒞 Y)) (@bundled.str topological_space (@Presheaf.X C 𝒞 Y))) (𝟙 (@Presheaf.X C 𝒞 Y)) ⁻¹' @open_set.s (@bundled.α topological_space (@Presheaf.X C 𝒞 Y)) (examples.topological_space (@Presheaf.X C 𝒞 Y)) X_1) _)

[Scott Morrison]

Which sadly is not definitely equal to X_1, although we can prove it is equal.

[Reid Barton]

oh no

[Scott Morrison]

In fact, we have a lemma prepared just for this!

[Reid Barton]

wait then

[Scott Morrison]

@[simp] def map_open_set_id_obj (X : Top) (U : open_set X.α) : map_open_set (𝟙 X) U = U :=
begin dsimp [map_open_set], cases U, congr, end

[Scott Morrison]

And rw [map_open_set_id_obj] says ...

[Scott Morrison]

failed

[Reid Barton]

I'm confused

[Reid Barton]

Doesn't this mean your goal is ill-typed?

[Scott Morrison]

(And erw is no better, nor does it seem that using conv to zoom in on it helps.)

[Scott Morrison]

That's what appears to be happening, I agree.

[Scott Morrison]

So how did Lean let me get this far?

[Reid Barton]

I had that happen too once, but I didn't understand how it happened, but it's almost certainly unrelated.

[Scott Morrison]

I do have a note a few lines earlier in my code It's hard to believe this typechecks!

[Scott Morrison]

structure Presheaf_hom (F G : Presheaf.{u v} C) :=
(f : F.X ⟶ G.X)
(c : G.𝒪 ⟹ ((map_open_set f) ⋙ F.𝒪))

namespace Presheaf_hom
def id (F : Presheaf.{u v} C) : Presheaf_hom F F :=
{ f := 𝟙 F.X,
  c := begin apply nat_trans.vcomp, swap, apply whisker_on_right (map_open_set_id _).inv, apply (functor.id_comp _ _ _).inv end
}

def comp {F G H : Presheaf.{u v} C} (α : Presheaf_hom F G) (β : Presheaf_hom G H) : Presheaf_hom F H :=
{ f := α.f ≫ β.f,
  c := β.c ⊟ (whisker_on_left (map_open_set β.f) α.c), -- It's hard to believe this typechecks!
}
end Presheaf_hom

[Scott Morrison]

In particular, I have to jump through some hoops to construct the natural transformation for id.

[Scott Morrison]

But Lean appears to be happy with me just writing the "obvious" answer for comp.

[Reid Barton]

I found composition/associativity things are often easier than identity/unitality things

[Scott Morrison]

(... in real life as well as Lean, for me!)

[Scott Morrison]

(identities are strange and confusing in higher dimensions!)

[Reid Barton]

how hard would it be to find the first place the goal becomes ill-typed?
Is the goal before the last simp comprehensible?

[Scott Morrison]

The only avenues I can work out are:
1) Go back and work out where this "ill-typed, or at least hard-to-see-its-well-typed" expression first appears, and then "do something different".
2) Work out how to "fix" implicit arguments.

[Scott Morrison]

(This is an example, by the way, of a situation it would be nice to have a good term inspector, where you can toggle on and off implicit arguments for subtrees.)

[Reid Barton]

Given that the implicit argument is not even defeq to the right thing, I think 2 isn't applicable in this case.
It looks to me like you hit a bug in Lean (which is probably not in the kernel, since it is only the goal which is ill-typed, but still very frustrating).

[Scott Morrison]

Oooh, I maybe found a way around it.

[Scott Morrison]

It's just a matter of dsimping expressions in a different order, so somehow it's not at all a principled solution.

[Scott Morrison]

Oh, no, the problem is there a step or two later. I was just doing something by hand that simp was doing anyway.

[Scott Morrison]

:-(

[Reid Barton]

I'm kind of surprised that the result of the tactic passes typechecking, even with sorry there

[Scott Morrison]

Shall I try for a proof of false? :-)

[Reid Barton]

Unfortunately I doubt you can prove false from a term which is ill-typed but only in that one of the type arguments is definitionally wrong (but propositionally correct)

[Scott Morrison]

Okay... this is bizarre, but cases X_1 seems to break the impasse.

[Reid Barton]

that's not surprising

[Scott Morrison]

Why is that?

[Reid Barton]

same reason why you used cases U to prove map_open_set_id_obj

[Reid Barton]

basically you have an equality that looks like <x.1, _> = x

[Scott Morrison]

Okay, and there's a (horrible) proof:

  comp_id' := λ X Y f, --sorry,
    begin
      ext,
      -- we check the functions first
      dsimp [Presheaf_hom.id, Presheaf_hom.comp],
      simp,
      -- and now the comorphisms
      dsimp [Presheaf_hom.id, Presheaf_hom.comp],
      simp,
      ext,
      dsimp [whisker_on_right, whiskering_on_right, whisker_on_left, whiskering_on_left],
      dsimp [map_open_set],
      simp,
      erw [category_theory.functor.map_id],
      simp,
      cases X_1,
      simp,
      apply congr_fun,
      simp,
    end,

[Reid Barton]

where x is a variable, and so they can never be definitionally equal. Buf after cases x, it's okay

[Scott Morrison]

I see.

[Reid Barton]

when you do comp, both sides look like <_, _>

[Reid Barton]

and that's why comp is easier

[Reid Barton]

This still feels weird to me, but I've seen it a few times

[Scott Morrison]

So maybe the summary from today is:

avoid cases when constructing stuff, because then you'll have horrible X.rec expressions to deal with later, but
remember to try cases when an implicit argument looks wrong!

[Reid Barton]

Well, in general when you need to prove (blah.mk _ _) = X, it will require doing cases on X

[Reid Barton]

I still think something very fishy is going on with your original code

[Scott Morrison]

Sure. The problem here was that it wasn't at all obvious to me that this was what was going on.

[Mario Carneiro]

The file you linked references category_theory.examples.topological_spaces but I can't find it in the repo

[Scott Morrison]

That's in mathlib

[Scott Morrison]

:-)

[Reid Barton]

I just finished building your repo locally so I can take a look

[Scott Morrison]

And just to confound you, Mario, lean-category-theory is currently pointing at a branch of mathlib on community, in which that file has been modified. :-)

[Reid Barton]

Anyways the situation you were in ought to have been impossible. If x : t and x : t' then t and t' should be definitionally equal. Not just propositionally equal.

[Reid Barton]

At least, as far as I understand.

[Scott Morrison]

yes.

[Mario Carneiro]

oh wow, mathlib category theory has grown quite a bit since I last checked

[Mario Carneiro]

-- Do I dare define `open_set` as a functor from Top to CAT? I don't like CAT.

def map_open_set
  {X Y : Top} (f : X ⟶ Y) : open_set Y.α ⥤ open_set X.α :=

Why is it a functor to CAT? It looks like open_set should be a (contravariant) functor from Top to Type

[Scott Morrison]

For each topological space X, we get the category of open sets and inclusions.

[Reid Barton]

The ill-typed goal I encountered involved Lean getting confused about the difference between quot and quotient, and so I had a goal involving some types of the form quot s a where s was a setoid, which I had trouble producing

[Mario Carneiro]

Okay, I think I'm starting to piece this together. There is an unnamed function comap f U (where f is a bundled continuous function and U is an open_set) which is the object part of map_open_set

[Mario Carneiro]

And what is true is that map_open_set (𝟙 X) U = comap (𝟙 X) U, which is isomorphic to U

[Mario Carneiro]

so you have a classic two-category problem

[Scott Morrison]

I don't know this classic. :-)

[Reid Barton]

I think Mario means 2-category?

[Mario Carneiro]

You have to worry about coherences since it's not an equality

[Scott Morrison]

Oh, okay! :-)

[Scott Morrison]

Yes.

[Reid Barton]

Like, the Top -> Cat thing could be only a pseudofunctor

[Mario Carneiro]

As Kevin learned a while ago, a propositional equality should not ever be treated as equality in a category, only isomorphism

[Mario Carneiro]

objects are either defeq or isomorphic

[Scott Morrison]

but where am I abusing that here?

[Mario Carneiro]

-- These next two are desperate attempts to solve problems below.
@[simp] def map_open_set_id_obj (X : Top) (U : open_set X.α) : map_open_set (𝟙 X) U = U :=
begin dsimp [map_open_set], cases U, congr, end
@[simp] def map_open_set_id (X : Top) : map_open_set (𝟙 X) ≅ functor.id (open_set X.α) :=

this is bad news

[Mario Carneiro]

this equality should be turned into an iso, given a name, and explicitly reasoned with

[Scott Morrison]

It's the first one that is evil

[Scott Morrison]

and I don't use it

[Scott Morrison]

the second one is fine, isn't it?

[Reid Barton]

the type looks fine, but now I am confused about the implementation

[Mario Carneiro]

I think? I can't parse it

[Scott Morrison]

I just pushed an update

[Mario Carneiro]

map_open_set (𝟙 X) is a functor, so what does ≅ mean here?

[Scott Morrison]

that has the working proof, and doesn't have the evil map_open_set_id_obj

[Scott Morrison]

iso is automatically natural isomorphism

[Scott Morrison]

sweet sweet typeclass magic finds the category of functors between two fixed categories

[Reid Barton]

isomorphism in the functor category

[Scott Morrison]

and correctly interprets iso

[Mario Carneiro]

and that doesn't have any 2-category mess in it?

[Scott Morrison]

no -- for a fixed pair of categories C and D

[Scott Morrison]

functors and natural transformations between them are a perfectly honest 1-category

[Scott Morrison]

(indeed, the prototypical example)

[Reid Barton]

Oh man this is confusing.

[Mario Carneiro]

so where did you get that bad application from? functor.map (Y.𝒪) (𝟙 X_1)

[Reid Barton]

I noticed that both of these worked, and was confused.

  { app := λ U, show map_open_set (𝟙 X) U ⟶ U, from 𝟙 U },
  { app := λ U, show U ⟶ U, from 𝟙 U },

[Reid Barton]

Even though we know map_open_set (𝟙 X) U = U is not a definitional equality

[Mario Carneiro]

hah, it's because the hom destructs it

[Reid Barton]

right

[Scott Morrison]

Yeah, and I think this is where the "bad" application is coming from.

[Scott Morrison]

Can you explain what "the hom destructs it" means?

[Reid Barton]

instance : has_subset (open_set α) :=
{ subset := λ U V, U.s ⊆ V.s }

[Reid Barton]

this is what defines the partial order, and therefore the hom types

[Scott Morrison]

oh ...

[Reid Barton]

it's not true that map_open_set (𝟙 X) U = U definitionally, but it is true that (map_open_set (𝟙 X) U).s = U.s because (contrary to my initial guess) preimage id is definitionally the identity

[Scott Morrison]

I see.

[Reid Barton]

Oh, wait...

[Reid Barton]

So maybe that weird goal was correctly typed, after all

[Scott Morrison]

Yeah.

[Scott Morrison]

And I could have replaced my evil lemma with

[Scott Morrison]

@[simp] def map_open_set_id_obj (X : Top) (U : open_set X.α) : (map_open_set (𝟙 X) U).s = U.s := rfl

[Scott Morrison]

and perhaps had it work...

[Scott Morrison]

Hmm,. you can indeed prove that via rfl, but I can't get it to help.

[Scott Morrison]

ah, I have to remove the dsimp [map_open_set], perhaps

[Mario Carneiro]

Scott, I'm trying to get your repo. How do you update everything with leanpkg?

[Scott Morrison]

leanpkg build?

[Scott Morrison]

It should notice if you don't have the right dependencies already in _target.

[Mario Carneiro]

I get version mismatch error

[Scott Morrison]

ah... Is your lean provided by elan?

[Scott Morrison]

This repo is set to use nightly-2018-06-21

[Scott Morrison]

but I think it should be safe to change that in leanpkg.toml file

[Scott Morrison]

What is the "official recommendation" these days?

[Mario Carneiro]

I've been using 3.4.1 even though a few bugfixes have come in

[Scott Morrison]

Since my student Keeley started forking Lean I've switched to using elan and don't notice these problems. :-)

[Mario Carneiro]

that's good to hear. You should write a tutorial :)

[Reid Barton]

for elan?

[Scott Morrison]

I really should borrow a windows machine, and write a tutorial for running elan on windows.

[Scott Morrison]

Ducking out for lunch. Thanks very much for the discussion today!

[Mario Carneiro]

Aha, I found some 2-categoricity:

structure Presheaf_hom (F G : Presheaf.{u v} C) :=
(f : F.X ⟶ G.X)
(c : G.𝒪 ⟹ ((map_open_set f) ⋙ F.𝒪))

Since Presheaf_hom has a component which is a functor, proving equality of homs is going to involve equality of objects

[Mario Carneiro]

I guess that can't really be avoided, but since G.𝒪 is a functor out of a skeletal category (a partial order category), it suffices to prove isomorphism instead of equality

[Mario Carneiro]

@[extensionality] lemma ext {F G : Presheaf.{u v} C} (α β : Presheaf_hom F G)
  (w : α.f = β.f) (h : α.c == β.c)
  : α = β :=

the heq here is evil. You should state some kind of composite equality here

[Scott Morrison]

Hi @Mario Carneiro, actually that component Preasheaf_hom.c is a natural transformation, not a functor, so equality is non-evil.

[Scott Morrison]

I agree that the ext lemma is evil. I will replace that.

[Mario Carneiro]

equality of natural transformations is not evil, equality of natural transformations in different categories is

[Scott Morrison]

Oh, so you're saying specifically the heq is evil.

[Scott Morrison]

I don't think we'll ever to to say anything about equalities of objects, however.

[Mario Carneiro]

I think I found the culprit. map_open_sets is a 2-categorical thing, since it takes homs to functors. This means that congruence says that equality of homs maps to natural iso of functors

[Mario Carneiro]

And this is the iso you should reference in the definition of ext

[Scott Morrison]

I'm filling in

def map_open_set_iso {X Y : Top} (f g : X ⟶ Y) (h : f = g) : map_open_set f ≅ map_open_set g := {

}

[Scott Morrison]

right now

[Kevin Buzzard]

This is a terrifying thread to wake up to. It reminds me of when I couldn't prove anything about real numbers because there was no norm_num. But instead of a beginner struggling to prove math-trivial things because of a lack of tools, it's experts and tool-makers having problems with something that looks math-trivial

[Kevin Buzzard]

I actually stopped thinking about pushing the perfectoid repo forward towards the definition of an adic space because this funky category showed up, Patrick was doing completions (which were also needed) and I knew someone had to do integral closures (which were also needed) so I went back to those and thought I'd wait a bit to see what the category experts thought about this category V_pre which had shown up "in the wild". I want to argue that we don't need V_pre, it's just a convenient container and I thought it would be a good test case. I could instead just make a new structure modelling the objects and muddle on from there and it would no doubt be fine at least as far as the ultimate goal is concerned, which is a definition.

[Mario Carneiro]

I think this thread is Scott having an epiphany similar to the one that prompted that blog post https://mathematicswithoutapologies.wordpress.com/2018/09/11/guest-post-by-kevin-buzzard/

[Mario Carneiro]

I think it boils down to "equalities of types are evil"

[Kevin Buzzard]

As I'm sure you realise, that comment (it was only supposed to be a comment!) was very much informed by the comments you made when I was having that big meltdown about equality a few months ago ("Kevin, stop trolling!").

[Kevin Buzzard]

A summer student, Ned Summers, was doing some 4th year category theory example sheet questions (using Scott's library as a dependency) and ran into these sorts of problems, and this time I was better equipped. Chris (who freely admits he knows nothing about category theory) had suggested some casts which had caused trouble for Ned, and I diagnosed the problem as exactly the same sort of thing: Ned had two objects X and Y and a proof that they were equal, and was doing exactly what a mathematican would do -- treating Hom(X,Z) as equal to Hom(Y,Z) etc etc. Equality in type theory is more delicate than that. Of course this doesn't change the fact that we are right, and your definition is rubbish -- but it's what we've got to work with ;-)

[Kenny Lau]

A summer student, Ned Summers

[Kevin Buzzard]

They've almost all gone now. Ned stopped on Friday. Only about three left. I am going to spend all day writing documentation and basic questions. Yesterday I said "we want ten basic examples and ten basic questions about metaprogramming" -- today I'm (hopefully) going to write ten basic examples and ten basic questions about set membership.

[Kevin Buzzard]

I asked a question on this chat probably last Wed or Thurs about how to generate "the identity morphism" between two objects which were provably equal, and Reid answered very quickly with some function called something like iso_of_eq which generated the data from the proof; it was because of my schemes meltdown that I had understood that this was what was missing.

[Chris Hughes]

I didn't suggest the use of eq.rec. My instinct would be that eq.rec for data should be avoided if at all possible

[Kevin Buzzard]

Maybe I got the wrong impression from Ned :-)

[Scott Morrison]

Thanks to some help from Mario and Reid, it is well sorted out now!

[Scott Morrison]

While I agree that I was making mistakes (being "evil") when I shouldn't have been, and the code is nicer as a result of today's exorcism, the fundamental cause of being stuck was something a bit different. I really need to catch up on sleep now, so I won't explain it now. :-)

[Scott Morrison]

The upshot is that <https://github.com/semorrison/lean-category-theory/blob/master/src/category_theory/presheaves.lean> contains the definition of bundled presheaves (i.e. a topological space and a presheaf on it), and the right notion of morphisms between these, and indeed the category structure.

[Scott Morrison]

It's certainly not all of V_pre, but it's the categorical theoretic core.

[Patrick Massot]

Yeah, "Lean does no magic" ™ but sometimes a good exorcism session is needed

[Scott Morrison]

Hopefully from this point on it is just adding bells and whistles (that stalk needs to be local, these valuations need to be jiggered by the whatsit).

[Scott Morrison]

Happily, the category of presheaves is actually pretty easy to PR now. I only have one dependency, about whiskering, and that looks easy to clean up. So this may be in mathlib soon.

[Kenny Lau]

to reduce an eq.rec you need the major premise to become refl somehow

that usually means finding the appropriate equality in the context and generalizing it until one side is a variable, and then subst, which is to say use eq.rec in the proof term

Mario Carneiro, 16/04/2018 04:39:04 (UTC)

[Kenny Lau]

underrated comment

[Kenny Lau]

wow I had an eq.rec in my goal and it took me nearly 2 hours to destruct it

[Reid Barton]

sounds about right

[Scott Morrison]

I feel like eq.rec is such a disaster that we need special VS Code plugin support: a little zulip box that pops up, with a message: "Help me, Mario!" ready to be sent...

[Kenny Lau]

ok so eq.rec isn't really the problem. The problem is sometimes you can't just rewrite something with an equality a = b because that something depends on a and b being those expressions. And the solution is to generalize a in all places in which that expression occurs, and then subst that equality

[Kenny Lau]

sometimes you can't just generalize a, but you have to generalize a lot of things

[Kenny Lau]

a strategy is to generalize all proofs first (set_option pp.proofs true), because that will always work because of proof irrelevance

[Scott Morrison]

Slowly making progress here. This now compiles:

def stalks_local (F : Presheaf.{u+1 u} TopRing) : Type u :=
Π x : F, local_ring (((TopRing.forget_to_CommRing).map_presheaf F).stalk_at x)

def V_pre_pre := Σ (F : Presheaf.{u+1 u} TopRing), stalks_local F

example : category.{u+1 u} V_pre_pre := by unfold V_pre_pre; apply_instance