Zulip Chat Archive

Stream: maths

Topic: weird type class issue


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

Consider this code:

import category_theory.category

open category_theory

universes u u₁ u₂ v v₁ v₂ w w₁ w₂

variables {C : Type u₁} [𝒞 : category.{u₁ u₂} C] --[@has_limits.{u₁ u₂} C 𝒞]
include 𝒞

-- todo should this be done as a subfunctor?
structure covering_family (U : C) :=
(I : Type u₂)
(obj : I  C)
(hom : Π {i : I}, obj i  U)

#print covering_family

structure coverage :=
(covers : Π {U : C}, set (covering_family U)) -- red squiggles under "covering_family"

I get the following error:

failed to synthesize type class instance for
C : Type u₁,
𝒞 : category C,
C : Type u₁,
𝒞 : category C,
U : C
 category C

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

Why are C and the category structure duplicated there? And why can't it resolve the type class issue?

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

what happens if you remove the include and write the variables directly as parameters for coverage?

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

These includes are all over the place in Scott's library. If you remove it you get red squiggles under the in obj i ⟶ U.

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

def coverage := Π {U : C}, set (covering_family U)

gives the error

failed to synthesize type class instance for
C : Type u₁,
𝒞 : category C,
U : C
 category C

So now the duplication is gone. But it still can't resolve the type class...

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

The following works but is very ugly.

def coverage := Π {U : C}, set (@covering_family _ 𝒞 U)

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

In general I think the fact that we need include 𝒞 all the time is a sign that something is wrong. But I have no clue what is wrong and how to fix it.

view this post on Zulip Reid Barton (Oct 18 2018 at 12:45):

I usually include the universe parameters when I run into this kind of issue, like covering_family.{u\1 u\2}. (BTW, usually we use a v-type letter for the morphism universe.)
I have no idea about the duplicate display in the error message though.

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

I currently have

import category_theory.examples.topological_spaces
import category_theory.opposites
import category_theory.yoneda
import category_theory.limits.equalizers
import category_theory.limits.products

open category_theory

universes u u₁ u₂ v v₁ v₂ w w₁ w₂

namespace category_theory.limits
variables {C : Type u₁} [𝒞 : category.{u₁ u₂} C]
include 𝒞

variables [has_coequalizers.{u₁ u₂} C] {Y Z : C} (f g : Y  Z)

def coequalizer.cofork := has_coequalizers.coequalizer.{u₁ u₂} f g
def coequalizer := (coequalizer.cofork f g).X
def coequalizer.π : Z  (coequalizer f g) := (coequalizer.cofork f g).π
@[search] def coequalizer.w : f  (coequalizer.π f g) = g  (coequalizer.π f g) := (coequalizer.cofork f g).w
def coequalizer.universal_property : is_coequalizer (coequalizer.cofork f g) :=
has_coequalizers.is_coequalizer.{u₁ u₂} C f g

def coequalizer.desc (P : C) (h : Z  P) (w : f  h = g  h) : coequalizer f g  P :=
(coequalizer.universal_property f g).desc { X := P, π := h, w := w }

@[extensionality] lemma coequalizer.hom_ext {Y Z : C} {f g : Y  Z} {X : C}
(h k : coequalizer f g  X) (w : coequalizer.π f g  h = coequalizer.π f g  k) : h = k :=
begin
  let s : cofork f g :=   X , coequalizer.π f g  h ,
  have q := (coequalizer.universal_property f g).uniq s h,
  have p := (coequalizer.universal_property f g).uniq s k,
  rw [q, p],
  solve_by_elim, refl
end

end category_theory.limits

section presheaf
open category_theory.limits
variables (X : Type u₁) [𝒳 : category.{u₁ v₁} X] (C : Type u₂) [𝒞 : category.{u₂ v₂} C]
include 𝒳 𝒞

def presheaf := Xᵒᵖ  C

variables {X} {C}

instance : category (presheaf X C) := by unfold presheaf; apply_instance

omit 𝒞
instance : has_coproducts (presheaf X (Type v₂)) := sorry

#print presheaf.category_theory.category

