Zulip Chat Archive

Stream: maths

Topic: category theory


view this post on Zulip Kenny Lau (Apr 01 2018 at 21:38):

https://github.com/kckennylau/category-theory/blob/master/src/adjunction_examples.lean

view this post on Zulip Kenny Lau (Apr 02 2018 at 10:02):

@[reducible] def Set.Prod_Hom (B : Type u) : adjunction examples.Set examples.Set :=
adjunction.make _ _
  (examples.Set.product_functor B)
  (examples.Set.Hom_functor_right B)
  (λ A C f x, f x.1 x.2)
  (λ A C f x y, f (x, y))
  (λ A₁ A₂ C₁ C₂ f g t, rfl)
  (λ A₁ A₂ C₁ C₂ f g t, rfl)
  (λ A C f, funext $ λ ⟨t₁, t₂⟩, rfl)
  (λ A C f, rfl)

view this post on Zulip Kenny Lau (Apr 02 2018 at 10:02):

so natural

view this post on Zulip Kenny Lau (Apr 02 2018 at 10:20):

@[reducible] def Top_Set : adjunction examples.Top examples.Set :=
adjunction.free_forgetful _
  examples.Top.discrete
  examples.Top.forgetful
  (λ S T f, ⟨f, continuous_top⟩)
  (λ S T f, f.1)
  (λ T₁ T₂ S₁ S₂ f g t z, rfl)
  (λ T₁ T₂ S₁ S₂ f g t, subtype.eq rfl)
  (λ S T f, subtype.eq rfl)
  (λ S T f, rfl)

@[reducible] def Set_Top : adjunction examples.Set examples.Top :=
adjunction.make _ _
  examples.Top.forgetful
  examples.Top.indiscrete
  (λ S T f, f.1)
  (λ S T f, ⟨f, continuous_bot⟩)
  (λ T₁ T₂ S₁ S₂ f g t, subtype.eq rfl)
  (λ T₁ T₂ S₁ S₂ f g t, rfl)
  (λ S T f, rfl)
  (λ S T f, subtype.eq rfl)

view this post on Zulip Kenny Lau (Apr 02 2018 at 10:20):

that moment when they're adjoint to each other

view this post on Zulip Kenny Lau (Apr 07 2018 at 17:25):

for a set S, denoting by L(S) the transitive closure of S, we see that for any transitive set T with S ⊆ T, then L(S) ⊆ T

view this post on Zulip Kenny Lau (Apr 07 2018 at 17:25):

I wonder if this is the left adjoint of some forgetful functor

view this post on Zulip Kenny Lau (Apr 07 2018 at 17:26):

well, working in the category of sets with inclusion as morphism, we see that Hom_Trans(L(S),T) = Hom_Set(S,R(T)), where Trans is the category of transitive sets

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 18:43):

What does this even mean? What is a transitive set?

view this post on Zulip Kenny Lau (Apr 07 2018 at 18:44):

A set X is transitive if for every x and y such that x∈y∈X, we have x∈X

view this post on Zulip Kenny Lau (Apr 07 2018 at 18:45):

if the transitive closure is indeed a left adjoint, then we get right-exactness for free

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 18:49):

Eew. I think I saw that notion in undergraduate set theory nearly 30 years ago, and I'm not sure I've seen it since. Maybe I saw it in the context of ordinals, which is something else I've not seen since.

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 18:53):

Are you making an assertion here? What is R(T)?

view this post on Zulip Kenny Lau (Apr 07 2018 at 18:53):

the forgetful functor that forgets the fact that T is transitive

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 18:53):

Is what you write true?

view this post on Zulip Kenny Lau (Apr 07 2018 at 18:53):

I believe so

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 18:54):

If S and T are both transitive, then you're asserting that the transitive maps from S to T are the same as the maps from S to T then?

view this post on Zulip Kenny Lau (Apr 07 2018 at 18:54):

yes, since here the morphisms are just inclusions, so there is only one morphism per pair of sets

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 18:55):

What does Hom_Set mean then?

view this post on Zulip Kenny Lau (Apr 07 2018 at 18:55):

oh, inclusion

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 18:57):

Do you have a question?

view this post on Zulip Kenny Lau (Apr 07 2018 at 18:57):

is my belief right

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 18:58):

What does Hom_Trans mean?

view this post on Zulip Kenny Lau (Apr 07 2018 at 18:58):

subcategory

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 18:58):

I don't know what anything means. It feels like you have made these categories up.

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 18:59):

It also seems that you are just as capable of writing down a proof of your assertion as I am. Why not check it in Lean? ;-)

view this post on Zulip Kenny Lau (Apr 07 2018 at 18:59):

because to hell with the category of sets in Lean

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 18:59):

What does Hom_Trans mean?

view this post on Zulip Kenny Lau (Apr 07 2018 at 18:59):

the inclusion in the category of transitive sets

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 18:59):

So at most one map between two sets?

view this post on Zulip Kenny Lau (Apr 07 2018 at 19:00):

yes

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 19:00):

" we see that for any transitive set T with S ⊆ T, then L(S) ⊆ T ". Is that your question?

view this post on Zulip Kenny Lau (Apr 07 2018 at 19:00):

well that's the UMP of transitive closure

view this post on Zulip Kenny Lau (Apr 07 2018 at 19:00):

which should be right

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 19:01):

But what is your question if it is not precisely that statement?

view this post on Zulip Kenny Lau (Apr 07 2018 at 19:01):

no idea

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 19:01):

We might be done then :-)

view this post on Zulip Kenny Lau (Apr 07 2018 at 19:02):

interesting

view this post on Zulip Reid Barton (Sep 01 2018 at 21:06):

Scott I guess I'll keep you updated on what I'm doing by sending pastebin links for now.

view this post on Zulip Reid Barton (Sep 01 2018 at 21:07):

https://pastebin.com/WmdNgPdx is limits and colimits in types (nice and easy) and small and filtered categories (also easy).

view this post on Zulip Reid Barton (Sep 01 2018 at 21:08):

Next I plan to try to show that small limits commute with filtered colimits

view this post on Zulip Reid Barton (Sep 01 2018 at 21:08):

Probably I won't finish that in the next few days.

view this post on Zulip Scott Morrison (Sep 01 2018 at 22:45):

Thanks, Reid, that patch has been applied!

view this post on Zulip Reid Barton (Sep 02 2018 at 15:54):

I defined the limit functor but the proofs aren't as concise as they should be, especially map_id'.
https://pastebin.com/QDM9H7TX

view this post on Zulip Reid Barton (Sep 02 2018 at 15:55):

Scott -- maybe the simp lemmas could be set up so that map_id' can be proved by obviously?
map_comp' is more complicated, since you have to use associativity (backwards)

view this post on Zulip Scott Morrison (Sep 02 2018 at 22:10):

@Reid Barton, in fact I already had this, obscurely hidden in universal/complete/default.lean, with slightly different proofs. I've incorporated some changes from yours, but left my proofs for now. Curiously, obviously does just fine for map_comp', but fails on map_id' because for some reason simp won't apply limit.lift_π.

view this post on Zulip Scott Morrison (Sep 02 2018 at 22:13):

I guess it was hiding in that directory because I wrote it for the sake of https://github.com/semorrison/lean-category-theory/blob/master/src/category_theory/universal/complete/functor_category.lean, a still incomplete proof that C \lea D has limits if D does.

view this post on Zulip Kenny Lau (Oct 20 2018 at 15:59):

@Scott Morrison Will you change some of the mathlib files to use category theory?

view this post on Zulip Kenny Lau (Oct 20 2018 at 16:00):

what's the plan for category theory?

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:00):

I think at first, not much. Things like has_products CommRing can first live under category_theory/, as we get used to them.

view this post on Zulip Kenny Lau (Oct 20 2018 at 16:01):

will they gradually assimilate into the main mathlib library?

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:01):

Eventually such facts should move out to their natural homes, immediately following where the underlying lemmas are actually proved.

view this post on Zulip Kenny Lau (Oct 20 2018 at 16:01):

nice

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:01):

I suspect in the long run a lot of files will want to import category_theory.isomorphism, to avoid having to define their own custom version of equiv for the structure at hand.

view this post on Zulip Kenny Lau (Nov 02 2018 at 09:58):

@Scott Morrison The new module will be:

class module (α : out_param $ Type u) (β : Type v) [out_param $ ring α]
  [add_comm_group β] extends semimodule α β

How will your category theory library deal with this?

view this post on Zulip Scott Morrison (Nov 02 2018 at 11:02):

Mostly users will just want the category of R-modules for some fixed R. After you've fixed the ring this is no more or less scary than bundling any other algebraic typeclass, I think.

view this post on Zulip Kenny Lau (Nov 02 2018 at 11:15):

@Scott Morrison I don't see how bundle can solve this

view this post on Zulip Scott Morrison (Nov 02 2018 at 11:16):

Oh, I didn't imply that we should use bundled. It's only intended for the simplest cases.

view this post on Zulip Scott Morrison (Nov 02 2018 at 11:18):

But structure Module (a : Type) [ring a] := (b : Type) (m : module a b), is presumably fine.

view this post on Zulip Scott Morrison (Nov 02 2018 at 11:18):

Maybe you haven't actually said what you're concerned about?

