evil version of IsLocallyFull

Stream: mathlib4

[Kenny Lau]

@Joël Riou @Robin Carlier I haven't worked out all the details yet, but,

Currently we have CategoryTheory.Functor.inducedTopology assuming CategoryTheory.Functor.IsLocallyFull, which I couldn't prove for my usecase, and I suspect there is an evil version of IsLocallyFull that I can define that will still give you an induced topology.

Again, I haven't worked out all the details, so I'm not sure if this works yet. The reason I'm pinging you two is to ask if you have come across something like this before, (because I'm essentially inventing this).

[Kenny Lau]

The evil version should look like $\forall S : \mathrm{Sieve}_X, \mathcal{F}_\ast S = \mathcal{F} " S$, and I claim (and again I'm not sure) that this is not equivalent to the existing IsLocallyFull

[Kenny Lau]

the difference is that F is not injective (evil), and here given f: FX -> FY I am allowed to replace FX with some FZ that is equal (evil) to FX (and Z is not equal (evil) to X)

[Robin Carlier]

I don’t think I ever came across something like this, but my experience with generalities on Grothendieck topologies is admittedly quite limited. The situation you describe does look very evil though.

[Kenny Lau]

I tried more times to try to prove that my functor is locally full, thinking that maybe I just missed something, but I don't think it's possible (I don't have a proof that it's impossible anyway), but I'll now try defining the evil version and hope that I have more success

[Kenny Lau]

@Robin Carlier I have now produced the evil versions of faithful and full and actually proved them:

[Kenny Lau]

import Mathlib

universe v v₁ v₂ u u₁ u₂

open CategoryTheory Category

namespace CategoryTheory.Functor

variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (G : C ⥤ D)
  (K : GrothendieckTopology D)

class IsLocallyFullEvil (G : C ⥤ D) : Prop where
  full (G) {X : D} {Y : C} (f : X ⟶ G.obj Y) :
    ∃ (X' : C) (g : X' ⟶ Y) (e : X = G.obj X'), eqToHom e ≫ G.map g = f

class IsLocallyFaithfulEvil (G : C ⥤ D) : Prop where
  faithful (G) {X X' Y : C} {f : X ⟶ Y} {g : X' ⟶ Y} (e : G.obj X = G.obj X')
    (e₂ : G.map f = eqToHom e ≫ G.map g) : ∃ h : X = X', f = eqToHom h ≫ g

variable [G.IsLocallyFullEvil] [G.IsLocallyFaithfulEvil]

def inducedTopologyEvil : GrothendieckTopology C where
  sieves _ S := K _ (S.functorPushforward G)
  top_mem' X := by
    change K _ _
    rw [Sieve.functorPushforward_top]
    exact K.top_mem _
  pullback_stable' X Y S iYX hS := by
    refine K.superset_covering ?_ (K.pullback_stable (G.map iYX) hS)
    rintro Z f ⟨W, iWX, iZW, hS, e⟩
    obtain ⟨Z, f, rfl, rfl⟩ := IsLocallyFullEvil.full G f
    obtain ⟨U, g, e, rfl⟩ := IsLocallyFullEvil.full G iZW
    rw [eqToHom_refl, id_comp] at e ⊢
    rw [assoc, ← map_comp, ← map_comp] at e
    obtain ⟨rfl, e⟩ := IsLocallyFaithfulEvil.faithful G _ e
    refine ⟨_, f, 𝟙 _, ?_, (id_comp _).symm⟩
    rw [eqToHom_refl, id_comp] at e
    exact congr(S.arrows $e).to_iff.mpr (S.downward_closed hS g)
  transitive' X S hS S' H' := by
    apply K.transitive hS
    rintro Y _ ⟨Z, g, i, hg, rfl⟩
    rw [Sieve.pullback_comp]
    apply K.pullback_stable i
    refine K.superset_covering ?_ (H' hg)
    rintro W _ ⟨Z', g', i', hg, rfl⟩
    refine ⟨Z', g' ≫ g , i', hg, ?_⟩
    simp

end CategoryTheory.Functor

namespace CategoryTheory.CostructuredArrow

variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (S : C ⥤ D) (T : D)
  (K : GrothendieckTopology C)

open GrothendieckTopology

instance : (proj S T).IsLocallyFullEvil where
  full {X Y} f := ⟨mk (S.map f ≫ Y.hom), homMk f, rfl, id_comp _⟩

instance : (proj S T).IsLocallyFaithfulEvil where
  faithful {X X' Y} f g e₁ e₂ := by
    obtain ⟨X, x, rfl⟩ := mk_surjective X
    obtain ⟨X', x', rfl⟩ := mk_surjective X'
    obtain ⟨Y, y, rfl⟩ := mk_surjective Y
    change X = X' at e₁; subst e₁
    rw [eqToHom_refl, id_comp] at e₂
    change f.left = g.left at e₂
    have wf : S.map f.left ≫ y = x := w f
    have wg : S.map g.left ≫ y = x' := w g
    rw [e₂] at wf
    have : x = x' := wf.symm.trans wg; subst this
    refine ⟨rfl, ?_⟩
    rw [eqToHom_refl, id_comp]
    exact (proj S T).map_injective e₂

variable {S T} in
def inducedTopology : GrothendieckTopology (CostructuredArrow S T) :=
  (proj S T).inducedTopologyEvil K

end CategoryTheory.CostructuredArrow

[Kenny Lau]

so the first part shows that my definitions are strong enough to produced the induced topology, and the sescond part shows that my definitions are weak enough that they are satisfied in my use case (which is CostructuredArrow)