# Constructing a coreflection functor from its components

Let $\mathbf{A}$ be a coreflective subcategory of $\mathbf{B}$ and for all $B$, $A_B\xrightarrow{c_B}B$ an $\mathbf{A}$-coreflection.

This is $\forall$ $\mathbf{B}$-objects $B$. I claim that there exists a unique functor $C:\mathbf{B}\to\mathbf{A}$ s.t. $C(B)=A_B$ $\forall$ $\mathbf{B}$-objects $B$, and for each $\mathbf{B}$-morphism $f:B\to B'$, the diagram

$$\require{AMScd} \begin{CD} C(B) @>{c_B}>> B\\ @V{C(f)}VV @V{f}VV \\ C(B') @>{c_{B'}}>> B' \end{CD}$$

commutes. It's easy to see why $C$ is uniquely defined on objects, but I'm struggling to prove that it is uniquely defined on $\mathbf{B}$-morphisms, and that it is a functor.

Definitions: Let $\mathbf{A}$ be a subcategory for $\mathbf{B}$, and let $B$ be a $\mathbf{B}$-object. Then an $\mathbf{A}$-coreflection for $B$ is a $\mathbf{B}$-morphism $A\xrightarrow{c}B$ from an $\mathbf{A}$-object $A$ to $B$ with the following universal property:

for any $\mathbf{B}$-morphism $A'\xrightarrow{F}B$ for some $\mathbf{A}$-object $A'$ to $B$, there exists a unique $\mathbf{A}$-morphism $f':A'\to A$ s.t. $f=c\circ f'$.

$\mathbf{A}$ is considered to be a coreflective subcategory of $\mathbf{B}$ when, for each $\mathbf{B}$-object $B$, there exists some $\mathbf{A}$-coreflection for $B$.

• In your title, you're saying some morphisms are coreflections. What does that mean? Do you mean a family of them, i.e., a functor? What text are you reading. Definitely consider rewriting you question. – Musa Al-hassy Jun 18 '16 at 16:29
• Hopefully it should be more clear now. I added some definitions at the bottom. – Monstrous Moonshine Jun 18 '16 at 17:18
• By the way, the textbook I'm using is Abstract and Concrete Categories: The Joy of Cats – by Adámek, Herrlich, and Strecker. – Monstrous Moonshine Jun 18 '16 at 17:36