view this post on Zulip Kenny Lau (Nov 02 2018 at 11:18):

well you forgot the add_comm_group

view this post on Zulip Kenny Lau (Nov 02 2018 at 11:18):

and actually that's all I'm concerned about

view this post on Zulip Scott Morrison (Nov 02 2018 at 11:19):

So structure Module (a : Type) [ring a] := (b : Type) (g : add_comm_group b) (m : module a b)...?

view this post on Zulip Kenny Lau (Nov 02 2018 at 11:22):

I'm not really sure how all of this works, because last time in my own category repo, I was wrestling with sigma

view this post on Zulip Scott Morrison (Nov 02 2018 at 11:27):

Yeah, I think just building custom structures, and then a few lemmas that peel back out the typeclasses as needed, is easiest.

view this post on Zulip Scott Morrison (Nov 02 2018 at 11:27):

I'll make a few more examples.

view this post on Zulip Kenny Lau (Nov 02 2018 at 11:55):

thanks

view this post on Zulip Kenny Lau (Nov 02 2018 at 16:46):

@Scott Morrison is bundled category a category? If not, what's the proper name?

view this post on Zulip Johan Commelin (Nov 02 2018 at 19:54):

I have a natural transformation a from F to G, and Lean is looking for a natural transformation from G.op to F.op. So I would like to provide a.op but this is not defined yet. What is the natural place to add this definition? In opposites.lean or in natural_transformation.lean?

view this post on Zulip Reid Barton (Nov 02 2018 at 20:00):

I think it makes sense to keep category/functor/natural_transformation "at the bottom" and so put a.op in opposites like F.op

view this post on Zulip Johan Commelin (Nov 02 2018 at 20:05):

Ok... fine with me. I could also imagine opposites being pretty "fundamental".

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:09):

It would be quite interesting if we know that functors form a category but not that categories form a category...

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:09):

I've searched all the files

view this post on Zulip Mario Carneiro (Nov 02 2018 at 20:10):

the problem is that categories form a 2-category

view this post on Zulip Mario Carneiro (Nov 02 2018 at 20:10):

so "categories form a category" is true but mostly useless

view this post on Zulip Reid Barton (Nov 02 2018 at 20:10):

Categories also form a perfectly good category, we just don't have it yet

view this post on Zulip Johan Commelin (Nov 02 2018 at 20:19):

Ok, I'm testing out a heresy:

def cocone (F : J  C) := cone F.op

The first problem I hit is that for c : cocone F the tip of the cocone c.X is now an object of C\op instead of C. Can this somehow be fixed? I would rather just write f : c.X \hom X instead of

f : @category.hom C _ c.X X

view this post on Zulip Reid Barton (Nov 02 2018 at 20:27):

I actually have this problem in ordinary informal math as well: it's hard to talk about both C and C^op at the same time.
Sometimes I write things like A\overline{A} for the object of C^op corresponding to the object AA of C, but I'm not really fond of it.

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:28):

"ordinary informal math" = category

view this post on Zulip Johan Commelin (Nov 02 2018 at 20:30):

Sure, so we could write X.op for such objects. But this problem is different. With my definition c.X lives in C^op by definition. But I'dd rather have it live in C... And somehow just writing f : (c.X : C) \hom X doesn't cut it....

view this post on Zulip Johan Commelin (Nov 02 2018 at 20:30):

Hmmm... I have to run. See y'all later.

view this post on Zulip Reid Barton (Nov 02 2018 at 20:52):

Perhaps we could have unop : C\op \to C?

view this post on Zulip Kenny Lau (Nov 02 2018 at 20:56):

or maybe an equivalence of categories C\op\op \cong C?

view this post on Zulip Kenny Lau (Nov 02 2018 at 21:22):

import algebra.module
import category_theory.examples.rings category_theory.opposites

universes u v w

variables (R : Type u) [ring R]

class Module (M : Type v) extends add_comm_group M, module R M

def Module.is_linear_map {M N : Type v} [Module R M] [Module R N] (f : M  N) : Prop :=
is_linear_map f

open category_theory category_theory.examples

instance Module.concrete_category : concrete_category (@Module.is_linear_map R _) :=
⟨λ _ _, by constructor; intros; refl,
λ _ _ _ _ _ _ _ _ hf hg, by cases hf; cases hg; constructor; intros; simp only [(), *]

@[reducible] def Mod := bundled (Module R)

@[reducible] def Cat := bundled category

instance : category Cat :=
{ hom := λ C D, @category_theory.functor C.1 C.2 D.1 D.2,
  id := λ C, @functor.id C.1 C.2,
  comp := λ C D E, @category_theory.functor.comp C.1 C.2 D.1 D.2 E.1 E.2,
  id_comp' := λ C D f, by cases f; refl,
  comp_id' := λ C D f, by cases f; refl }

def Mod : Ringᵒᵖ  Cat :=
{ obj := λ R, bundled.mk _ (Mod R.1),
  map' := λ R S φ, concrete_functor (begin end) (begin end) }

view this post on Zulip Reid Barton (Nov 02 2018 at 21:34):

This looks good, but then the real test is whether it's convenient to use objects of Mod R as modules and vice versa, and the same for Cat

view this post on Zulip Reid Barton (Nov 02 2018 at 21:36):

At a minimum you want the instance that gets you the Module back out from x : Mod R

view this post on Zulip Reid Barton (Nov 02 2018 at 21:37):

analogous to instance (x : Ring) : ring x := x.str

view this post on Zulip Kenny Lau (Nov 02 2018 at 21:37):

that's just interface

view this post on Zulip Kenny Lau (Nov 02 2018 at 21:37):

anyone can write an interface

view this post on Zulip Reid Barton (Nov 02 2018 at 21:38):

anyone can define Cat, too

view this post on Zulip Reid Barton (Nov 02 2018 at 21:38):

Finding a good interface is the important thing

view this post on Zulip Chris Hughes (Nov 02 2018 at 21:38):

Interfaces are hard.

view this post on Zulip Kenny Lau (Nov 02 2018 at 21:40):

I think opposite can have a better interface

view this post on Zulip Kenny Lau (Nov 02 2018 at 22:36):

@Scott Morrison how should we define an additive category?

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:36):

ugh, yeah, defining enriched categories may take a lot of work to do in general. :-(

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:37):

If you _just_ want additive categories (which is very reasonable, later we can retrofit them as special cases of enriched categories)

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:38):

then I don't think it's too bad

view this post on Zulip Kenny Lau (Nov 02 2018 at 22:38):

ok, then how?

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:38):

Just have a new typeclass [additive_category C], with fields hom_abelian : add_comm_group (X \hom Y) and comp_bilinear : ...

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:39):

and then some defs that create instances from these fields

view this post on Zulip Kenny Lau (Nov 02 2018 at 22:39):

can we instead declare it as a functor from the Hom category to the Ab category

view this post on Zulip Kenny Lau (Nov 02 2018 at 22:40):

such that some triangle commutes

view this post on Zulip Kenny Lau (Nov 02 2018 at 22:40):

I guess Hom isn't a category

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:40):

yeah, I'm not sure what you mean

view this post on Zulip Kenny Lau (Nov 02 2018 at 22:41):

there must be a way to do this category-theoretically...

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:41):

Well... I think often it's better to have the definitions "explicit" and then have lemmas saying "you can interpret this in categorical terms"

view this post on Zulip Kenny Lau (Nov 02 2018 at 22:41):

sure

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:41):

In particular, for monoidal categories (or 2-categories), which I really want to get back to,

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:42):

it turns out to be a really bad idea to say that a monoidal category is a category equipped with a functor (C x C) \func C, such that ...

view this post on Zulip Kenny Lau (Nov 02 2018 at 22:42):

why isn't Lean ready for a category theory library?

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:42):

and instead you should do everything grossly: a function tensorObjects, a function tensorMorphisms, and then have a lemma saying these form that functor

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:43):

This sounds like a really bad idea, but the way lean's notation system and elaborator work, you run into endless misery making the functor the "primary" description of the tensor product.

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:43):

It's very unfortunate. :-(

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:45):

why isn't Lean ready for a category theory library?

Speaking to mathematicians, Lean, like every other ITP system, is not ready to do mathematics in. :-)

Lean is terrible, just less terrible than all the others!

view this post on Zulip Reid Barton (Nov 02 2018 at 23:17):

I don't know whether this would be easier or harder, but you don't actually need monoidal categories to do enriched categories; you could enrich in a multicategory instead

view this post on Zulip Kevin Buzzard (Nov 02 2018 at 23:23):

I've found it quite good fun doing abstract maths in Lean. I've not used categories though. But stuff like commutative algebra seems to come out nicely.

view this post on Zulip Kenny Lau (Nov 02 2018 at 23:24):

right, until the module thing came along

view this post on Zulip Chris Hughes (Nov 02 2018 at 23:27):

Lean is often good at abstract stuff. I think maybe abstract usually means it has to be done on paper more formally, because there's less real world intuition.

view this post on Zulip Scott Morrison (Nov 03 2018 at 07:16):

But stuff like commutative algebra seems to come out nicely.

Stockholm syndrome. :-)

view this post on Zulip Reid Barton (Nov 05 2018 at 00:44):

