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

OAlg.Entity.Slice.Liftable

Contents

Liftables
Limes
Proposition
Exception

Description

liftable slices.

Synopsis

data Liftable (p :: Perspective) (i :: Type -> Type) x where
- LiftableProjective :: forall (i :: Type -> Type) x. Sliced i x => x -> (Slice 'To i x -> Slice 'To i x) -> Liftable 'Projective i x
- LiftableInjective :: forall (i :: Type -> Type) x. Sliced i x => x -> (Slice 'From i x -> Slice 'From i x) -> Liftable 'Injective i x
lift :: forall (p :: Perspective) (i :: Type -> Type) x. Liftable p i x -> Slice (ToSite p) i x -> Slice (ToSite p) i x
lftbBase :: forall (s :: Perspective) (i :: Type -> Type) x. Liftable s i x -> x
lftMapS :: forall (h :: Type -> Type -> Type) (i :: Type -> Type) (p :: Perspective) x y. (CategoryDisjunctive h, HomSlicedMultiplicative i h, p ~ Dual (Dual p)) => Inv2 h x y -> SDualBi (Liftable p i) x -> SDualBi (Liftable p i) y
lftMapCov :: forall (h :: Type -> Type -> Type) (i :: Type -> Type) x y (p :: Perspective). (CategoryDisjunctive h, HomSlicedMultiplicative i h) => Variant2 'Covariant (Inv2 h) x y -> Liftable p i x -> Liftable p i y
lftMapCnt :: forall (h :: Type -> Type -> Type) (i :: Type -> Type) x y (p :: Perspective). (CategoryDisjunctive h, HomSlicedMultiplicative i h) => Variant2 'Contravariant (Inv2 h) x y -> Liftable p i x -> Liftable (Dual p) i y
data LiftableCone (i :: Type -> Type) s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x where
- LiftableKernelCone :: forall x (i :: Type -> Type). KernelCone N1 x -> (Slice 'To i x -> Slice 'To i x) -> LiftableCone i Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) ('S N0) x
- LiftableCokernelCone :: forall x (i :: Type -> Type). CokernelCone N1 x -> (Slice 'From i x -> Slice 'From i x) -> LiftableCone i Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S N0) x
lftcLiftable :: forall (i :: Type -> Type) x s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N'). Sliced i x => LiftableCone i s p d t n m x -> Liftable p i x
lftcMapS :: forall (h :: Type -> Type -> Type) (i :: Type -> Type) (p :: Perspective) (t :: DiagramType) x y s (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') (m :: N'). (CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h, p ~ Dual (Dual p), t ~ Dual (Dual t)) => Inv2 h x y -> SDualBi (LiftableCone i s p d t n m) x -> SDualBi (LiftableCone i s p d t n m) y
lftcMapCov :: forall (h :: Type -> Type -> Type) (i :: Type -> Type) x y s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N'). (CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h) => Variant2 'Covariant (Inv2 h) x y -> LiftableCone i s p d t n m x -> LiftableCone i s p d t n m y
lftcMapCnt :: forall (h :: Type -> Type -> Type) (i :: Type -> Type) x y s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N'). (CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h) => Variant2 'Contravariant (Inv2 h) x y -> LiftableCone i s p d t n m x -> LiftableCone i s (Dual p) d (Dual t) n m y
type LiftableKernels (i :: Type -> Type) = KernelsG (LiftableCone i) Diagram N1
type LiftableKernel (i :: Type -> Type) = KernelG (LiftableCone i) Diagram N1
lftlKernel :: forall (i :: Type -> Type) x. Sliced i x => LiftableKernel i x -> Slice 'To i x -> Slice 'To i x
type LiftableCokernels (i :: Type -> Type) = CokernelsG (LiftableCone i) Diagram N1
type LiftableCokernel (i :: Type -> Type) = CokernelG (LiftableCone i) Diagram N1
lftlCokernel :: forall (i :: Type -> Type) x. Sliced i x => LiftableCokernel i x -> Slice 'From i x -> Slice 'From i x
relLiftable :: forall x (p :: Perspective) (i :: Type -> Type). Multiplicative x => XOrtOrientation x -> Liftable p i x -> Statement
data LiftableException = NotLiftable

Liftables

data Liftable (p :: Perspective) (i :: Type -> Type) x where Source #

liftable slices.

Property Let l be in Liftable p i x for an i-sliced Multiplicative structure x, then holds:

