oalg-base-1.1.4.0: Algebraic structures on oriented entities and limits as a tool kit to solve algebraic problems.

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

OAlg.Limes.KernelsAndCokernels

Contents

Kernels
- Construction
  - Orientation
Cokernels
- Construction
  - Orientation
Duality
Proposition

Description

kernels and cokernels, i.e. limits in a Distributive structure of Diagram (Parallel d) making all arrows zero.

Synopsis

type Kernels n = Limits Dst Projective (Parallel LeftToRight) N2 n
type Kernel n = Limes Dst Projective (Parallel LeftToRight) N2 n
type KernelCone n = Cone Dst Projective (Parallel LeftToRight) N2 n
type KernelDiagram n = Diagram (Parallel LeftToRight) N2 n
kernelFactor :: KernelCone N1 c -> c
kernelDiagram :: Oriented c => c -> KernelDiagram N1 c
kernels :: Distributive a => Kernels N1 a -> Kernels n a
kernels0 :: Distributive a => Kernels N0 a
kernels1 :: Distributive a => Kernels N1 a -> Kernels (n + 1) a
krnEqls :: (Distributive a, Abelian a) => Kernels n a -> Equalizers (n + 1) a
eqlKrns :: Distributive a => Equalizers (n + 1) a -> Kernels n a
kernelZero :: Distributive c => p c -> Orientation (Point c) -> Kernel N1 c
kernelsOrnt :: Entity p => p -> Kernels n (Orientation p)
type Cokernels n = Limits Dst Injective (Parallel RightToLeft) N2 n
type Cokernel n = Limes Dst Injective (Parallel RightToLeft) N2 n
type CokernelCone n = Cone Dst Injective (Parallel RightToLeft) N2 n
type CokernelDiagram n = Diagram (Parallel RightToLeft) N2 n
cokernelFactor :: CokernelCone N1 c -> c
cokernelDiagram :: Oriented c => c -> CokernelDiagram N1 c
cokernels :: Distributive a => Cokernels N1 a -> Cokernels n a
cokernels' :: Distributive a => p n -> Cokernels N1 a -> Cokernels n a
cokernelsOrnt :: Entity p => p -> Cokernels n (Orientation p)
krnLimesDuality :: Distributive a => LimesDuality Dst (Kernel n) (Cokernel n) a
cokrnLimesDuality :: Distributive a => LimesDuality Dst (Cokernel n) (Kernel n) a
prpIsKernel :: Distributive a => Kernel n a -> FinList n a -> a -> Statement
prpIsCokernel :: Distributive a => Cokernel n a -> FinList n a -> a -> Statement

Kernels

type Kernels n = Limits Dst Projective (Parallel LeftToRight) N2 n Source #

kernels for Distributive structures.

type Kernel n = Limes Dst Projective (Parallel LeftToRight) N2 n Source #

kernel as a Limes.

type KernelCone n = Cone Dst Projective (Parallel LeftToRight) N2 n Source #

Cone for a kernel.

type KernelDiagram n = Diagram (Parallel LeftToRight) N2 n Source #

Diagram for a kernel.

kernelFactor :: KernelCone N1 c -> c Source #

the factor of its shell.

kernelDiagram :: Oriented c => c -> KernelDiagram N1 c Source #

the kernel diagram of a given factor.

Construction

kernels :: Distributive a => Kernels N1 a -> Kernels n a Source #

promoting kernels.

kernels0 :: Distributive a => Kernels N0 a Source #

kernels for zero arrows.

kernels1 :: Distributive a => Kernels N1 a -> Kernels (n + 1) a Source #

promoting kernels.

krnEqls :: (Distributive a, Abelian a) => Kernels n a -> Equalizers (n + 1) a Source #

the induced equalizers where its first arrow is zero.

eqlKrns :: Distributive a => Equalizers (n + 1) a -> Kernels n a Source #

the induced kernels given by adjoining a zero arrow as first arrow.

kernelZero :: Distributive c => p c -> Orientation (Point c) -> Kernel N1 c Source #

the kernel of the zero factor given by the orientation, i.e. one

Orientation

kernelsOrnt :: Entity p => p -> Kernels n (Orientation p) Source #

kernels for Orientation.

Cokernels

type Cokernels n = Limits Dst Injective (Parallel RightToLeft) N2 n Source #

cokernels for Distributive structures.

type Cokernel n = Limes Dst Injective (Parallel RightToLeft) N2 n Source #

cokernel as Limes.

type CokernelCone n = Cone Dst Injective (Parallel RightToLeft) N2 n Source #

Cone for a cokernel.

type CokernelDiagram n = Diagram (Parallel RightToLeft) N2 n Source #

Diagram for a cokernel.

cokernelFactor :: CokernelCone N1 c -> c Source #

the factor of its shell.

cokernelDiagram :: Oriented c => c -> CokernelDiagram N1 c Source #

the cokernel diagram of a given factor.

Construction

cokernels :: Distributive a => Cokernels N1 a -> Cokernels n a Source #

promoting cokernels.

cokernels' :: Distributive a => p n -> Cokernels N1 a -> Cokernels n a Source #

cokernels given by an additional proxy for n.

Orientation

cokernelsOrnt :: Entity p => p -> Cokernels n (Orientation p) Source #

cokernels for Orientation.

Duality

krnLimesDuality :: Distributive a => LimesDuality Dst (Kernel n) (Cokernel n) a Source #

duality from Kernel to Cokernel.

cokrnLimesDuality :: Distributive a => LimesDuality Dst (Cokernel n) (Kernel n) a Source #

duality between Cokernel to Kernel.

Proposition

prpIsKernel :: Distributive a => Kernel n a -> FinList n a -> a -> Statement Source #

checks if the arrows of the kernel diagram are equal to the given ones and if its shell is equal to the given arrow.

Property Let LimesProjective ('ConeKerenl d k') _ = ker be in Kernel n a, fs in FinList n a and k be in a, then the statement prpIsKernel ker fs k holds if and only if

fs == dgArrows d.
k == k'.

prpIsCokernel :: Distributive a => Cokernel n a -> FinList n a -> a -> Statement Source #

checks if the arrows of the cokernel diagram are equal to the given ones and if its shell is equal to the given arrow.

Property Let LimesInjective ('ConeCokerenl d k') _ = coker be in Cokernel n a, fs in FinList n a and k be in a, then the statement prpIsCokernel coker fs k holds if and only if

fs == dgArrows d.
k == k'.