Scott, are you attached to the name category_theory.embedding?
How about fully_faithful?

view this post on Zulip Reid Barton (Nov 05 2018 at 00:47):

embedding is ambiguous, I feel. Someone may think it implies "injective on objects" for example. The nlab gives a variety of definitions.

view this post on Zulip Reid Barton (Nov 05 2018 at 00:48):

(Also it collides with the top-level embedding of topological spaces, which is not category_theory's fault but it did cause some extremely confusing behavior during one of my lean-homotopy-theory mathlib version bumps.)

view this post on Zulip Scott Morrison (Nov 05 2018 at 02:00):

Yes, we should definitely change this.

view this post on Zulip Johan Commelin (Nov 05 2018 at 18:52):

@Scott Morrison Do you have any idea why this would fail?

failed to synthesize type class instance for
X : Type u₁,
𝒳 : category X,
U : X,
f : covering_family U,
p : f.index × f.index
 category (Xᵒᵖ  Type v₁)

view this post on Zulip Scott Morrison (Nov 05 2018 at 18:54):

either you're missing the import, or something is weird with universe levels?

view this post on Zulip Johan Commelin (Nov 05 2018 at 18:55):

I have

def presheaf := Xᵒᵖ  C

variables {X} {C}

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

in the same file.

view this post on Zulip Scott Morrison (Nov 05 2018 at 18:57):

Turn on pp.universes?

view this post on Zulip Johan Commelin (Nov 05 2018 at 18:57):

I'll try that. I also see

[class_instances] (0) ?x_0 : category (Xᵒᵖ ⥤ Type v₁) := @functor.category ?x_40 ?x_41 ?x_42 ?x_43
failed is_def_eq

in the trace.

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:00):

Ok, that gave me

failed to synthesize type class instance for
X : Type u₁,
𝒳 : category.{u₁ v₁} X,
U : X,
f : covering_family.{u₁ v₁} U,
p : f.index × f.index
 category.{(max u₁ (v₁+1)) v₁} (Xᵒᵖ  Type v₁)

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:00):

Maybe I don't understand universes well enough...

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:00):

Should that last v_1 be a v_1 + 1?

view this post on Zulip Reid Barton (Nov 05 2018 at 19:02):

I think it should be max u_1 v_1, if I calculated right

view this post on Zulip Reid Barton (Nov 05 2018 at 19:03):

Ah, Scott was kind enough to write out the universe parameters in instance functor.category.

view this post on Zulip Reid Barton (Nov 05 2018 at 19:03):

My guess: perhaps you are doing something where you actually need X to be a small category?

view this post on Zulip Reid Barton (Nov 05 2018 at 19:04):

it's hard to say what to do without knowing where that goal is coming from

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:04):

But in yoneda Scott is doing the same thing as I'm doing. Now I'm really confused.

variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C]
include 𝒞

def yoneda : C  ((Cᵒᵖ)  (Type v₁)) :=

view this post on Zulip Reid Barton (Nov 05 2018 at 19:05):

Sure you can write down X\op \func Type v_1, but it might not have v_1-small hom sets.

view this post on Zulip Reid Barton (Nov 05 2018 at 19:06):

Which is what your goal is asking for

view this post on Zulip Mario Carneiro (Nov 05 2018 at 19:07):

how big are the homsets of the functor category?

view this post on Zulip Scott Morrison (Nov 05 2018 at 19:08):

variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C] (D : Type u₂) [𝒟 : category.{u₂ v₂} D]
include 𝒞 𝒟

instance functor.category :
  category.{(max u₁ v₁ u₂ v₂) (max u₁ v₂)} (C ⥤ D) :=

view this post on Zulip Scott Morrison (Nov 05 2018 at 19:08):

I wrote the universe levels explicitly in the definition, as documentation for just these moments. :-)

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:09):

Thanks! I'm probably dense, but I'm still confused why Scott could write what he wrote for yoneda, and now I want to apply it and Lean complains...

view this post on Zulip Scott Morrison (Nov 05 2018 at 19:10):

The danger is always the u1 appearing the morphism universe level.

view this post on Zulip Reid Barton (Nov 05 2018 at 19:10):

Apply what how? What is the actual math?

view this post on Zulip Scott Morrison (Nov 05 2018 at 19:10):

So in Yoneda, we don't care about the universe level of the morphisms in the resulting category.

view this post on Zulip Scott Morrison (Nov 05 2018 at 19:10):

But you _do_ care.

view this post on Zulip Scott Morrison (Nov 05 2018 at 19:11):

You need a category category.{(max u₁ (v₁+1)) v₁} (Xᵒᵖ ⥤ Type v₁)

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:11):

Ooops... I crashed the machine I was logged into...

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:11):

I was working on the sheaf branch.

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:12):

https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/sheaf.lean#L41

view this post on Zulip Scott Morrison (Nov 05 2018 at 19:13):

But with category.{u1 v1} X, you're going to find Xop \func Type v1 only has a category structure with

view this post on Zulip Scott Morrison (Nov 05 2018 at 19:13):

objects in universe max u1 (v1+1) (which is fine)

view this post on Zulip Scott Morrison (Nov 05 2018 at 19:13):

and morphisms in universe max u1 v1

view this post on Zulip Scott Morrison (Nov 05 2018 at 19:14):

which breaks your constraint

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:14):

I see. So now I should convince Lean that it should be looking for a more relaxed constraint...

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:16):

First need to build mathlib on a new machine. (What is the emoji for compiling?)

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:19):

I propose :fencing: for compiling because of https://www.xkcd.com/303/

view this post on Zulip Reid Barton (Nov 05 2018 at 19:24):

I guess this is one of the points where one uses universes in a more serious way

view this post on Zulip Mario Carneiro (Nov 05 2018 at 19:26):

is this what representable functors are for?

view this post on Zulip Reid Barton (Nov 05 2018 at 19:27):

In math one could just pass to a universe in which X is a small category

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:27):

is this what representable functors are for?

They're used in the Fermat's Last Theorem proof to produce rings out of thin air.

view this post on Zulip Reid Barton (Nov 05 2018 at 19:31):

I think your options are

  • Assume X is a small_category.{v_1}
  • Have sieve take values in presheaves valued in Type (max u_1 v_1)
  • Redesign limits so that you can talk about the limit of a w-sized diagram in a category.{u v} (but I don't think this sounds like a good idea)

view this post on Zulip Reid Barton (Nov 05 2018 at 19:33):

The first two are both versions of the math "just pick a universe in which X looks small", and it's a matter of where you want to put that shift of universe

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:33):

The fpqc topology has some issues with large limits. @Johan Commelin are you planning on writing something sufficently general to deal with the fpqc topology?

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:33):

Yes.

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:33):

I want to do sheaves in the biggest generality possible.

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:33):

Conrad would argue that the fpqc topology "does not exist"

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:34):

I think I'll go for option 2.

view this post on Zulip Reid Barton (Nov 05 2018 at 19:34):

Are they actual issues or just issues for people who don't believe in universes?

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:34):

I don't fully understand the issues

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:35):

I think a little bit of both. You need to do resizing at some point. Like we were discussing kappa-small stuff a while ago.

view this post on Zulip Reid Barton (Nov 05 2018 at 19:35):

I think if you express any topology other than the Zariski one naturally in Lean it will have the same issues as the fpqc topology--otherwise you will need to manually replace your category with an essentially equivalent small one

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:35):

I do understand that the issue with an fpqc cover is that you can't make a set of all fpqc covers

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:35):

I'm not sure this is accurate Reid

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:36):

With the etale topology there is in some formal sense not a set of etale covers

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:36):

but there is a set of etale covers such that every etale cover is isomorphic to a cover in your set

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:36):

with fpqc the problem is genuinely worse

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:36):

because an arbitrary morphism of fields is fpqc

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:37):

so there is not even a set of isomorphism classes of etale covers of spec(field)

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:37):

I don't know whether thinking about things in a more universey way makes these two problems become the same

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:38):

but in ZFC I've always had the impression that they were not the same

view this post on Zulip Reid Barton (Nov 05 2018 at 19:38):

Right, that is what I mean--you would not be able to define etale covers as just "a scheme with an etale map to X", because that will live in a too large universe--you need to manually replace the category with an equivalent small one with some kind of cardinality argument

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:38):

right

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:38):

but you can't do that for fpqc

view this post on Zulip Reid Barton (Nov 05 2018 at 19:38):

right

view this post on Zulip Reid Barton (Nov 05 2018 at 19:39):

so there are two kinds of issues which could arise then

view this post on Zulip Reid Barton (Nov 05 2018 at 19:40):

one is if you don't accept the universe axiom, then you can't talk about such large collections like the category of sheaves for the fpqc topology on X at all

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:40):

I believe Conrad is strictly ZFC so rejects the fpqc topology

view this post on Zulip Reid Barton (Nov 05 2018 at 19:40):

but that's not an issue if you do accept universes

view this post on Zulip Scott Morrison (Nov 05 2018 at 19:41):

@Johan Commelin I pushed my (inconclusive) changes to the sheaf branch. Now my dog insists on a walk (in the rain).

view this post on Zulip Reid Barton (Nov 05 2018 at 19:41):

but then a second issue which might come up is: you need to take a limit of sets or something, but because the indexing diagram of the limit is large it could take you outside the category you called Set. And that is a real issue even if you believe in universes

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:46):

