functor ext lemma?

Stream: maths

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Alex J. Best]

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)!

[Kevin Buzzard]

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!

[Alex J. Best]

Oh but "tidy says" just

  simp at *,
  refl,

[Alex J. Best]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Alex J. Best]

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

[Patrick Massot]

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

[Alex J. Best]

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

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Alex J. Best]

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"

[Kevin Buzzard]

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:X\to Y$ continuous. Definition is $f^*\mathcal{F}(U)=\lim_{f(U)\subseteq V}\mathcal{F}(V)$ where $\lim$ is a (filtered) colimit. Need to check it's a presheaf, so need to check that the restriction map from $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 $E$ 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 $Y$ which contain $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).

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

I'm trying to prove that $f^*$ is a functor from (𝒞-valued) presheaves on $Y$ to presheaves on $X$ with notation as above. The restriction map is as follows: if $U_1\subseteq U_2$ then there's a (forgetful) functor $E$ from the category of open subsets $V$ of $Y$ with $f(U_2)\subseteq V$ to the category of open subsets $V$ of $Y$ with $f(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 $f^*\mathcal{F}$. Now say $U_1=U_2$. Then $E$ 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 $E$ 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 $f^*\mathcal{F}$ is a sheaf, and axiom Hid for sheaves says that restriction from $U$ to $U$ has to be equal to the identity map. However if I only know that $E$ 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 $E$ is equal to, not just isomorphic to, the identity functor, flying in the face of much of what has gone before.

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

In short, the issue is that $f^*(U)$ is a colimit of a functor, and if I replace the functor with an isomorphic functor (e.g. because I replace $U$ with an equal $U'$) 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.

[Kevin Buzzard]

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

[Kevin Buzzard]

AARGH MY MOTIVE IS NOT TYPE CORRECT

[Chris Hughes]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Chris Hughes]

That looks impossible.

[Kevin Buzzard]

My proof of equality uses subtype.eta

[Kevin Buzzard]

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 :-/

[Chris Hughes]

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.

[Chris Hughes]

No idea if this is a sustainable strategy.

[Kevin Buzzard]

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

[Kevin Buzzard]

[note that ⟶ is a category theory hom]

[Kevin Buzzard]

self-contained gist

[Kevin Buzzard]

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

[Johan Commelin]

That doesn't generalise...

[Johan Commelin]

@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).

[Johan Commelin]

This proves your Hid challenge:

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

[Kevin Buzzard]

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!

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Johan Commelin]

Pretty smart, right?

[Kevin Buzzard]

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

[Kevin Buzzard]

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.