Pro-étale cohomology

4.2. Generated topologies🔗

The previous section established a relationship between the coherent topologies on \mathcal{C} and \pro{\mathcal{C}}. In the situations we are interested in, the topologies don't necessarily agree with the coherent topologies though (see Lemma 4.1.1).

To remedy the situation, we make the following definitions:

Definition4.2.1
Group: Pro-categories, precoherent categories, the coherent topology and generated topologies, used to compare sites with their pro-completions. (16)
Group member previews
Preview
Proposition 4.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 0used by 1XL∃∀N

Let \mathcal{U} be a one-hypercover in a site \mathcal{C}. We say \mathcal{U} is exact if taking filtered colimits preserves the multiequalizer diagram of \mathcal{U}.

Any finite one-hypercover is exact, because filtered colimits commute with finite limits.

Definition4.2.2
Group: Pro-categories, precoherent categories, the coherent topology and generated topologies, used to compare sites with their pro-completions. (16)
Group member previews
Preview
Proposition 4.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Proposition 4.2.3
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Let F\colon \mathcal{C} \to \mathcal{D} be a functor between sites. We say a one-hypercover \mathcal{U} of an object X in \mathcal{D} is relatively pro-representable if it is exact and \mathcal{U} can be written as the componentwise cofiltered limit of one-hypercovers in \mathcal{C}.

Lean code for Definition4.2.2●1 definition
  • defdefined in Proetale/Pro/Basic.lean
    complete
    def CategoryTheory.GrothendieckTopology.oneHypercoverRelativelyRepresentable.{w,
    v₁, v₂, u₁, u₂, u_3}
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D)
  (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) : K.OneHypercoverFamily
    def CategoryTheory.GrothendieckTopology.oneHypercoverRelativelyRepresentable.{w,
    v₁, v₂, u₁, u₂, u_3}
  {C : Type u₁}
  [CategoryTheory.Category.{v₁, u₁} C]
  {D : Type u₂}
  [CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D)
  (J :
    CategoryTheory.GrothendieckTopology C)
  (K :
    CategoryTheory.GrothendieckTopology
      D) :
  K.OneHypercoverFamily
    The family of `1`-hypercovers of `D` (think: `= Pro C`) that is a limit
of `1`-hypercovers in `C`.

We shall show that if `D = Pro C`, the finite `1`-hypercovers for a suitable topology
on `D` satisfy this.

Concretely, a one-hypercover \mathcal{U} = (U_{\alpha}, U_{\alpha \beta \gamma}) is relatively pro-representable if there exist

  1. a cofiltered diagram \mathcal{I},

  2. functors V_{\alpha}\colon \mathcal{I} \to \mathcal{C} and V_{\alpha \beta \gamma}\colon \mathcal{I} \to \mathcal{C},

  3. natural transformations p_1 \colon V_{\alpha \beta \gamma} \to V_{\alpha} and p_2\colon V_{\alpha \beta \gamma} \to V_{\beta},

such that

  1. U_{\alpha} = \lim_i V_{\alpha}(i) and U_{\alpha \beta \gamma} = \lim_i V_{\alpha \beta \gamma}(i), and

  2. for every i \in \mathcal{I}, the induced pre-one-hypercover (V_{\alpha}(i), V_{\alpha \beta \gamma}(i)) is a one-hypercover.

Suppose \mathcal{C} is coherent, \mathcal{D} = \pro{\mathcal{C}} and F \colon \mathcal{C} \to \pro{\mathcal{C}} the inclusion. If both \mathcal{C} and \pro{\mathcal{C}} are equipped with the coherent topologies, the topology on \pro{\mathcal{C}} is generated by relatively pro-representable one-hypercovers.

The analogue of Proposition 4.1.3 is:

Proposition4.2.3
Group: Pro-categories, precoherent categories, the coherent topology and generated topologies, used to compare sites with their pro-completions. (16)
Group member previews
Preview
Proposition 4.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 1used by 1✓L∃∀N

Suppose the topology on \mathcal{D} is generated by relatively pro-representable one-hypercovers and let P be a presheaf on \mathcal{D}. If P \circ F^{\mathrm{op}} is a sheaf on \mathcal{C} and P preserves filtered colimits, then P is a sheaf on \mathcal{D}.

Lean code for Proposition4.2.3●1 theorem
  • theoremdefined in Proetale/Pro/Basic.lean
    complete
    theorem CategoryTheory.Presheaf.IsSheaf.of_preservesFilteredColimitsOfSize.{w,
    v₁, v₂, u₁, u₂, u_2, u_3, u_4}
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D}
  {A : Type u_2} [CategoryTheory.Category.{u_3, u_2} A]
  (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D)
  (P : CategoryTheory.Functor Dᵒᵖ A)
  (h : CategoryTheory.Presheaf.IsSheaf J (F.op.comp P))
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v₂, u_3,
        u₂, u_2}
      P]
  [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, u_3, u_2} A]
  [CategoryTheory.AB5OfSize.{w, w, u_3, u_2} A]
  [(CategoryTheory.GrothendieckTopology.oneHypercoverRelativelyRepresentable
          F J K ⊓
        K.finiteOneHypercover).IsGenerating] :
  CategoryTheory.Presheaf.IsSheaf K P
    theorem CategoryTheory.Presheaf.IsSheaf.of_preservesFilteredColimitsOfSize.{w,
    v₁, v₂, u₁, u₂, u_2, u_3, u_4}
  {C : Type u₁}
  [CategoryTheory.Category.{v₁, u₁} C]
  {D : Type u₂}
  [CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  {A : Type u_2}
  [CategoryTheory.Category.{u_3, u_2} A]
  (J :
    CategoryTheory.GrothendieckTopology C)
  (K :
    CategoryTheory.GrothendieckTopology D)
  (P : CategoryTheory.Functor Dᵒᵖ A)
  (h :
    CategoryTheory.Presheaf.IsSheaf J
      (F.op.comp P))
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w,
        w, v₂, u_3, u₂, u_2}
      P]
  [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w,
        w, u_3, u_2}
      A]
  [CategoryTheory.AB5OfSize.{w, w, u_3,
        u_2}
      A]
  [(CategoryTheory.GrothendieckTopology.oneHypercoverRelativelyRepresentable
          F J K ⊓
        K.finiteOneHypercover).IsGenerating] :
  CategoryTheory.Presheaf.IsSheaf K P
    Let `K` be a topology generated by limits of finite `1`-hypercovers in `C`. Then if `P` is a
presheaf on `D` (think: `= Pro C`) such that

1. `P` restricted to `C` is a sheaf, and
2. `P` preserves filtered colimits, then

`P` is a sheaf.
Proof for Proposition 4.2.3
uses 0

By the assumption, it suffices to check the sheaf condition for every relatively pro-representable one-hypercover \mathcal{U} = \lim F(\mathcal{V}_i). Because P preserves filtered colimits, one computes that the sheaf condition for \mathcal{U} is the filtered colimit of the sheaf conditions for \mathcal{V}_i. But P \circ F^{\mathrm{op}} is a sheaf and filtered colimits preserve the equalizers because \mathcal{U} is exact.