@Scott Morrison Thanks! I'll take a look!

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:49):

Looking through old emails I've exchanged with Conrad on the fpqc matter, he basically says "fppf is enough for everything, and anyone who wants to work with fpqc -- well, that's their problem, and they can work out the details for themselves"

view this post on Zulip Reid Barton (Nov 05 2018 at 19:54):

Another possible approach is https://ncatlab.org/nlab/show/small+presheaf

view this post on Zulip Reid Barton (Nov 05 2018 at 19:57):

I think you can also think of this as like Ind, but with no restriction on the indexing diagrams you allow

view this post on Zulip Reid Barton (Nov 05 2018 at 19:58):

However I don't know whether this is useful for applications in algebraic geometry

view this post on Zulip Reid Barton (Nov 05 2018 at 19:58):

https://ncatlab.org/nlab/show/large+site is a not particularly encouraging page

view this post on Zulip Johan Commelin (Nov 05 2018 at 20:09):

@Reid Barton Hmmzz, I'm not really making any progress...

view this post on Zulip Reid Barton (Nov 05 2018 at 20:09):

I expect you will have other problems, too :slight_smile:

view this post on Zulip Johan Commelin (Nov 05 2018 at 20:09):

/me is not designed to think about universe issues...

view this post on Zulip Johan Commelin (Nov 05 2018 at 20:10):

What do you think is the best solution for now? Making X small?

view this post on Zulip Reid Barton (Nov 05 2018 at 20:11):

certainly easiest for the time being

view this post on Zulip Reid Barton (Nov 05 2018 at 20:11):

and you don't really lose any generality

view this post on Zulip Johan Commelin (Nov 05 2018 at 20:11):

Ok, then I'll leave the headaches for the sheaves refactor that Mario will work on next summer (-;

view this post on Zulip Reid Barton (Nov 05 2018 at 20:12):

I think your next problem was going to be: you have some coproducts indexed on a Type v_1, but now the morphism size is max u_1 v_1

view this post on Zulip Reid Barton (Nov 05 2018 at 20:12):

so you would need to add some ulift to align them

view this post on Zulip Johan Commelin (Nov 05 2018 at 20:17):

You're completely right.

view this post on Zulip Johan Commelin (Nov 05 2018 at 20:18):

So I want my indexing type to be small small

view this post on Zulip Johan Commelin (Nov 05 2018 at 20:18):

In which universe should the indexing type of a covering family live?

view this post on Zulip Johan Commelin (Nov 05 2018 at 20:19):

max u_1 v_1?

view this post on Zulip Reid Barton (Nov 05 2018 at 20:19):

I thought you were going to make X small instead

view this post on Zulip Reid Barton (Nov 05 2018 at 20:19):

so u_1 = v_1

view this post on Zulip Reid Barton (Nov 05 2018 at 20:19):

if not, then I'm not sure

view this post on Zulip Johan Commelin (Nov 05 2018 at 20:22):

Yes, I am going to do that. So then I should just take u_1, right?

view this post on Zulip Reid Barton (Nov 05 2018 at 20:24):

Whatever the universe level of X is. It seems we tend to call it v in category_theory

view this post on Zulip Reid Barton (Nov 05 2018 at 20:28):

Well, or u

view this post on Zulip Johan Commelin (Nov 05 2018 at 21:01):

@Scott Morrison Wouldn't it be useful to have has_pullbacks_of_has_limits be an instance in general?

view this post on Zulip Scott Morrison (Nov 05 2018 at 21:02):

I'm afraid of doing that before we know that the pullbacks thus produced are "nice enough".

view this post on Zulip Johan Commelin (Nov 05 2018 at 21:02):

Ok, I see.

view this post on Zulip Scott Morrison (Nov 05 2018 at 21:02):

I suspect that you'll only want that instance "in desperation", when you don't have access to a construction of pullbacks that is defeq to something easier to work with than the general limit.

view this post on Zulip Johan Commelin (Nov 05 2018 at 21:03):

Hmmm, ok

view this post on Zulip Johan Commelin (Nov 05 2018 at 21:03):

So now I've made two small edits to sheaf.

view this post on Zulip Johan Commelin (Nov 05 2018 at 21:04):

Do you have a minute to look at the errors that remain? I'm very bad at fighting these universe issues.

view this post on Zulip Scott Morrison (Nov 05 2018 at 21:08):

hah, we've been duplicating effort :-)

view this post on Zulip Johan Commelin (Nov 05 2018 at 21:11):

Well, I didn't do much...

view this post on Zulip Johan Commelin (Nov 05 2018 at 21:13):

Do you think the library is ready for this? Or am I making too big a jump?

view this post on Zulip Scott Morrison (Nov 05 2018 at 21:14):

We're almost there. :-)

view this post on Zulip Scott Morrison (Nov 05 2018 at 21:14):

And this is exactly the sort of stress testing of limits that we need.

view this post on Zulip Scott Morrison (Nov 05 2018 at 21:14):

I committed a little, but it's still badly broken, and I have to get the kids to school/me to work.

view this post on Zulip Johan Commelin (Nov 05 2018 at 21:14):

Sure, those are more important than silly sheaves (-;

view this post on Zulip Johan Commelin (Nov 05 2018 at 21:15):

See you later

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 21:19):

I've just been reading SGA4 in the bath

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 21:19):

As you do

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 21:20):

And very early on when talking about limits and colimits

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 21:20):

They assume that the diagram is u-small

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 21:21):

ie isomorphic to an element of the universe u

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 21:21):

Their categories are u-categories

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 21:21):

Ie hom sets are all in u

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 21:22):

But the limits are over u-small diagrams consistently

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 21:28):

Example theorem : the category of u-abelian groups has u-limits. This means that you take the category whose objects are abelian groups in some universe, and then take a limit but only over a category which is itself an element of u

view this post on Zulip Reid Barton (Nov 05 2018 at 21:31):

That's essentially our setup too, see https://github.com/leanprover-community/mathlib/blob/limits-others-new/category_theory/limits/limits.lean#L21-L22

view this post on Zulip Johan Commelin (Nov 05 2018 at 21:39):

@Scott Morrison In things like coequalizer.desc should the argument w get an auto_param obviously?

view this post on Zulip Scott Morrison (Nov 05 2018 at 21:45):

Yes, that seems plausible.

view this post on Zulip Johan Commelin (Nov 05 2018 at 21:50):

@Scott Morrison I just pushed some more silly stuff. Didn't make fundamental progress.

view this post on Zulip Johan Commelin (Nov 06 2018 at 07:37):

@Scott Morrison I don't think functor.const should be in cones. It is more fundamental. Should this be moved to functor or something?

view this post on Zulip Scott Morrison (Nov 06 2018 at 07:58):

Sounds good.

view this post on Zulip Reid Barton (Nov 10 2018 at 17:08):

@Johan Commelin did you ever find a setup for typing the functor arrow in emacs?

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:04):

Nah, haven't looked into it yet. Sorry. Maybe some other emacs user can tell us how to fix this. @Sebastian Ullrich ?

view this post on Zulip Gabriel Ebner (Nov 10 2018 at 18:21):

The input abbreviations for emacs are defined here: https://github.com/leanprover/lean-mode/blob/9d6b8471e2044310b4cd7cd3213b1fc8f78ec499/lean-input.el#L407 It should be straightforward to submit a PR adding the new arrows (you might also want to add Scott's calligraphic symbols).

view this post on Zulip Gabriel Ebner (Nov 10 2018 at 18:25):

These are the relevant changes in the vscode extension:
\McB, etc. https://github.com/leanprover/vscode-lean/commit/46ef6b277f4b90ef440730e3b2f73f9381aa08b0#diff-7c2385f0b8db521fe81e3d20489e5f12
\bbA, etc. https://github.com/leanprover/vscode-lean/commit/0080ed0f7c80b199abf31212a7eb9356d3cbc896#diff-7c2385f0b8db521fe81e3d20489e5f12
\functor https://github.com/leanprover/vscode-lean/commit/d3988d9fae1ab4a7e4785486a08c5eddcd33c575#diff-7c2385f0b8db521fe81e3d20489e5f12

view this post on Zulip Gabriel Ebner (Nov 10 2018 at 18:25):

In the long term, we might want to have a common source for these abbreviations that is shared by the editor extensions.

view this post on Zulip Johan Commelin (Nov 10 2018 at 18:25):

@Gabriel Ebner Thanks a lot for the links! Once I find some time, I hope to add a PR.

view this post on Zulip Johan Commelin (Nov 15 2018 at 13:04):

Do we know that composition of functors is associative? I can't find it...

view this post on Zulip Reid Barton (Nov 15 2018 at 13:07):

I don't think so, but it is true by defeq at least

view this post on Zulip Johan Commelin (Nov 15 2018 at 13:11):

I see. So I guess this should be added sooner rather than later.

view this post on Zulip Scott Morrison (Nov 15 2018 at 19:56):

It's in lean-category-theory, under functor_categories/isomorphisms.lean.

view this post on Zulip Scott Morrison (Nov 15 2018 at 19:56):

At least -- it constructs the equality as a natural isomorphism.

