被覆系

definition.icon

$ \mathrm{Cov}(x) \subset

$ \mathrm{Cov}(x)

$ U = \left\{ U_i\colon \right\}

where

code:sig

2-signature <Diagram with cocone: _J, C; _x, _T; _μ>

fixed-in CAT

Data

0-morph _J : Set

C : CAT

1-morph _x : 1 -> C

_T : _J -> C

2-morph _μ : _T => ! * _x

: _J -> C

被覆系とは余錐の集合であり以下を満たすもの

code:sig

∀ Λ2 = <: J2, C; x2, T2; μ2>

∀ x> : x1 -> x2

∃ Λ1

∀ j1: J1

∃ j2 : J2

∃ k : j1.T1 -> j2.T2

code:diagram

j1.T1 ----- k ----> j2.T2

| |

| |

j1.μ1 j2.μ2

| |

v v

x1 ------ x> ------> x2

j2 = j1.J>, k = j1.T>

code:sig

∀ Λ2 = <Cocone: J2, C; x2, T2; μ2>

∀ x> : x1 -> x2

∃ Λ1 = <Cocone: J1, C; x1, T1; μ1>

∃ J> : J1 -> J2

∃ T> : T1 => J> * T2

μ> : μ1 ; ! * x> = T> ; J> * μ_2

: T1 => ! * x2

: J1 -> C

code:diagram

j1.T1 -- j1.T> -> j1. J> * T2

| |

| |

j1.μ1 j1. J> * μ2

| |

v v

x1 ----- x> -------> x2

余錐の圏？