Kernel pairs of covering morphisms become coequalizers of sheaves

Let J be a subcanonical Grothendieck topology on a category C, and let q : X ⟶ Y be a morphism which generates a covering sieve of Y, with kernel pair p₁ p₂ : R ⟶ X. A J-sheaf of types P satisfies the sheaf condition for the single morphism q, so P(Y) ⟶ P(X) ⇉ P(R) is an equalizer. By the Yoneda lemma for sheaves, this says that the image of R ⇉ X ⟶ Y under the Yoneda embedding J.yoneda into J-sheaves is a coequalizer (IsKernelPair.isColimitYonedaCofork).

In other words, Y represents the quotient sheaf of X by the equivalence relation R. For schemes and the fppf topology, this says that the base of an fppf covering morphism represents the fppf quotient sheaf of its source by its kernel pair. This is how quotients of schemes by finite group actions and by finite locally free equivalence relations are shown to represent fppf quotient sheaves.

Main definitions

• CategoryTheory.IsKernelPair.isColimitYonedaCofork: the Yoneda image of the cofork R ⇉ X ⟶ Y is a colimit in J-sheaves.

References

• M. Demazure and A. Grothendieck, Schémas en groupes (SGA 3), Exposé IV, §3, and Exposé V, §4.

noncomputable def CategoryTheory.IsKernelPair.isColimitYonedaCofork {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {R X Y : C} {p₁ p₂ : R ⟶ X} {q : X ⟶ Y} (h : IsKernelPair q p₁ p₂) (hq : Sieve.generate (Presieve.singleton q) ∈ J Y) : Limits.IsColimit (Limits.Cofork.ofπ (J.yoneda.map q) ⋯)

If q : X ⟶ Y generates a covering sieve of Y and p₁ p₂ : R ⟶ X is its kernel pair, the Yoneda embedding into J-sheaves sends R ⇉ X ⟶ Y to a coequalizer. Thus Y represents the quotient sheaf of X by the equivalence relation R.