view this post on Zulip Scott Morrison (Nov 15 2018 at 19:56):

I thought it would be good to also prove the the unitors and associator for functors satisfy the triangles and pentagon equations, but didn't do that.

view this post on Zulip Scott Morrison (Nov 15 2018 at 20:45):

@Johan Commelin, it turned out this was easy to do, so there's a new PR adding unitors and associators for functors, as well as checking the pentagon and triangle. (These will be necessary one day when we want an example of a 2-category!)

view this post on Zulip Johan Commelin (Nov 16 2018 at 05:35):

@Scott Morrison @Reid Barton I have a question about yoneda. I find the yoneda.lean file a bit confusing. Is there an easy way to extract that F.obj U is canonically the same as yoneda.obj ⟹ F, where U : X and F : presheaf X? Or is this something that we have to add to this file?

view this post on Zulip Reid Barton (Nov 16 2018 at 05:42):

In the adjunctions branch I just sort of ignored most of the contents of yoneda.lean and added an equiv which I could actually understand

view this post on Zulip Reid Barton (Nov 16 2018 at 05:42):

though I feel this approach isn't ideal either

view this post on Zulip Johan Commelin (Nov 16 2018 at 08:09):

@Scott Morrison I don't think this is in your Yoneda file in an equivalent form, is it?

@[simp] lemma yoneda_sections (U : X) (F : presheaf X) :
(yoneda.obj U  F)  F.obj U :=
{ hom := show (yoneda.obj U  F)  (F.obj U), from λ α, α.app U (𝟙 U),
  inv := show F.obj U  yoneda.obj U  F, from λ s,
  { app := λ V, show _  F.obj V, from λ i, F.map i s,
    naturality' := λ V₁ V₂ i, by tidy; erw F.map_comp; tidy },
  hom_inv_id' :=
  begin
    ext α V i,
    tidy {trace_result := tt},
    have := congr (α.naturality i),
    dsimp at this,
    erw (this rfl),
    simp
  end,
  inv_hom_id' := by tidy; erw F.map_id; tidy }

That hom_inv_id' is particularly nasty. Would tidy + rewrite_search be able to deal with that?

view this post on Zulip Scott Morrison (Nov 16 2018 at 08:16):

No, we've already got this. This iso is just a component of the natural isomorphism produced in yoneda_lemma.

view this post on Zulip Scott Morrison (Nov 16 2018 at 08:16):

@[simp] lemma yoneda_sections (X : C) (F : Cᵒᵖ ⥤ Type v₁) : (yoneda.obj X ⟹ F) ≅ ulift.{u₁} (F.obj X) :=
nat_iso.app (yoneda_lemma C) (X, F)

view this post on Zulip Scott Morrison (Nov 16 2018 at 08:16):

should do it.

view this post on Zulip Scott Morrison (Nov 16 2018 at 08:17):

If you're already working in a small category you can remove the ulift.

view this post on Zulip Scott Morrison (Nov 16 2018 at 08:18):

yoneda_lemma is the natural isomorphism between the two functors starting with (X, F). You can either embed X into presheafs, via the yoneda embedding, and then take hom, or you can just evaluate F on X.

view this post on Zulip Scott Morrison (Nov 16 2018 at 08:25):

And

omit 𝒞
def ulift_trivial (V : Type u₁) : ulift.{u₁} V ≅ V := by tidy

@[simp] def yoneda_sections_small {C : Type u₁} [small_category C] (X : C) (F : Cᵒᵖ ⥤ Type u₁) : (yoneda.obj X ⟹ F) ≅ F.obj X :=
nat_iso.app (yoneda_lemma C) (X, F) ≪≫ ulift_trivial _

gives you the version you want, for small categories.

view this post on Zulip Scott Morrison (Nov 16 2018 at 08:25):

Shall I just push this as a separate PR?

view this post on Zulip Scott Morrison (Nov 16 2018 at 08:26):

Sorry, it was an obvious omission in writing yoneda.lean, just writing out the main result in components.

view this post on Zulip Scott Morrison (Nov 16 2018 at 08:53):

This is available at https://github.com/leanprover/mathlib/pull/480.

view this post on Zulip Scott Morrison (Nov 16 2018 at 08:53):

It depends on the limits PR, because it's not worth backporting, but you're welcome to merge into the sheaf branch.

view this post on Zulip Johan Commelin (Nov 16 2018 at 16:18):

@Scott Morrison Ok cool! I kept on struggling with that product category. But this looks really nice!

view this post on Zulip Johan Commelin (Nov 17 2018 at 07:46):

@Scott Morrison Is iso_of_is_iso missing in the library?

view this post on Zulip Scott Morrison (Nov 17 2018 at 07:46):

Yes, lots of iso stuff is missing, that I've just been discovering now. :-)

view this post on Zulip Scott Morrison (Nov 17 2018 at 07:46):

I've been filling it in the monoidal categories repository, which is where I need it immediately.

view this post on Zulip Scott Morrison (Nov 17 2018 at 07:47):

Is it holding you up? I can make yet another PR to mathlib with some improvements to the iso and is_iso interface.

view this post on Zulip Johan Commelin (Nov 17 2018 at 07:49):

def iso_of_is_iso {X Y : C} {f : X  Y} (h : is_iso f) : X  Y :=
{ hom := f,
  ..h}

That's whay I have at the top of my file now.

view this post on Zulip Scott Morrison (Nov 17 2018 at 07:50):

Ok, if that's keeping you afloat for now, I'll finish up a few things before making a "fixing isos" PR. It turns out there are at least a dozen other things missing too. :-)

view this post on Zulip Scott Morrison (Nov 17 2018 at 07:51):

As I'm sure Mario has told us many times before, you actually have to use this stuff!

view this post on Zulip Johan Commelin (Nov 17 2018 at 08:29):

@Scott Morrison I just pushed a whole bunch of stuff to the sheaf branch. If you want more data points for how stuff is used...

view this post on Zulip Johan Commelin (Nov 17 2018 at 08:29):

I'm gathering stuff that should move elsewhere at the top of the file. If it fits into PRs that you are preparing, please take it.

view this post on Zulip David Michael Roberts (Nov 20 2018 at 23:42):

I do understand that the issue with an fpqc cover is that you can't make a set of all fpqc covers

The issue is that there is not even a set of fpqc covers whose elements refine all possible fpqc covers, whereas for fppf and coarser this is true, even when there's not a set of isomorphism classes of covers. This is a genuine problem, and there is a model of ZF whose category of sets forms a large site with this 'feature' (with covers=surjective functions).

view this post on Zulip David Michael Roberts (Nov 20 2018 at 23:44):

One can of course consider whether a given presheaf is a fpqc sheaf or not, but forget trying to fpcq-sheafify in general. The hypotheses of the general adjoint functor theorem are not satisfied, so one cannot construct the left adjoint to Sh_fpqc(Aff) --> PreSh(Aff).

view this post on Zulip Johan Commelin (Nov 27 2018 at 14:10):

I currently have

@[simp] lemma map_left_id : map_left R (nat_trans.id L)  functor.id _ :=
{ hom :=
  { app := λ X, { left := 𝟙 _, right := 𝟙 _ } },
  inv :=
  { app := λ X, { left := 𝟙 _, right := 𝟙 _ } } }

but that is a worthless simp-lemma because of . I think that in fact equality should hold:

@[simp] lemma map_left_id' : map_left R (nat_trans.id L) = functor.id _ := sorry

But I have no idea how to prove that two terms of a structure are equal. Is it true that they are equal if all their fields are equal? Is this somewhere in mathlib?

view this post on Zulip Reid Barton (Nov 27 2018 at 14:13):

This is generally what extensionality lemmas do... but you're probably going to have a bad time working with equality of functors

view this post on Zulip Reid Barton (Nov 27 2018 at 14:14):

what's map_left?

view this post on Zulip Reid Barton (Nov 27 2018 at 14:15):

Never mind, I figured it out from one of your other messages

view this post on Zulip Patrick Massot (Nov 27 2018 at 14:16):

Not sure it will help, but your question looks like the classic:

structure johan :=
(a : )
(aone : a = 1)

lemma johan.ext (X Y : johan) (h : X.a = Y.a) : X = Y :=
begin
  cases X,
  cases Y,
  congr ; assumption
end

view this post on Zulip Patrick Massot (Nov 27 2018 at 14:17):

sorry about the silly example, but I wanted a structure including at least one data and one proof field

view this post on Zulip Johan Commelin (Nov 27 2018 at 14:19):

@Patrick Massot Thanks, I should have thought about cases.

view this post on Zulip Reid Barton (Nov 27 2018 at 14:19):

I think what you have now is the best way

view this post on Zulip Johan Commelin (Nov 27 2018 at 14:19):

@Reid Barton Well, but working with natural isomorphisms is also a massive pain atm.

view this post on Zulip Reid Barton (Nov 27 2018 at 14:21):

I guarantee it is not as bad as rewriting morphisms across equalities of objects and then trying to reason about the result

view this post on Zulip Patrick Massot (Nov 27 2018 at 14:23):

We should really setup a FAQ somewhere

view this post on Zulip Johan Commelin (Nov 27 2018 at 19:48):

@Scott Morrison I have no idea if this makes any sense, but I regularly get errors like these:

type mismatch at application
  colimit.pre_map (comma.fst yoneda (functor.of_obj X)  F) ((comma.map_right_id' yoneda (functor.of_obj X)).hom)
term
  (comma.map_right_id' yoneda (functor.of_obj X)).hom
has type
  comma.map_right yoneda (𝟙 (functor.of_obj X))  functor.id (comma yoneda (functor.of_obj X)) : Type (max
        (max ? v)
        v
        ?)
but is expected to have type
  ?m_3  ?m_4 : Type v

Would it help to just get rid of the notation , and always speak of natural transformations as homs in the functor category?

view this post on Zulip Johan Commelin (Nov 27 2018 at 19:48):

Or is this a stupid universe issue again? (I just realise there are annoying ? in the error...)

view this post on Zulip Johan Commelin (Nov 27 2018 at 19:50):

Ok, never mind. It's a universe issue.

view this post on Zulip Kenny Lau (Nov 27 2018 at 20:20):

@Johan Commelin how do you get that many colours

view this post on Zulip Johan Commelin (Nov 27 2018 at 20:22):

I had less syntax, instead of lean :upside_down: @Kenny Lau

view this post on Zulip Scott Morrison (Nov 27 2018 at 20:40):

I guarantee it is not as bad as rewriting morphisms across equalities of objects and then trying to reason about the result

Yes. This. Please don't prove equalities between functors, you are just setting yourself up for suffering.

view this post on Zulip Reid Barton (Nov 27 2018 at 21:50):

Would it help to just get rid of the notation , and always speak of natural transformations as homs in the functor category?

I have actually wondered about this too, after a few minor annoyances involving the difference between nat_trans.vcomp and category.comp.

view this post on Zulip Reid Barton (Nov 27 2018 at 21:50):

It's hard to predict which one you will get once you start talking about colimits in categories of presheaves, as Johan has probably also experienced.

view this post on Zulip Reid Barton (Nov 27 2018 at 21:57):

It might be a rather invasive change though, or even not workable for some reason

view this post on Zulip Scott Morrison (Nov 27 2018 at 22:33):

I've experienced the same pain, but haven't tried removing . It seems a reasonable experiment, however.

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:12):

I don't like the idea of setting myself up for suffering.

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:12):

But I'm suffering hard at the moment.

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:13):

After all functor.id ⋙ F is not defeq to F, and so we need some natural isomorphisms, and I just get the general feeling that we are walking headfirst into nasty 2-categorical territory.

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:14):

