Zulip Chat Archive

Stream: maths

Topic: functor ext lemma?


view this post on Zulip Kevin Buzzard (Dec 22 2019 at 12:16):

Is this just what I'm stuck with in dependent type theory? I want to prove two functors are equal.

import category_theory.functor
import topology.opens

/-
structure functor (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D] :
  Type (max v₁ v₂ u₁ u₂) :=
(obj       : C → D)
(map       : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y)))
(map_id'   : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
(map_comp' : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) . obviously)

infixr ` ⥤ `:26 := functor       -- type as \func --
-/

variables {X : Type*} [topological_space X]

open topological_space

def res_functor {Y₁ Y₂ : set X} (hY : Y₂  Y₁) :
    {V : opens X // Y₁  V}  {V : opens X // Y₂  V} :=
{ obj := λ V, V.1, set.subset.trans hY V.2,
  map := λ _ _, id}

-- is this supposed to be a such a kerfuffle
example (Y : set X) : res_functor (set.subset.refl Y) = 𝟭 _ :=
begin
  unfold res_functor,
  unfold category_theory.functor.id,
  rw category_theory.functor.mk.inj_eq, -- is there an ext lemma missing?
  split,
  { ext,
    apply subtype.eq,
    refl},
  { -- aargh I have heqs
    apply heq_of_eq,
    ext}
end

view this post on Zulip Kevin Buzzard (Dec 22 2019 at 12:22):

The reason I get heqs is I guess because (obj X) ⟶ (obj Y) changes when I change obj to something equal to obj. I would be happy with some kind of procedure where I am first asked to prove that the two obj maps are equal and then after that I'm asked to prove that the map maps are equal (rather than hequal). Does that even make sense in Lean's type theory?

view this post on Zulip Kevin Buzzard (Dec 22 2019 at 12:27):

@Reid Barton @Scott Morrison @Mario Carneiro to do the kind of algebraic geometry I want to do, I really want to make this category theory stuff work. But I still don't really understand the limitations of dependent type theory in this context. It's clear as an end user what I want to do here -- the objs are the same, the maps are the same, so the functors are the same. The above example is distilled from some proof that pushforwards and pullbacks for sheaves of objects in a category are adjoint functors, and it's what is stopping automation from taking over in some diagram chase. Here's what I'm doing in case anyone is interested.

view this post on Zulip Alex J. Best (Dec 22 2019 at 12:32):

I don't know what the "correct" way is but

  unfold res_functor,
  unfold category_theory.functor.id,
  tidy

is a lot easier on the eye (and brain)!

view this post on Zulip Kevin Buzzard (Dec 22 2019 at 12:33):

I tidied too early! I just try tidy and obviously (not really knowing what they do yet) and then go back to first principles. I think I need some crash course in when to use tidy. Thanks!

view this post on Zulip Alex J. Best (Dec 22 2019 at 12:33):

Oh but "tidy says" just

  simp at *,
  refl,

view this post on Zulip Alex J. Best (Dec 22 2019 at 12:35):

Yeah I'm also slightly surprised that tidy doesn't work if unfolding needs doing in this case

view this post on Zulip Kevin Buzzard (Dec 22 2019 at 12:35):

There's maybe either a missing simp lemma or a missing ext lemma, but I'm too much of a beginner in this area to know how to fix this properly.

view this post on Zulip Kevin Buzzard (Dec 22 2019 at 12:46):

I can't rewrite this lemma in my application anyway :-( (motive is not type correct, and neither erw nor simp only fixes it). Am I not supposed to be proving that functors are equal? Functors are terms not types, I thought equality would be a good idea...

view this post on Zulip Alex J. Best (Dec 22 2019 at 12:58):

Can you get away with just constructing a natural isomorphism of your functors?

view this post on Zulip Patrick Massot (Dec 22 2019 at 12:59):

Yes, that's the standard answer in category theory: do you really mean equal here?

view this post on Zulip Alex J. Best (Dec 22 2019 at 13:03):

example (Y : set X) : res_functor (set.subset.refl Y)  𝟭 _ := by obviously

view this post on Zulip Kevin Buzzard (Dec 22 2019 at 14:08):

I am a mere mathematician and hence don't understand equality properly, but for two functors from C to D to be equal I mean that F(o) = G(o) for all objects o of C and F(f) = G(f) for all morphisms (this makes sense only because of the condition on the objects). Is this a bad notion of equality in Lean's set-up of category theory? Is it a mathematically irrelevant notion?

view this post on Zulip Kevin Buzzard (Dec 22 2019 at 14:19):

I am trying to do a very mundane thing -- pull back a presheaf. I want to prove that pullback is a functor and checking that it sends identities to identities involves checking that two morphisms are equal. However constructing the morphisms involves constructing maps between colimits if one is pulling back presheaves and this involves limit cones which are made from functors. I wanted to argue that two functors were equal to proceed but perhaps this is not the right approach

view this post on Zulip Alex J. Best (Dec 22 2019 at 14:31):

It looks like there is precedent for using natural iso even if equality holds in fact: in line 62 of category_theory/precedent.lean @Reid Barton wrote about two constant functors "These are actually equal, of course, but not definitionally equal (the equality requires F.map (𝟙 _) = 𝟙 _). A natural isomorphism is more convenient than an equality between functors"

view this post on Zulip Kevin Buzzard (Dec 22 2019 at 14:40):

Oh good catch Alex. I will then consider switching to nat isos. Here are some more details of why I thought I needed this. I type them as much for myself as for anyone else. Trying to define pullback of presheaves (taking values in a general category e.g. cat of comm rings) on a top space. Have f:XYf:X\to Y continuous. Definition is fF(U)=limf(U)VF(V)f^*\mathcal{F}(U)=\lim_{f(U)\subseteq V}\mathcal{F}(V) where lim\lim is a (filtered) colimit. Need to check it's a presheaf, so need to check that the restriction map from fF(U)f^*\mathcal{F}(U) to itself is equal to the identity map. This is a map between colimits and I defined it using

limits.colimit.pre :
  Π {J K : Type u_1} [_inst_1 : small_category J] [_inst_2 : small_category K] {C : Type u_2}
  [𝒞 : category_theory.category C] (F : J ⥤ C) [_inst_3 : limits.has_colimit F] (E : K ⥤ J)
  [_inst_4 : limits.has_colimit (E ⋙ F)], limits.colimit (E ⋙ F) ⟶ limits.colimit F

What I have in my situation is a functor EE which is "equal" to the identity functor in the sense that it is a functor from a small category to itself which is equal to the identity functor whichever way you look at it: with notation above, J and K are both the category of open subsets of YY which contain f(U)f(U) and E is a functor which should be equal to the identity functor but which I can quite believe is not defeq to the identity functor (indeed rfl fails).

view this post on Zulip Kevin Buzzard (Dec 22 2019 at 14:47):

One last thing before I stop randomly posting my thoughts and actually go away and think: I am specifically avoiding all mentions of categories for opens X and the definition of a presheaf; the only category in sight is the one where the presheaf is taking values:

structure topological_space.presheaf (X : Type v) [topological_space X]
  (C : Type u) [𝒞 : category.{v} C] :=
(val : Π (U : opens X), C) -- ℱ
(res   :  (U V) (HVU : V  U), val U  val V)
(Hid   :  (U), res U U (set.subset.refl U) = 𝟙 (val U))
(Hcomp :  (U V W) (HWV : W  V) (HVU : V  U),
  res U W (set.subset.trans HWV HVU) = res U V HVU  res V W HWV)

I am doing it because people have experimented with the definition of a presheaf as a functor on the category whose objects are opens (these definitions are already in mathlib I believe) but I find this approach hard to work with because one is immediately launched head first into the category theory library. With this more mundane method the category theory is more limited and there is more of a separation of concerns (there is only one category involved, for example), and I've found it much easier to learn how to use the limits library etc. It's as much a learning exercise as anything else, and as you can see from the above I still have plenty to learn. I'm not suggesting we should do it like this in mathlib, but it seems to me to be a great set-up for experimentation and trying to work out what works and what doesn't work.

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 01:05):

It looks like there is precedent for using natural iso even if equality holds in fact: in line 62 of category_theory/precedent.lean Reid Barton wrote about two constant functors "These are actually equal, of course, but not definitionally equal (the equality requires F.map (𝟙 _) = 𝟙 _). A natural isomorphism is more convenient than an equality between functors"

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Category.20theory/near/148666324

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 01:51):

OK so there is something going on which I don't understand.

I'm trying to prove that ff^* is a functor from (𝒞-valued) presheaves on YY to presheaves on XX with notation as above. The restriction map is as follows: if U1U2U_1\subseteq U_2 then there's a (forgetful) functor EE from the category of open subsets VV of YY with f(U2)Vf(U_2)\subseteq V to the category of open subsets VV of YY with f(U1)Vf(U_1)\subseteq V. In category_theory/limits/limits.lean there is colimit.pre which defines a morphism from the colimit of E ⋙ F to the colimit of F and this is what I used for the restiction map for fFf^*\mathcal{F}. Now say U1=U2U_1=U_2. Then EE equals the identity functor, except that apparently this is not what we are supposed to say. OK so Alex above noted that obviously proves that EE is isomorphic to the identity functor, and everyone is telling me that this is the correct thing to say. But I'm trying to prove that fFf^*\mathcal{F} is a sheaf, and axiom Hid for sheaves says that restriction from UU to UU has to be equal to the identity map. However if I only know that EE is isomorphic to the identity functor then I can only deduce that E ⋙ F is isomorphic to F and so their colimits will only be isomorphic and have no reason to be equal; hence I can't even talk about the identity map between these things.

I want to conclude that in this case I have to prove that EE is equal to, not just isomorphic to, the identity functor, flying in the face of much of what has gone before.

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 01:53):

