Copyright | (c) Erich Gut |
---|---|
License | BSD3 |
Maintainer | zerich.gut@gmail.com |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Cokernel
-Kernel
Adjunction
for Slice
d structures.
Synopsis
- slcAdjunction :: (SliceCokernelTo i c, SliceKernelFrom i c) => i c -> Adjunction (SliceCokernelKernel i c) (SliceFactor From i c) (SliceFactor To i c)
- data SliceCokernelKernel i c x y where
- SliceCokernel :: SliceCokernelKernel i c (SliceFactor To i c) (SliceFactor From i c)
- SliceKernel :: SliceCokernelKernel i c (SliceFactor From i c) (SliceFactor To i c)
- class (Distributive c, Sliced i c) => SliceCokernelTo i c where
- sliceCokernelTo :: Slice To i c -> Cokernel N1 c
- class (Distributive c, Sliced i c) => SliceKernelFrom i c where
- sliceKernelFrom :: Slice From i c -> Kernel N1 c
- slcCokerKer :: (SliceCokernelTo i c, SliceKernelFrom i c) => Slice To i c -> SliceFactor To i c
- slcKerCoker :: (SliceCokernelTo i c, SliceKernelFrom i c) => Slice From i c -> SliceFactor From i c
- xSliceFactorTo :: (Multiplicative c, Sliced i c) => XOrtSite To c -> i c -> X (SliceFactor To i c)
- xSliceFactorFrom :: (Multiplicative c, Sliced i c) => XOrtSite From c -> i c -> X (SliceFactor From i c)
- prpHomMltSliceCokernelKernel :: (SliceCokernelTo i c, SliceKernelFrom i c) => XOrtSite To c -> XOrtSite From c -> i c -> Statement
Adjunction
slcAdjunction :: (SliceCokernelTo i c, SliceKernelFrom i c) => i c -> Adjunction (SliceCokernelKernel i c) (SliceFactor From i c) (SliceFactor To i c) Source #
the cokernel-kenrel adjunction.
Homomorphism
data SliceCokernelKernel i c x y where Source #
the left and right homomorphisms for the cokernel-kernel adjunction slcAdjunction
.
SliceCokernel :: SliceCokernelKernel i c (SliceFactor To i c) (SliceFactor From i c) | |
SliceKernel :: SliceCokernelKernel i c (SliceFactor From i c) (SliceFactor To i c) |
Instances
class (Distributive c, Sliced i c) => SliceCokernelTo i c where Source #
Distributive
structures c
having to each
a
Slice
To
i cCokernel
.
Property Let h =
be in SliceTo
_ h'
for a
Slice
To
i ci
sliced, Distributive
structure c
, then holds:
where
diagram
(universalCone
coker) ==
cokernelDiagram
h'coker =
.sliceCokernelTo
h
class (Distributive c, Sliced i c) => SliceKernelFrom i c where Source #
Distributive
structures c
having to each
a
Slice
From
i cKernel
.
Property Let h =
be in SliceFrom
_ h'
for a
Slice
From
i ci
sliced, Distributive
structure c
, then holds:
where
diagram
(universalCone
ker) ==
kernelDiagram
h'coker =
.sliceKernelFrom
h
Unit
slcCokerKer :: (SliceCokernelTo i c, SliceKernelFrom i c) => Slice To i c -> SliceFactor To i c Source #
the right unit of the cokernel-kernel adjunction slcAdjunction
.
slcKerCoker :: (SliceCokernelTo i c, SliceKernelFrom i c) => Slice From i c -> SliceFactor From i c Source #
the left unit of the cokernel-kenrel adjunction slcAdjunction
.
X
xSliceFactorTo :: (Multiplicative c, Sliced i c) => XOrtSite To c -> i c -> X (SliceFactor To i c) Source #
random variable for
.SliceFactor
To
i c
xSliceFactorFrom :: (Multiplicative c, Sliced i c) => XOrtSite From c -> i c -> X (SliceFactor From i c) Source #
random variable for
.SliceFactor
From
i c
Proposition
prpHomMltSliceCokernelKernel :: (SliceCokernelTo i c, SliceKernelFrom i c) => XOrtSite To c -> XOrtSite From c -> i c -> Statement Source #
validity for the values of SliceCokernelKernel
to be HomMultiplicative
.