Because, say what you like, but Lean isn't very good at working with the canonical natural isomorphism between functor.id ⋙ F and F.

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:15):

I've got the following context:

C : Type v,
𝒞 : small_category C,
D : Type u,
𝒟 : category D,
F : C  D,
_inst_1 : has_colimits D,
X : presheaf C
 colimit.pre (comma.fst yoneda (functor.of_obj X)  F) (comma.map_right yoneda (𝟙 (functor.of_obj X))) =
    𝟙 (colimit (comma.fst yoneda (functor.of_obj X)  F))

This might look a bit daunting, but (comma.map_right yoneda (𝟙 (functor.of_obj X))) is naturally isomorphic to functor.id _

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:16):

@Scott Morrison I'm really lost here. The maths is trivial. But Lean is fighting back hard.

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:27):

Want to point me to a file and a commit?

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:30):

@Scott Morrison https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/presheaf.lean#L69

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:31):

Maybe I still don't know how to let the library do the heavy lifting for me...

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:38):

woah, checking out that branch is like stepping into the future. adjunctions, cocompletions, groupoids, oh my.

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:40):

Well, most of that is by Reid.

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:41):

Or I should say: all of that is by Reid.

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:43):

Can we not call functors f, when they could perfectly well be F?

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:44):

Also, I feel you're slightly overusing variables. Things like map and map' should have the variable F : C \func D visible right there at the definition.

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:45):

variables are great for implicit arguments, or even the primary argument if they are the sole primary argument for 20 definitions in a row...

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:45):

Sure. I was using F for presheaves, but I decided that maybe I shouldn't yet do that.

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:47):

Anyway, you shouldn't look too much at the sheaf.lean file. It will need a major rewrite once I have working presheaves.

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:49):

Lots of stuff doesn't compile?

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:49):

In the imports of presheaf.lean

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:50):

Hmmm... I thought those were fine... but maybe stuff broke.

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:50):

e.g. limits/limits.lean and adjunctions.lean

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:51):

adjunctions probably don't compile

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:51):

limits should work, but maybe it broke after I merged in Reid's branch

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:51):

Ok, I see the thing you probably need, which is naturality in the second argument of colimit.pre

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:51):

I can try to provide you that, and you can try to get stuff to compile :-)

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:53):

Ok, so I have colimit.pre_map

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:53):

yes, but that's naturality in the first argument, which isn't what you need

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:53):

But I guess we need to upgrade pre into a functor?

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:53):

unfortunately I think that might need to wait for 2-categories, I'm not sure. :-)

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:54):

Right... but it is where this stuff is sucking us into, not?

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:54):

I'm actually not sure where I should do this work. The main limits branch is now a bit stranded, as Reid has been pulling stuff out into separate PRs.

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:54):

Doing work on the limits branch now may get orphaned, I'm not sure.

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:54):

Maybe dump it into sheafy_preamble

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:55):

I've been using that file to collect all sorts of facts that I need.

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:56):

Yeah, I'm worried about that getting orphaned too. :-)

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:56):

We're playing a bit fast and loose with our branches at the moment.

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:56):

Very much.

view this post on Zulip Johan Commelin (Nov 28 2018 at 08:57):

So what exactly is the statement that you are trying to prove?

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:57):

@Reid Barton, I'd really like to straighten out the limits branches a bit. What is the best way to "rebase" (possibly by hand) everything remaining on top of limits-2? Is this a bad thing to want to do?

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:58):

No idea :-) I hadn't even started.

view this post on Zulip Scott Morrison (Nov 28 2018 at 08:59):

Say we have a natural transformation a : E \natt E'.

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:00):

colim.map (a >>> F) gives a map from colim (E >>> F) to colim (E' >>> F)

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:00):

presumably the triangle, obtained by mapping both of those to colim F via colim.pre, commutes?

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:01):

So then if a is invertible, we have colim.pre F E = colim.map (a^{-1} >>> F) >> colim.pre F E' >> colim.map (a >>> F).

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:02):

and hopefully now if E' is the identity, as in your case, everything quickly simplifies from there

view this post on Zulip Johan Commelin (Nov 28 2018 at 09:03):

So pre_map is saying that this triangle commutes.

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:04):

No. pre_map is about changing the functor F, not the functor E.

view this post on Zulip Johan Commelin (Nov 28 2018 at 09:04):

But if E' = functor.id _ it still doesn't simplify, because functor.id _ >>> F is not F. For example colimit.pre F (functor.id _) = \b1 (colimit F) does not typecheck :sad:

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:04):

I've just been looking at the history of the sheaf branch.

view this post on Zulip Johan Commelin (Nov 28 2018 at 09:05):

@Scott Morrison I think you are confusing map_pre and pre_map.

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:05):

And ... you're up shit creek without a paddle. :-)

view this post on Zulip Johan Commelin (Nov 28 2018 at 09:05):

pre_map is something I added. It is in sheafy_preamble.lean

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:05):

Getting sheaf back on top of master after limits-2 is merged is going to suck.

view this post on Zulip Johan Commelin (Nov 28 2018 at 09:06):

@Scott Morrison I will probably just copy-paste stuff into a new branch...

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:06):

I'm looking at

lemma colimit.pre_map {K : Type v} [small_category K] [has_colimits_of_shape K C] (E : K ⥤ J) :
  colimit.pre F E ≫ colim.map α = colim.map (whisker_left E α) ≫ colimit.pre G E :=
by ext; rw [←assoc, colimit.ι_pre, colim.ι_map, ←assoc, colim.ι_map, assoc, colimit.ι_pre]; refl

in limits-2.

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:07):

I see. But yes, your pre_map is what we need. :-)

view this post on Zulip Johan Commelin (Nov 28 2018 at 09:07):

Aaahrg... so the names have changed...

view this post on Zulip Johan Commelin (Nov 28 2018 at 09:08):

What is called pre_map in limits-2 used to be map_pre on your old limits branch.

view this post on Zulip Johan Commelin (Nov 28 2018 at 09:08):

Ok, so in presheaf.lean you can see that I already erwd the pre_map-thingy.

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:08):

I see. :-) Reid must have fixed it. :-) As I said, up a creek! :-)

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:08):

Well, I can't see that, because nothing compiles. :-)

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:09):

So, you need to keep the colim.map in there for the unitor.

view this post on Zulip Johan Commelin (Nov 28 2018 at 09:09):

Sorry, I need to run to a seminar...

view this post on Zulip Johan Commelin (Nov 28 2018 at 09:10):

And I'm sorry that stuff doens't compile. I still have some sort of interactive VScode when I work on this...

view this post on Zulip Johan Commelin (Nov 28 2018 at 09:10):

Maybe I should just wait till limits are merged, and then start from scratch.

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:10):

You just want to know that

colimit.pre F (functor.id _) = colimit.map (left_unitor F)

