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

OAlg.Limes.Exact.ConsecutiveZero

Contents

Consecutive Zero
- Duality
Consecutive Zero Hom
- Duality
X

Description

chain diagrams with consecutive zero arrows.

Synopsis

newtype ConsecutiveZero (t :: Site) (n :: N') x = ConsecutiveZero (Diagram ('Chain t) (n + 3) (n + 2) x)
cnzSite :: forall (t :: Site) (n :: N') x. ConsecutiveZero t n x -> Either (t :~: 'From) (t :~: 'To)
cnzDiagram :: forall (t :: Site) (n :: N') x. ConsecutiveZero t n x -> Diagram ('Chain t) (n + 3) (n + 2) x
cnzPoints :: forall x (t :: Site) (n :: N'). Oriented x => ConsecutiveZero t n x -> FinList (n + 3) (Point x)
cnzArrows :: forall (t :: Site) (n :: N') x. ConsecutiveZero t n x -> FinList (n + 2) x
cnzHead :: forall x (t :: Site) (n :: N'). Distributive x => ConsecutiveZero t n x -> ConsecutiveZero t N0 x
cnzTail :: forall d (t :: Site) (n :: N'). Distributive d => ConsecutiveZero t (n + 1) d -> ConsecutiveZero t n d
cnzMapS :: forall h (t :: Site) x y (n :: N'). (HomDistributiveDisjunctive h, t ~ Dual (Dual t)) => h x y -> SDualBi (ConsecutiveZero t n) x -> SDualBi (ConsecutiveZero t n) y
cnzMapCov :: forall (h :: Type -> Type -> Type) x y (t :: Site) (n :: N'). HomDistributiveDisjunctive h => Variant2 'Covariant h x y -> ConsecutiveZero t n x -> ConsecutiveZero t n y
cnzMapCnt :: forall (h :: Type -> Type -> Type) x y (t :: Site) (n :: N'). HomDistributiveDisjunctive h => Variant2 'Contravariant h x y -> ConsecutiveZero t n x -> ConsecutiveZero (Dual t) n y
newtype ConsecutiveZeroHom (t :: Site) (n :: N') x = ConsecutiveZeroHom (DiagramTrafo ('Chain t) (n + 3) (n + 2) x)
cnzHomSite :: forall (t :: Site) (n :: N') x. ConsecutiveZeroHom t n x -> Either (t :~: 'From) (t :~: 'To)
cnzHomArrows :: forall (t :: Site) (n :: N') x. ConsecutiveZeroHom t n x -> FinList (n + 3) x
cnzHomHead :: forall x (t :: Site) (n :: N'). Distributive x => ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t N0 x
cnzHomTail :: forall x (t :: Site) (n :: N'). Distributive x => ConsecutiveZeroHom t (n + 1) x -> ConsecutiveZeroHom t n x
cnzHomMapS :: forall h (t :: Site) x y (n :: N'). (HomDistributiveDisjunctive h, t ~ Dual (Dual t)) => h x y -> SDualBi (ConsecutiveZeroHom t n) x -> SDualBi (ConsecutiveZeroHom t n) y
cnzHomMapCov :: forall (h :: Type -> Type -> Type) x y (t :: Site) (n :: N'). HomDistributiveDisjunctive h => Variant2 'Covariant h x y -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n y
cnzHomMapCnt :: forall (h :: Type -> Type -> Type) x y (t :: Site) (n :: N'). HomDistributiveDisjunctive h => Variant2 'Contravariant h x y -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom (Dual t) n y
xSomeConsecutiveZeroHomOrnt :: N -> X (SomeConsecutiveZeroHom OS)
data SomeConsecutiveZeroHom x where
- SomeConsecutiveZeroHom :: forall (t :: Site) (n :: N') x. (Typeable t, Attestable n) => ConsecutiveZeroHom t n x -> SomeConsecutiveZeroHom x

Consecutive Zero

newtype ConsecutiveZero (t :: Site) (n :: N') x Source #

chain diagrams with consecutive zero arrows.

Properties Let ConsecutiveZero c be in ConsecutiveZero t n x for a Distributive structure x, then holds:

If c matches DiagramChainTo _ ds then holds: d * d' is zero for all ..d:|d'.. in ds.
If c matches DiagramChainFrom _ ds then holds: d' * d is zero for all ..d:|d'.. in ds.

Constructors

ConsecutiveZero (Diagram ('Chain t) (n + 3) (n + 2) x)

Instances

Instances details

(HomDistributiveDisjunctive h, t ~ Dual (Dual t)) => ApplicativeG (SDualBi (ConsecutiveZero t n)) h (->) Source #
Instance details Defined in OAlg.Limes.Exact.ConsecutiveZero Methods amapG :: h x y -> SDualBi (ConsecutiveZero t n) x -> SDualBi (ConsecutiveZero t n) y Source #
(HomDistributiveDisjunctive h, t ~ Dual (Dual t), FunctorialOriented h) => FunctorialG (SDualBi (ConsecutiveZero t n)) h (->) Source #
Instance details Defined in OAlg.Limes.Exact.ConsecutiveZero
(ShowPoint x, Show x) => Show (ConsecutiveZero t n x) Source #
Instance details Defined in OAlg.Limes.Exact.ConsecutiveZero Methods showsPrec :: Int -> ConsecutiveZero t n x -> ShowS # show :: ConsecutiveZero t n x -> String # showList :: [ConsecutiveZero t n x] -> ShowS #
(EqPoint x, Eq x) => Eq (ConsecutiveZero t n x) Source #
Instance details Defined in OAlg.Limes.Exact.ConsecutiveZero Methods (==) :: ConsecutiveZero t n x -> ConsecutiveZero t n x -> Bool # (/=) :: ConsecutiveZero t n x -> ConsecutiveZero t n x -> Bool #
Distributive x => Validable (ConsecutiveZero t n x) Source #
Instance details Defined in OAlg.Limes.Exact.ConsecutiveZero Methods valid :: ConsecutiveZero t n x -> Statement Source #
type Dual1 (ConsecutiveZero t n :: Type -> Type) Source #
Instance details Defined in OAlg.Limes.Exact.ConsecutiveZero type Dual1 (ConsecutiveZero t n :: Type -> Type) = ConsecutiveZero (Dual t) n

cnzSite :: forall (t :: Site) (n :: N') x. ConsecutiveZero t n x -> Either (t :~: 'From) (t :~: 'To) Source #

proof that the site is either From or To.

cnzDiagram :: forall (t :: Site) (n :: N') x. ConsecutiveZero t n x -> Diagram ('Chain t) (n + 3) (n + 2) x Source #

the underlying chain diagram.

cnzPoints :: forall x (t :: Site) (n :: N'). Oriented x => ConsecutiveZero t n x -> FinList (n + 3) (Point x) Source #

the points according to its underlying diagram.

cnzArrows :: forall (t :: Site) (n :: N') x. ConsecutiveZero t n x -> FinList (n + 2) x Source #

the arrows according to its underlying diagram.

cnzHead :: forall x (t :: Site) (n :: N'). Distributive x => ConsecutiveZero t n x -> ConsecutiveZero t N0 x Source #

the two first arrows as a ConsecutiveZero.

cnzTail :: forall d (t :: Site) (n :: N'). Distributive d => ConsecutiveZero t (n + 1) d -> ConsecutiveZero t n d Source #

dropping the first arrow.

Duality

cnzMapS :: forall h (t :: Site) x y (n :: N'). (HomDistributiveDisjunctive h, t ~ Dual (Dual t)) => h x y -> SDualBi (ConsecutiveZero t n) x -> SDualBi (ConsecutiveZero t n) y Source #

mapping of ConsecutiveZero.

cnzMapCov :: forall (h :: Type -> Type -> Type) x y (t :: Site) (n :: N'). HomDistributiveDisjunctive h => Variant2 'Covariant h x y -> ConsecutiveZero t n x -> ConsecutiveZero t n y Source #

covariant mapping of ConsecutiveZero.

cnzMapCnt :: forall (h :: Type -> Type -> Type) x y (t :: Site) (n :: N'). HomDistributiveDisjunctive h => Variant2 'Contravariant h x y -> ConsecutiveZero t n x -> ConsecutiveZero (Dual t) n y Source #

contravariant mapping of ConsecutiveZero.

Consecutive Zero Hom

newtype ConsecutiveZeroHom (t :: Site) (n :: N') x Source #

homomorphism between two consecutive zero chains.

Property Let ConsecutiveZeroHom t be in ConsecutiveZeroHom t n x within a Distributive structure x, then holds

start t and end t are consecutive zero chains.

Constructors

ConsecutiveZeroHom (DiagramTrafo ('Chain t) (n + 3) (n + 2) x)

Instances

Instances details

(HomDistributiveDisjunctive h, t ~ Dual (Dual t)) => ApplicativeG (SDualBi (ConsecutiveZeroHom t n)) h (->) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

Methods

amapG :: h x y -> SDualBi (ConsecutiveZeroHom t n) x -> SDualBi (ConsecutiveZeroHom t n) y Source #

(HomDistributiveDisjunctive h, FunctorialOriented h, t ~ Dual (Dual t)) => FunctorialG (SDualBi (ConsecutiveZeroHom t n)) h (->) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

(ShowPoint x, Show x) => Show (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

Methods

showsPrec :: Int -> ConsecutiveZeroHom t n x -> ShowS #

show :: ConsecutiveZeroHom t n x -> String #

showList :: [ConsecutiveZeroHom t n x] -> ShowS #

(EqPoint x, Eq x) => Eq (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

Methods

(==) :: ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x -> Bool #

(/=) :: ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x -> Bool #

(Distributive x, Typeable t, Typeable n) => Validable (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

Methods

valid :: ConsecutiveZeroHom t n x -> Statement Source #

(Distributive x, Abelian x, Typeable t, Typeable n) => Abelian (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

Methods

negate :: ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x Source #

(-) :: ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x Source #

ztimes :: Z -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x Source #

(Distributive x, Typeable t, Typeable n) => Additive (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

Methods

zero :: Root (ConsecutiveZeroHom t n x) -> ConsecutiveZeroHom t n x Source #

(+) :: ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x Source #

ntimes :: N -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x Source #

(Algebraic x, Typeable t, Typeable n) => Algebraic (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

(Distributive x, Typeable t, Typeable n) => Distributive (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

(Distributive x, Typeable t, Typeable n) => Fibred (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

Methods

root :: ConsecutiveZeroHom t n x -> Root (ConsecutiveZeroHom t n x) Source #

(Eq x, EqPoint x) => EqRoot (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

(Show x, ShowPoint x) => ShowRoot (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

(Typeable x, Typeable t, Typeable n) => TypeableRoot (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

Distributive x => ValidableRoot (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

(Distributive x, Typeable t, Typeable n) => FibredOriented (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

(Distributive x, Typeable t, Typeable n) => Multiplicative (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

Methods

one :: Point (ConsecutiveZeroHom t n x) -> ConsecutiveZeroHom t n x Source #

(*) :: ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x Source #

npower :: ConsecutiveZeroHom t n x -> N -> ConsecutiveZeroHom t n x Source #

(Distributive x, Typeable t, Typeable n) => Oriented (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

Methods

orientation :: ConsecutiveZeroHom t n x -> Orientation (Point (ConsecutiveZeroHom t n x)) Source #

start :: ConsecutiveZeroHom t n x -> Point (ConsecutiveZeroHom t n x) Source #

end :: ConsecutiveZeroHom t n x -> Point (ConsecutiveZeroHom t n x) Source #

(Eq x, EqPoint x) => EqPoint (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

(Show x, ShowPoint x) => ShowPoint (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

(Typeable x, Typeable t, Typeable n) => TypeablePoint (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

Distributive x => ValidablePoint (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

(Algebraic x, Typeable t, Typeable n) => Vectorial (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

Associated Types

type Scalar (ConsecutiveZeroHom t n x)
Instance details Defined in OAlg.Limes.Exact.ConsecutiveZero type Scalar (ConsecutiveZeroHom t n x) = Scalar x

Methods

(!) :: Scalar (ConsecutiveZeroHom t n x) -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x Source #

type Dual1 (ConsecutiveZeroHom t n :: Type -> Type) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

type Dual1 (ConsecutiveZeroHom t n :: Type -> Type) = ConsecutiveZeroHom (Dual t) n

type Root (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

type Root (ConsecutiveZeroHom t n x) = Orientation (ConsecutiveZero t n x)

type Point (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

type Point (ConsecutiveZeroHom t n x) = ConsecutiveZero t n x

type Scalar (ConsecutiveZeroHom t n x) Source #

Instance details

Defined in OAlg.Limes.Exact.ConsecutiveZero

type Scalar (ConsecutiveZeroHom t n x) = Scalar x

cnzHomSite :: forall (t :: Site) (n :: N') x. ConsecutiveZeroHom t n x -> Either (t :~: 'From) (t :~: 'To) Source #

proof that the site is either From or To.

cnzHomArrows :: forall (t :: Site) (n :: N') x. ConsecutiveZeroHom t n x -> FinList (n + 3) x Source #

the underlying arrows.

cnzHomHead :: forall x (t :: Site) (n :: N'). Distributive x => ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t N0 x Source #

the first two arrows of the given ConsecutiveZeroHom.

cnzHomTail :: forall x (t :: Site) (n :: N'). Distributive x => ConsecutiveZeroHom t (n + 1) x -> ConsecutiveZeroHom t n x Source #

dropping the first arrow.

Duality

cnzHomMapS :: forall h (t :: Site) x y (n :: N'). (HomDistributiveDisjunctive h, t ~ Dual (Dual t)) => h x y -> SDualBi (ConsecutiveZeroHom t n) x -> SDualBi (ConsecutiveZeroHom t n) y Source #

mapping of ConsecutiveZeroHom.

cnzHomMapCov :: forall (h :: Type -> Type -> Type) x y (t :: Site) (n :: N'). HomDistributiveDisjunctive h => Variant2 'Covariant h x y -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n y Source #

covariant mapping of ConsecutiveZeroHom.

cnzHomMapCnt :: forall (h :: Type -> Type -> Type) x y (t :: Site) (n :: N'). HomDistributiveDisjunctive h => Variant2 'Contravariant h x y -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom (Dual t) n y Source #

contravariant mapping of ConsecutiveZeroHom.

X

xSomeConsecutiveZeroHomOrnt :: N -> X (SomeConsecutiveZeroHom OS) Source #

random variable for ConsecutiveZeroHom t n OS with a maximal n of the given one.

data SomeConsecutiveZeroHom x where Source #

some ConsecutiveZeroHom.

Constructors

SomeConsecutiveZeroHom :: forall (t :: Site) (n :: N') x. (Typeable t, Attestable n) => ConsecutiveZeroHom t n x -> SomeConsecutiveZeroHom x

Instances

Instances details

Distributive x => Validable (SomeConsecutiveZeroHom x) Source #
Instance details Defined in OAlg.Limes.Exact.ConsecutiveZero Methods valid :: SomeConsecutiveZeroHom x -> Statement Source #