| Copyright | (c) Erich Gut |
|---|---|
| License | BSD3 |
| Maintainer | zerich.gut@gmail.com |
| Safe Haskell | None |
| Language | Haskell2010 |
OAlg.Limes.Cone.FactorChain
Contents
Description
predicate for a factor with end point at the starting point of a given chain.
Synopsis
- data FactorChain (d :: DiagramType -> N' -> N' -> Type -> Type) (s :: Site) (n :: N') x = FactorChain x (d ('Chain s) (n + 1) n x)
- cnPrjChainTo :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) x (n :: N'). (Diagrammatic d, Multiplicative x) => FactorChain d 'To n x -> Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x
- cnPrjChainToInv :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x -> FactorChain d 'To n x
- cnPrjChainFrom :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) x (n :: N'). (Diagrammatic d, Multiplicative x) => FactorChain d 'From n x -> Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x
- cnPrjChainFromInv :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x -> FactorChain d 'From n x
Chain
data FactorChain (d :: DiagramType -> N' -> N' -> Type -> Type) (s :: Site) (n :: N') x Source #
predicate for a factor with end point at the starting point of the given chain.
Property
- Let
FactorChainf dFactorChainTon aMultiplicativestructureathen holds:endf==chnToStart(diagramd) - Let
FactorChainf dFactorChainFromn aMultiplicativestructureathen holds:endf==chnFromStart(diagramd)
Constructors
| FactorChain x (d ('Chain s) (n + 1) n x) |
Instances
| (Show x, ShowPoint x) => Show (FactorChain Diagram s n x) Source # | |
Defined in OAlg.Limes.Cone.FactorChain | |
| (Eq x, EqPoint x) => Eq (FactorChain Diagram s n x) Source # | |
Defined in OAlg.Limes.Cone.FactorChain Methods (==) :: FactorChain Diagram s n x -> FactorChain Diagram s n x -> Bool # (/=) :: FactorChain Diagram s n x -> FactorChain Diagram s n x -> Bool # | |
| (Diagrammatic d, Oriented x) => Validable (FactorChain d 'From n x) Source # | |
Defined in OAlg.Limes.Cone.FactorChain | |
| (Diagrammatic d, Oriented x) => Validable (FactorChain d 'To n x) Source # | |
Defined in OAlg.Limes.Cone.FactorChain | |
cnPrjChainTo :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) x (n :: N'). (Diagrammatic d, Multiplicative x) => FactorChain d 'To n x -> Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x Source #
the induced Projective cone with ending factor given by the given FactorChain.
Property Let h = be in
FactorChain f dFactorChain To n aMultiplicative structure a and
ConeProjective d' _ (_:|..:|c:|Nil) = cnPrjChainTo hd' and == dc .== f
cnPrjChainToInv :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x -> FactorChain d 'To n x Source #
the underlying factor chain of a projective chain to cone, i.e the inverse of
cnPrjChainToInv.
cnPrjChainFrom :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) x (n :: N'). (Diagrammatic d, Multiplicative x) => FactorChain d 'From n x -> Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x Source #
the induced Projective cone with starting factor given by the given FactorChain.
Property Let h = be in
FactorChain f dFactorChain From n aMultiplicative structure a and
ConeProjective d' _ (c:|_) = cnPrjChainFrom hd' and == dc .== f
cnPrjChainFromInv :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') x. Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x -> FactorChain d 'From n x Source #
the underlying factor chain of a projective chain from cone, i.e. the inverse of
cnPrjChainFrom.