0
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Musa Al-hassy Jun 18 '16 at 16:29
  • $\begingroup$ Hopefully it should be more clear now. I added some definitions at the bottom. $\endgroup$ – Monstrous Moonshine Jun 18 '16 at 17:18
  • $\begingroup$ By the way, the textbook I'm using is Abstract and Concrete Categories: The Joy of Cats – by Adámek, Herrlich, and Strecker. $\endgroup$ – Monstrous Moonshine Jun 18 '16 at 17:36
3
$\begingroup$

$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)$.

| cite | improve this answer | |
$\endgroup$
1
$\begingroup$

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 :-)

Addendum

@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!

I must admit that his presentation seems more professional and succinct than my own but that's to be expected since I've just learned a bit about this concept today.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ A coreflection (and a coreflective subcategory) is the dual concept of a reflection (and a reflective subcategory). A subcategory is coreflective if and only if it's dual is a reflective subcategory of the dual of the larger category (the result for reflections and coreflections is analogous). $\endgroup$ – Monstrous Moonshine Jun 19 '16 at 18:49

Your Answer

By clicking β€œPost Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.