If l matches LiftableProjective x lft, then holds: For all t in Slice To i x holds:
1. If start x /= start (slice t) then the evaluation of lft t ends up in a NotLiftable-exception.
2. If start x == start (slice t) then holds: Let t' = lft t in
  1. t' is valid.
  2. start (slice t') == end x,
  3. slice t == slice t' * x.
If l matches LiftableInjective x lft, then holds: For all f in Slice From i x holds:
1. If end x /= end (slice f) then the evaluation of lft f ends up in a NotLiftable-exception.
2. If end x == end (slice f), then holds: Let f' = lft f in
  1. f' is valid.
  2. end (slice f') == start x.
  3. slice f == x * slice f'.

Constructors

LiftableProjective :: forall (i :: Type -> Type) x. Sliced i x => x -> (Slice 'To i x -> Slice 'To i x) -> Liftable 'Projective i x
LiftableInjective :: forall (i :: Type -> Type) x. Sliced i x => x -> (Slice 'From i x -> Slice 'From i x) -> Liftable 'Injective i x

Instances

Instances details

(CategoryDisjunctive h, HomSlicedMultiplicative i h, p ~ Dual (Dual p)) => ApplicativeG (SDualBi (Liftable p i)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable Methods amapG :: Inv2 h x y -> SDualBi (Liftable p i) x -> SDualBi (Liftable p i) y Source #
(CategoryDisjunctive h, HomSlicedMultiplicative i h, p ~ Dual (Dual p)) => FunctorialG (SDualBi (Liftable p i)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable
Show x => Show (Liftable s i x) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable Methods showsPrec :: Int -> Liftable s i x -> ShowS # show :: Liftable s i x -> String # showList :: [Liftable s i x] -> ShowS #
(Multiplicative x, XStandardOrtOrientation x) => Validable (Liftable s i x) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable Methods valid :: Liftable s i x -> Statement Source #
type Dual1 (Liftable p i :: Type -> Type) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable type Dual1 (Liftable p i :: Type -> Type) = Liftable (Dual p) i

lift :: forall (p :: Perspective) (i :: Type -> Type) x. Liftable p i x -> Slice (ToSite p) i x -> Slice (ToSite p) i x Source #

the lifting map.

lftbBase :: forall (s :: Perspective) (i :: Type -> Type) x. Liftable s i x -> x Source #

the underlying factor.

lftMapS :: forall (h :: Type -> Type -> Type) (i :: Type -> Type) (p :: Perspective) x y. (CategoryDisjunctive h, HomSlicedMultiplicative i h, p ~ Dual (Dual p)) => Inv2 h x y -> SDualBi (Liftable p i) x -> SDualBi (Liftable p i) y Source #

mapping of Liftable.

lftMapCov :: forall (h :: Type -> Type -> Type) (i :: Type -> Type) x y (p :: Perspective). (CategoryDisjunctive h, HomSlicedMultiplicative i h) => Variant2 'Covariant (Inv2 h) x y -> Liftable p i x -> Liftable p i y Source #

covariant mapping of Liftable.

lftMapCnt :: forall (h :: Type -> Type -> Type) (i :: Type -> Type) x y (p :: Perspective). (CategoryDisjunctive h, HomSlicedMultiplicative i h) => Variant2 'Contravariant (Inv2 h) x y -> Liftable p i x -> Liftable (Dual p) i y Source #

contravariant mapping of Liftable.

Limes

Cone

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

kernel respectively cokernel cones with a liftable factor.

Property Let c be in LiftableCone i s p d t n m x for a Distributive structure x, then holds: lftcLiftable c is valid.

Constructors

LiftableKernelCone :: forall x (i :: Type -> Type). KernelCone N1 x -> (Slice 'To i x -> Slice 'To i x) -> LiftableCone i Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) ('S N0) x
LiftableCokernelCone :: forall x (i :: Type -> Type). CokernelCone N1 x -> (Slice 'From i x -> Slice 'From i x) -> LiftableCone i Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S N0) x

Instances

Instances details

Conic (LiftableCone i) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable Methods cone :: forall s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. LiftableCone i s p d t n m x -> Cone s p d t n m x Source #
(CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h, p ~ Dual (Dual p), t ~ Dual (Dual t), s ~ Dst) => NaturalConic (Inv2 h) (LiftableCone i) s p Diagram t n m Source #
Instance details Defined in OAlg.Entity.Slice.Liftable
(CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h, p ~ Dual (Dual p), t ~ Dual (Dual t)) => ApplicativeG (SDualBi (LiftableCone i s p d t n m)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable Methods amapG :: Inv2 h x y -> SDualBi (LiftableCone i s p d t n m) x -> SDualBi (LiftableCone i s p d t n m) y Source #
(CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h, p ~ Dual (Dual p), t ~ Dual (Dual t)) => ApplicativeG (SDualBi (ConeG (LiftableCone i) s p d t n m)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable Methods amapG :: Inv2 h x y -> SDualBi (ConeG (LiftableCone i) s p d t n m) x -> SDualBi (ConeG (LiftableCone i) s p d t n m) y Source #
(CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h, p ~ Dual (Dual p), t ~ Dual (Dual t)) => FunctorialG (SDualBi (LiftableCone i s p d t n m)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable
(CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h, p ~ Dual (Dual p), t ~ Dual (Dual t)) => FunctorialG (SDualBi (ConeG (LiftableCone i) s p d t n m)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable
(CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h, p ~ Dual (Dual p), t ~ Dual (Dual t), s ~ Dst) => NaturalTransformable (Inv2 h) (->) (SDualBi (ConeG (LiftableCone i) s p Diagram t n m)) (SDualBi (ConeG Cone s p Diagram t n m)) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable
Oriented x => Show (LiftableCone i s p d t n m x) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable Methods showsPrec :: Int -> LiftableCone i s p d t n m x -> ShowS # show :: LiftableCone i s p d t n m x -> String # showList :: [LiftableCone i s p d t n m x] -> ShowS #
(Distributive x, Sliced i x, XStandardOrtOrientation x) => Validable (LiftableCone i s p d t n m x) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable Methods valid :: LiftableCone i s p d t n m x -> Statement Source #
type Dual1 (LiftableCone i s p d t n m :: Type -> Type) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable type Dual1 (LiftableCone i s p d t n m :: Type -> Type) = LiftableCone i s (Dual p) d (Dual t) n m

lftcLiftable :: forall (i :: Type -> Type) x s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N'). Sliced i x => LiftableCone i s p d t n m x -> Liftable p i x Source #

the associated Liftable.

lftcMapS :: forall (h :: Type -> Type -> Type) (i :: Type -> Type) (p :: Perspective) (t :: DiagramType) x y s (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') (m :: N'). (CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h, p ~ Dual (Dual p), t ~ Dual (Dual t)) => Inv2 h x y -> SDualBi (LiftableCone i s p d t n m) x -> SDualBi (LiftableCone i s p d t n m) y Source #

mapping of LiftableCone.

lftcMapCov :: forall (h :: Type -> Type -> Type) (i :: Type -> Type) x y s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N'). (CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h) => Variant2 'Covariant (Inv2 h) x y -> LiftableCone i s p d t n m x -> LiftableCone i s p d t n m y Source #

covariant mapping of LiftableCone.

lftcMapCnt :: forall (h :: Type -> Type -> Type) (i :: Type -> Type) x y s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N'). (CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h) => Variant2 'Contravariant (Inv2 h) x y -> LiftableCone i s p d t n m x -> LiftableCone i s (Dual p) d (Dual t) n m y Source #

contravariant mapping of LiftableCone.

Kernel

type LiftableKernels (i :: Type -> Type) = KernelsG (LiftableCone i) Diagram N1 Source #

liftable kernels according to a slice index i.

type LiftableKernel (i :: Type -> Type) = KernelG (LiftableCone i) Diagram N1 Source #

liftable kenrel according to a slice index i.

lftlKernel :: forall (i :: Type -> Type) x. Sliced i x => LiftableKernel i x -> Slice 'To i x -> Slice 'To i x Source #

the liftable property for LiftableKernel.

Cokernel

type LiftableCokernels (i :: Type -> Type) = CokernelsG (LiftableCone i) Diagram N1 Source #

liftable cokernels according to a slice index i.

type LiftableCokernel (i :: Type -> Type) = CokernelG (LiftableCone i) Diagram N1 Source #

liftable cokernel according to a slice index i.

lftlCokernel :: forall (i :: Type -> Type) x. Sliced i x => LiftableCokernel i x -> Slice 'From i x -> Slice 'From i x Source #

the liftable property for LiftableCokernel.

Proposition

relLiftable :: forall x (p :: Perspective) (i :: Type -> Type). Multiplicative x => XOrtOrientation x -> Liftable p i x -> Statement Source #

validity accroding to Liftable.

Exception

data LiftableException Source #

liftable exceptions which are sub exceptions of SomeOAlgException.

Constructors

NotLiftable

Instances

Instances details

Exception LiftableException Source #
Instance details Defined in OAlg.Entity.Slice.Liftable Methods toException :: LiftableException -> SomeException # fromException :: SomeException -> Maybe LiftableException # displayException :: LiftableException -> String #
Show LiftableException Source #
Instance details Defined in OAlg.Entity.Slice.Liftable Methods showsPrec :: Int -> LiftableException -> ShowS # show :: LiftableException -> String # showList :: [LiftableException] -> ShowS #
Eq LiftableException Source #
Instance details Defined in OAlg.Entity.Slice.Liftable Methods (==) :: LiftableException -> LiftableException -> Bool # (/=) :: LiftableException -> LiftableException -> Bool #