oalg-base-3.0.0.0: Algebraic structures on oriented entities and limits as a tool kit to solve algebraic problems.
Copyright(c) Erich Gut
LicenseBSD3
Maintainerzerich.gut@gmail.com
Safe HaskellNone
LanguageHaskell2010

OAlg.Entity.Slice.Definition

Description

definition of slicing a Multiplicative structures according a given indexed Point.

Synopsis

Slice

data Slice (s :: Site) (i :: Type -> Type) x where Source #

slice over x by a given Site and indexed by i.

Constructors

SliceFrom :: forall (i :: Type -> Type) x. i x -> x -> Slice 'From i x 
SliceTo :: forall (i :: Type -> Type) x. i x -> x -> Slice 'To i x 

Instances

Instances details
Multiplicative x => Opl x (Slice 'From i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

(*>) :: x -> Slice 'From i x -> Slice 'From i x Source #

(Multiplicative x, Sliced i x) => OrientedOpl x (Slice 'From i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

(HomSlicedOriented i h, s ~ Dual (Dual s)) => ApplicativeG (SDualBi (Slice s i)) h (->) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

amapG :: h x y -> SDualBi (Slice s i) x -> SDualBi (Slice s i) y Source #

(HomSlicedOriented i h, FunctorialOriented h, s ~ Dual (Dual s)) => FunctorialG (SDualBi (Slice s i)) h (->) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

(Show1 i, Show x) => Show (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

showsPrec :: Int -> Slice s i x -> ShowS #

show :: Slice s i x -> String #

showList :: [Slice s i x] -> ShowS #

(Eq1 i, Eq x) => Eq (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

(==) :: Slice s i x -> Slice s i x -> Bool #

(/=) :: Slice s i x -> Slice s i x -> Bool #

(Sliced i x, Ord x) => Ord (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

compare :: Slice s i x -> Slice s i x -> Ordering #

(<) :: Slice s i x -> Slice s i x -> Bool #

(<=) :: Slice s i x -> Slice s i x -> Bool #

(>) :: Slice s i x -> Slice s i x -> Bool #

(>=) :: Slice s i x -> Slice s i x -> Bool #

max :: Slice s i x -> Slice s i x -> Slice s i x #

min :: Slice s i x -> Slice s i x -> Slice s i x #

Sliced i x => Validable (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

valid :: Slice s i x -> Statement Source #

(Multiplicative x, Sliced i x, XStandardOrtSite 'From x) => XStandard (Slice 'From i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

xStandard :: X (Slice 'From i x) Source #

(Multiplicative x, Sliced i x, XStandardOrtSite 'To x) => XStandard (Slice 'To i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

xStandard :: X (Slice 'To i x) Source #

(Distributive x, Abelian x, Sliced i x) => Abelian (Slice 'From i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

negate :: Slice 'From i x -> Slice 'From i x Source #

(-) :: Slice 'From i x -> Slice 'From i x -> Slice 'From i x Source #

ztimes :: Z -> Slice 'From i x -> Slice 'From i x Source #

(Distributive x, Sliced i x) => Additive (Slice 'From i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

zero :: Root (Slice 'From i x) -> Slice 'From i x Source #

(+) :: Slice 'From i x -> Slice 'From i x -> Slice 'From i x Source #

ntimes :: N -> Slice 'From i x -> Slice 'From i x Source #

(Distributive x, Sliced i x, Typeable s) => Fibred (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

root :: Slice s i x -> Root (Slice s i x) Source #

EqPoint x => EqRoot (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

ShowPoint x => ShowRoot (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

TypeablePoint x => TypeableRoot (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

ValidablePoint x => ValidableRoot (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

(Oriented x, Sliced i x, Typeable s) => Oriented (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

orientation :: Slice s i x -> Orientation (Point (Slice s i x)) Source #

start :: Slice s i x -> Point (Slice s i x) Source #

end :: Slice s i x -> Point (Slice s i x) Source #

EqPoint x => EqPoint (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

ShowPoint x => ShowPoint (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

TypeablePoint x => TypeablePoint (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

ValidablePoint x => ValidablePoint (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

(Distributive x, Vectorial x, Sliced i x) => Vectorial (Slice 'From i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Associated Types

type Scalar (Slice 'From i x) 
Instance details

Defined in OAlg.Entity.Slice.Definition

type Scalar (Slice 'From i x) = Scalar x

Methods

(!) :: Scalar (Slice 'From i x) -> Slice 'From i x -> Slice 'From i x Source #

type Dual1 (Slice s i :: Type -> Type) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

type Dual1 (Slice s i :: Type -> Type) = Slice (Dual s) i
type Root (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

type Root (Slice s i x) = Point x
type Point (Slice s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

type Point (Slice s i x) = Point x
type Scalar (Slice 'From i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

type Scalar (Slice 'From i x) = Scalar x

slice :: forall (s :: Site) (i :: Type -> Type) x. Slice s i x -> x Source #

the underlying slice.

slSiteType :: forall (s :: Site) (i :: Type -> Type) x. Slice s i x -> Either (s :~: 'From) (s :~: 'To) Source #

the Site type of a slice.

slMap :: forall (i :: Type -> Type) h (s :: Site) x y. (HomSlicedOriented i h, s ~ Dual (Dual s)) => h x y -> SDualBi (Slice s i) x -> SDualBi (Slice s i) y Source #

mapping of slices.

slMapCov :: forall (i :: Type -> Type) (h :: Type -> Type -> Type) x y (s :: Site). HomSlicedOriented i h => Variant2 'Covariant h x y -> Slice s i x -> Slice s i y Source #

mapping of slices under a covariant homomorphism.

Note As IsoO Ort Op is generated by toDualOpOrt and its inverse, the slicePoint is invariant under these mappings and as such slMapCov maps valid slices to valid slices.

slMapCnt :: forall (i :: Type -> Type) (h :: Type -> Type -> Type) x y (s :: Site). HomSlicedOriented i h => Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y Source #

mapping of slices under a contravariant homomorphism.

Factor

data SliceFactor (s :: Site) (i :: Type -> Type) x Source #

factor between two slices.

Property Let SliceFactor a b f be in SliceFactor s i x for a Multiplicative structure x constrained by Sliced i x then holds:

  1. If a matches SliceFrom _ a' then holds: Let SliceFrom _ b' = b in

    1. orientation f == end a' :> end b'.
    2. b' == f * a'.

  2. If a matches SliceTo _ a' then holds: Let SliceTo _ b' = b in

    1. orientation f == start a' :> start b'.
    2. a' == b' * f .

Constructors

SliceFactor (Slice s i x) (Slice s i x) x 

Instances

Instances details
(Multiplicative x, Sliced i x, XStandardOrtSite 'From x) => XStandardOrtSite 'From (SliceFactor 'From i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

xStandardOrtSite :: XOrtSite 'From (SliceFactor 'From i x) Source #

XStandardOrtSite 'From (SliceFactor 'To (Proxy :: Type -> Type) OS) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

xStandardOrtSite :: XOrtSite 'From (SliceFactor 'To (Proxy :: Type -> Type) OS) Source #

(Multiplicative x, Sliced i x, XStandardOrtSite 'To x) => XStandardOrtSite 'To (SliceFactor 'To i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

xStandardOrtSite :: XOrtSite 'To (SliceFactor 'To i x) Source #

(HomSlicedMultiplicative i h, s ~ Dual (Dual s)) => ApplicativeG (SDualBi (SliceFactor s i)) h (->) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

amapG :: h x y -> SDualBi (SliceFactor s i) x -> SDualBi (SliceFactor s i) y Source #

(HomSlicedMultiplicative i h, FunctorialOriented h, s ~ Dual (Dual s)) => FunctorialG (SDualBi (SliceFactor s i)) h (->) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

(Show1 i, Show x) => Show (SliceFactor s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

showsPrec :: Int -> SliceFactor s i x -> ShowS #

show :: SliceFactor s i x -> String #

showList :: [SliceFactor s i x] -> ShowS #

(Eq1 i, Eq x) => Eq (SliceFactor s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

(==) :: SliceFactor s i x -> SliceFactor s i x -> Bool #

(/=) :: SliceFactor s i x -> SliceFactor s i x -> Bool #

(Multiplicative x, Sliced i x) => Validable (SliceFactor s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

valid :: SliceFactor s i x -> Statement Source #

(Multiplicative x, Sliced i x, XStandardOrtSite 'From x) => XStandard (SliceFactor 'From i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

xStandard :: X (SliceFactor 'From i x) Source #

(Multiplicative x, Sliced i x, XStandardOrtSite 'To x) => XStandard (SliceFactor 'To i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

xStandard :: X (SliceFactor 'To i x) Source #

(Multiplicative x, Sliced i x, Typeable s) => Multiplicative (SliceFactor s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

one :: Point (SliceFactor s i x) -> SliceFactor s i x Source #

(*) :: SliceFactor s i x -> SliceFactor s i x -> SliceFactor s i x Source #

npower :: SliceFactor s i x -> N -> SliceFactor s i x Source #

(Multiplicative x, Sliced i x, Typeable s) => Oriented (SliceFactor s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

orientation :: SliceFactor s i x -> Orientation (Point (SliceFactor s i x)) Source #

start :: SliceFactor s i x -> Point (SliceFactor s i x) Source #

end :: SliceFactor s i x -> Point (SliceFactor s i x) Source #

(Eq1 i, Eq x) => EqPoint (SliceFactor s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

(Show1 i, Show x) => ShowPoint (SliceFactor s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

(Typeable i, Typeable x, Typeable s) => TypeablePoint (SliceFactor s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Sliced i x => ValidablePoint (SliceFactor s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

(Multiplicative x, Sliced i x, XStandardOrtSite 'From x) => XStandardPoint (SliceFactor 'From i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

(Multiplicative x, Sliced i x, XStandardOrtSite 'To x) => XStandardPoint (SliceFactor 'To i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

(Multiplicative x, Sliced i x, XStandardOrtSite 'From x) => XStandardOrtSiteFrom (SliceFactor 'From i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

XStandardOrtSiteFrom (SliceFactor 'To (Proxy :: Type -> Type) OS) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

(Multiplicative x, Sliced i x, XStandardOrtSite 'To x) => XStandardOrtSiteTo (SliceFactor 'To i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

type Dual1 (SliceFactor s i :: Type -> Type) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

type Dual1 (SliceFactor s i :: Type -> Type) = SliceFactor (Dual s) i
type Point (SliceFactor s i x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

type Point (SliceFactor s i x) = Slice s i x

slfFactor :: forall (s :: Site) (i :: Type -> Type) x. SliceFactor s i x -> x Source #

the underlying factor.

slfIndex :: Sliced i x => f (SliceFactor 'To i x) -> i x Source #

the associated index.

slfMap :: forall (i :: Type -> Type) h (s :: Site) x y. (HomSlicedMultiplicative i h, s ~ Dual (Dual s)) => h x y -> SDualBi (SliceFactor s i) x -> SDualBi (SliceFactor s i) y Source #

mapping of slices factor.

slfMapCov :: forall (i :: Type -> Type) (h :: Type -> Type -> Type) x y (s :: Site). HomSlicedMultiplicative i h => Variant2 'Covariant h x y -> SliceFactor s i x -> SliceFactor s i y Source #

mapping of slices factor under a covariant homomorphism.

slfMapCnt :: forall (i :: Type -> Type) (h :: Type -> Type -> Type) x y (s :: Site). HomSlicedMultiplicative i h => Variant2 'Contravariant h x y -> SliceFactor s i x -> SliceFactor (Dual s) i y Source #

mapping of slices factor under a contravariant homomorphism.

Duality

toDualOpOrtSld :: forall (i :: Type -> Type) x. Sliced i x => Variant2 'Contravariant (IsoO (Ort, Sld i) Op) x (Op x) Source #

contravariant isomorphism on Sliced Oriented structures.

toDualOpOrtSld' :: forall (i :: Type -> Type) x q. Sliced i x => q i -> Variant2 'Contravariant (IsoO (Ort, Sld i) Op) x (Op x) Source #

contravariant isomorphism on Sliced Oriented structures according to the proxy type.

toDualOpMltSld :: forall (i :: Type -> Type) x. (Sliced i x, Multiplicative x) => Variant2 'Contravariant (IsoO (Mlt, Sld i) Op) x (Op x) Source #

contravariant isomorphism on Sliced Multiplicative structures.

toDualOpMltSld' :: forall (i :: Type -> Type) x q. (Sliced i x, Multiplicative x) => q i -> Variant2 'Contravariant (IsoO (Mlt, Sld i) Op) x (Op x) Source #

contravariant isomorphism on Sliced Multiplicative structures according to the proxy type.

Hom

data SliceFactorDrop (s :: Site) x y where Source #

dropping a slice factor.

Constructors

SliceFactorFromDrop :: forall y (i :: Type -> Type). (Multiplicative y, Sliced i y) => SliceFactorDrop 'From (SliceFactor 'From i y) y 
SliceFactorToDrop :: forall y (i :: Type -> Type). (Multiplicative y, Sliced i y) => SliceFactorDrop 'To (SliceFactor 'To i y) y 

Instances

Instances details
ApplicativeG Id (SliceFactorDrop s) (->) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

amapG :: SliceFactorDrop s x y -> Id x -> Id y Source #

ApplicativeG Pnt (SliceFactorDrop s) (->) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

amapG :: SliceFactorDrop s x y -> Pnt x -> Pnt y Source #

Morphism (SliceFactorDrop s) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Associated Types

type ObjectClass (SliceFactorDrop s) 
Instance details

Defined in OAlg.Entity.Slice.Definition

type ObjectClass (SliceFactorDrop s) = Mlt

Methods

homomorphous :: SliceFactorDrop s x y -> Homomorphous (ObjectClass (SliceFactorDrop s)) x y Source #

domain :: SliceFactorDrop s x y -> Struct (ObjectClass (SliceFactorDrop s)) x Source #

range :: SliceFactorDrop s x y -> Struct (ObjectClass (SliceFactorDrop s)) y Source #

Eq2 (SliceFactorDrop s) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

eq2 :: SliceFactorDrop s x y -> SliceFactorDrop s x y -> Bool Source #

Show2 (SliceFactorDrop s) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

show2 :: SliceFactorDrop s a b -> String Source #

Validable2 (SliceFactorDrop s) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

valid2 :: SliceFactorDrop s x y -> Statement Source #

HomMultiplicative (SliceFactorDrop s) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

HomOriented (SliceFactorDrop s) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Show (SliceFactorDrop s x y) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

showsPrec :: Int -> SliceFactorDrop s x y -> ShowS #

show :: SliceFactorDrop s x y -> String #

showList :: [SliceFactorDrop s x y] -> ShowS #

Eq (SliceFactorDrop s x y) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

(==) :: SliceFactorDrop s x y -> SliceFactorDrop s x y -> Bool #

(/=) :: SliceFactorDrop s x y -> SliceFactorDrop s x y -> Bool #

Validable (SliceFactorDrop s x y) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

valid :: SliceFactorDrop s x y -> Statement Source #

type ObjectClass (SliceFactorDrop s) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

type ObjectClass (SliceFactorDrop s) = Mlt

Limes

data DiagramSlicedCenter (i :: Type -> Type) (t :: Site) (n :: N') (m :: N') x where Source #

predicate for a Star t diagram with center Point given by the index type i x.

Property Let DiagramSlicedCenter i d be in DiagramSlicedCenter i t n m x then holds: slicePoint i == dgCenter d.

Constructors

DiagramSlicedCenter :: forall (i :: Type -> Type) x (t :: Site) (n :: N') (m :: N'). Sliced i x => i x -> Diagram ('Star t) n m x -> DiagramSlicedCenter i t n m x 

Instances

Instances details
Oriented x => Show (DiagramSlicedCenter i t n m x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

showsPrec :: Int -> DiagramSlicedCenter i t n m x -> ShowS #

show :: DiagramSlicedCenter i t n m x -> String #

showList :: [DiagramSlicedCenter i t n m x] -> ShowS #

Oriented x => Validable (DiagramSlicedCenter i t n m x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

valid :: DiagramSlicedCenter i t n m x -> Statement Source #

data LimesSlicedTip (i :: Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') x where Source #

predicate for a limes with a sliced tip of the universal cone.

Property Let LimesSlicedTip i l be in LimesSlicedTip i s p t n m x then holds: tip (universalCone l) == slicePoint i.

Constructors

LimesSlicedTip :: forall (i :: Type -> Type) x s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N'). Sliced i x => i x -> Limes s p t n m x -> LimesSlicedTip i s p t n m x 

Instances

Instances details
Oriented x => Show (LimesSlicedTip i s p t n m x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

showsPrec :: Int -> LimesSlicedTip i s p t n m x -> ShowS #

show :: LimesSlicedTip i s p t n m x -> String #

showList :: [LimesSlicedTip i s p t n m x] -> ShowS #

(Oriented x, XStandardEligibleCone s p t n m x, XStandardEligibleConeFactor s p t n m x, Typeable t, Typeable n, Typeable m) => Validable (LimesSlicedTip i s p t n m x) Source # 
Instance details

Defined in OAlg.Entity.Slice.Definition

Methods

valid :: LimesSlicedTip i s p t n m x -> Statement Source #

lstLimes :: forall (i :: Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') x. LimesSlicedTip i s p t n m x -> Limes s p t n m x Source #

the underlying limes.

Projective

slfTerminalPoint :: forall x (i :: Type -> Type). (Multiplicative x, Sliced i x) => TerminalPoint (SliceFactor 'To i x) Source #

terminal point for factors sliced to a Point.

slfPullback :: forall x (n :: N') (i :: Type -> Type). Multiplicative x => Products n (SliceFactor 'To i x) -> DiagramSlicedCenter i 'To (n + 1) n x -> Pullback n x Source #

the induced pullback.

Injective

slfLimitsInjective :: forall x (i :: Type -> Type) (t :: DiagramType) (n :: N') (m :: N'). (Multiplicative x, Sliced i x) => Limits Mlt 'Injective t n m x -> Limits Mlt 'Injective t n m (SliceFactor 'To i x) Source #

the induced Injective Limits.

X

xSliceTo :: Sliced i x => XOrtSite 'To x -> i x -> X (Slice 'To i x) Source #

the induced random variable.

xSliceFrom :: Sliced i x => XOrtSite 'From x -> i x -> X (Slice 'From i x) Source #

the induced random variable.

xosXOrtSiteToSliceFactorTo :: (Multiplicative x, Sliced i x) => XOrtSite 'To x -> i x -> XOrtSite 'To (SliceFactor 'To i x) Source #

the induced random variable.

xosXOrtSiteFromSliceFactorFrom :: (Multiplicative x, Sliced i x) => XOrtSite 'From x -> i x -> XOrtSite 'From (SliceFactor 'From i x) Source #

the induced random variable.

xosAdjTerminal :: forall x (i :: Type -> Type). (Multiplicative x, Sliced i x) => Q -> XOrtSite 'To (SliceFactor 'To i x) -> XOrtSite 'To (SliceFactor 'To i x) Source #

adjoins a terminal point with the given probability to the random variable of the points of the given XOrtSite To of the SliceFactor To i x. Such a terminal point is given by one s where s is the slice point.