$C(f)$ is just the factorization of $f\circ c_B$ through $c_{B'}$ required by the definition of the coreflection arrow. Functoriality then follows using uniqueness: the identity of $A_B$ makes the square for $c(\mathrm{id}_B)$ commute, and similarly for a composition of $c(f)$ with $c(g)$.

Thank-you for giving me the definitions! This is my first time with the concept of coreflective subcategories! Below is my answer to your problem; after rephrasing the definitions a bit to introduce some handy-dandy notation!

Hope it help!

# Set up

Say a subcategory 𝓐 of 𝓑, is coreflective iff we have operations

Core : Obj 𝓑 → Obj 𝓐
[_]  : Obj 𝓑 → Mor 𝓑


that interact by the typing rule: for an 𝓑-object B,

“[]-type”  [ B ] : Core B ⟶ B


and we have a third operation

⟨_⟩   : Mor 𝓑 → Mor 𝓐


that interacts with the previous two by the axiom: for any 𝓑-morphism f and 𝓐-morphism g, we have

“⟨⟩-char” ⟨ f ⟩ = g ≡ f = [ Tgt f ] ∘ g


Interestingly, taking g ≔ ⟨ f ⟩ in this characterisation yields the property mentioned in the OP's universal property:

“[]-⟨⟩-char”  f = [ Tgt f ] ∘ ⟨ f ⟩


Using this equality, we can then derive

“⟨⟩-type”   ⟨ f ⟩ : Src f ⟶ Core (Tgt f)


# Making Core into a functor

We'd like to extend Core to be defined on arrows as well; let this extension be named 𝑪.

Then, we need

𝑪 : 𝓑 ⟶ 𝓐
𝑪 B = Core B
𝑪 (f : X ⟶ B) : Core X ⟶ Core B


For the definition on arrows, we have that

⟨ f ⟩ : X ⟶ Core B , [ X ] : Core X ⟶ X


thus one candidate is

𝑪 f ≔ ⟨ f ⟩ ∘ [ Src f ]


Let's try it out and see if it works!

# 𝑪 functorial

## 𝑪 preserves composition

  𝑪 f ∘ 𝑪 g
={ definition of 𝑪 }
⟨ f ⟩ ∘ [ Src f ] ∘ ⟨ g ⟩ ∘ [ Src g ]
={ f ∘ g is well defined iff Src f = Tgt g }
⟨ f ⟩ ∘ [ Tgt g ] ∘ ⟨ g ⟩ ∘ [ Src g ]
={ []-⟨⟩-char }
⟨ f ⟩ ∘ g ∘ [ Src g ]
={ can continue if ⟨ f ⟩ ∘ g = ⟨ f ∘ g ⟩ , to be proved later }
⟨ f ∘ g ⟩ ∘ [ Src g ]
={ Src (f ∘ g) = Src g }
⟨ f ∘ g ⟩ ∘ [ Src (f ∘ g) ]
={ definition of 𝑪 }
𝑪 (f ∘ g)


It remains to show the claim,

   ⟨ f ⟩ ∘ g = ⟨ f ∘ g ⟩
≡{ ⟨⟩-char }
f ∘ g = [ Tgt (f ∘ g) ] ∘ ⟨ f ⟩ ∘ g
≡{ Tgt (f ∘ g) = Tgt f }
f ∘ g = [ Tgt f ] ∘ ⟨ f ⟩ ∘ g
≡{ []-⟨⟩-char }
f ∘ g = f ∘ g
≡{ reflexitivity of equality }
true


such a fusion of bracketing ⟨⟩ and composition may well be termed ⟨⟩-∘-fusion'.

## 𝑪 preserves identity

   𝑪 Idₓ
={ definition of 𝑪 }
⟨ Idₓ ⟩ ∘ [ X ]
={ ⟨⟩-∘-fusion }
⟨ Idₓ ∘ [ X ] ⟩
={ identity is unit of composition }
⟨[ X ]⟩
={ claim }
Id (Core X)
={ definition of 𝑪 }
Id (𝑪 X)


It remains to prove the claim, suppressing arguments to Id,

  ⟨[ X ]⟩ = Id
≡{ ⟨⟩-char }
[ X ] = [ Tgt ([ X ]) ] ∘ Id
≡{ []-typing }
[ X ] = [ X ] ∘ Id
≡{ unit of composition and reflexitivty of equality }
true


# The desired property

(*)  ∀ f : X ⟶ Y    •     f ∘ [ X ] = [ Y ] ∘ 𝑪 f


## 𝑪 satisfies property (*)

  [ Tgt f ] ∘ 𝑪 f
={ definition of 𝑪 }
[ Tgt f ] ∘ ⟨ f ⟩ ∘ [ Src f ]
={ []-⟨⟩-char }
f ∘ [ Src f ]


## 𝑪 is the only functor satisfying (*)

Suppose a given functor C' satisfies (*) then it must be the same as 𝑪:

  𝑪 f
={ definition of 𝑪 }
⟨ f ⟩ ∘ [ Src f ]
={ unit of composition and ⟨⟩-∘-fusion }
⟨ Id (Tgt f) ⟩ ∘ f ∘ [ Src f ]
={ assumption of C' satisfying (*) }
⟨ Id (Tgt f) ⟩ ∘ [ Tgt f ] ∘ C' f
={ definition of 𝑪 --suppressing implicit argument to Id }
𝑪 Id ∘ C' f
={ 𝑪 functor }
Id ∘ C' f
={ unit of composition }
C' f


# Conclusion

I don't really know what a coreflection is; I have no intuitive understanding of it :-( Let me know if you, the reader, do!

However, I introduced some notations with rules and massaged the symbols here and there to prove the result and that's a fun game :-)

@Kevin, in another answer here, says “$C(f)$ is just the factorization of $f ∘ c_B$ through $c_B′$ required by the definition of the coreflection arrow.” In my notation, he's saying 𝑪 f = ⟨ f ∘ [ Src f ] ⟩` which is fact identical to the definition of 𝑪 we found above due to ⟨⟩-∘-fusion!