Am I allowed to prove that functors from a small category to itself are equal?

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 01:58):

example (Y : set X) : res_functor (set.subset.refl Y)  𝟭 _ :=
begin
  /- `tidy` says -/
  fsplit,
    { fsplit,
      { intros X_1, cases X_1, cases X_1_val, dsimp at *, fsplit, dsimp at *, fsplit, intros a a_1, assumption },
      { intros X_1 Y_1 f, refl}},
    { fsplit,
      { intros X_1, cases X_1, cases X_1_val, dsimp at *, fsplit, dsimp at *, fsplit, intros a a_1, assumption },
      { intros X_1 Y_1 f, refl }},
      { apply_auto_param },
      { apply_auto_param }
end

example (Y : set X) : res_functor (set.subset.refl Y) = 𝟭 _ := begin
  unfold res_functor,
  unfold category_theory.functor.id,
  simp, refl,
end

tidy makes a meal of proving they're isomorphic but has little trouble proving they're equal after the unfold hint.

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 02:00):

In short, the issue is that f(U)f^*(U) is a colimit of a functor, and if I replace the functor with an isomorphic functor (e.g. because I replace UU with an equal UU') then the colimit gets (presumably) replaced by an isomorphic colimit, so it no longer makes sense to talk about a map between the two colimits being equal to the identity map, which is what one of the axioms of a presheaf is.

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 02:04):