(that's not meant to be real code).

view this post on Zulip Scott Morrison (Nov 28 2018 at 09:12):

Okay, in any case, keep bugging me about this. I'd both like to help, and like to see the resolution. I think it's going to be fine. :-)

view this post on Zulip Johan Commelin (Nov 28 2018 at 11:06):

@Scott Morrison Thanks for all your comments. I'll see if I can make any progress.

view this post on Zulip Reid Barton (Nov 28 2018 at 12:46):

Oh yeah, I noticed all the limit. lemmas had names of the form limit.foo_bar if the left-hand side looked like limit.foo ... >> limit.bar ..., and so I reversed the components of all the names of the corresponding colimit lemmas because they have the composition on the left-hand side in the other order.

view this post on Zulip Reid Barton (Nov 28 2018 at 12:47):

Actually I just copied and pasted the limit lemmas to make colimit versions, I ignored whatever was there before (which I think was not a full set of matching lemmas)

view this post on Zulip Johan Commelin (Nov 28 2018 at 12:51):

@Scott Morrison I fixed a bunch of compile issues, which we due to functor.const being picked from the wrong namespace (even though category_theory seems to be open). I really hope Lean 4 will kick a lot of these things out of the root namespace, because these conflicts are quite annoying.

view this post on Zulip Reid Barton (Nov 28 2018 at 12:52):

Yeah I encountered that same functor.const issue too, not sure what caused it to crop up suddenly

view this post on Zulip Keeley Hoek (Nov 28 2018 at 12:55):

Does @[priority] affect that kind of resolution?

view this post on Zulip Reid Barton (Nov 28 2018 at 13:18):

I can try to produce a rebased version of my adjunctions branch, that shouldn't take too long.

view this post on Zulip Reid Barton (Nov 28 2018 at 13:48):

It looks like Johan has mostly just been working on one file, so probably easiest to just copy the sheaf branch into a new branch indeed

view this post on Zulip Reid Barton (Nov 28 2018 at 13:53):

Oh, also the specific shape limit stuff isn't in limits-2 yet. I do have a copy that at least builds on top of limits-2 though, so I can push that somewhere as a temporary measure for you, Johan

view this post on Zulip Johan Commelin (Nov 28 2018 at 13:54):

Ooh, don't worry too much about this

view this post on Zulip Johan Commelin (Nov 28 2018 at 13:55):

I think it's best to fix it after limits-2 is merged.

view this post on Zulip Reid Barton (Nov 28 2018 at 13:59):

Ah, fair enough. I'll hold off on these things then

view this post on Zulip Johan Commelin (Nov 28 2018 at 15:48):

I'm very confused about https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/commas.lean#L155-L156
I thought I understood rfl by now. But apparently this is not rfl. If someone can explain this mystery, I would be very grateful.

view this post on Zulip Gabriel Ebner (Nov 28 2018 at 15:51):

map_right_id' should be a def. Theorems don't unfold (except for special circumstances / options).

view this post on Zulip Johan Commelin (Nov 28 2018 at 15:52):

Aaah, it should certainly be a def. Let me try again.

view this post on Zulip Johan Commelin (Nov 28 2018 at 15:53):

@Gabriel Ebner Cool! Now it works.

view this post on Zulip Kevin Buzzard (Nov 28 2018 at 17:12):

Computer scientists have such weird ideas about what a theorem is :-)

view this post on Zulip Johan Commelin (Nov 28 2018 at 17:25):

@Scott Morrison @Reid Barton I suggest we replace of_obj with of.obj after defining

namespace functor
variables {C : Type u} [𝒞 : category.{u v} C]
include 𝒞

def of : C  (punit  C) := const punit

namespace of
@[simp] lemma obj_obj (X : C) : (of.obj X).obj = λ _, X := rfl
@[simp] lemma obj_map (X : C) : (of.obj X).map = λ _ _ _, 𝟙 X := rfl
@[simp] lemma map_app {X Y : C} (f : X  Y) : (of.map f).app = λ _, f := rfl
end of

end functor

Is that ok?

view this post on Zulip Reid Barton (Nov 28 2018 at 17:28):

Yes, that seems sensible

view this post on Zulip Reid Barton (Nov 28 2018 at 22:27):

@Scott Morrison I fixed a bunch of compile issues, which we due to functor.const being picked from the wrong namespace (even though category_theory seems to be open). I really hope Lean 4 will kick a lot of these things out of the root namespace, because these conflicts are quite annoying.

If someone could track this down, it would be super helpful. I'm not sure what changed here.

view this post on Zulip Johan Commelin (Nov 30 2018 at 13:33):

@Reid Barton @Scott Morrison Do you think we need something like this? I find it extremely annoying that Lean refuses some of my morphisms because the come from an opposite category. I understand why Lean complains, but getting it to accept the arrow is extremely annoying. This might help...

namespace category.hom
variables {C : Type u} [𝒞 : category.{u v} C]
include 𝒞

def op {X Y : C} (f : X  Y) : @category.hom _ category_theory.opposite Y X := f
def deop {X Y : Cᵒᵖ} (f : X  Y) : @category.hom _ 𝒞 Y X := f

@[simp] lemma op_deop {X Y : C} (f : X  Y) : f.op.deop = f := rfl
@[simp] lemma deop_op {X Y : Cᵒᵖ} (f : X  Y) : f.deop.op = f := rfl

end category.hom

view this post on Zulip Scott Morrison (Nov 30 2018 at 23:51):

