Copyright | (c) Erich Gut |
---|---|
License | BSD3 |
Maintainer | zerich.gut@gmail.com |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
eligible factors between Cone
s.
Synopsis
- cnEligibleFactor :: a -> Cone s p t n m a -> Cone s p t n m a -> Bool
- data EligibleFactor s p t n m a where
- 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
- elfFactorCone :: EligibleFactor s p t n m a -> (a, Cone s p t n m a)
- elfMap :: Hom s h => h a b -> EligibleFactor s p t n m a -> EligibleFactor s p t n m b
- coEligibleFactor :: EligibleFactor s p t n m a -> Dual (EligibleFactor s p t n m a)
- 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
- elfFromOpOp :: ConeStruct s a -> EligibleFactor s p t n m (Op (Op a)) -> EligibleFactor s p t n m a
- xopEligibleFactor :: ConeStruct s a -> XOrtPerspective p a -> Cone s p t n m a -> X (EligibleFactor s p t n m a)
- data XOrtPerspective p a where
- XOrtProjective :: XOrtSite To a -> XOrtPerspective Projective a
- XOrtInjective :: XOrtSite From a -> XOrtPerspective Injective a
- class XStandardOrtPerspective p a where
- xosEligibleFactorPrj :: XOrtSite To a -> Cone s Projective t n m a -> X (EligibleFactor s Projective t n m a)
- 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)
Eligible Factor
cnEligibleFactor :: a -> Cone s p t n m a -> Cone s p t n m a -> Bool Source #
eligibility of a factor between two cones.
Property Let x
be in a
and
f
, t
in
with
Cone
s p t n m a
, then holds:cnDiagram
f ==
cnDiagram
t
If
p
is equal toProjective
then holds:
iscnEligibleFactor
x f tTrue
if and only ifIf
p
is equal toInjective
then holds:
iscnEligibleFactor
x f tTrue
if and only if
data EligibleFactor s p t n m a where Source #
predicate for eligible factors between cones.
Property Let e
be in
for a EligibleFactor
s p t n m aMultiplicative
structure a
, then holds:
- If
e
matches
then holds:EligibleFactorTo
l x c
andcnDiagram
l==
cnDiagram
c
.cnEligibleFactor
x c l - If
e
matches
then holds:EligibleFactorFrom
l x c
andcnDiagram
l==
cnDiagram
c
.cnEligibleFactor
x l c
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) Source # | |
Defined in OAlg.Limes.Cone.EligibleFactor 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) Source # | |
Defined in OAlg.Limes.Cone.EligibleFactor valid :: EligibleFactor s p t n m a -> Statement Source # | |
type Dual (EligibleFactor s p t n m a :: Type) Source # | |
Defined in OAlg.Limes.Cone.EligibleFactor |
elfFactorCone :: EligibleFactor s p t n m a -> (a, Cone s p t n m a) Source #
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 Source #
mapping of a eligible factor.
Duality
coEligibleFactor :: EligibleFactor s p t n m a -> Dual (EligibleFactor s p t n m a) Source #
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 Source #
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 Source #
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) Source #
the induced random variable of eligible factors.
data XOrtPerspective p a where Source #
random variable given by a XOrtSite
.
XOrtProjective :: XOrtSite To a -> XOrtPerspective Projective a | |
XOrtInjective :: XOrtSite From a -> XOrtPerspective Injective a |
class XStandardOrtPerspective p a where Source #
standard random variable for XOrtPerspective
.
Instances
XStandardOrtSiteFrom a => XStandardOrtPerspective 'Injective a Source # | |
Defined in OAlg.Limes.Cone.EligibleFactor | |
XStandardOrtSiteTo a => XStandardOrtPerspective 'Projective a Source # | |
Defined in OAlg.Limes.Cone.EligibleFactor |
xosEligibleFactorPrj :: XOrtSite To a -> Cone s Projective t n m a -> X (EligibleFactor s Projective t n m a) Source #
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) Source #
the induced random variable of eligible factors.