I cannot see any way of proceeding short of proving that the functors are equal.

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 02:07):

AARGH MY MOTIVE IS NOT TYPE CORRECT

view this post on Zulip Chris Hughes (Dec 23 2019 at 02:07):

You only need equality of the objects for everything else to work, not the homs right? So maybe that's the in between that you need?

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 02:08):

I need that two colimits are equal and that a map between them is the identity

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 02:09):

The problem is that one is the colimit of a functor F and the other is the colimit of E >>> F where E is (not definitionally) equal to the identity functor.

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 02:11):

Maybe I should try to make E defeq to the identity functor :-/

view this post on Zulip Chris Hughes (Dec 23 2019 at 02:12):

That looks impossible.

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 02:13):

My proof of equality uses subtype.eta

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 02:19):

h : res_functor _ = 𝟭 {V // f '' U.val ⊆ ↑V}
⊢ limits.colimit.pre (to_aux_functor ℱ (f '' U.val)) (res_functor _) = 𝟙 (aux_colimit ℱ (f '' ↑U))

I can't rw h or erw h or simp only [h]. So I can't work with equality and I can't work with isomorphism :-/

view this post on Zulip Chris Hughes (Dec 23 2019 at 02:23):

The standard way to do this is to prove the rewrite you want to do except with res_functor _ replaced with a variable so subst works, and then apply it to this case.

view this post on Zulip Chris Hughes (Dec 23 2019 at 02:24):

No idea if this is a sustainable strategy.

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 02:32):

