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

OAlg.Limes.KernelsAndCokernels

Contents

Kernels
- Construction
  - Orientation
Cokernels
- Construction
  - Orientation
Proposition
X

Description

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

Synopsis

type Kernels (n :: N') = KernelsG Cone Diagram n
type KernelsG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimitsG c Dst 'Projective d ('Parallel 'LeftToRight) N2 n
type Kernel (n :: N') = KernelG Cone Diagram n
type KernelG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimesG c Dst 'Projective d ('Parallel 'LeftToRight) N2 n
type KernelCone (n :: N') = KernelConic Cone Diagram n
type KernelConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = c Dst 'Projective d ('Parallel 'LeftToRight) N2 n
type KernelDiagram (n :: N') = KernelDiagrammatic Diagram n
type KernelDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d ('Parallel 'LeftToRight) N2 n
kernelFactor :: forall c (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. Conic c => KernelConic c d n x -> x
kernelDiagram :: Oriented x => x -> KernelDiagram N1 x
kernels :: forall x (n :: N'). Distributive x => Kernels N1 x -> Kernels n x
kernels' :: forall x q (n :: N'). Distributive x => q n -> Kernels N1 x -> Kernels n x
kernels0 :: Distributive x => Kernels N0 x
kernels1 :: forall x (n :: N'). Distributive x => Kernels N1 x -> Kernels (n + 1) x
krnEqls :: forall x (n :: N'). (Distributive x, Abelian x) => Kernels n x -> Equalizers (n + 1) x
eqlKrns :: forall x (n :: N'). Distributive x => Equalizers (n + 1) x -> Kernels n x
kernelZero :: Distributive x => p x -> Orientation (Point x) -> Kernel N1 x
kernelsOrnt :: forall p (n :: N'). Entity p => p -> Kernels n (Orientation p)
type Cokernels (n :: N') = CokernelsG Cone Diagram n
type CokernelsG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimitsG c Dst 'Injective d ('Parallel 'RightToLeft) N2 n
type Cokernel (n :: N') = CokernelG Cone Diagram n
type CokernelG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimesG c Dst 'Injective d ('Parallel 'RightToLeft) N2 n
type CokernelCone (n :: N') = CokernelConic Cone Diagram n
type CokernelConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = c Dst 'Injective d ('Parallel 'RightToLeft) N2 n
type CokernelDiagram (n :: N') = CokernelDiagrammatic Diagram n
type CokernelDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d ('Parallel 'RightToLeft) N2 n
cokernelFactor :: forall c (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. Conic c => CokernelConic c d n x -> x
cokernelDiagram :: Oriented x => x -> CokernelDiagram N1 x
cokernels :: forall x (n :: N'). Distributive x => Cokernels N1 x -> Cokernels n x
cokernels' :: forall x q (n :: N'). Distributive x => q n -> Cokernels N1 x -> Cokernels n x
coKernelsG :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). (Distributive x, TransformableGRefl o Dst, NaturalConicBi (IsoO Dst o) c Dst 'Projective d ('Parallel 'LeftToRight) N2 n) => KernelsG c d n x -> CokernelsG c d n (o x)
cokernelsOrnt :: forall p (n :: N'). Entity p => p -> Cokernels n (Orientation p)
prpIsKernel :: forall a (n :: N'). Distributive a => Kernel n a -> FinList n a -> a -> Statement
prpIsCokernel :: forall x (n :: N'). Distributive x => Cokernel n x -> FinList n x -> x -> Statement
class XStandardEligibleConeG Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x => XStandardEligibleConeKernel (n :: N') x
class XStandardEligibleConeKernel N1 c => XStandardEligibleConeKernel1 c
class XStandardEligibleConeFactorG Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x => XStandardEligibleConeFactorKernel (n :: N') x
class XStandardEligibleConeFactorKernel N1 c => XStandardEligibleConeFactorKernel1 c
class XStandardEligibleConeG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n x => XStandardEligibleConeCokernel (n :: N') x
class XStandardEligibleConeCokernel N1 c => XStandardEligibleConeCokernel1 c
class XStandardEligibleConeFactorG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n x => XStandardEligibleConeFactorCokernel (n :: N') x
class XStandardEligibleConeFactorCokernel N1 c => XStandardEligibleConeFactorCokernel1 c

Kernels

type Kernels (n :: N') = KernelsG Cone Diagram n Source #

kernels for Distributive structures.

type KernelsG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimitsG c Dst 'Projective d ('Parallel 'LeftToRight) N2 n Source #

generic kernels for Distributive structures.

type Kernel (n :: N') = KernelG Cone Diagram n Source #

kernel as a KernelG.

type KernelG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimesG c Dst 'Projective d ('Parallel 'LeftToRight) N2 n Source #

generic kernel as a LimesG.

type KernelCone (n :: N') = KernelConic Cone Diagram n Source #

Cone for a kernel.

type KernelConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = c Dst 'Projective d ('Parallel 'LeftToRight) N2 n Source #

Conic object for a kernel.

type KernelDiagram (n :: N') = KernelDiagrammatic Diagram n Source #

Diagram for a kernel.

type KernelDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d ('Parallel 'LeftToRight) N2 n Source #

Diagrammatic object for a kernel.

kernelFactor :: forall c (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. Conic c => KernelConic c d n x -> x Source #

the factor of its shell.

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

the kernel diagram of a given factor.

Construction

kernels :: forall x (n :: N'). Distributive x => Kernels N1 x -> Kernels n x Source #

promoting kernels.

kernels' :: forall x q (n :: N'). Distributive x => q n -> Kernels N1 x -> Kernels n x Source #

promoting kernels according to the given proxy type.

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

kernels for zero arrows.

kernels1 :: forall x (n :: N'). Distributive x => Kernels N1 x -> Kernels (n + 1) x Source #

promoting kernels.

krnEqls :: forall x (n :: N'). (Distributive x, Abelian x) => Kernels n x -> Equalizers (n + 1) x Source #

the induced equalizers where its first arrow is zero.

eqlKrns :: forall x (n :: N'). Distributive x => Equalizers (n + 1) x -> Kernels n x Source #

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

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

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

Orientation

kernelsOrnt :: forall p (n :: N'). Entity p => p -> Kernels n (Orientation p) Source #

kernels for Orientation.

Cokernels

type Cokernels (n :: N') = CokernelsG Cone Diagram n Source #

cokernels for Distributive structures.

type CokernelsG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimitsG c Dst 'Injective d ('Parallel 'RightToLeft) N2 n Source #

generic cokernels for Distributive structures.

type Cokernel (n :: N') = CokernelG Cone Diagram n Source #

cokernel as a CokernelG.

type CokernelG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimesG c Dst 'Injective d ('Parallel 'RightToLeft) N2 n Source #

generic cokernel as a LimesG.

type CokernelCone (n :: N') = CokernelConic Cone Diagram n Source #

Cone for a cokernel.

type CokernelConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = c Dst 'Injective d ('Parallel 'RightToLeft) N2 n Source #

Conic object for a cokernel.

type CokernelDiagram (n :: N') = CokernelDiagrammatic Diagram n Source #

Diagram for a cokernel.

type CokernelDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d ('Parallel 'RightToLeft) N2 n Source #

Diagrammatic object for a cokernel.

cokernelFactor :: forall c (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. Conic c => CokernelConic c d n x -> x Source #

the factor of its shell.

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

the cokernel diagram of a given factor.

Construction

cokernels :: forall x (n :: N'). Distributive x => Cokernels N1 x -> Cokernels n x Source #

promoting cokernels.

cokernels' :: forall x q (n :: N'). Distributive x => q n -> Cokernels N1 x -> Cokernels n x Source #

promoting cokernels according to the given proxy type.

coKernelsG :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). (Distributive x, TransformableGRefl o Dst, NaturalConicBi (IsoO Dst o) c Dst 'Projective d ('Parallel 'LeftToRight) N2 n) => KernelsG c d n x -> CokernelsG c d n (o x) Source #

to co-object of kernels.

Orientation

cokernelsOrnt :: forall p (n :: N'). Entity p => p -> Cokernels n (Orientation p) Source #

cokernels for Orientation.

Proposition

prpIsKernel :: forall a (n :: N'). 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 :: forall x (n :: N'). Distributive x => Cokernel n x -> FinList n x -> x -> 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