{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE CPP #-}
module Data.Function.Affine (
Affine(..)
, evalAffine
, fromOffsetSlope
, lensEmbedding, correspondingDirections
) where
import Data.Semigroup
import Data.MemoTrie
import Data.VectorSpace
import Data.AffineSpace
import Data.Tagged
import Data.Manifold.Types.Primitive
import Data.Manifold.PseudoAffine
import Data.Manifold.WithBoundary
import Data.Manifold.Atlas
import Data.Embedding
import qualified Prelude
import qualified Control.Applicative as Hask
import Data.Functor (($>))
import Control.Category.Constrained.Prelude hiding ((^))
import Control.Category.Constrained.Reified
import Control.Arrow.Constrained
import Control.Monad.Constrained
import Data.Foldable.Constrained
import Math.LinearMap.Category
import Control.Lens
data Affine s d c where
Affine :: (ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
instance Category (Affine s) where
type Object (Affine s) x = ( Manifold x
, Atlas' x
, Scalar (Needle x) ~ s )
id :: forall a. Object (Affine s) a => Affine s a a
id = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
Affine ChartIndex b :->: (c, LinearMap s (Needle b) (Needle c))
f . :: forall a b c.
(Object (Affine s) a, Object (Affine s) b, Object (Affine s) c) =>
Affine s b c -> Affine s a b -> Affine s a c
. Affine ChartIndex a :->: (b, LinearMap s (Needle a) (Needle b))
g = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \ChartIndex a
ixa -> case forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex a :->: (b, LinearMap s (Needle a) (Needle b))
g ChartIndex a
ixa of
(b
b, LinearMap s (Needle a) (Needle b)
ða'b) -> case forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex b :->: (c, LinearMap s (Needle b) (Needle c))
f forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => m -> ChartIndex m
lookupAtlas b
b of
(c
c, LinearMap s (Needle b) (Needle c)
ðb'c) -> (c
c, LinearMap s (Needle b) (Needle c)
ðb'c forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. LinearMap s (Needle a) (Needle b)
ða'b)
instance ∀ s . (ScalarManifold s, Eq s) => Cartesian (Affine s) where
type UnitObject (Affine s) = ZeroDim s
swap :: forall a b.
(ObjectPair (Affine s) a b, ObjectPair (Affine s) b a) =>
Affine s (a, b) (b, a)
swap = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap
attachUnit :: forall unit a.
(unit ~ UnitObject (Affine s), ObjectPair (Affine s) a unit) =>
Affine s a (a, unit)
attachUnit = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> \a
a -> ((a
a,forall s. ZeroDim s
Origin), forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit)
detachUnit :: forall unit a.
(unit ~ UnitObject (Affine s), ObjectPair (Affine s) a unit) =>
Affine s (a, unit) a
detachUnit = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint
forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> \(a
a,ZeroDim s
Origin::ZeroDim s) -> (a
a, forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit)
regroup :: forall a b c.
(ObjectPair (Affine s) a b, ObjectPair (Affine s) b c,
ObjectPair (Affine s) a (b, c), ObjectPair (Affine s) (a, b) c) =>
Affine s (a, (b, c)) ((a, b), c)
regroup = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k (a, (b, c)) ((a, b), c)
regroup forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k (a, (b, c)) ((a, b), c)
regroup
regroup' :: forall a b c.
(ObjectPair (Affine s) a b, ObjectPair (Affine s) b c,
ObjectPair (Affine s) a (b, c), ObjectPair (Affine s) (a, b) c) =>
Affine s ((a, b), c) (a, (b, c))
regroup' = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k ((a, b), c) (a, (b, c))
regroup' forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k ((a, b), c) (a, (b, c))
regroup'
instance ∀ s . (ScalarManifold s, Eq s) => Morphism (Affine s) where
Affine ChartIndex b :->: (c, LinearMap s (Needle b) (Needle c))
f *** :: forall b b' c c'.
(ObjectPair (Affine s) b b', ObjectPair (Affine s) c c') =>
Affine s b c -> Affine s b' c' -> Affine s (b, b') (c, c')
*** Affine ChartIndex b' :->: (c', LinearMap s (Needle b') (Needle c'))
g = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(ChartIndex b
ixα,ChartIndex b'
ixβ) -> case (forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex b :->: (c, LinearMap s (Needle b) (Needle c))
f ChartIndex b
ixα, forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex b' :->: (c', LinearMap s (Needle b') (Needle c'))
g ChartIndex b'
ixβ) of
((c
fα, LinearMap s (Needle b) (Needle c)
ðα'f), (c'
gβ,LinearMap s (Needle b') (Needle c')
ðβ'g)) -> ((c
fα,c'
gβ), LinearMap s (Needle b) (Needle c)
ðα'fforall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
***LinearMap s (Needle b') (Needle c')
ðβ'g)
instance ∀ s . (ScalarManifold s, Eq s) => PreArrow (Affine s) where
Affine ChartIndex b :->: (c, LinearMap s (Needle b) (Needle c))
f &&& :: forall b c c'.
(Object (Affine s) b, ObjectPair (Affine s) c c') =>
Affine s b c -> Affine s b c' -> Affine s b (c, c')
&&& Affine ChartIndex b :->: (c', LinearMap s (Needle b) (Needle c'))
g = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \ChartIndex b
ix -> case (forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex b :->: (c, LinearMap s (Needle b) (Needle c))
f ChartIndex b
ix, forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex b :->: (c', LinearMap s (Needle b) (Needle c'))
g ChartIndex b
ix) of
((c
fα, LinearMap s (Needle b) (Needle c)
ðα'f), (c'
gβ,LinearMap s (Needle b) (Needle c')
ðβ'g)) -> ((c
fα,c'
gβ), LinearMap s (Needle b) (Needle c)
ðα'fforall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&&LinearMap s (Needle b) (Needle c')
ðβ'g)
terminal :: forall b. Object (Affine s) b => Affine s b (UnitObject (Affine s))
terminal = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \ChartIndex b
_ -> (forall s. ZeroDim s
Origin, forall v. AdditiveGroup v => v
zeroV)
fst :: forall x y. ObjectPair (Affine s) x y => Affine s (x, y) x
fst = forall x y.
(Manifold (x, y), Atlas (x, y), LinearSpace (Needle x),
LinearSpace (Needle y), Scalar (Needle x) ~ s,
Scalar (Needle y) ~ s, HasTrie (ChartIndex x),
HasTrie (ChartIndex y)) =>
Affine s (x, y) x
afst
where afst :: ∀ x y . ( Manifold (x, y), Atlas (x, y)
, LinearSpace (Needle x), LinearSpace (Needle y)
, Scalar (Needle x) ~ s, Scalar (Needle y) ~ s
, HasTrie (ChartIndex x), HasTrie (ChartIndex y) )
=> Affine s (x,y) x
afst :: forall x y.
(Manifold (x, y), Atlas (x, y), LinearSpace (Needle x),
LinearSpace (Needle y), Scalar (Needle x) ~ s,
Scalar (Needle y) ~ s, HasTrie (ChartIndex x),
HasTrie (ChartIndex y)) =>
Affine s (x, y) x
afst = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint @(x,y) forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> \(x
x,y
_::y) -> (x
x, forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst)
snd :: forall x y. ObjectPair (Affine s) x y => Affine s (x, y) y
snd = forall x y.
(Manifold (x, y), Atlas (x, y), LinearSpace (Needle x),
LinearSpace (Needle y), Scalar (Needle x) ~ s,
Scalar (Needle y) ~ s, HasTrie (ChartIndex x),
HasTrie (ChartIndex y)) =>
Affine s (x, y) y
asnd
where asnd :: ∀ x y . ( Manifold (x, y), Atlas (x, y)
, LinearSpace (Needle x), LinearSpace (Needle y)
, Scalar (Needle x) ~ s, Scalar (Needle y) ~ s
, HasTrie (ChartIndex x), HasTrie (ChartIndex y) )
=> Affine s (x,y) y
asnd :: forall x y.
(Manifold (x, y), Atlas (x, y), LinearSpace (Needle x),
LinearSpace (Needle y), Scalar (Needle x) ~ s,
Scalar (Needle y) ~ s, HasTrie (ChartIndex x),
HasTrie (ChartIndex y)) =>
Affine s (x, y) y
asnd = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> \(x
_::x,y
y) -> (y
y, forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd)
instance ∀ s . (ScalarManifold s, Eq s) => WellPointed (Affine s) where
const :: forall b x.
(Object (Affine s) b, ObjectPoint (Affine s) x) =>
x -> Affine s b x
const x
x = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const (x
x, forall v. AdditiveGroup v => v
zeroV)
unit :: CatTagged (Affine s) (UnitObject (Affine s))
unit = forall {k} (s :: k) b. b -> Tagged s b
Tagged forall s. ZeroDim s
Origin
instance EnhancedCat (->) (Affine s) where
arr :: forall b c.
(Object (Affine s) b, Object (Affine s) c, Object (->) b,
Object (->) c) =>
Affine s b c -> b -> c
arr Affine s b c
f = forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall x y s.
(Manifold x, Atlas x, HasTrie (ChartIndex x), Manifold y,
s ~ Scalar (Needle x), s ~ Scalar (Needle y)) =>
Affine s x y -> x -> (y, LinearMap s (Needle x) (Needle y))
evalAffine Affine s b c
f
instance EnhancedCat (Affine s) (LinearMap s) where
arr :: forall b c.
(Object (LinearMap s) b, Object (LinearMap s) c,
Object (Affine s) b, Object (Affine s) c) =>
LinearMap s b c -> Affine s b c
arr = forall x y.
(LinearSpace x, Atlas x, HasTrie (ChartIndex x), LinearSpace y,
Scalar x ~ s, Scalar y ~ s) =>
(LinearManifoldWitness x, LinearManifoldWitness y)
-> LinearMap s x y -> Affine s x y
alarr (forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness, forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness)
where alarr :: ∀ x y . ( LinearSpace x, Atlas x, HasTrie (ChartIndex x)
, LinearSpace y
, Scalar x ~ s, Scalar y ~ s )
=> (LinearManifoldWitness x, LinearManifoldWitness y)
-> LinearMap s x y -> Affine s x y
alarr :: forall x y.
(LinearSpace x, Atlas x, HasTrie (ChartIndex x), LinearSpace y,
Scalar x ~ s, Scalar y ~ s) =>
(LinearManifoldWitness x, LinearManifoldWitness y)
-> LinearMap s x y -> Affine s x y
alarr (LinearManifoldWitness x
LinearManifoldWitness, LinearManifoldWitness y
LinearManifoldWitness) LinearMap s x y
f
= forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint
forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> \x
x₀ -> let y₀ :: y
y₀ = LinearMap s x y
f forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ x
x₀
in (forall v. AdditiveGroup v => v -> v
negateV y
y₀, LinearMap s x y
f)
instance ( Atlas x, HasTrie (ChartIndex x), Manifold y
, LinearManifold (Needle x), Scalar (Needle x) ~ s
, LinearManifold (Needle y), Scalar (Needle y) ~ s
) => Semimanifold (Affine s x y) where
type Needle (Affine s x y) = Affine s x (Needle y)
.+~^ :: Affine s x y -> Needle (Affine s x y) -> Affine s x y
(.+~^) = case ( forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness :: SemimanifoldWitness y ) of
(SemimanifoldWitness y
SemimanifoldWitness) -> \(Affine ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f) (Affine ChartIndex x
:->: (Needle y, LinearMap s (Needle x) (Needle (Needle y)))
g)
-> forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \ChartIndex x
ix -> case (forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f ChartIndex x
ix, forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x
:->: (Needle y, LinearMap s (Needle x) (Needle (Needle y)))
g ChartIndex x
ix) of
((y
fx₀,LinearMap s (Needle x) (Needle y)
f'), (Needle y
gx₀,LinearMap s (Needle x) (Needle y)
g')) -> (y
fx₀forall x. Semimanifold x => x -> Needle x -> x
.+~^Needle y
gx₀, LinearMap s (Needle x) (Needle y)
f'forall v. AdditiveGroup v => v -> v -> v
^+^LinearMap s (Needle x) (Needle y)
g')
semimanifoldWitness :: SemimanifoldWitness (Affine s x y)
semimanifoldWitness = case forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @y of
SmfdWBoundWitness y
OpenManifoldWitness -> case forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @y of
SemimanifoldWitness y
SemimanifoldWitness -> forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @y forall x.
(Semimanifold (Needle x), Needle (Needle x) ~ Needle x) =>
SemimanifoldWitness x
SemimanifoldWitness
instance ( Atlas x, HasTrie (ChartIndex x), Manifold y
, LinearManifold (Needle x), Scalar (Needle x) ~ s
, LinearManifold (Needle y), Scalar (Needle y) ~ s
) => PseudoAffine (Affine s x y) where
Affine s x y
p.-~. :: Affine s x y -> Affine s x y -> Maybe (Needle (Affine s x y))
.-~.Affine s x y
q = forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure (Affine s x y
pforall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~!Affine s x y
q)
.-~! :: HasCallStack =>
Affine s x y -> Affine s x y -> Needle (Affine s x y)
(.-~!) = case ( forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness :: SemimanifoldWitness y ) of
(SemimanifoldWitness y
SemimanifoldWitness) -> \(Affine ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f) (Affine ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
g)
-> forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \ChartIndex x
ix -> case (forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f ChartIndex x
ix, forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
g ChartIndex x
ix) of
((y
fx₀,LinearMap s (Needle x) (Needle y)
f'), (y
gx₀,LinearMap s (Needle x) (Needle y)
g')) -> (y
fx₀forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~!y
gx₀, LinearMap s (Needle x) (Needle y)
f'forall v. AdditiveGroup v => v -> v -> v
^-^LinearMap s (Needle x) (Needle y)
g')
pseudoAffineWitness :: PseudoAffineWitness (Affine s x y)
pseudoAffineWitness = case forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness :: SemimanifoldWitness y of
SemimanifoldWitness y
SemimanifoldWitness -> forall x.
PseudoAffine (Needle x) =>
SemimanifoldWitness x -> PseudoAffineWitness x
PseudoAffineWitness (forall x.
(Semimanifold (Needle x), Needle (Needle x) ~ Needle x) =>
SemimanifoldWitness x
SemimanifoldWitness)
instance ( Atlas x, HasTrie (ChartIndex x)
, LinearManifold (Needle x), Scalar (Needle x) ~ s
, LinearManifold (Needle y), Scalar (Needle y) ~ s
, Manifold y, Scalar (Needle y) ~ s )
=> AffineSpace (Affine s x y) where
type Diff (Affine s x y) = Affine s x (Needle y)
.+^ :: Affine s x y -> Diff (Affine s x y) -> Affine s x y
(.+^) = forall x. Semimanifold x => x -> Needle x -> x
(.+~^); .-. :: Affine s x y -> Affine s x y -> Diff (Affine s x y)
(.-.) = forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
(.-~!)
instance ( Atlas x, HasTrie (ChartIndex x)
, LinearManifold (Needle x), Scalar (Needle x) ~ s
, LinearManifold y, Scalar y ~ s, Num' s )
=> AdditiveGroup (Affine s x y) where
zeroV :: Affine s x y
zeroV = case forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness :: LinearManifoldWitness y of
LinearManifoldWitness y
LinearManifoldWitness -> forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const (forall v. AdditiveGroup v => v
zeroV, forall v. AdditiveGroup v => v
zeroV)
^+^ :: Affine s x y -> Affine s x y -> Affine s x y
(^+^) = case ( forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness :: LinearManifoldWitness y
, forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness :: DualSpaceWitness y ) of
(LinearManifoldWitness y
LinearManifoldWitness, DualSpaceWitness y
DualSpaceWitness) -> forall x. Semimanifold x => x -> Needle x -> x
(.+~^)
negateV :: Affine s x y -> Affine s x y
negateV = case forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness :: LinearManifoldWitness y of
LinearManifoldWitness y
LinearManifoldWitness -> \(Affine ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f) -> forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$
forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> forall v. AdditiveGroup v => v -> v
negateVforall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
***forall v. AdditiveGroup v => v -> v
negateV
instance ( Atlas x, HasTrie (ChartIndex x)
, LinearManifold (Needle x), Scalar (Needle x) ~ s
, LinearManifold y, Scalar y ~ s, Num' s )
=> VectorSpace (Affine s x y) where
type Scalar (Affine s x y) = s
*^ :: Scalar (Affine s x y) -> Affine s x y -> Affine s x y
(*^) = case forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness :: LinearManifoldWitness y of
LinearManifoldWitness y
LinearManifoldWitness -> \Scalar (Affine s x y)
μ (Affine ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f) -> forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$
forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> (Scalar (Affine s x y)
μforall v. VectorSpace v => Scalar v -> v -> v
*^)forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
***(Scalar (Affine s x y)
μforall v. VectorSpace v => Scalar v -> v -> v
*^)
evalAffine :: ∀ x y s . ( Manifold x, Atlas x, HasTrie (ChartIndex x)
, Manifold y
, s ~ Scalar (Needle x), s ~ Scalar (Needle y) )
=> Affine s x y -> x -> (y, LinearMap s (Needle x) (Needle y))
evalAffine :: forall x y s.
(Manifold x, Atlas x, HasTrie (ChartIndex x), Manifold y,
s ~ Scalar (Needle x), s ~ Scalar (Needle y)) =>
Affine s x y -> x -> (y, LinearMap s (Needle x) (Needle y))
evalAffine (Affine ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f) x
x = (y
fx₀forall x. Semimanifold x => x -> Needle x -> x
.+~^(LinearMap s (Needle x) (Needle y)
ðx'f forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ Needle x
v), LinearMap s (Needle x) (Needle y)
ðx'f)
where Just Needle x
v = x
x forall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~. forall m. Atlas m => ChartIndex m -> m
chartReferencePoint ChartIndex x
chIx
chIx :: ChartIndex x
chIx = forall m. Atlas m => m -> ChartIndex m
lookupAtlas x
x
(y
fx₀, LinearMap s (Needle x) (Needle y)
ðx'f) = forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f ChartIndex x
chIx
fromOffsetSlope :: ∀ x y s . ( LinearSpace x, Atlas x, HasTrie (ChartIndex x)
, Manifold y
, s ~ Scalar x, s ~ Scalar (Needle y) )
=> y -> LinearMap s x (Needle y) -> Affine s x y
fromOffsetSlope :: forall x y s.
(LinearSpace x, Atlas x, HasTrie (ChartIndex x), Manifold y,
s ~ Scalar x, s ~ Scalar (Needle y)) =>
y -> LinearMap s x (Needle y) -> Affine s x y
fromOffsetSlope = case ( forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness :: LinearManifoldWitness x ) of
(LinearManifoldWitness x
LinearManifoldWitness)
-> \y
y0 LinearMap s x (Needle y)
ðx'y -> forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint
forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> \x
x₀ -> let δy :: Needle y
δy = LinearMap s x (Needle y)
ðx'y forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ x
x₀
in (y
y0forall x. Semimanifold x => x -> Needle x -> x
.+~^Needle y
δy, LinearMap s x (Needle y)
ðx'y)
instance EnhancedCat (Embedding (Affine s)) (Embedding (LinearMap s)) where
arr :: forall b c.
(Object (Embedding (LinearMap s)) b,
Object (Embedding (LinearMap s)) c,
Object (Embedding (Affine s)) b,
Object (Embedding (Affine s)) c) =>
Embedding (LinearMap s) b c -> Embedding (Affine s) b c
arr (Embedding LinearMap s b c
e LinearMap s c b
p) = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding (forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr LinearMap s b c
e) (forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr LinearMap s c b
p)
lensEmbedding :: ∀ k x c s .
( Num' s
, LinearSpace x, LinearSpace c, Object k x, Object k c
, Scalar x ~ s, Scalar c ~ s
, EnhancedCat k (LinearMap s) )
=> Lens' x c -> Embedding k c x
lensEmbedding :: forall (k :: * -> * -> *) x c s.
(Num' s, LinearSpace x, LinearSpace c, Object k x, Object k c,
Scalar x ~ s, Scalar c ~ s, EnhancedCat k (LinearMap s)) =>
Lens' x c -> Embedding k c x
lensEmbedding Lens' x c
l = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding (forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (\c
c -> forall v. AdditiveGroup v => v
zeroV forall a b. a -> (a -> b) -> b
& Lens' x c
l forall s t a b. ASetter s t a b -> b -> s -> t
.~ c
c)
:: LinearMap s c x) )
(forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (forall s a. s -> Getting a s a -> a
^.Lens' x c
l)
:: LinearMap s x c) )
correspondingDirections :: ∀ x c t s
. ( WithField s AffineManifold c
, WithField s AffineManifold x
, SemiInner (Needle c), SemiInner (Needle x)
, RealFrac' s
, Traversable t )
=> (c, x) -> t (Needle c, Needle x) -> Maybe (Embedding (Affine s) c x)
correspondingDirections :: forall x c (t :: * -> *) s.
(WithField s AffineManifold c, WithField s AffineManifold x,
SemiInner (Needle c), SemiInner (Needle x), RealFrac' s,
Traversable t) =>
(c, x)
-> t (Needle c, Needle x) -> Maybe (Embedding (Affine s) c x)
correspondingDirections (c
c₀, x
x₀) t (Needle c, Needle x)
dirMap
= Maybe
(ReifiedLens' (Diff c) (t (Scalar (Diff c))),
ReifiedLens' (Diff x) (t (Scalar (Diff x))))
freeEmbeddings forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding (forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ChartIndex c -> (x, LinearMap s (Needle c) (Needle x))
c2x)
(forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ChartIndex x -> (c, LinearMap s (Needle x) (Needle c))
x2c)
where freeEmbeddings :: Maybe
(ReifiedLens' (Diff c) (t (Scalar (Diff c))),
ReifiedLens' (Diff x) (t (Scalar (Diff x))))
freeEmbeddings = forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Monoidal f r t, ObjectPair r a b, ObjectPair t (f a) (f b),
Object t (f (a, b))) =>
t (f a, f b) (f (a, b))
fzip ( forall v (t :: * -> *) r.
(HasCallStack, SemiInner v, RealFrac' (Scalar v), Traversable t) =>
t v -> Maybe (ReifiedLens' v (t (Scalar v)))
embedFreeSubspace forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fstforall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$>t (Needle c, Needle x)
dirMap
, forall v (t :: * -> *) r.
(HasCallStack, SemiInner v, RealFrac' (Scalar v), Traversable t) =>
t v -> Maybe (ReifiedLens' v (t (Scalar v)))
embedFreeSubspace forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
sndforall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$>t (Needle c, Needle x)
dirMap )
c2t :: Lens' (Needle c) (t s)
c2t :: Lens' (Needle c) (t s)
c2t = case Maybe
(ReifiedLens' (Diff c) (t (Scalar (Diff c))),
ReifiedLens' (Diff x) (t (Scalar (Diff x))))
freeEmbeddings of Just (Lens Lens (Diff c) (Diff c) (t s) (t s)
ct, ReifiedLens' (Diff x) (t s)
_) -> Lens (Diff c) (Diff c) (t s) (t s)
ct
x2t :: Lens' (Needle x) (t s)
x2t :: Lens' (Needle x) (t s)
x2t = case Maybe
(ReifiedLens' (Diff c) (t (Scalar (Diff c))),
ReifiedLens' (Diff x) (t (Scalar (Diff x))))
freeEmbeddings of Just (ReifiedLens' (Diff c) (t s)
_, Lens Lens (Diff x) (Diff x) (t s) (t s)
xt) -> Lens (Diff x) (Diff x) (t s) (t s)
xt
c2x :: ChartIndex c -> (x, LinearMap s (Needle c) (Needle x))
c2x :: ChartIndex c -> (x, LinearMap s (Needle c) (Needle x))
c2x ChartIndex c
ιc
= ( x
x₀ forall x. Semimanifold x => x -> Needle x -> x
.+~^ (forall v. AdditiveGroup v => v
zeroV forall a b. a -> (a -> b) -> b
& Lens' (Needle x) (t s)
x2t forall s t a b. ASetter s t a b -> b -> s -> t
.~ Needle c
δcforall s a. s -> Getting a s a -> a
^.Lens' (Needle c) (t s)
c2t)
, forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Diff c
dc -> forall v. AdditiveGroup v => v
zeroV forall a b. a -> (a -> b) -> b
& Lens' (Needle x) (t s)
x2t forall s t a b. ASetter s t a b -> b -> s -> t
.~ Diff c
dcforall s a. s -> Getting a s a -> a
^.Lens' (Needle c) (t s)
c2t )
where Just Needle c
δc = forall m. Atlas m => ChartIndex m -> m
chartReferencePoint ChartIndex c
ιc forall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~. c
c₀
x2c :: ChartIndex x
-> (c, LinearMap s (Needle x) (Needle c))
x2c :: ChartIndex x -> (c, LinearMap s (Needle x) (Needle c))
x2c ChartIndex x
ιx
= ( c
c₀ forall x. Semimanifold x => x -> Needle x -> x
.+~^ (forall v. AdditiveGroup v => v
zeroV forall a b. a -> (a -> b) -> b
& Lens' (Needle c) (t s)
c2t forall s t a b. ASetter s t a b -> b -> s -> t
.~ Needle x
δxforall s a. s -> Getting a s a -> a
^.Lens' (Needle x) (t s)
x2t)
, forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Diff x
dx -> forall v. AdditiveGroup v => v
zeroV forall a b. a -> (a -> b) -> b
& Lens' (Needle c) (t s)
c2t forall s t a b. ASetter s t a b -> b -> s -> t
.~ Diff x
dxforall s a. s -> Getting a s a -> a
^.Lens' (Needle x) (t s)
x2t )
where Just Needle x
δx = forall m. Atlas m => ChartIndex m -> m
chartReferencePoint ChartIndex x
ιx forall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~. x
x₀