Isomorphic covers in pretopology

Stream: mathlib4

[Andrew Yang]

Is the following true?
If $J$ is a pretopology on $C$, $\{ Y_i \to X \}_{i \in I}$ is a cover of $X$, and $Y'_i \cong Y_i$ is another family, then $\{ Y'_i \to Y_i \to X \}_{i \in I}$ is also a cover of $X$.

lemma Pretopology.ofArrows_mem_of_iso {C : Type*} [Category C] [HasPullbacks C]
    {ι : Type*} {X : C} {Y Y' : ι → C} (f : ∀ i, Y i ⟶ X)
    (e : ∀ i, Y' i ≅ Y i) (J : Pretopology C) (H : Presieve.ofArrows Y f ∈ J X) :
    Presieve.ofArrows Y' ((e _).hom ≫ f ·) ∈ J X := by
  sorry

Answer: It is not (at least in mathlib)

inductive M | A | B

inductive M.Hom : M → M → Type
 | id X : M.Hom X X
 | flip : M.Hom A A
 | l : M.Hom A B
 | r : M.Hom A B

def M.Hom.comp : ∀ {X Y Z : M}, X.Hom Y → Y.Hom Z → X.Hom Z
  | _, _, _, .id _, g => g
  | _, _, _, g, .id _ => g
  | _, _, _, .flip, .l => .r
  | _, _, _, .flip, .r => .l
  | _, _, _, .flip, .flip => .id _

instance : Category M where
  Hom := M.Hom
  id := M.Hom.id
  comp := M.Hom.comp
  id_comp f := by cases f <;> rfl
  comp_id f := by cases f <;> rfl
  assoc f g h := by cases f <;> cases g <;> cases h <;> rfl

instance {X Y : M} (f : X ⟶ Y) : Mono f := by
  rcases f
  · show Mono (𝟙 _); infer_instance
  · constructor
    rintro _ ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
  · constructor
    rintro _ ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
  · constructor
    rintro _ ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl

attribute [instance] hasPullback_of_left_iso hasPullback_of_right_iso in
instance : HasPullbacks M := by
  apply (config := { allowSynthFailures := true }) hasPullbacks_of_hasLimit_cospan
  rintro X Y Z ⟨⟩ g
  · show HasPullback (𝟙 _) _
    infer_instance
  · rcases g
    · show HasPullback _ (𝟙 _); infer_instance
    · infer_instance
  · rcases g
    · show HasPullback _ (𝟙 _); infer_instance
    · infer_instance
    · show HasPullback (C := M) (M.Hom.flip ≫ M.Hom.r) M.Hom.r; infer_instance
  · rcases g
    · show HasPullback _ (𝟙 _); infer_instance
    · show HasPullback (C := M) M.Hom.r (M.Hom.flip ≫ M.Hom.r); infer_instance
    · infer_instance

def M.pretopology : Pretopology M where
  coverings X := { S | ∃ Y, ∃ (f : Y ⟶ X), S = .singleton f }
  has_isos _ _ _ _ := ⟨_, _, rfl⟩
  pullbacks := by
    rintro _ _ _ _ ⟨_, _, rfl⟩
    simp only [Presieve.pullback_singleton, Set.mem_setOf_eq]
    exact ⟨_, _, rfl⟩
  transitive := by
    rintro X S Ti ⟨Y, f, rfl⟩ hS'
    choose Z fZ hZ using hS'
    refine ⟨_, fZ f .mk ≫ f, ?_⟩
    refine funext₂ fun W fW ↦ eq_iff_iff.mpr ⟨?_, ?_⟩
    · rintro ⟨_, fW', c, ⟨⟩, e, rfl⟩
      rcases (hZ _ _).le _ e
      exact .mk
    · rintro ⟨⟩
      exact ⟨_, _, _, .mk, (hZ _ _).ge _ .mk, rfl⟩

def M.flipIso : M.A ≅ M.A where
  hom := .flip
  inv := .flip
  hom_inv_id := rfl
  inv_hom_id := rfl

example : False := by
  obtain ⟨b, f, hf⟩ := Pretopology.ofArrows_mem_of_iso (C := M) (f := fun b : Bool ↦ M.Hom.l)
    (e := fun b ↦ bif b then .refl _ else M.flipIso) M.pretopology
    ⟨_, .l, funext₂ (fun X f ↦ eq_iff_iff.mpr <| by
      constructor
      · rintro ⟨i⟩
        exact .mk
      · rintro ⟨⟩
        exact ⟨true⟩)⟩
  rcases f
  · cases hf.ge _ .mk
  · cases hf.le _ (.mk false)
  · cases hf.le _ (.mk true)

But is this true mathematically? Is our definition of Pretopology not strong enough?

[Andrew Yang]

cc @Joël Riou @Christian Merten

[Christian Merten]

This is true if Y is injective (as a function!).

[Andrew Yang]

But should it not be true for non injective Y?
This is exceptionally bad when you consider this with our formulation of pullbacks. It says that if $Y_i$ is a cover, then $Y_i \times_X Z$ is also a cover of $Z$, where here $Y_i \times_X Z$ is some random Nonempty.some of a pullback, and there is no guarantee that this is injective even if $Y_i$ is.

[Christian Merten]

I agree, it should be true for non-injective Y.
So is the issue that Presieve.ofArrows Y f does not only depend on the range of Y and f?

[Andrew Yang]

Yeah and bind only allow sieves depending on the range of Y.

[Andrew Yang]

I claim that Pretopology need this extra condition

∀ {X : C} (S T : Presieve X), S ≤ T.isoClosure → T ≤ S.isoClosure → T ∈ J X → S ∈ J X

where

def CategoryTheory.Presieve.isoClosure {C : Type*} [Category C]
    {X : C} (S : Presieve X) : Presieve X :=
  fun Y ↦ { f | ∃ Z, ∃ (e : Z ≅ Y), S (e.hom ≫ f) }

[Christian Merten]

What is the idea behind defining Presieve X as ∀ ⦃Y⦄, Set (Y ⟶ X) in the first place? To be precise, what goes wrong with:

variable {C : Type*} [Category C]

structure HomTo (X : C) where
  source : C
  hom : source ⟶ X

def Presieve' (X : C) := Set (HomTo X)

def Presieve'.ofArrows {X : C} {ι : Type*} (Y : ι → C) (f : ∀ i, Y i ⟶ X) :
    Presieve' X :=
  Set.range (fun i ↦ ⟨Y i, f i⟩)

[Andrew Yang]

First of all I don't think this solves the titular question.
Secondly, I think you are just un-currying ∀ (Y), (Y ⟶ X) -> Prop and we like to curry things in mathlib.

[Andrew Yang]

But AlgebraicGeometry.Scheme.zariskiPretopology doesn't satisfy the definition...
It doesn't even satisfy the titular question, because you can have a cover that is (set-theoretically) big but essentially small, and the topology is defined only by the small covers. Do we want to change that and allow big covers as well?

[Joël Riou]

I would say that pretopologies are only a way to construct Grothendieck topologies. There is no similar issue with topologies.

[Andrew Yang]

Here's my use case:
I want to show some functor is a sheaf in Scheme.zariskiTopology.over X, and naturally I tried docs#CategoryTheory.Presieve.isSheaf_pretopology and I am led to showing something like Scheme.zariskiPretopology.toGrothendieck.over X = (Scheme.zariskiPretopology.over X).toGrothendieck But the over of an pretopology isn't necessarily a pretopology and the RHS makes no sense because of the pullback field and the issue above.

[Joël Riou]

If this can help, we could introduce a typeclass Pretopology.RespectsIso?
In any case, we need to introduce lemmas which characterizes the Zariski sheaves on Scheme (and Over X) by saying that the "restrictions" to Opens V for all V are sheaves (and also in terms of the sheaf condition for the families given by OpenCover).

[Andrew Yang]

The thing is AlgebraicGeometry.Scheme.zariskiPretopology (as it currently is) doesn't satisfy RespectsIso because of set-theoretic concerns.

[Christian Merten]

Andrew Yang said:

Here's my use case:
I want to show some functor is a sheaf in Scheme.zariskiTopology.over X, and naturally I tried docs#CategoryTheory.Presieve.isSheaf_pretopology and I am led to showing something like Scheme.zariskiPretopology.toGrothendieck.over X = (Scheme.zariskiPretopology.over X).toGrothendieck But the over of an pretopology isn't necessarily a pretopology and the RHS makes no sense because of the pullback field and the issue above.

Does docs#AlgebraicGeometry.Scheme.overGrothendieckTopology_eq_toGrothendieck_overPretopology help?

[Andrew Yang]

Yes it works. So this issue is not immediate bugging me now. But shouldn't (and do we not need) this over thing to work for all topologies that is not necessarily defined by some morphism property (e.g. fpqc)?

[Christian Merten]

We will (hopefully) need this for the fpqc topology in the coming weeks, yes. But I think if we just take intersections with the pretopology given by QuasiCompact covers (or just assume QuasiCompact in docs#AlgebraicGeometry.Scheme.pretopology) it should still work on the level of Grothendieck topologies?

[Christian Merten]

A similar phenomenon with size issues arises here (docs#AlgebraicGeometry.Scheme.grothendieckTopology_eq_inf) btw, but it only happens on the level of pretopologies.

[Andrew Yang]

or just assume QuasiCompact in Scheme.pretopology

This approach still screams to me that this is not in the right generality and we are making our lives more painful.

[Christian Merten]

Maybe @Joël Riou knows of a natural example of a topology on schemes where coverings are not assumed to be "quasicompact"? (by "quasicompact" I mean, they satisfy the finiteness conditions in the definition of fpqc).

[Christian Merten]

Andrew Yang said:

or just assume QuasiCompact in Scheme.pretopology

This approach still screams to me that this is not in the right generality and we are making our lives more painful.

But are you fine with taking intersections then?

[Andrew Yang]

or just assume QuasiCompact in Scheme.pretopology

Okay maybe this is fine because it is defining a pretopology anyway. I should be saying that every thing that works with an arbitrary pretopology should work for an arbitrary pretopology. Or else we need to massage our pretopology into the right form before we can apply anything.

[Andrew Yang]

(e.g. eq_toGrothendieck_overPretopology or even Scheme.Cover)

[Christian Merten]

But is there a general CategoryTheory.Pretopology.over with good definitional properties?

[Andrew Yang]

def CategoryTheory.Presieve.overForget
    {X : C} {Y : Over X} (P : Presieve Y) :
    Presieve Y.left :=
      fun _ ↦ { f | P (Over.homMk (U := Over.mk (f ≫ Y.hom)) f rfl) }

def CategoryTheory.Pretopology.over
    (J : Pretopology C) (X : C) [J.IsNice] : Pretopology (Over X) where
  coverings Y := { S | S.overForget ∈ J Y.left }

This works (under a better definition of pullbacks that Scheme.pretopology does not yet satisfy)

[Joël Riou]

Yes, at some point, if we absolutely need it, we may improve the pullbacks condition so as to allow any pullback instead of the arbitrarily chosen pullback of the limits API.

[Christian Merten]

Andrew Yang said:

def CategoryTheory.Presieve.overForget
    {X : C} {Y : Over X} (P : Presieve Y) :
    Presieve Y.left :=
      fun _ ↦ { f | P (Over.homMk (U := Over.mk (f ≫ Y.hom)) f rfl) }

def CategoryTheory.Pretopology.over
    (J : Pretopology C) (X : C) [J.IsNice] : Pretopology (Over X) where
  coverings Y := { S | S.overForget ∈ J Y.left }

This works (under a better definition of pullbacks that Scheme.pretopology does not yet satisfy)

Does this give the same pretopology as docs#AlgebraicGeometry.Scheme.overPretopology though? Doesn't your definition mean that the component maps in the covering won't necessarily be over X?

[Andrew Yang]

The X-structure on U is by definition U.map i >> Y.hom here so U.map i commutes with them by rfl.

[Christian Merten]

Ah yes, you are right.