OAlg.Data.Generator

Generator for finitely generated Points within a Distributive structure.

Generator

data Generator s a where

generator for finitely generated Points within a Distributive structure.

Property Let Generator d k' k'' coker ker lft be in Generator and let DiagramChainTo g (p:|p':|Nil) = d

         p           p'
  g <<------- g' <------< g''

then holds:

1. coker is the cokernel of p' with p as the shell of its universal cone.
2. ker is the kernel of p with p' as the shell of its universal cone.
3. 'KenrelSliceFromSomeFreeTip k'' k' ker is valid.

4. For all h = SliceFrom _ h' in Slice From (Free k) a with end h' == g holds:

   1. lft h is valid.
   2. orientation (lft h) == start h :> start p.
   3. p * lft h == h'.

            g'
           ^ |
          /  |
  lft h  /   | p
        /    |
       /     v
      * ---> g
         h'

Constructors

GeneratorTo :: (Attestable k', Sliced (Free k') a, Attestable k'', Sliced (Free k'') a) => Diagram (Chain To) N3 N2 a -> Free k' a -> Free k'' a -> Cokernel N1 a -> Kernel N1 a -> (forall (k :: N'). Slice From (Free k) a -> a) -> Generator To a

Instances

(Distributive a, XStandardOrtSiteFrom a, XStandardOrtSiteTo a, XStandardSomeFreeSliceFromLiftable a) => Validable (Generator 'To a)

Defined in OAlg.Data.Generator

Methods

valid :: Generator 'To a -> Statement

X

newtype XSomeFreeSliceFromLiftable a

random variable of factors in a having a free start and as end-point the given one.

Constructors

XSomeFreeSliceFromLiftable (Point a -> X (SomeFreeSlice From a))

Instances

(Oriented a, XStandardPoint a) => Validable (XSomeFreeSliceFromLiftable a)

Defined in OAlg.Data.Generator

Methods

valid :: XSomeFreeSliceFromLiftable a -> Statement

xsfsfl :: XSomeFreeSliceFromLiftable a -> Point a -> X (SomeFreeSlice From a)

the underlying random variable for some free slice.

class XStandardSomeFreeSliceFromLiftable a where

random variable of lift-able free slice froms.

Property Let a be in instance of XStandardSomeFreeSliceFromLiftable then holds: For all p in Point a and SomeFreeSlice (SliceFrom _ h) in the range of xStandardSomeFreeSliceFromLiftable p holds: end h == p.

Methods

xStandardSomeFreeSliceFromLiftable :: XSomeFreeSliceFromLiftable a