Coequalizer of a pair of functions

The coequalizer of two functions f g : α → β is the pair (μ, p : β → μ) that satisfies the following universal property: Every function u : β → γ with u ∘ f = u ∘ g factors uniquely via p.

In this file we define the coequalizer and provide the basic API.

inductive Function.Coequalizer.Rel {α : Type u_1} {β : Type u_2} (f g : α → β) : β → β → Prop

The relation generating the equivalence relation used for defining Function.coequalizer.

• intro {α : Type u_1} {β : Type u_2} {f g : α → β} (x : α) : Rel f g (f x) (g x)

def Function.Coequalizer {α : Type u_1} {β : Type v} (f g : α → β) : Type v

The coequalizer of two functions f g : α → β is the pair (μ, p : β → μ) that satisfies the following universal property: Every function u : β → γ with u ∘ f = u ∘ g factors uniquely via p.

Equations

• Function.Coequalizer f g = Quot (Function.Coequalizer.Rel f g)

def Function.Coequalizer.mk {α : Type u_1} {β : Type u_2} (f g : α → β) (x : β) : Coequalizer f g

The canonical projection to the coequalizer.

Equations

• Function.Coequalizer.mk f g x = Quot.mk (Function.Coequalizer.Rel f g) x

theorem Function.Coequalizer.condition {α : Type u_1} {β : Type u_2} (f g : α → β) (x : α) : mk f g (f x) = mk f g (g x)

theorem Function.Coequalizer.mk_surjective {α : Type u_1} {β : Type u_2} (f g : α → β) : Surjective (mk f g)

def Function.Coequalizer.desc {α : Type u_1} {β : Type u_2} (f g : α → β) {γ : Type u_3} (u : β → γ) (hu : u ∘ f = u ∘ g) : Coequalizer f g → γ

Any map u : β → γ with u ∘ f = u ∘ g factors via Function.Coequalizer.mk.

Equations

• Function.Coequalizer.desc f g u hu = Quot.lift u ⋯

@[simp]

theorem Function.Coequalizer.desc_mk {α : Type u_1} {β : Type u_2} (f g : α → β) {γ : Type u_3} (u : β → γ) (hu : u ∘ f = u ∘ g) (x : β) : desc f g u hu (mk f g x) = u x