Zulip Chat Archive

Stream: maths

Topic: Covers

view this post on Zulip Adam Topaz (Mar 23 2021 at 01:10):

Hi everyone,
I would like to formalize the following definition:

This should be straightforward. The only possible hickup is the universes as one quantifies over types.

import category_theory.category

open category_theory

universes v u w

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

def SR := Σ (α : Type w), α  C

instance : category (SR C) :=
{ hom := λ x y, Σ (h : x.1  y.1), (Π (i : x.1), x.2 i  y.2 (h i)),
  id := λ x, id, λ i, 𝟙 _⟩,
  comp := λ x y z f g, g.1  f.1, λ i, (f.2 i)  (g.2 _)⟩ }

However, I would also like to have a formulation of the following concept:

And this point seems to be incompatible with the way grothendieck pretopologies are defined in mathlib. Specifically docs#category_theory.presieve uses sets of morphisms as opposed to maps from some indexing set. I could take the range of some function but I feel like this will get clunky very quickly.

What do people think about approaching these two definitions from the stacks project? (I'm not settled on the definition in the code above BTW).

@Scott Morrison @Bhavik Mehta

view this post on Zulip Bhavik Mehta (Mar 23 2021 at 02:18):

I think a good comparison for this is the definition of sites/pretopologies in the stacks project: https://stacks.math.columbia.edu/tag/00VG - this definition turns out to be incredibly awkward to work with in dtt, specifically because of the maps from the indexing set. For a concrete example, you run into huge issues when you want to compare between sites and sieves: working with sets of morphisms gives you obvious equality but even in the stacks project they need to specifically define notions of equality, and even then those definitions (I think) need the dreaded eq_to_homs anyway.

view this post on Zulip Bhavik Mehta (Mar 23 2021 at 02:19):

I'm hesitant about using that implementation of SR that you give but I can't think of anything better - though I suspect you can convert from maps from the indexing set to a set of morphisms defined by an inductive definition

view this post on Zulip Bhavik Mehta (Mar 23 2021 at 02:22):

Perhaps not the most helpful comparison but I'm thinking of this along the same lines as https://github.com/leanprover-community/mathlib/blob/9f56a0bf9c8a50ff12701922a97e238cc668413c/src/category_theory/sites/sieves.lean#L59 - if you think of the singleton family as indexed by the unit type I feel like it's the same idea, originally I had a much less pleasant definition

def singleton : presieve X :=
λ Z g,  (H : Z = Y), eq_to_hom H  f = g

which did work, but then Reid suggested this inductive type and everything got a lot nicer - I think in your case something similar applies

view this post on Zulip Bhavik Mehta (Mar 23 2021 at 02:27):

In general when there is a question about universes I think it's often a good idea to look for alternate definitions in the literature which don't have universe parameters - I don't know if this applies in your context though?

view this post on Zulip Bhavik Mehta (Mar 23 2021 at 02:31):

Looking at the definition from SGA which stacks says is essentially equivalent (provided my French isn't too rusty), that defines a semirepresentable object as a presheaf isomorphic to a direct sum of representable presheaves; though I think this doesn't help with the universes problem

view this post on Zulip Kevin Buzzard (Mar 23 2021 at 08:22):

When universes are getting in the way I usually just get lazy and become less polymorphic, after having done a quick check in my head that the examples in thinking about all have everything in the same universe...

Last updated: May 09 2021 at 10:11 UTC