This sounds fine to me. I agree dealing with opposites is gross. :-(

view this post on Zulip Johan Commelin (Dec 03 2018 at 15:38):

@Reid Barton Have you had similar experiences? What is your opinion on my proposed solution?

view this post on Zulip Scott Morrison (Dec 04 2018 at 09:55):

Hi @Johan Commelin, I am experimenting with making op irreducible, and thus _requiring_ the use of op or deop (and corresponding op_obj and deop_obj on objects).

view this post on Zulip Scott Morrison (Dec 04 2018 at 09:55):

It is slightly grosser, but I think we've all discovered that too much can go mysteriously wrong with the current implementation of opposites.

view this post on Zulip Johan Commelin (Dec 04 2018 at 10:00):

@Scott Morrison Aah, that sounds like a good idea!

view this post on Zulip Johan Commelin (Dec 04 2018 at 10:01):

I hadn't thought about making it irreducible. Those boundaries are useful, but I'm not yet aware of how to make the system help us.

view this post on Zulip Johan Commelin (Dec 04 2018 at 10:01):

So yes, I think it is very good if we have to be explicit about oping and deoping.

view this post on Zulip Scott Morrison (Dec 04 2018 at 11:30):

#510

view this post on Zulip Johan Commelin (Dec 04 2018 at 11:53):

@Scott Morrison Looks good to me. I do wonder if we can remove the _obj suffix to make things a bit shorter. We could rename the existing op to op_cat.

view this post on Zulip Johan Commelin (Dec 04 2018 at 11:53):

I think this is a good PR, but I regret that a lot of stuff is also becoming somewhat uglier.

view this post on Zulip Kevin Buzzard (Dec 11 2018 at 16:53):

@Ramon Fernandez Mir is making me engage with the category theory stuff! Is there a name for this map: (λ f r, f r : (FF.obj x ⟶ FF.obj y) → (FF.obj x → FF.obj y)) ? I'm changing a long arrow to a short one. The target of the functor FF is the category CommRing, so I want to take an abstract element of the hom set and actually produce the ring hom. There's a coercion that does it magically, but I actually have a set of abstract homs and want a set of concrete homs and I have to feed set.image something.

view this post on Zulip Johan Commelin (Dec 11 2018 at 17:18):

@Kevin Buzzard Could you provide slightly more context? I typically get away without doing anything.

view this post on Zulip Kevin Buzzard (Dec 11 2018 at 17:26):

We had a functor FF from a small category J to CommRing and two objects x and y of J, and we wanted the set of maps from FF(x)FF(x) to FF(y)FF(y) coming from J.

view this post on Zulip Johan Commelin (Dec 11 2018 at 17:28):

I see, and FF.obj x \hom FF.obj y is a subtype, but you want a set?

view this post on Zulip Johan Commelin (Dec 11 2018 at 17:28):

Is that correct? If so, I think subtype.val would be the function you are looking for.

view this post on Zulip Johan Commelin (Dec 11 2018 at 17:29):

I don't know by heart how CommRing is defined.

view this post on Zulip Kevin Buzzard (Dec 11 2018 at 17:31):

I'm trying to get from category_theory.category.hom R S to R -> S

view this post on Zulip Kevin Buzzard (Dec 11 2018 at 17:32):

I can just evaluate a term of type category_theory.category.hom R S at r and get s : S

view this post on Zulip Kevin Buzzard (Dec 11 2018 at 17:34):

but I was wondering what the name of the coercion was, because I needed to refer to the map itself when doing something else.

view this post on Zulip Johan Commelin (Dec 11 2018 at 17:55):

@Kevin Buzzard On line 90 of category.lean you can find

{ hom   := λa b, subtype (hom a.2 b.2),

(This is in the instance of concrete_category --> category.) So the map you want is called subtype.val.

view this post on Zulip Reid Barton (Dec 11 2018 at 18:13):

I think there is (or should be?) some more high-level name for this, like forget

view this post on Zulip Johan Commelin (Dec 11 2018 at 18:26):

@Kevin Buzzard That's right. As Reid mentioned, there is a forgetful functor. You will have to

import category_theory.types

view this post on Zulip Reid Barton (Dec 11 2018 at 18:29):

Ah that's where it is

view this post on Zulip Reid Barton (Dec 14 2018 at 05:15):

@Kevin Buzzard did you end up using forget? I'm inclined to make its "C" argument implicit, would that help or hurt you?

view this post on Zulip Kevin Buzzard (Dec 14 2018 at 06:51):

I didn't do anything. I was talking about it with Ramon at our last meeting and haven't thought about it since

view this post on Zulip Kevin Buzzard (Dec 14 2018 at 06:52):

I am completely snowed under with teaching and reference writing

view this post on Zulip Ramon Fernandez Mir (Dec 23 2018 at 19:05):

@Reid Barton sorry I just saw this. I was playing with that code a few days ago and I didn't manage to make it work with forget. What is the "C" argument meant to be?

view this post on Zulip Gun Pinyo (Aug 07 2019 at 21:23):

In https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/category.lean,
Could anyone tells me why objects are not a field but a parameter to the definition of category? What is the advantage of it? Also, why the definition of a category is a class rather than an ordinary structure?

view this post on Zulip Kenny Lau (Aug 07 2019 at 21:24):

It allows us to say that the "set" of all groups have a category structure on it

view this post on Zulip Kenny Lau (Aug 07 2019 at 21:24):

so given two groups G and H, Lean can infer what G \hom H means

view this post on Zulip Kenny Lau (Aug 07 2019 at 21:25):

structure instances can't be automatically inferred

view this post on Zulip Gun Pinyo (Aug 07 2019 at 21:30):

Ok, but what if want to say something like "let C be a category" I need to explicitly state its object and become "let C be a category that has objects as blah". I find this quite wired.

I know that this can be solved using Σ obj : Type*, category obj but this is a little bit ad-hoc, does mathlib has a definition for this?

view this post on Zulip Kenny Lau (Aug 07 2019 at 21:31):

Let X be a type that has a category structure C on it

view this post on Zulip Gun Pinyo (Aug 07 2019 at 21:38):

This way of defining a category really see a category as an underlining structure of some type. However, many interesting categories focus more on the morphism whereas object carries almost no information e.g. the category of simplexes in which I believe that it has type as category ℕ.

view this post on Zulip Kenny Lau (Aug 07 2019 at 21:39):

This is an interesting example.

view this post on Zulip Kenny Lau (Aug 07 2019 at 21:40):

I don't know what to do with it.

view this post on Zulip Scott Morrison (Aug 07 2019 at 21:49):

You just do something like def \Delta := \nat, and then instance : category \Delta. This is what type synonyms are for.

view this post on Zulip Scott Morrison (Aug 07 2019 at 21:49):

But yes, my initial starts on the category theory library did use bundled categories.

view this post on Zulip Scott Morrison (Aug 07 2019 at 21:50):

The payoff, which has not yet been realised in mathlib, of using unbundled categories is that it would allow us to use uniform notation \iso, \hom, \otimes etc across all examples.

view this post on Zulip Scott Morrison (Aug 07 2019 at 21:51):

Mostly this hasn't happened because the category theoretic notion of iso between rings, say, would only allow talking about isomorphisms between rings in the same universe.

view this post on Zulip Scott Morrison (Aug 07 2019 at 21:51):

This distinction matters, I think for equiv (rather than just using iso in category Type), where it's pretty common to want to shift universes.

view this post on Zulip Scott Morrison (Aug 07 2019 at 21:52):

On the other hand it's rare that one deals with isomorphisms of rings in different universes.

view this post on Zulip Scott Morrison (Aug 07 2019 at 21:52):

(but it does happen, sure)

view this post on Zulip Scott Morrison (Aug 07 2019 at 21:53):

If I were king, I'd use iso instead of mul_equiv, algebra_equiv, homeomorphism, etc. etc., and even use iso in Type, adding an extra pequiv for talking about equivalences that cross universe levels.

view this post on Zulip Scott Morrison (Aug 07 2019 at 21:54):

@Gun Pinyo, there is src/category_theory/Cat.lean, which defines bundled categories in mathlib, although doesn't do very much with them.

view this post on Zulip Kevin Buzzard (Aug 07 2019 at 22:49):

(but it does happen, sure)

Why do you say this? In maths I never leave Type. This universe polymorphism is just something which the CS people want to make us use and this is one point where it adds to the confusion.

view this post on Zulip Mario Carneiro (Aug 08 2019 at 00:05):

Is Cat a category? If so, you aren't working in Type

view this post on Zulip Mario Carneiro (Aug 08 2019 at 00:07):

Maybe that's not the best example, but Type (u+1) makes several appearances in mathlib

view this post on Zulip Mario Carneiro (Aug 08 2019 at 00:08):

Perhaps you don't think it's important to have ordinals or cardinals or surreals or a model of ZFC

view this post on Zulip Mario Carneiro (Aug 08 2019 at 00:13):

Probably the only one of those you use regularly are cardinals. Of course there are ways to do cardinals in ZFC as well, but the question is not whether it's possible but whether it is easy to work that way. Jeremy told me today that he believes that FLT can probably be proven in primitive recursive arithmetic (PRA), a weak subsystem of Peano arithmetic, but such a proof would obviously look almost unrecognizable compared to Wiles' proof

view this post on Zulip Gun Pinyo (Aug 08 2019 at 00:18):

You just do something like def \Delta := \nat, and then instance : category \Delta. This is what type synonyms are for.

Well, def \Delta := \nat is the abuse of notation, what if I want to define the category of cubes then I should do def \square := \nat then suddenly we have \Delta = \square which shouldn't be true.

view this post on Zulip Gun Pinyo (Aug 08 2019 at 00:26):

@Scott Morrison If the advantage of unbundled categories couldn't be used in practice, should we go back and use bundled one (as the main def) as before?

view this post on Zulip Scott Morrison (Aug 08 2019 at 01:35):

@Gun Pinyo, I don't think you should think of that as abuse of notation. It is used all over mathlib, and is just part of how typeclasses are used in dependent type theory. After building the API for \Delta or for \square, one should then mark \Delta as [irreducible], preventing people from seeing the implementation detail that it is definitionally equal to nat.

view this post on Zulip Scott Morrison (Aug 08 2019 at 01:35):

I don't think that the advantages of unbundled categories can't be used in practice, we're just not there yet. :-)

view this post on Zulip Scott Morrison (Aug 08 2019 at 01:36):

The algebraists are currently busy bundling ring homs and similar gadgets, and this actually makes it easier to use the uniform notions provided by the the category theory library.

view this post on Zulip Scott Morrison (Aug 08 2019 at 01:37):

@Kevin Buzzard

Why do you say this? In maths I never leave Type.

So let's get rid of ring_equiv and friends... :-) If you're happy not being able to change universe levels across a ring_equiv, there's not much advantage over just using the uniform iso.

view this post on Zulip Scott Morrison (Aug 08 2019 at 01:39):

There is the point that in an iso you need to explicitly say that both directions are ring homomorphisms, while the default constructor of ring_equiv only asks that you prove this in one direction, but solving this is just a tiny bit of plumbing. (i.e. we can provide an alternative constructor for isomorphisms of rings, etc)

view this post on Zulip Johan Commelin (Aug 08 2019 at 05:20):

@Gun Pinyo Just for the record, I think that @Johannes Hölzl also developped some stuff with cubes. In particular he had a definition of cubical homology, I think. @Johannes Hölzl do you still have this code somewhere?

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

import category_theory.natural_isomorphism category_theory.limits.limits

open category_theory category_theory.limits

universes v u

example (C : Type u) [𝒞 : category.{v} C] [has_limits.{v} C] (J : Type v) [small_category J] (F G : J  C)
  (h : F  G) : limit F  limit G :=
begin
  sorry
end

Is that true? [remark: in my application, F and G are equal but not defeq :-/ ]

view this post on Zulip Kenny Lau (Dec 23 2019 at 06:13):

import category_theory.natural_isomorphism category_theory.limits.limits

open category_theory category_theory.limits

universes v u

example (C : Type u) [𝒞 : category.{v} C] [has_limits.{v} C] (J : Type v) [small_category J] (F G : J  C)
  (h : F  G) : limit F  limit G :=
{ hom := limit.lift G limit F, λ X, limit.π F X  h.1.1 X, λ X Y f, by simp; rw [ limit.w F f, category.assoc, h.1.2 f]; obviously,
  inv := limit.lift F limit G, λ X, limit.π G X  h.2.1 X, λ X Y f, by simp; rw [ limit.w G f, category.assoc, h.2.2 f]; obviously }

view this post on Zulip Kenny Lau (Dec 23 2019 at 06:13):

surely there's a better proof

view this post on Zulip Johan Commelin (Dec 23 2019 at 10:14):

I think this stuff is already in mathlib

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

I couldn't find the one I posted but I can quite believe I missed it. Library_search couldn't find it either

view this post on Zulip Johan Commelin (Dec 23 2019 at 10:15):

It's probably not exactly this, but a slight variant


Last updated: May 18 2021 at 08:14 UTC