end presheaf

-- todo should this be done as a subfunctor?
structure covering_family {X : Type u₁} [category.{u₁ v₁} X] (U : X) :=
(index : Type v₁)
(obj : index  X)
(hom : Π (i : index), obj i  U)

namespace covering_family
open category_theory.limits
variables {X : Type u₁} [𝒳 : category.{u₁ v₁} X]
include 𝒳

variables {U : X}

def sieve (f : covering_family U) : presheaf X (Type v₁) :=
@coequalizer _ _ (sorry)
(@Sigma _ _ _ (f.index × f.index) (λ p, _))
(@Sigma _ _ _ f.index (((yoneda X) : X  presheaf X (Type v₁))  f.obj))
_ _

def sheaf_condition (f : (covering_family U)) {C : Type u₂} [category.{u₂ v₂} C] (F : presheaf X C) : Prop := sorry

end covering_family

structure coverage {X : Type u₁} [category.{u₁ u₂} X] :=
(covers   : Π (U : X), set (covering_family U))
(property :  {U V : X} (g : V  U) (f : (covering_family U)),
             h : (covering_family V),  j : h.index,  {i : f.index} {k : h.obj j  f.obj i},
            h.hom j  g = k  f.hom i)

class site (X : Type u₁) extends category.{u₁ u₂} X :=
(coverage : @coverage X (by assumption))

section sheaf
variables (X : Type u₁) [𝒳 : site.{u₁ v₁} X] (C : Type u₂) [𝒞 : category.{u₂ v₂} C]
include 𝒳 𝒞

structure sheaf :=
(presheaf : presheaf X C)
(sheaf_condition :  {U : X} (f : (@covering_family _ 𝒳.to_category U)), f.sheaf_condition presheaf)

end sheaf



namespace topological_space

variables {X : Type u} [topological_space X]

instance : site (opens X) :=
{ coverage :=
  { covers := λ U, λ Us, begin sorry -- the union of the Ui should be U
    end,
    property := sorry } }

end topological_space

Lean is especially unhappy about the part where I try to define the sieve.

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

Currently I'm just going to wait till some PR's get merged.

view this post on Zulip Reid Barton (Oct 18 2018 at 13:05):

Lots of those _s in sieve still need to be filled in, right?

view this post on Zulip Reid Barton (Oct 18 2018 at 13:05):

Or at least... 3 I guess?

view this post on Zulip Johan Commelin (Oct 18 2018 at 13:14):

Yes, that is right. But I need fibre products for the for the _ in the first Sigma. :sad:

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

In general I think the fact that we need include 𝒞 all the time is a sign that something is wrong. But I have no clue what is wrong and how to fix it.

So there are two issues which come up a lot due to the way category theory uses universe variables.
1. The include 𝒞 thing is a workaround for a specific elaborator bug where it doesn't correctly account for universe parameters of variables that have been included by the "square bracket rule". If you hit this bug then you will see an error about something like "bad tactic or buggy elaborator".
2. It also often happens that you have to help Lean out with some explicit universe parameters. I think what is going on is that one of the parameters is not constrained by anything (usually the v), and so Lean is looking for a category.{u ?u_1} C instance. Apparently it's unwilling to take an instance category.{u v} C for some specific v and specialize ?u_1 to v. I'm not sure whether this is a bug or just something where the system doesn't work in the way we would usually prefer.

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

I see. I wouldn't mind if universe unification was slightly more greedy in this case.

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

Your covering_family thing is the second issue.

view this post on Zulip Reid Barton (Oct 18 2018 at 13:43):

Maybe we would like to have something like out_param on the universe parameter v, but that's not currently possible

view this post on Zulip Reid Barton (Oct 18 2018 at 13:44):

Also I don't really understand how out_param works, so I could be way off-base.

view this post on Zulip Reid Barton (Oct 18 2018 at 13:52):

Maybe the clearest example of this is something like terminal_object (C : Type u) [category.{u v} C] [has_terminal_object.{u v} C] : C where you could have a type C : Type u equipped with two totally different category.{u v} and category.{u w} structures with different terminal objects. The type of terminal_object C is just C which has Type u so there is no way you could ever constrain the v parameter.

