{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DataKinds #-}
module OAlg.Limes.MinimaAndMaxima
(
Minima, Minimum, MinimumCone, MinimumDiagram
, minimaTo, minimaFrom
, Maxima, Maximum, MaximumCone, MaximumDiagram
, maximaTo, maximaTo', maximaFrom, maximaFrom'
, maxLimitsDualityTo, maxLimitsDualityFrom
)
where
import Data.Typeable
import OAlg.Prelude
import OAlg.Entity.Natural
import OAlg.Entity.Diagram
import OAlg.Structure.Multiplicative
import OAlg.Limes.Cone
import OAlg.Limes.Definition
import OAlg.Limes.Limits
type MinimumDiagram t n = Diagram (Chain t) (n+1) n
type MinimumCone t n = Cone Mlt Projective (Chain t) (n+1) n
type Minimum t n = Limes Mlt Projective (Chain t) (n+1) n
type Minima t n = Limits Mlt Projective (Chain t) (n+1) n
minimaTo :: Multiplicative a => Minima To n a
minimaTo :: forall a (n :: N'). Multiplicative a => Minima 'To n a
minimaTo = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits forall a (n :: N').
Multiplicative a =>
MinimumDiagram 'To n a -> Minimum 'To n a
lMin where
lMin :: Multiplicative a => MinimumDiagram To n a -> Minimum To n a
lMin :: forall a (n :: N').
Multiplicative a =>
MinimumDiagram 'To n a -> Minimum 'To n a
lMin MinimumDiagram 'To n a
d = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Mlt 'Projective ('Chain 'To) (n + 1) n a
l forall {n :: N'} {a}.
Cone Mlt 'Projective ('Chain 'To) ('S n) n a -> a
u where
l :: Cone Mlt 'Projective ('Chain 'To) (n + 1) n a
l = forall a (n :: N').
Multiplicative a =>
FactorChain 'To n a
-> Cone Mlt 'Projective ('Chain 'To) (n + 1) n a
cnPrjChainTo (forall (s :: Site) (n :: N') a.
a -> Diagram ('Chain s) (n + 1) n a -> FactorChain s n a
FactorChain (forall c. Multiplicative c => Point c -> c
one (forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'To) n m a -> Point a
chnToStart MinimumDiagram 'To n a
d)) MinimumDiagram 'To n a
d)
u :: Cone Mlt 'Projective ('Chain 'To) ('S n) n a -> a
u Cone Mlt 'Projective ('Chain 'To) ('S n) n a
c = a
f where FactorChain a
f Diagram ('Chain 'To) (n + 1) n a
_ = forall (n :: N') a.
Cone Mlt 'Projective ('Chain 'To) (n + 1) n a
-> FactorChain 'To n a
cnPrjChainToInv Cone Mlt 'Projective ('Chain 'To) ('S n) n a
c
minimaFrom :: Multiplicative a => Minima From n a
minimaFrom :: forall a (n :: N'). Multiplicative a => Minima 'From n a
minimaFrom = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits forall a (n :: N').
Multiplicative a =>
MinimumDiagram 'From n a -> Minimum 'From n a
lMin where
lMin :: Multiplicative a => MinimumDiagram From n a -> Minimum From n a
lMin :: forall a (n :: N').
Multiplicative a =>
MinimumDiagram 'From n a -> Minimum 'From n a
lMin MinimumDiagram 'From n a
d = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Mlt 'Projective ('Chain 'From) (n + 1) n a
l forall {n :: N'} {a}.
Cone Mlt 'Projective ('Chain 'From) ('S n) n a -> a
u where
l :: Cone Mlt 'Projective ('Chain 'From) (n + 1) n a
l = forall a (n :: N').
Multiplicative a =>
FactorChain 'From n a
-> Cone Mlt 'Projective ('Chain 'From) (n + 1) n a
cnPrjChainFrom (forall (s :: Site) (n :: N') a.
a -> Diagram ('Chain s) (n + 1) n a -> FactorChain s n a
FactorChain (forall c. Multiplicative c => Point c -> c
one (forall (n :: N') (m :: N') a.
Diagram ('Chain 'From) n m a -> Point a
chnFromStart MinimumDiagram 'From n a
d)) MinimumDiagram 'From n a
d)
u :: Cone Mlt 'Projective ('Chain 'From) ('S n) n a -> a
u Cone Mlt 'Projective ('Chain 'From) ('S n) n a
c = a
f where FactorChain a
f Diagram ('Chain 'From) (n + 1) n a
_ = forall (n :: N') a.
Cone Mlt 'Projective ('Chain 'From) (n + 1) n a
-> FactorChain 'From n a
cnPrjChainFromInv Cone Mlt 'Projective ('Chain 'From) ('S n) n a
c
type MaximumDiagram t n = Diagram (Chain t) (n+1) n
type MaximumCone t n = Cone Mlt Injective (Chain t) (n+1) n
type Maximum t n = Limes Mlt Injective (Chain t) (n+1) n
type Maxima t n = Limits Mlt Injective (Chain t) (n+1) n
maxLimitsDualityTo :: Multiplicative a => LimitsDuality Mlt (Maxima To n) (Minima From n) a
maxLimitsDualityTo :: forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Maxima 'To n) (Minima 'From n) a
maxLimitsDualityTo = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
(n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Limits s p t n m a)
-> (g (Op a) :~: Dual (Limits s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> LimitsDuality s f g a
LimitsDuality forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl
maxLimitsDualityFrom :: Multiplicative a
=> LimitsDuality Mlt (Maxima From n) (Minima To n) a
maxLimitsDualityFrom :: forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Maxima 'From n) (Minima 'To n) a
maxLimitsDualityFrom = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
(n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Limits s p t n m a)
-> (g (Op a) :~: Dual (Limits s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> LimitsDuality s f g a
LimitsDuality forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl
maximaTo :: Multiplicative a => Maxima To n a
maximaTo :: forall a (n :: N'). Multiplicative a => Maxima 'To n a
maximaTo = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Maxima 'To n) (Minima 'From n) a
maxLimitsDualityTo forall a (n :: N'). Multiplicative a => Minima 'From n a
minimaFrom
maximaFrom :: Multiplicative a => Maxima From n a
maximaFrom :: forall a (n :: N'). Multiplicative a => Maxima 'From n a
maximaFrom = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Maxima 'From n) (Minima 'To n) a
maxLimitsDualityFrom forall a (n :: N'). Multiplicative a => Minima 'To n a
minimaTo
maximaTo' :: Multiplicative a => p n -> f a -> Maxima To n a
maximaTo' :: forall a (p :: N' -> *) (n :: N') (f :: * -> *).
Multiplicative a =>
p n -> f a -> Maxima 'To n a
maximaTo' p n
_ f a
_ = forall a (n :: N'). Multiplicative a => Maxima 'To n a
maximaTo
maximaFrom' :: Multiplicative a => p n -> f a -> Maxima From n a
maximaFrom' :: forall a (p :: N' -> *) (n :: N') (f :: * -> *).
Multiplicative a =>
p n -> f a -> Maxima 'From n a
maximaFrom' p n
_ f a
_ = forall a (n :: N'). Multiplicative a => Maxima 'From n a
maximaFrom