OAlg.Limes.Cone.EligibleFactor

eligible factors between Cones.

Eligible Factor

cnEligibleFactor :: a -> Cone s p t n m a -> Cone s p t n m a -> Bool

eligibility of a factor between two cones.

Property Let x be in a and f, t in Cone s p t n m a with cnDiagram f == cnDiagram t, then holds:

1. If p is equal to Projective then holds: cnEligibleFactor x f t is True if and only if

   1. orientation x == tip f :> tip t.
   2. ti * x == fi for all ti in shell t and fi in shell f.

2. If p is equal to Injective then holds: cnEligibleFactor x f t is True if and only if

   1. orientation x == tip f :> tip t.
   2. x * ti == fi for all ti in shell t and fi in shell f.

data EligibleFactor s p t n m a where

predicate for eligible factors between cones.

Property Let e be in EligibleFactor s p t n m a for a Multiplicative structure a, then holds:

1. If e matches EligibleFactorTo l x c then holds: cnDiagram l == cnDiagram c and cnEligibleFactor x c l.
2. If e matches EligibleFactorFrom l x c then holds: cnDiagram l == cnDiagram c and cnEligibleFactor x l c.

Constructors

EligibleFactorTo :: Cone s Projective t n m a -> a -> Cone s Projective t n m a -> EligibleFactor s Projective t n m a

EligibleFactorFrom :: Cone s Injective t n m a -> a -> Cone s Injective t n m a -> EligibleFactor s Injective t n m a

Instances

Show a => Show (EligibleFactor s p t n m a)

Defined in OAlg.Limes.Cone.EligibleFactor

Methods

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

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

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

Oriented a => Validable (EligibleFactor s p t n m a)

Defined in OAlg.Limes.Cone.EligibleFactor

Methods

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

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

Defined in OAlg.Limes.Cone.EligibleFactor

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

elfFactorCone :: EligibleFactor s p t n m a -> (a, Cone s p t n m a)

the underlying factor together with its cone.

elfMap :: Hom s h => h a b -> EligibleFactor s p t n m a -> EligibleFactor s p t n m b

mapping of a eligible factor.

Duality

coEligibleFactor :: EligibleFactor s p t n m a -> Dual (EligibleFactor s p t n m a)

to the dual, with its inverse coEligibleFactorInv.

coEligibleFactorInv :: ConeStruct s a -> (Dual (Dual p) :~: p) -> (Dual (Dual t) :~: t) -> Dual (EligibleFactor s p t n m a) -> EligibleFactor s p t n m a

from the dual, with its inverse coEligibleFactor.

elfFromOpOp :: ConeStruct s a -> EligibleFactor s p t n m (Op (Op a)) -> EligibleFactor s p t n m a

from the bidual.

X

xopEligibleFactor :: ConeStruct s a -> XOrtPerspective p a -> Cone s p t n m a -> X (EligibleFactor s p t n m a)

the induced random variable of eligible factors.

data XOrtPerspective p a where

random variable given by a XOrtSite.

Constructors

XOrtProjective :: XOrtSite To a -> XOrtPerspective Projective a

XOrtInjective :: XOrtSite From a -> XOrtPerspective Injective a

class XStandardOrtPerspective p a where

standard random variable for XOrtPerspective.

Methods

xStandardOrtPerspective :: XOrtPerspective p a

Instances

XStandardOrtSiteFrom a => XStandardOrtPerspective 'Injective a

Defined in OAlg.Limes.Cone.EligibleFactor

Methods

xStandardOrtPerspective :: XOrtPerspective 'Injective a

XStandardOrtSiteTo a => XStandardOrtPerspective 'Projective a

Defined in OAlg.Limes.Cone.EligibleFactor

Methods

xStandardOrtPerspective :: XOrtPerspective 'Projective a

xosEligibleFactorPrj :: XOrtSite To a -> Cone s Projective t n m a -> X (EligibleFactor s Projective t n m a)

the induced random variable of eligible factors.

xosEligibleFactorInj :: ConeStruct s a -> (Dual (Dual t) :~: t) -> XOrtSite From a -> Cone s Injective t n m a -> X (EligibleFactor s Injective t n m a)

the induced random variable of eligible factors.