view this post on Zulip Johan Commelin (Oct 19 2018 at 12:21):

The issues aren't gone, but my definition of sieve is converging onto something far more readable then I had before:

import category_theory.examples.topological_spaces
import category_theory.opposites
import category_theory.yoneda
import category_theory.limits

open category_theory

universes u u₁ u₂ v v₁ v₂ w w₁ w₂

namespace category_theory.limits
variables {C : Type u₁} [𝒞 : category.{u₁ u₂} C]
include 𝒞

variables [has_coequalizers.{u₁ u₂} C] {Y Z : C} (f g : Y  Z)

def coequalizer.cofork := has_coequalizers.coequalizer.{u₁ u₂} f g
def coequalizer := (coequalizer.cofork f g).X
def coequalizer.π : Z  (coequalizer f g) := (coequalizer.cofork f g).π
@[search] def coequalizer.w : f  (coequalizer.π f g) = g  (coequalizer.π f g) := (coequalizer.cofork f g).w
def coequalizer.universal_property : is_coequalizer (coequalizer.cofork f g) :=
has_coequalizers.is_coequalizer.{u₁ u₂} C f g

def coequalizer.desc (P : C) (h : Z  P) (w : f  h = g  h) : coequalizer f g  P :=
(coequalizer.universal_property f g).desc { X := P, π := h, w := w }

@[extensionality] lemma coequalizer.hom_ext {Y Z : C} {f g : Y  Z} {X : C}
(h k : coequalizer f g  X) (w : coequalizer.π f g  h = coequalizer.π f g  k) : h = k :=
begin
  let s : cofork f g :=   X , coequalizer.π f g  h ,
  have q := (coequalizer.universal_property f g).uniq s h,
  have p := (coequalizer.universal_property f g).uniq s k,
  rw [q, p],
  solve_by_elim, refl
end

end category_theory.limits

section presheaf
open category_theory.limits
variables (X : Type u₁) [𝒳 : category.{u₁ v₁} X] (C : Type u₂) [𝒞 : category.{u₂ v₂} C]
include 𝒳 𝒞

def presheaf := Xᵒᵖ  C

variables {X} {C}

instance : category (presheaf X C) := by unfold presheaf; apply_instance

omit 𝒞
instance presheaf.has_coequalizers : @has_coequalizers (presheaf X (Type v₁)) presheaf.category_theory.category := sorry
instance presheaf.has_coproducts : @has_coproducts (presheaf X (Type v₁)) presheaf.category_theory.category := sorry
instance presheaf.has_pullbacks : @has_pullbacks (presheaf X (Type v₁)) presheaf.category_theory.category := sorry

end presheaf

-- todo should this be done as a subfunctor?
structure covering_family {X : Type u₁} [category.{u₁ v₁} X] (U : X) :=
(index : Type v₁)
(obj : index  X)
(map : Π (i : index), obj i  U)

namespace covering_family
open category_theory.limits
variables {X : Type u₁} [𝒳 : category.{u₁ v₁} X]
include 𝒳

variables {U : X}

def sieve (f : covering_family U) : presheaf X (Type v₁) :=
let CP := (((yoneda X) : X  presheaf X (Type v₁))  f.obj) in
coequalizer
  (Sigma.desc (λ p : (f.index × f.index), (Sigma.ι CP p.1)  (pullback.π₁ ((yoneda X).map (f.map p.1)) ((yoneda X).map (f.map p.2)))))
  (Sigma.desc (λ p : (f.index × f.index), (Sigma.ι CP p.2)  (pullback.π₂ ((yoneda X).map (f.map p.1)) ((yoneda X).map (f.map p.2)))))

def sheaf_condition (f : (covering_family U)) {C : Type u₂} [category.{u₂ v₂} C] (F : presheaf X C) : Prop := sorry

end covering_family

view this post on Zulip Johan Commelin (Oct 19 2018 at 12:22):

But there are still a lot of typeclass issues.


Last updated: May 12 2021 at 06:14 UTC