example {J K : Type v} [_inst_1 : small_category J]
[small_category K] {C : Type u} [𝒞 : category_theory.category C] (F : J  C)
[limits.has_colimit F] (E₁ E₂ : K  J) [limits.has_colimit (E₁  F)] [limits.has_colimit (E₂  F)]
(h : E₁ = E₂) : limits.colimit.pre F E₁ = limits.colimit.pre F E₂ := sorry

doesn't compile: Lean complains that they can't be equal because they have different types :-/

type mismatch at application
  limits.colimit.pre F E₁ = limits.colimit.pre F E₂
term
  limits.colimit.pre F E₂
has type
  limits.colimit (E₂ ⋙ F) ⟶ limits.colimit F
but is expected to have type
  limits.colimit (E₁ ⋙ F) ⟶ limits.colimit F

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 02:35):

[note that is a category theory hom]

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 02:40):

self-contained gist

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 03:03):

I think the best idea is just to give up on using limits.colimits.pre completely and just do everything from first principles

view this post on Zulip Johan Commelin (Dec 23 2019 at 08:51):

That doesn't generalise...

view this post on Zulip Johan Commelin (Dec 23 2019 at 08:54):

@Kevin Buzzard Note that natural iso's contain data, and hence should be def. Also, the data-parts should probably not be filled in by tidy (even though you can use tidy? to see what to do, but should be filled in with term mode. Hopefully, you would then get two (canonically :see_no_evil:) isomorphic functors, that are defeq on objects. It would then make sense to talk about an identity morphism between them (after evaluation on some object).

view this post on Zulip Johan Commelin (Dec 23 2019 at 11:07):

This proves your Hid challenge:

      ext,
      rw limits.colimit.ι_pre,
      erw category.comp_id,
      tidy,

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 11:12):

as does this:

        unfold limits.colimit.pre,
        dsimp,
        ext V,
        dsimp,
        rw limits.colimit.ι_desc,
        dsimp,
        erw category_theory.category.comp_id,
        tidy,

but yours is better ;-) Thanks!

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 11:13):

I see that both of us need an erw in a situation where it's completely clear that a rw will work ;-)

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 11:16):

In fact my proof simplifies to yours. I unfold something and do some other rewrite, and after simplification I end up where you were.

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 11:25):

ext, in this context, seems to be taking a goal of the form m1=m2 where the m_i are morphisms in a category, and replacing it with a goal of the form F(j)>>m1 = F(j)>>m2. It seems to be explicitly using the fact that the source or target of the m_i is a colimit and it's somehow using a universal property of colimits?

view this post on Zulip Johan Commelin (Dec 23 2019 at 11:56):

Pretty smart, right?

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 12:00):

Yes! Hey, I just managed to do a definitional rewrite which none of rw, erw or simp only would let me do, using conv mode

view this post on Zulip Kevin Buzzard (Dec 23 2019 at 12:19):

ooh I just did it again, and the first time I tried it it failed, so I replaced a proof of something with a different proof and then it worked. I think that's the first time I've seen Lean care about what proof I offer of a proposition.


Last updated: May 06 2021 at 18:20 UTC