OAlg.Limes.Cone.Definition

definition of Cones over Diagrams.

Cone

data Cone s p t n m a where

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.

Constructors

ConeProjective :: Multiplicative a => Diagram t n m a -> Point a -> FinList n a -> Cone Mlt Projective t n m a

ConeInjective :: Multiplicative a => Diagram t n m a -> Point a -> FinList n a -> Cone Mlt Injective t n m a

ConeKernel :: Distributive a => Diagram (Parallel LeftToRight) N2 m a -> a -> Cone Dst Projective (Parallel LeftToRight) N2 m a

ConeCokernel :: Distributive a => Diagram (Parallel RightToLeft) N2 m a -> a -> Cone Dst Injective (Parallel RightToLeft) N2 m a

Instances

HomDistributive h => Applicative1 h (Cone Dst p t n m)

Defined in OAlg.Limes.Cone.Definition

Methods

amap1 :: h a b -> Cone Dst p t n m a -> Cone Dst p t n m b

HomMultiplicative h => Applicative1 h (Cone Mlt p t n m)

Defined in OAlg.Limes.Cone.Definition

Methods

amap1 :: h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b

Show (Cone s p t n m a)

Defined in OAlg.Limes.Cone.Definition

Methods

showsPrec :: Int -> Cone s p t n m a -> ShowS

show :: Cone s p t n m a -> String

showList :: [Cone s p t n m a] -> ShowS

Eq (Cone s p t n m a)

Defined in OAlg.Limes.Cone.Definition

Methods

(==) :: Cone s p t n m a -> Cone s p t n m a -> Bool

(/=) :: Cone s p t n m a -> Cone s p t n m a -> Bool

Validable (Cone s p t n m a)

Defined in OAlg.Limes.Cone.Definition

Methods

valid :: Cone s p t n m a -> Statement

