Coequalizer in Type

Stream: Is there code for X?

[Christian Merten]

Do we have the coequalizer of two plain functions without importing category theory? I.e. something like

import Mathlib.Data.Quot

inductive Function.Coequalizer.Rel {E F : Type*} (σ τ : E → F) : F → F → Prop where
  | intro (x : E) : Rel σ τ (σ x) (τ x)

def Function.coequalizer {E : Type u} {F : Type v} (σ τ : E → F) : Type v :=
  Quot (Function.Coequalizer.Rel σ τ)

namespace Function.Coequalizer

variable (σ τ : E → F)

def mk (f : F) : Function.coequalizer σ τ :=
  Quot.mk _ f

lemma condition (e : E) : mk σ τ (σ e) = mk σ τ (τ e) :=
  Quot.sound (.intro e)

lemma mk_surjective : Function.Surjective (Function.Coequalizer.mk σ τ) :=
  Quot.mk_surjective

def desc {G : Type*} (u : F → G) (hu : u ∘ σ = u ∘ τ) : Function.coequalizer σ τ → G :=
  Quot.lift u (fun _ _ (.intro e) ↦ congrFun hu e)

@[simp] lemma desc_mk {G : Type*} (u : F → G) (hu : u ∘ σ = u ∘ τ) (f : F) :
    desc σ τ u hu (mk σ τ f) = u f :=
  rfl

end Function.Coequalizer

and if no, do we want it?

[Andrew Yang]

I don't think we do. What do you need this for?

[Christian Merten]

I need it for: given two functions $\sigma, \tau \colon E \to F$ and an $R$-algebra $S$, the equalizer of the induced algebra maps $S^F \to S^E$ is isomorphic to $S^{\mathrm{coeq}(\sigma, \tau)}$, i.e.

@[simps!]
def AlgHom.compRight (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] (σ : E → F) :
    (F → S) →ₐ[R] E → S :=
  Pi.algHom R _ (fun f ↦ Pi.evalAlgHom R _ (σ f))

def AlgHom.equalizerCompRightEquiv (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    (σ τ : E → F) :
    AlgHom.equalizer (AlgHom.compRight R S σ) (AlgHom.compRight R S τ) ≃ₐ[R]
      Function.coequalizer σ τ → S :=
  AlgEquiv.ofAlgHom
    (Pi.algHom R _ (Function.Coequalizer.desc σ τ
      (fun f ↦ (Pi.evalAlgHom R (fun _ ↦ S) f).comp
        (equalizer (compRight R S σ) (compRight R S τ)).val)
        (by ext f ⟨x, hx⟩; exact congrFun hx f)))
    (AlgHom.codRestrict (.compRight _ _ (Function.Coequalizer.mk _ _))
      (equalizer _ _)
      (fun x ↦ by ext e; simp only [compRight_apply]; rw [Function.Coequalizer.condition]))
    (by
      ext f x
      obtain ⟨x, rfl⟩ := Function.Coequalizer.mk_surjective _ _ x
      simp)
    (by ext f x; simp)

(I don't really care that it is the coequalizer, I just need that it is again of the form $S^D$ for some type $D$, but showing that $D = \mathrm{coeq}(\sigma, \tau)$ is not harder.)

[Andrew Yang]

Then I guess we probably could have it?

[Andrew Yang]

But replace docs#CategoryTheory.Limits.Types.CoequalizerRel by the new thing once it's done.

[Christian Merten]

#21824