Copyright	(c) Erich Gut
License	BSD3
Maintainer	zerich.gut@gmail.com
Safe Haskell	None
Language	Haskell2010

OAlg.Limes.Exact.Deviation

Contents

Deviation
Deviation Hom
Variance
- Duality
Variance Hom
- Duality
Proposition

Description

measuring the deviation exactness.

Synopsis

deviation :: forall x (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N'). (Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d, Typeable t, Typeable n) => VarianceG t k c d n x -> Point x
deviations :: forall x (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N'). (Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d, Typeable t, Attestable n) => VarianceG t k c d n x -> Deviation (n + 1) x
type Deviation (n :: N') = Diagram 'Discrete n N0
dvZeroPoint :: forall x (n :: N'). ZeroPoint x -> Any n -> ZeroPoint (DeviationHom n x)
dvZeroPoint' :: forall (n :: N') q x. Attestable n => q n -> ZeroPoint x -> ZeroPoint (DeviationHom n x)
deviationHom :: forall x (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') (t :: Site). (Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d, Attestable n) => VarianceGHom t k c d n x -> DeviationHom (n + 1) x
type DeviationHom (n :: N') = DiagramTrafo 'Discrete n N0
variance :: forall x (t :: Site) (n :: N'). Distributive x => Kernels N1 x -> Cokernels N1 x -> ConsecutiveZero t n x -> Variance t n x
data VarianceG (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x where
- VarianceG :: forall (t :: Site) (n :: N') x (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). ConsecutiveZero t n x -> FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x) -> VarianceG t k c d n x
type Variance (t :: Site) = VarianceG t Cone Cone Diagram
isExact :: forall x (t :: Site) (n :: N'). (Distributive x, Typeable t, Attestable n) => Kernels N1 x -> Cokernels N1 x -> ConsecutiveZero t n x -> Bool
isExactVariance :: forall x (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N'). (Distributive x, NaturalConicBi (IsoO Dst Op) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConicBi (IsoO Dst Op) c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, Typeable t, Attestable n) => VarianceG t k c d n x -> Bool
vrcConsZeroHom :: forall x (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N'). (Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d) => VarianceG t k c d n x -> ConsecutiveZeroHom t n x
vrcSite :: forall (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. VarianceG t k c d n x -> Either (t :~: 'From) (t :~: 'To)
vrcHead :: forall x (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). Distributive x => VarianceG t k c d n x -> VarianceG t k c d N0 x
vrcTail :: forall x (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). Distributive x => VarianceG t k c d (n + 1) x -> VarianceG t k c d n x
type NaturalKernelCokernel (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = (NaturalConic h k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConic h k Dst 'Injective d ('Parallel 'RightToLeft) N2 N1, NaturalConic h c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConic h c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
type EntityDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) x = (Typeable d, Entity (d ('Parallel 'LeftToRight) N2 N1 x), Entity (d ('Parallel 'RightToLeft) N2 N1 x), Entity (d ('Parallel 'LeftToRight) N2 N1 (Op x)), Entity (d ('Parallel 'RightToLeft) N2 N1 (Op x)))
type ObjectKernelCokernel (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) x = (Diagrammatic d, Object (k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x), Object (k Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 (Op x)), Object (c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x), Object (c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 (Op x)))
vrcMapS :: forall (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (t :: Site) x y (n :: N'). (HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalConicBi (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConicBi (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1, t ~ Dual (Dual t)) => Inv2 h x y -> SDualBi (VarianceG t k c d n) x -> SDualBi (VarianceG t k c d n) y
vrcMapCov :: forall (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) x y (t :: Site) (n :: N'). (HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalConic (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConic (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) => Variant2 'Covariant (Inv2 h) x y -> VarianceG t k c d n x -> VarianceG t k c d n y
vrcMapCnt :: forall (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) x y (t :: Site) (n :: N'). (HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalConic (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConic (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) => Variant2 'Contravariant (Inv2 h) x y -> VarianceG t k c d n x -> VarianceG (Dual t) c k d n y
varianceHom :: forall x (t :: Site) (n :: N'). (Distributive x, Typeable t, Attestable n) => Kernels N1 x -> Cokernels N1 x -> ConsecutiveZeroHom t n x -> VarianceHom t n x
data VarianceGHom (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x = VarianceGHom (VarianceG t k c d n x) (VarianceG t k c d n x) (FinList (n + 3) x)
type VarianceHom (t :: Site) = VarianceGHom t Cone Cone Diagram
vrcHomSite :: forall (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. VarianceGHom t k c d n x -> Either (t :~: 'From) (t :~: 'To)
vrcHomConsZeroHom :: forall (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. VarianceGHom t k c d n x -> ConsecutiveZeroHom t n x
vrcHomMapS :: forall (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (t :: Site) x y (n :: N'). (HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalConicBi (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConicBi (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1, t ~ Dual (Dual t)) => Inv2 h x y -> SDualBi (VarianceGHom t k c d n) x -> SDualBi (VarianceGHom t k c d n) y
vrcHomMapCov :: forall (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) x y (t :: Site) (n :: N'). (HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalConic (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConic (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) => Variant2 'Covariant (Inv2 h) x y -> VarianceGHom t k c d n x -> VarianceGHom t k c d n y
vrcHomMapCnt :: forall (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) x y (t :: Site) (n :: N'). (HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalConic (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConic (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) => Variant2 'Contravariant (Inv2 h) x y -> VarianceGHom t k c d n x -> VarianceGHom (Dual t) c k d n y
prpVarianceG :: forall x (d :: DiagramType -> N' -> N' -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N'). (Distributive x, EntityDiagrammatic d x, NaturalKernelCokernel (IsoO Dst Op) k c d, ObjectKernelCokernel k c d x) => XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x -> XEligibleConeFactorG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x -> XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x -> XEligibleConeFactorG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x -> VarianceG t k c d n x -> Statement
prpVarianceGHom :: forall x (d :: DiagramType -> N' -> N' -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N'). (Distributive x, EntityDiagrammatic d x, NaturalKernelCokernel (IsoO Dst Op) k c d, ObjectKernelCokernel k c d x, Typeable t, Typeable n) => XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x -> XEligibleConeFactorG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x -> XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x -> XEligibleConeFactorG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x -> VarianceGHom t k c d n x -> Statement
prpDeviationOrntSymbol :: Statement

Deviation

deviation :: forall x (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N'). (Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d, Typeable t, Typeable n) => VarianceG t k c d n x -> Point x Source #

the deviation of being exact, i.e. the Point a' in the diagram of VarianceG.

deviations :: forall x (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N'). (Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d, Typeable t, Attestable n) => VarianceG t k c d n x -> Deviation (n + 1) x Source #

the induced Deviations.

type Deviation (n :: N') = Diagram 'Discrete n N0 Source #

measuring the deviations.

dvZeroPoint :: forall x (n :: N'). ZeroPoint x -> Any n -> ZeroPoint (DeviationHom n x) Source #

zero point for DeviationHom n x.

dvZeroPoint' :: forall (n :: N') q x. Attestable n => q n -> ZeroPoint x -> ZeroPoint (DeviationHom n x) Source #

zero point for DeviationHom n x according to the given proxy type.

Deviation Hom

deviationHom :: forall x (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') (t :: Site). (Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d, Attestable n) => VarianceGHom t k c d n x -> DeviationHom (n + 1) x Source #

the induced homomorphism between Deviations.

type DeviationHom (n :: N') = DiagramTrafo 'Discrete n N0 Source #

transormation between Deviations.

Variance

variance :: forall x (t :: Site) (n :: N'). Distributive x => Kernels N1 x -> Cokernels N1 x -> ConsecutiveZero t n x -> Variance t n x Source #

the variance according to Kernels and Cokernels.

data VarianceG (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x where Source #

measuring the deviation of a consecutive zero chain of being exact accordind to the given generalized kernels and cokernels. The exactness is given by deviations.

Properties Let VarianceG c vs be in VarianceG t k c d n x for a Distributive structure x, then for all (ker 0, coker 0), (ker 1, coker 1) .. (ker i,coker i) .. (ker n,coker n) in vs, and d 0, d 1 .. d i, d (i+1) .. d (n+1) in cnzArrows t holds:

If t matches ConsecutiveZero (DiagramChainTo _ _) then holds (see diagram below):
1. ker i is a kernel of d i.
2. coker i is a cokernel of d' (i+1), where d' (i+1) is the universal factor given by ker i and d (i+1).

               d i          d (i+1)               
c :  ... a <------------ b <------------ c ...
                         ^              || 
                         |              || 
                         | ker i        || one
                         |              || 
                         ^              || 
         a'<<----------- b'<------------ c 
              coker i        d' (i+1)

If t matches ConsecutiveZero (DiagramChainFrom _ _) then holds (see diagram below):
1. coker i is a cokernel of d i.
2. ker i is a kernel of d' (i+1), where d' (i+1) is the universal factor given by coker i and d (i+1).

               d i          d (i+1)               
c :  ... a ------------> b ------------> c ...
                         v              || 
                         |              || 
                         | coker i      || one
                         v              || 
                         v              || 
         a'>>----------> b'------------> c 
              ker i          d' (i+1)

Constructors

VarianceG :: forall (t :: Site) (n :: N') x (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type). ConsecutiveZero t n x -> FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x) -> VarianceG t k c d n x

Instances

Instances details

(HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalKernelCokernel (Inv2 h) k c d, t ~ Dual (Dual t)) => ApplicativeG (SDualBi (VarianceG t k c d n)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Limes.Exact.Deviation Methods amapG :: Inv2 h x y -> SDualBi (VarianceG t k c d n) x -> SDualBi (VarianceG t k c d n) y Source #
(HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalKernelCokernel (Inv2 h) k c d, t ~ Dual (Dual t)) => FunctorialG (SDualBi (VarianceG t k c d n)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Limes.Exact.Deviation
(Distributive x, XStandardEligibleConeKernel N1 x, XStandardEligibleConeFactorKernel N1 x, XStandardEligibleConeCokernel N1 x, XStandardEligibleConeFactorCokernel N1 x) => Validable (VarianceG t Cone Cone Diagram n x) Source #
Instance details Defined in OAlg.Limes.Exact.Deviation Methods valid :: VarianceG t Cone Cone Diagram n x -> Statement Source #
type Dual1 (VarianceG t k c d n :: Type -> Type) Source #
Instance details Defined in OAlg.Limes.Exact.Deviation type Dual1 (VarianceG t k c d n :: Type -> Type) = VarianceG (Dual t) c k d n

type Variance (t :: Site) = VarianceG t Cone Cone Diagram Source #

the variance according to Kernels and Cokernels

isExact :: forall x (t :: Site) (n :: N'). (Distributive x, Typeable t, Attestable n) => Kernels N1 x -> Cokernels N1 x -> ConsecutiveZero t n x -> Bool Source #

testing of being exact, i.e. the deviations of its variance are all ZeroPoints.

isExactVariance :: forall x (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N'). (Distributive x, NaturalConicBi (IsoO Dst Op) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConicBi (IsoO Dst Op) c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, Typeable t, Attestable n) => VarianceG t k c d n x -> Bool Source #

testing of being exact, i.e. the deviations are all ZeroPoints.

vrcConsZeroHom :: forall x (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N'). (Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d) => VarianceG t k c d n x -> ConsecutiveZeroHom t n x Source #

the induce homomorphism of consecutive zero-able chains.

Property Let v = VarianceG c vs be in VarianceG t k c d n x, then holds:

If c matches ConsecutiveZero ('DiagramChainTo _ _) then holds:
1. end (vrcConsZeroHom v) == c.
2. ti is given by the diagram below.

                                v              w               
top:      end t         a <------------ b <------------ c <------------ d ...
            ^           ^               ^              ||              ||
            |           |               |              ||              ||
          t |           | t0 = 0        | t1 = ker0 v  || t2 = one c   || t3 = one d ...
            |           |               |              ||              ||
            |           |               ^              ||              || 
bottom:  start t        a'<<----------- b'<------------ c <------------ d ...
                          v' = coker0 w'        w'

If c matches ConsecutiveZero (DiagramChainFrom _ _) then holds:
1. start (vrcConsZeroHom v) == c.
2. t i is given by the diagram below.

                                 v               w
top:      sart t        a ------------> b -------------> c ------------> d ...
            |           |               |               ||              ||
            |           |               |               ||              ||
          t |           | t0 = 0        | t1 = coker0 v || t2 = one c   || t3 = one d ...
            |           |               v               ||              ||
            v           v               v               ||              ||
bottom:   end t         a'>-----------> b'-------------> c ------------> d ...
                          v' = ker0 w'          w'

vrcSite :: forall (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. VarianceG t k c d n x -> Either (t :~: 'From) (t :~: 'To) Source #

proof that the site is either From or To.

vrcHead :: forall x (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). Distributive x => VarianceG t k c d n x -> VarianceG t k c d N0 x Source #

the head.

vrcTail :: forall x (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). Distributive x => VarianceG t k c d (n + 1) x -> VarianceG t k c d n x Source #

the tail.

type NaturalKernelCokernel (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = (NaturalConic h k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConic h k Dst 'Injective d ('Parallel 'RightToLeft) N2 N1, NaturalConic h c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConic h c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) Source #

natural conics for kernels and cokenrels.

type EntityDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) x = (Typeable d, Entity (d ('Parallel 'LeftToRight) N2 N1 x), Entity (d ('Parallel 'RightToLeft) N2 N1 x), Entity (d ('Parallel 'LeftToRight) N2 N1 (Op x)), Entity (d ('Parallel 'RightToLeft) N2 N1 (Op x))) Source #

diagrammatic object admitting Entity.

type ObjectKernelCokernel (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) x = (Diagrammatic d, Object (k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x), Object (k Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 (Op x)), Object (c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x), Object (c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 (Op x))) Source #

kernels and cokernels admitting Object

Duality

vrcMapS :: forall (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (t :: Site) x y (n :: N'). (HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalConicBi (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConicBi (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1, t ~ Dual (Dual t)) => Inv2 h x y -> SDualBi (VarianceG t k c d n) x -> SDualBi (VarianceG t k c d n) y Source #

mapping of VarianceG.

vrcMapCov :: forall (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) x y (t :: Site) (n :: N'). (HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalConic (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConic (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) => Variant2 'Covariant (Inv2 h) x y -> VarianceG t k c d n x -> VarianceG t k c d n y Source #

covariant mapping of VarianceG.

vrcMapCnt :: forall (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) x y (t :: Site) (n :: N'). (HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalConic (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConic (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) => Variant2 'Contravariant (Inv2 h) x y -> VarianceG t k c d n x -> VarianceG (Dual t) c k d n y Source #

contravariant mapping of VarianceG.

Variance Hom

varianceHom :: forall x (t :: Site) (n :: N'). (Distributive x, Typeable t, Attestable n) => Kernels N1 x -> Cokernels N1 x -> ConsecutiveZeroHom t n x -> VarianceHom t n x Source #

constructing a VarianceGHom by a ConsecutiveZeroHom according to the given Kernels and Cokernels.

data VarianceGHom (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x Source #

homomorphism between variances.

Property Let t be in VarianceGHom t k c d n x, the holds:

the induced homomorphism vrcHomConsZeroHom t is valid.

Constructors

VarianceGHom (VarianceG t k c d n x) (VarianceG t k c d n x) (FinList (n + 3) x)

Instances

Instances details

(HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalKernelCokernel (Inv2 h) k c d, t ~ Dual (Dual t)) => ApplicativeG (SDualBi (VarianceGHom t k c d n)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Limes.Exact.Deviation Methods amapG :: Inv2 h x y -> SDualBi (VarianceGHom t k c d n) x -> SDualBi (VarianceGHom t k c d n) y Source #
(HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalKernelCokernel (Inv2 h) k c d, t ~ Dual (Dual t)) => FunctorialG (SDualBi (VarianceGHom t k c d n)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Limes.Exact.Deviation
(Distributive x, XStandardEligibleConeKernel N1 x, XStandardEligibleConeFactorKernel N1 x, XStandardEligibleConeCokernel N1 x, XStandardEligibleConeFactorCokernel N1 x, Typeable t, Typeable n) => Validable (VarianceGHom t Cone Cone Diagram n x) Source #
Instance details Defined in OAlg.Limes.Exact.Deviation Methods valid :: VarianceGHom t Cone Cone Diagram n x -> Statement Source #
type Dual1 (VarianceGHom t k c d n :: Type -> Type) Source #
Instance details Defined in OAlg.Limes.Exact.Deviation type Dual1 (VarianceGHom t k c d n :: Type -> Type) = VarianceGHom (Dual t) c k d n

type VarianceHom (t :: Site) = VarianceGHom t Cone Cone Diagram Source #

homomorphism according to Kernel and Cokernel.

vrcHomSite :: forall (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. VarianceGHom t k c d n x -> Either (t :~: 'From) (t :~: 'To) Source #

proof that the site is either From or To.

vrcHomConsZeroHom :: forall (t :: Site) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. VarianceGHom t k c d n x -> ConsecutiveZeroHom t n x Source #

the induce homomorphism between consecutive zero chains.

Duality

vrcHomMapS :: forall (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (t :: Site) x y (n :: N'). (HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalConicBi (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConicBi (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1, t ~ Dual (Dual t)) => Inv2 h x y -> SDualBi (VarianceGHom t k c d n) x -> SDualBi (VarianceGHom t k c d n) y Source #

mapping of VarianceGHom.

vrcHomMapCov :: forall (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) x y (t :: Site) (n :: N'). (HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalConic (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConic (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) => Variant2 'Covariant (Inv2 h) x y -> VarianceGHom t k c d n x -> VarianceGHom t k c d n y Source #

covariant mapping of VarianceGHom.

vrcHomMapCnt :: forall (h :: Type -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) x y (t :: Site) (n :: N'). (HomDistributiveDisjunctive h, CategoryDisjunctive h, NaturalConic (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1, NaturalConic (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) => Variant2 'Contravariant (Inv2 h) x y -> VarianceGHom t k c d n x -> VarianceGHom (Dual t) c k d n y Source #

contravariant mapping of VarianceGHom.

Proposition

prpVarianceG :: forall x (d :: DiagramType -> N' -> N' -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N'). (Distributive x, EntityDiagrammatic d x, NaturalKernelCokernel (IsoO Dst Op) k c d, ObjectKernelCokernel k c d x) => XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x -> XEligibleConeFactorG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x -> XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x -> XEligibleConeFactorG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x -> VarianceG t k c d n x -> Statement Source #

validity according to VarianceG.

prpVarianceGHom :: forall x (d :: DiagramType -> N' -> N' -> Type -> Type) (k :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N'). (Distributive x, EntityDiagrammatic d x, NaturalKernelCokernel (IsoO Dst Op) k c d, ObjectKernelCokernel k c d x, Typeable t, Typeable n) => XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x -> XEligibleConeFactorG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x -> XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x -> XEligibleConeFactorG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x -> VarianceGHom t k c d n x -> Statement Source #

validity according to VarianceGHom.

prpDeviationOrntSymbol :: Statement Source #

validity of some properties for d ~ Orientation Symbol.