cone over a diagram.

Properties Let c be in Cone s p t n m a then holds:

1. If c matches ConeProjective d t cs for a Multiplicative structure a then holds:

   1. For all ci in cs holds: start ci == t and end ci == pi where pi in dgPoints d.
   2. For all aij in dgArrows d holds: aij * ci == cj where ci, cj in cs.

2. If c matches ConeInjective d t cs for a Multiplicative structure a then holds:

   1. For all ci in cs holds: end ci == t and start ci == pi where pi in dgPoints d.
   2. For all aij in dgArrows d holds: cj * aij == ci where ci, cj in cs.

3. If c matches ConeKernel p k for a Distributive structure a then holds:

   1. end k == p0 where p0 in dgPoints p
   2. For all a in dgArrows p holds: a * k == zero (t :> p1) where t = start k and p0, p1 in dgPoints p.

4. If c matches ConeCokernel p k for a Distributive structure a then holds:

   1. start k == p0 where p0 in cnPoints c
   2. For all a in dgArrows p holds: k * a == zero (p1 :> t) where t = end k and p0, p1 in dgPoints p.

concept of Projective and Injective.

the underlying diagram.

reflexivity of the underlying diagram type.

the tip of a cone.

Property Let c be in Cone s p t n m a for a Oriented structure then holds:

1. If p is equal to Projective then holds: start ci == tip c for all ci in shell c.
2. If p is equal to Injective then holds: end ci == tip c for all ci in shell c.

the shell of a cone.

Property Let c be in Cone s p t n m a for a Oriented structure then holds:

1. If p is equal to Projective then holds: fmap end (shell c) == cnPoints c.
2. If p is equal to Injective then holds: fmap start (shell c) == cnPoints c.

the arrows of the underlying diagram, i.e. dgArrows . cnDiagram.

the points of the underlying diagram, i.e. dgPoints . cnDiagram.

mapping of a cone.

mapping of a cone under a Multiplicative homomorphism.

mapping of a cone under a Distributive homomorphism.

embedding of a cone in a distributive structure to its multiplicative cone.

the kernel cone of a zero headed parallel cone, i.e. the inverse of cnZeroHead.

the cokernel cone of a zero headed parallel cone, i.e. the inverse of cnZeroHead.

subtracts to every arrow of the underlying parallel diagram the first arrow and adapts the shell accordingly.

predicate for cones where the first arrow of its underlying diagram is equal to zero.

to the dual, with its inverse coConeZeroHead.

from the bidual.

from the dual, with its inverse coConeZeroHead.

to g (Op a).

from g (Op a).

Op-duality between cone types.

to the dual cone, with its inverse coConeInv.

from the dual cone, with its inverse coCone.

from Op . Op.

cone structures.

the opposite cone structure.

the Multiplicative structure of a cone structure.

the associated structure of a cone structure.

the projective cone on Orientation with the underlying given diagram and tip with the given point.

the injective cone on Orientation with the underlying given diagram and tip with the given point.

the induced Projective cone with ending factor given by the given FactorChain.

Property Let h = FactorChain f d be in FactorChain To n a for a Multiplicative structure a and ConeProjective d' _ (_:|..:|c:|Nil) = cnPrjChainTo h then holds: d' == d and c == f.

the underlying factor chain of a projective chain to cone, i.e the inverse of cnPrjChainToInv.

the induced Projective cone with starting factor given by the given FactorChain.

Property Let h = FactorChain f d be in FactorChain From n a for a Multiplicative structure a and ConeProjective d' _ (c:|_) = cnPrjChainFrom h then holds: d' == d and c == f.

the underlying factor chain of a projective chain from cone, i.e. the inverse of cnPrjChainFrom.

predicate for a factor with end point at the starting point of the given chain.

Property

1. Let FactorChain f d be in FactorChain To n a for a Multiplicative structure a then holds: end f == chnToStart d.
2. Let FactorChain f d be in FactorChain From n a for a Multiplicative structure a then holds: end f == chnFromStart d.