(Entity p, t ~ 'Parallel 'RightToLeft, n ~ N2, XStandard p, XStandard (Diagram t n m (Orientation p))) => XStandard (Cone Dst 'Injective t n m (Orientation p))

Defined in OAlg.Limes.Cone.Definition

Methods

xStandard :: X (Cone Dst 'Injective t n m (Orientation p))

(Entity p, t ~ 'Parallel 'LeftToRight, n ~ N2, XStandard p, XStandard (Diagram t n m (Orientation p))) => XStandard (Cone Dst 'Projective t n m (Orientation p))

Defined in OAlg.Limes.Cone.Definition

Methods

xStandard :: X (Cone Dst 'Projective t n m (Orientation p))

(Entity p, XStandard p, XStandard (Diagram t n m (Orientation p))) => XStandard (Cone Mlt 'Injective t n m (Orientation p))

Defined in OAlg.Limes.Cone.Definition

Methods

xStandard :: X (Cone Mlt 'Injective t n m (Orientation p))

(Entity p, XStandard p, XStandard (Diagram t n m (Orientation p))) => XStandard (Cone Mlt 'Projective t n m (Orientation p))

Defined in OAlg.Limes.Cone.Definition

Methods

xStandard :: X (Cone Mlt 'Projective t n m (Orientation p))

(Typeable s, Typeable p, Typeable t, Typeable n, Typeable m, Typeable a) => Entity (Cone s p t n m a)

Defined in OAlg.Limes.Cone.Definition

(Oriented a, Typeable s, Typeable p, Typeable d, Typeable m) => Oriented (Cone s p ('Parallel d) N2 m a)

Defined in OAlg.Limes.Cone.Definition

Associated Types

type Point (Cone s p ('Parallel d) N2 m a)

Methods

orientation :: Cone s p ('Parallel d) N2 m a -> Orientation (Point (Cone s p ('Parallel d) N2 m a))

start :: Cone s p ('Parallel d) N2 m a -> Point (Cone s p ('Parallel d) N2 m a)

end :: Cone s p ('Parallel d) N2 m a -> Point (Cone s p ('Parallel d) N2 m a)

type Dual (Cone s p t n m a :: Type)

Defined in OAlg.Limes.Cone.Definition

type Dual (Cone s p t n m a :: Type) = Cone s (Dual p) (Dual t) n m (Op a)

type Point (Cone s p ('Parallel d) N2 m a)

Defined in OAlg.Limes.Cone.Definition

type Point (Cone s p ('Parallel d) N2 m a) = Point a

data Perspective

concept of Projective and Injective.

Constructors

Projective

Injective

Instances

Bounded Perspective

Defined in OAlg.Limes.Perspective

Methods

minBound :: Perspective

maxBound :: Perspective

Enum Perspective

Defined in OAlg.Limes.Perspective

Methods

succ :: Perspective -> Perspective

pred :: Perspective -> Perspective

toEnum :: Int -> Perspective

fromEnum :: Perspective -> Int

enumFrom :: Perspective -> [Perspective]

enumFromThen :: Perspective -> Perspective -> [Perspective]

enumFromTo :: Perspective -> Perspective -> [Perspective]

enumFromThenTo :: Perspective -> Perspective -> Perspective -> [Perspective]

Show Perspective

Defined in OAlg.Limes.Perspective

Methods

showsPrec :: Int -> Perspective -> ShowS

show :: Perspective -> String

showList :: [Perspective] -> ShowS

Eq Perspective

Defined in OAlg.Limes.Perspective

Methods

(==) :: Perspective -> Perspective -> Bool

(/=) :: Perspective -> Perspective -> Bool

Ord Perspective

Defined in OAlg.Limes.Perspective

Methods

compare :: Perspective -> Perspective -> Ordering

(<) :: Perspective -> Perspective -> Bool

(<=) :: Perspective -> Perspective -> Bool

(>) :: Perspective -> Perspective -> Bool

(>=) :: Perspective -> Perspective -> Bool

max :: Perspective -> Perspective -> Perspective

min :: Perspective -> Perspective -> Perspective

type Dual 'Injective

Defined in OAlg.Limes.Perspective

type Dual 'Injective = 'Projective

type Dual 'Projective

Defined in OAlg.Limes.Perspective

type Dual 'Projective = 'Injective

cnDiagram :: Cone s p t n m a -> Diagram t n m a

the underlying diagram.

cnDiagramTypeRefl :: Cone s p t n m a -> Dual (Dual t) :~: t

reflexivity of the underlying diagram type.

tip :: Cone s p t n m a -> Point a

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.

shell :: Cone s p t n m a -> FinList n a

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.

cnArrows :: Cone s p t n m a -> FinList m a

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

cnPoints :: Oriented a => Cone s p t n m a -> FinList n (Point a)

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

cnMap :: Hom s h => h a b -> Cone s p t n m a -> Cone s p t n m b

mapping of a cone.

cnMapMlt :: Hom Mlt h => h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b

mapping of a cone under a Multiplicative homomorphism.

cnMapDst :: Hom Dst h => h a b -> Cone Dst p t n m a -> Cone Dst p t n m b

mapping of a cone under a Distributive homomorphism.

Distributive

cnZeroHead :: Cone Dst p t n m a -> ConeZeroHead Mlt p t n (m + 1) a

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

cnKernel :: (Distributive a, p ~ Projective, t ~ Parallel LeftToRight) => ConeZeroHead Mlt p t n (m + 1) a -> Cone Dst p t n m a

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

cnCokernel :: (Distributive a, p ~ Injective, t ~ Parallel RightToLeft) => ConeZeroHead Mlt p t n (m + 1) a -> Cone Dst p t n m a

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

cnDiffHead :: (Distributive a, Abelian a) => Cone Mlt p (Parallel d) n (m + 1) a -> ConeZeroHead Mlt p (Parallel d) n (m + 1) a

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

newtype ConeZeroHead s p t n m a

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

Constructors

ConeZeroHead (Cone s p t n m a)

Instances

Show (ConeZeroHead s p t n m a)

Defined in OAlg.Limes.Cone.Definition

Methods

showsPrec :: Int -> ConeZeroHead s p t n m a -> ShowS

show :: ConeZeroHead s p t n m a -> String

showList :: [ConeZeroHead s p t n m a] -> ShowS

Eq (ConeZeroHead s p t n m a)

Defined in OAlg.Limes.Cone.Definition

Methods

(==) :: ConeZeroHead s p t n m a -> ConeZeroHead s p t n m a -> Bool

(/=) :: ConeZeroHead s p t n m a -> ConeZeroHead s p t n m a -> Bool

Distributive a => Validable (ConeZeroHead s p d n ('S m) a)

Defined in OAlg.Limes.Cone.Definition

Methods

valid :: ConeZeroHead s p d n ('S m) a -> Statement

(Distributive a, Typeable s, Typeable p, Typeable t, Typeable n, Typeable m) => Entity (ConeZeroHead s p t n ('S m) a)

Defined in OAlg.Limes.Cone.Definition

type Dual (ConeZeroHead s p t n m a :: TYPE LiftedRep)

Defined in OAlg.Limes.Cone.Definition

type Dual (ConeZeroHead s p t n m a :: TYPE LiftedRep) = ConeZeroHead s (Dual p) (Dual t) n m (Op a)

coConeZeroHead :: ConeZeroHead s p t n m a -> Dual (ConeZeroHead s p t n m a)

to the dual, with its inverse coConeZeroHead.

czFromOpOp :: ConeStruct s a -> ConeZeroHead s p t n m (Op (Op a)) -> ConeZeroHead s p t n m a

from the bidual.

coConeZeroHeadInv :: ConeStruct s a -> (Dual (Dual p) :~: p) -> (Dual (Dual t) :~: t) -> Dual (ConeZeroHead s p t n m a) -> ConeZeroHead s p t n m a

from the dual, with its inverse coConeZeroHead.

Duality

cnToOp :: ConeDuality s f g a -> f a -> g (Op a)

to g (Op a).

cnFromOp :: ConeDuality s f g a -> g (Op a) -> f a

from g (Op a).

data ConeDuality s f g a where

Op-duality between cone types.

Constructors

ConeDuality :: ConeStruct s a -> (f a :~: Cone s p t n m a) -> (g (Op a) :~: Dual (Cone s p t n m a)) -> (Dual (Dual p) :~: p) -> (Dual (Dual t) :~: t) -> ConeDuality s f g a

coCone :: Cone s p t n m a -> Dual (Cone s p t n m a)

to the dual cone, with its inverse coConeInv.

coConeInv :: ConeStruct s a -> (Dual (Dual p) :~: p) -> (Dual (Dual t) :~: t) -> Dual (Cone s p t n m a) -> Cone s p t n m a

from the dual cone, with its inverse coCone.

cnFromOpOp :: ConeStruct s a -> Cone s p t n m (Op (Op a)) -> Cone s p t n m a

from Op . Op.

Cone Struct

data ConeStruct s a where

cone structures.

Constructors

ConeStructMlt :: Multiplicative a => ConeStruct Mlt a

ConeStructDst :: Distributive a => ConeStruct Dst a

Instances

Show (ConeStruct s a)

Defined in OAlg.Limes.Cone.Definition

Methods

showsPrec :: Int -> ConeStruct s a -> ShowS

show :: ConeStruct s a -> String

showList :: [ConeStruct s a] -> ShowS

Eq (ConeStruct s a)

Defined in OAlg.Limes.Cone.Definition

Methods

(==) :: ConeStruct s a -> ConeStruct s a -> Bool

(/=) :: ConeStruct s a -> ConeStruct s a -> Bool

cnStructOp :: ConeStruct s a -> ConeStruct s (Op a)

the opposite cone structure.

cnStructMlt :: ConeStruct s a -> Struct Mlt a

the Multiplicative structure of a cone structure.

cnStruct :: ConeStruct s a -> Struct s a

the associated structure of a cone structure.

Orientation

cnPrjOrnt :: Entity p => p -> Diagram t n m (Orientation p) -> Cone Mlt Projective t n m (Orientation p)

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

cnInjOrnt :: Entity p => p -> Diagram t n m (Orientation p) -> Cone Mlt Injective t n m (Orientation p)

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

Chain

cnPrjChainTo :: Multiplicative a => FactorChain To n a -> Cone Mlt Projective (Chain To) (n + 1) n a

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.

cnPrjChainToInv :: Cone Mlt Projective (Chain To) (n + 1) n a -> FactorChain To n a

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

cnPrjChainFrom :: Multiplicative a => FactorChain From n a -> Cone Mlt Projective (Chain From) (n + 1) n a

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.

cnPrjChainFromInv :: Cone Mlt Projective (Chain From) (n + 1) n a -> FactorChain From n a

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

data FactorChain s n a

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.

Constructors

FactorChain a (Diagram (Chain s) (n + 1) n a)

Instances

Oriented a => Show (FactorChain s n a)

Defined in OAlg.Limes.Cone.Definition

Methods

showsPrec :: Int -> FactorChain s n a -> ShowS

show :: FactorChain s n a -> String

showList :: [FactorChain s n a] -> ShowS

Oriented a => Eq (FactorChain s n a)

Defined in OAlg.Limes.Cone.Definition

Methods

(==) :: FactorChain s n a -> FactorChain s n a -> Bool

(/=) :: FactorChain s n a -> FactorChain s n a -> Bool

Oriented a => Validable (FactorChain 'From n a)

Defined in OAlg.Limes.Cone.Definition

Methods

valid :: FactorChain 'From n a -> Statement

Oriented a => Validable (FactorChain 'To n a)

Defined in OAlg.Limes.Cone.Definition

Methods

valid :: FactorChain 'To n a -> Statement

(Multiplicative a, Typeable n) => Entity (FactorChain 'From n a)

Defined in OAlg.Limes.Cone.Definition

(Multiplicative a, Typeable n) => Entity (FactorChain 'To n a)

Defined in OAlg.Limes.Cone.Definition