Copyright	(c) Erich Gut
License	BSD3
Maintainer	zerich.gut@gmail.com
Safe Haskell	None
Language	Haskell2010

OAlg.Entity.Slice.Adjunction

Contents

Adjunction
Diagram
Limits
X
Proposition

Description

Cokernel-Kernel Adjunction for Sliced structures.

Synopsis

data SliceAdjunction (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) d x y where
- SliceCokernel :: forall (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) d. SliceCokernels i c d -> SliceAdjunction i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
- SliceKernel :: forall (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) d. SliceKernels i c d -> SliceAdjunction i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
slcAdjunction :: forall d i (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceCokernels i c d -> SliceKernels i c d -> i d -> Adjunction (SliceAdjunction i c d) (SliceFactor 'From i d) (SliceFactor 'To i d)
slcCokerKer :: forall d (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceCokernels i c d -> SliceKernels i c d -> Slice 'To i d -> SliceFactor 'To i d
slcKerCoker :: forall d (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceCokernels i c d -> SliceKernels i c d -> Slice 'From i d -> SliceFactor 'From i d
data SliceDiagram (i :: Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x where
- SliceDiagramKernel :: forall (i :: Type -> Type) x. Sliced i x => Slice 'From i x -> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) ('S N0) x
- SliceDiagramCokernel :: forall (i :: Type -> Type) x. Sliced i x => Slice 'To i x -> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) ('S N0) x
sdgMapS :: forall (i :: Type -> Type) h (t :: DiagramType) x y (n :: N') (m :: N'). (HomSlicedOriented i h, t ~ Dual (Dual t)) => h x y -> SDualBi (SliceDiagram i t n m) x -> SDualBi (SliceDiagram i t n m) y
sdgMapCov :: forall (i :: Type -> Type) (h :: Type -> Type -> Type) x y (t :: DiagramType) (n :: N') (m :: N'). HomSlicedOriented i h => Variant2 'Covariant h x y -> SliceDiagram i t n m x -> SliceDiagram i t n m y
sdgMapCnt :: forall (i :: Type -> Type) (h :: Type -> Type -> Type) x y (t :: DiagramType) (n :: N') (m :: N'). HomSlicedOriented i h => Variant2 'Contravariant h x y -> SliceDiagram i t n m x -> SliceDiagram i (Dual t) n m y
type SliceCokernels (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) = CokernelsG c (SliceDiagram i) N1
slcCokernelsCone :: forall x (i :: Type -> Type). (Distributive x, Sliced i x) => Cokernels N1 x -> SliceCokernels i Cone x
sliceCokernel :: forall d (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceCokernels i c d -> SliceFactor 'To i d -> SliceFactor 'From i d
type SliceKernels (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) = KernelsG c (SliceDiagram i) N1
slcKernelsCone :: forall x (i :: Type -> Type). Distributive x => Kernels N1 x -> SliceKernels i Cone x
sliceKernel :: forall d (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceKernels i c d -> SliceFactor 'From i d -> SliceFactor 'To i d
xSliceFactorFrom :: (Multiplicative d, Sliced i d) => XOrtSite 'From d -> i d -> X (SliceFactor 'From i d)
prpHomOrtSliceAdjunction :: forall d i (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceCokernels i c d -> SliceKernels i c d -> XOrtSite 'To d -> XOrtSite 'From d -> i d -> Statement
prpHomMltSliceAdjunction :: forall d i (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceCokernels i c d -> SliceKernels i c d -> XOrtSite 'To d -> XOrtSite 'From d -> i d -> Statement

Adjunction

data SliceAdjunction (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) d x y where Source #

the left and right homomorphisms for the cokernel-kernel adjunction slcAdjunction within a Distributive structure d.

Constructors

SliceCokernel :: forall (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) d. SliceCokernels i c d -> SliceAdjunction i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
SliceKernel :: forall (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) d. SliceKernels i c d -> SliceAdjunction i c d (SliceFactor 'From i d) (SliceFactor 'To i d)

Instances

Instances details

(Distributive d, Sliced i d, Conic c) => ApplicativeG Id (SliceAdjunction i c d) (->) Source #

Instance details

Defined in OAlg.Entity.Slice.Adjunction

Methods

amapG :: SliceAdjunction i c d x y -> Id x -> Id y Source #

(Distributive d, Sliced i d, Conic c) => ApplicativeG Pnt (SliceAdjunction i c d) (->) Source #

Instance details

Defined in OAlg.Entity.Slice.Adjunction

Methods

amapG :: SliceAdjunction i c d x y -> Pnt x -> Pnt y Source #

(Multiplicative d, Sliced i d) => Morphism (SliceAdjunction i c d) Source #

Instance details

Defined in OAlg.Entity.Slice.Adjunction

Associated Types

type ObjectClass (SliceAdjunction i c d)
Instance details Defined in OAlg.Entity.Slice.Adjunction type ObjectClass (SliceAdjunction i c d) = Mlt

Methods

homomorphous :: SliceAdjunction i c d x y -> Homomorphous (ObjectClass (SliceAdjunction i c d)) x y Source #

domain :: SliceAdjunction i c d x y -> Struct (ObjectClass (SliceAdjunction i c d)) x Source #

range :: SliceAdjunction i c d x y -> Struct (ObjectClass (SliceAdjunction i c d)) y Source #

TransformableObjectClassTyp (SliceAdjunction i c d) Source #

Instance details

Defined in OAlg.Entity.Slice.Adjunction

Show2 (SliceAdjunction i c d) Source #

Instance details

Defined in OAlg.Entity.Slice.Adjunction

Methods

show2 :: SliceAdjunction i c d a b -> String Source #

(Distributive d, Sliced i d, Conic c) => HomMultiplicative (SliceAdjunction i c d) Source #

Instance details

Defined in OAlg.Entity.Slice.Adjunction

(Distributive d, Sliced i d, Conic c) => HomOriented (SliceAdjunction i c d) Source #

Instance details

Defined in OAlg.Entity.Slice.Adjunction

type ObjectClass (SliceAdjunction i c d) Source #

Instance details

Defined in OAlg.Entity.Slice.Adjunction

type ObjectClass (SliceAdjunction i c d) = Mlt

slcAdjunction :: forall d i (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceCokernels i c d -> SliceKernels i c d -> i d -> Adjunction (SliceAdjunction i c d) (SliceFactor 'From i d) (SliceFactor 'To i d) Source #

the cokernel-kenrel adjunction.

slcCokerKer :: forall d (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceCokernels i c d -> SliceKernels i c d -> Slice 'To i d -> SliceFactor 'To i d Source #

the right unit of the cokernel-kernel adjunction slcAdjunction.

slcKerCoker :: forall d (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceCokernels i c d -> SliceKernels i c d -> Slice 'From i d -> SliceFactor 'From i d Source #

the left unit of the cokernel-kenrel adjunction slcAdjunction.

Diagram

data SliceDiagram (i :: Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x where Source #

slice as a kernel respectively cokernel diagram.

Constructors

SliceDiagramKernel :: forall (i :: Type -> Type) x. Sliced i x => Slice 'From i x -> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) ('S N0) x
SliceDiagramCokernel :: forall (i :: Type -> Type) x. Sliced i x => Slice 'To i x -> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) ('S N0) x

Instances

Instances details

Attestable k => NaturalDiagrammaticFree Dst (SliceDiagram (Free k)) N2 N1 Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction
(CategoryDisjunctive h, HomSlicedOriented i h, FunctorialOriented h, t ~ Dual (Dual t)) => NaturalDiagrammatic h (SliceDiagram i) t n m Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction
(CategoryDisjunctive h, HomSlicedOriented i h, FunctorialOriented h, t ~ Dual (Dual t)) => NaturalTransformable h (->) (SDualBi (DiagramG (SliceDiagram i) t n m)) (SDualBi (DiagramG Diagram t n m)) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction
Diagrammatic (SliceDiagram i) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction Methods diagram :: forall (t :: DiagramType) (n :: N') (m :: N') x. SliceDiagram i t n m x -> Diagram t n m x Source #
(HomSlicedOriented i h, t ~ Dual (Dual t)) => ApplicativeG (SDualBi (DiagramG (SliceDiagram i) t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction Methods amapG :: h x y -> SDualBi (DiagramG (SliceDiagram i) t n m) x -> SDualBi (DiagramG (SliceDiagram i) t n m) y Source #
(CategoryDisjunctive h, HomSlicedOriented i h, FunctorialOriented h, t ~ Dual (Dual t)) => FunctorialG (SDualBi (DiagramG (SliceDiagram i) t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction
Show (SliceDiagram i t n m x) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction Methods showsPrec :: Int -> SliceDiagram i t n m x -> ShowS # show :: SliceDiagram i t n m x -> String # showList :: [SliceDiagram i t n m x] -> ShowS #
Eq (SliceDiagram i t n m x) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction Methods (==) :: SliceDiagram i t n m x -> SliceDiagram i t n m x -> Bool # (/=) :: SliceDiagram i t n m x -> SliceDiagram i t n m x -> Bool #
Validable (SliceDiagram i t n m x) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction Methods valid :: SliceDiagram i t n m x -> Statement Source #
type Dual1 (SliceDiagram i t n m :: Type -> Type) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction type Dual1 (SliceDiagram i t n m :: Type -> Type) = SliceDiagram i (Dual t) n m

sdgMapS :: forall (i :: Type -> Type) h (t :: DiagramType) x y (n :: N') (m :: N'). (HomSlicedOriented i h, t ~ Dual (Dual t)) => h x y -> SDualBi (SliceDiagram i t n m) x -> SDualBi (SliceDiagram i t n m) y Source #

mapping a slice diagram.

sdgMapCov :: forall (i :: Type -> Type) (h :: Type -> Type -> Type) x y (t :: DiagramType) (n :: N') (m :: N'). HomSlicedOriented i h => Variant2 'Covariant h x y -> SliceDiagram i t n m x -> SliceDiagram i t n m y Source #

mapping a slice diagram according to a covariant homomorphism.

sdgMapCnt :: forall (i :: Type -> Type) (h :: Type -> Type -> Type) x y (t :: DiagramType) (n :: N') (m :: N'). HomSlicedOriented i h => Variant2 'Contravariant h x y -> SliceDiagram i t n m x -> SliceDiagram i (Dual t) n m y Source #

mapping a slice diagram according to a contravariant homomorphism.

Limits

type SliceCokernels (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) = CokernelsG c (SliceDiagram i) N1 Source #

generalized cokernels according to a slice diagram.

slcCokernelsCone :: forall x (i :: Type -> Type). (Distributive x, Sliced i x) => Cokernels N1 x -> SliceCokernels i Cone x Source #

the induced slice cokernels for Cones.

sliceCokernel :: forall d (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceCokernels i c d -> SliceFactor 'To i d -> SliceFactor 'From i d Source #

the slice factor From according to the given slice cokernels and a slice To. It is the base for SliceCokernel.

type SliceKernels (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) = KernelsG c (SliceDiagram i) N1 Source #

generalized kernels according to a slice diagram.

slcKernelsCone :: forall x (i :: Type -> Type). Distributive x => Kernels N1 x -> SliceKernels i Cone x Source #

the induced slice kernels for Cones.

sliceKernel :: forall d (i :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceKernels i c d -> SliceFactor 'From i d -> SliceFactor 'To i d Source #

the slice factor To according to the given slice kernels and a slice From. It is the base for SliceKernel.

X

xSliceFactorFrom :: (Multiplicative d, Sliced i d) => XOrtSite 'From d -> i d -> X (SliceFactor 'From i d) Source #

random variable for SliceFactor From i d.

Proposition

prpHomOrtSliceAdjunction :: forall d i (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceCokernels i c d -> SliceKernels i c d -> XOrtSite 'To d -> XOrtSite 'From d -> i d -> Statement Source #

validity for the values of SliceAdjunction to be HomOriented.

prpHomMltSliceAdjunction :: forall d i (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). (Distributive d, Sliced i d, Conic c) => SliceCokernels i c d -> SliceKernels i c d -> XOrtSite 'To d -> XOrtSite 'From d -> i d -> Statement Source #

validity for the values of SliceAdjunction being HomMultiplicative.