Covers

Stream: maths

[Adam Topaz]

Hi everyone,
I would like to formalize the following definition:
https://stacks.math.columbia.edu/tag/01G0

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:
https://stacks.math.columbia.edu/tag/01G3

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

[Bhavik Mehta]

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.

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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?

[Bhavik Mehta]

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

[Kevin Buzzard]

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