-- |
-- Module      : Data.Manifold.FibreBundle
-- Copyright   : (c) Justus Sagemüller 2018
-- License     : GPL v3
-- 
-- Maintainer  : (@) jsag $ hvl.no
-- Stability   : experimental
-- Portability : portable
-- 

{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE UnicodeSyntax              #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE DefaultSignatures          #-}
{-# LANGUAGE CPP                        #-}
{-# LANGUAGE PatternSynonyms            #-}
#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE UndecidableSuperClasses    #-}
#endif


module Data.Manifold.FibreBundle where


import Data.AdditiveGroup
import Data.VectorSpace
import Math.LinearMap.Category

import Data.Manifold.Types.Primitive
import Data.Manifold.PseudoAffine

import Math.Rotations.Class
    
import qualified Prelude as Hask

import Control.Category.Constrained.Prelude hiding ((^))
import Control.Category.Discrete
import Control.Arrow.Constrained

import Linear (V2(V2), V3(V3), V4(V4))

import Data.Tagged


pattern TangentBundle :: m -> Needle m -> FibreBundle m (Needle m)
pattern $bTangentBundle :: m -> Needle m -> FibreBundle m (Needle m)
$mTangentBundle :: forall r m.
FibreBundle m (Needle m)
-> (m -> Needle m -> r) -> (Void# -> r) -> r
TangentBundle p v = FibreBundle p v

infixr 5 :@.
-- | Provided for convenience. Flipped synonym of 'FibreBundle', restricted to manifolds
--   without boundary (so the type of the whole can be inferred from its interior).
pattern (:@.) :: f -> m -> FibreBundle m f
pattern f $b:@. :: f -> m -> FibreBundle m f
$m:@. :: forall r f m. FibreBundle m f -> (f -> m -> r) -> (Void# -> r) -> r
:@. p = FibreBundle p f

-- | A zero vector in the fibre bundle at the given position. Intended to be used
--   with tangent-modifying lenses such as 'Math.Manifold.Real.Coordinates.delta'.
tangentAt :: (AdditiveGroup (Needle m)) => m -> TangentBundle m
tangentAt :: m -> TangentBundle m
tangentAt m
p = Needle m
forall v. AdditiveGroup v => v
zeroV Needle m -> m -> TangentBundle m
forall f m. f -> m -> FibreBundle m f
:@. m
p

data TransportOnNeedleWitness k m f where
  TransportOnNeedle :: (ParallelTransporting (LinearFunction (Scalar (Needle m)))
                                             (Needle m) (Needle f))
                     => TransportOnNeedleWitness k m f

data ForgetTransportProperties k m f where
  ForgetTransportProperties :: ParallelTransporting (->) m f
                     => ForgetTransportProperties k m f

class (PseudoAffine m, Category k, Object k f)
           => ParallelTransporting k m f where
  transportOnNeedleWitness :: TransportOnNeedleWitness k m f
  default transportOnNeedleWitness
      :: ParallelTransporting (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f)
           => TransportOnNeedleWitness k m f
  transportOnNeedleWitness = TransportOnNeedleWitness k m f
forall m f (k :: * -> * -> *).
ParallelTransporting
  (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f) =>
TransportOnNeedleWitness k m f
TransportOnNeedle
  forgetTransportProperties :: ForgetTransportProperties k m f
  default forgetTransportProperties :: ParallelTransporting (->) m f
           => ForgetTransportProperties k m f
  forgetTransportProperties = ForgetTransportProperties k m f
forall m f (k :: * -> * -> *).
ParallelTransporting (->) m f =>
ForgetTransportProperties k m f
ForgetTransportProperties
  
  parallelTransport :: m -> Needle m -> k f f
  translateAndInvblyParTransport
        :: m -> Needle m -> (m, (k f f, k f f))
  translateAndInvblyParTransport m
p Needle m
v
              = (m
q, ( m -> Needle m -> k f f
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport m
p Needle m
v
                    , m -> Needle m -> k f f
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport m
q (Needle m -> k f f) -> Needle m -> k f f
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ m
pm -> m -> Needle m
forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~!m
q ))
   where q :: m
q = m
pm -> Needle m -> m
forall x. Semimanifold x => x -> Needle x -> x
.+~^Needle m
v

instance ∀ m s . (PseudoAffine m, s ~ (Scalar (Needle m)), Num' s)
      => ParallelTransporting Discrete m (ZeroDim s) where
  transportOnNeedleWitness :: TransportOnNeedleWitness Discrete m (ZeroDim s)
transportOnNeedleWitness = case (PseudoAffineWitness m
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
    (PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness)) -> TransportOnNeedleWitness Discrete m (ZeroDim s)
forall m f (k :: * -> * -> *).
ParallelTransporting
  (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f) =>
TransportOnNeedleWitness k m f
TransportOnNeedle
  forgetTransportProperties :: ForgetTransportProperties Discrete m (ZeroDim s)
forgetTransportProperties = case (PseudoAffineWitness m
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
    (PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness))
        -> ForgetTransportProperties Discrete m (ZeroDim s)
forall m f (k :: * -> * -> *).
ParallelTransporting (->) m f =>
ForgetTransportProperties k m f
ForgetTransportProperties
  parallelTransport :: m -> Needle m -> Discrete (ZeroDim s) (ZeroDim s)
parallelTransport m
_ Needle m
_ = Discrete (ZeroDim s) (ZeroDim s)
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance ∀ m s . (PseudoAffine m, s ~ (Scalar (Needle m)), Num' s)
      => ParallelTransporting (LinearFunction s) m (ZeroDim s) where
  transportOnNeedleWitness :: TransportOnNeedleWitness (LinearFunction s) m (ZeroDim s)
transportOnNeedleWitness = case (PseudoAffineWitness m
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
    (PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness)) -> TransportOnNeedleWitness (LinearFunction s) m (ZeroDim s)
forall m f (k :: * -> * -> *).
ParallelTransporting
  (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f) =>
TransportOnNeedleWitness k m f
TransportOnNeedle
  forgetTransportProperties :: ForgetTransportProperties (LinearFunction s) m (ZeroDim s)
forgetTransportProperties = case (PseudoAffineWitness m
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
    (PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness))
        -> ForgetTransportProperties (LinearFunction s) m (ZeroDim s)
forall m f (k :: * -> * -> *).
ParallelTransporting (->) m f =>
ForgetTransportProperties k m f
ForgetTransportProperties
  parallelTransport :: m -> Needle m -> LinearFunction s (ZeroDim s) (ZeroDim s)
parallelTransport m
_ Needle m
_ = LinearFunction s (ZeroDim s) (ZeroDim s)
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance ∀ m s . (PseudoAffine m, s ~ (Scalar (Needle m)), Num' s)
      => ParallelTransporting (->) m (ZeroDim s) where
  transportOnNeedleWitness :: TransportOnNeedleWitness (->) m (ZeroDim s)
transportOnNeedleWitness = case (PseudoAffineWitness m
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
    (PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness)) -> TransportOnNeedleWitness (->) m (ZeroDim s)
forall m f (k :: * -> * -> *).
ParallelTransporting
  (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f) =>
TransportOnNeedleWitness k m f
TransportOnNeedle
  forgetTransportProperties :: ForgetTransportProperties (->) m (ZeroDim s)
forgetTransportProperties = case (PseudoAffineWitness m
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
    (PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness))
        -> ForgetTransportProperties (->) m (ZeroDim s)
forall m f (k :: * -> * -> *).
ParallelTransporting (->) m f =>
ForgetTransportProperties k m f
ForgetTransportProperties
  parallelTransport :: m -> Needle m -> ZeroDim s -> ZeroDim s
parallelTransport m
_ Needle m
_ = ZeroDim s -> ZeroDim s
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id

instance (Category k, Object k ℝ) => ParallelTransporting k ℝ ℝ where
  parallelTransport :: ℝ -> Needle ℝ -> k ℝ ℝ
parallelTransport ℝ
_ Needle ℝ
_ = k ℝ ℝ
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance (Category k, Object k ℝ²) => ParallelTransporting k ℝ² ℝ² where
  parallelTransport :: ℝ² -> Needle ℝ² -> k ℝ² ℝ²
parallelTransport ℝ²
_ Needle ℝ²
_ = k ℝ² ℝ²
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance (Category k, Object k ℝ³) => ParallelTransporting k ℝ³ ℝ³ where
  parallelTransport :: ℝ³ -> Needle ℝ³ -> k ℝ³ ℝ³
parallelTransport ℝ³
_ Needle ℝ³
_ = k ℝ³ ℝ³
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance (Category k, Object k ℝ⁴) => ParallelTransporting k ℝ⁴ ℝ⁴ where
  parallelTransport :: ℝ⁴ -> Needle ℝ⁴ -> k ℝ⁴ ℝ⁴
parallelTransport ℝ⁴
_ Needle ℝ⁴
_ = k ℝ⁴ ℝ⁴
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id

instance (Category k, Object k ℝ) => ParallelTransporting k S¹ ℝ where
  parallelTransport :: S¹ -> Needle S¹ -> k ℝ ℝ
parallelTransport S¹
_ Needle S¹
_ = k ℝ ℝ
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id

instance (EnhancedCat k (LinearMap ℝ), Object k ℝ²)
             => ParallelTransporting k S² ℝ² where
  parallelTransport :: S² -> Needle S² -> k ℝ² ℝ²
parallelTransport S²
p Needle S²
v = ((k ℝ² ℝ², k ℝ² ℝ²) -> k ℝ² ℝ²
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst ((k ℝ² ℝ², k ℝ² ℝ²) -> k ℝ² ℝ²)
-> ((S², (k ℝ² ℝ², k ℝ² ℝ²)) -> (k ℝ² ℝ², k ℝ² ℝ²))
-> (S², (k ℝ² ℝ², k ℝ² ℝ²))
-> k ℝ² ℝ²
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
. (S², (k ℝ² ℝ², k ℝ² ℝ²)) -> (k ℝ² ℝ², k ℝ² ℝ²)
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd) (S² -> Needle S² -> (S², (k ℝ² ℝ², k ℝ² ℝ²))
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> (m, (k f f, k f f))
translateAndInvblyParTransport S²
p Needle S²
v)
  translateAndInvblyParTransport :: S² -> Needle S² -> (S², (k ℝ² ℝ², k ℝ² ℝ²))
translateAndInvblyParTransport (S²Polar ℝ
θ₀ ℝ
φ₀) Needle S²
𝐯
     | ℝ
d ℝ -> ℝ -> Bool
forall a. Ord a => a -> a -> Bool
< ℝ
forall a. Floating a => a
pi     = (ℝ -> ℝ -> S²
forall r. r -> r -> S²_ r
S²Polar ℝ
θ₁ ℝ
φ₁, (LinearMap ℝ ℝ² ℝ² -> k ℝ² ℝ²
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 ℝ ℝ² ℝ²
fwd, LinearMap ℝ ℝ² ℝ² -> k ℝ² ℝ²
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 ℝ ℝ² ℝ²
bwd))
     | ℝ
d ℝ -> ℝ -> Bool
forall a. Ord a => a -> a -> Bool
< ℝ
2ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
*ℝ
forall a. Floating a => a
pi   = S² -> Needle S² -> (S², (k ℝ² ℝ², k ℝ² ℝ²))
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> (m, (k f f, k f f))
translateAndInvblyParTransport (ℝ -> ℝ -> S²
forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ ℝ
φ₀)
                      (ℝ² -> (S², (k ℝ² ℝ², k ℝ² ℝ²))) -> ℝ² -> (S², (k ℝ² ℝ², k ℝ² ℝ²))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ℝ²
Needle S²
𝐯ℝ² -> ℝ -> ℝ²
forall v s. (VectorSpace v, s ~ Scalar v) => v -> s -> v
^*(-(ℝ
2ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
*ℝ
forall a. Floating a => a
piℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
-ℝ
d)ℝ -> ℝ -> ℝ
forall a. Fractional a => a -> a -> a
/ℝ
d)
     | Bool
otherwise  = S² -> Needle S² -> (S², (k ℝ² ℝ², k ℝ² ℝ²))
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> (m, (k f f, k f f))
translateAndInvblyParTransport (ℝ -> ℝ -> S²
forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ ℝ
φ₀)
                      (ℝ² -> (S², (k ℝ² ℝ², k ℝ² ℝ²))) -> ℝ² -> (S², (k ℝ² ℝ², k ℝ² ℝ²))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ let revolutions :: Integer
revolutions = ℝ -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
floor (ℝ -> Integer) -> ℝ -> Integer
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ℝ
dℝ -> ℝ -> ℝ
forall a. Fractional a => a -> a -> a
/(ℝ
2ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
*ℝ
forall a. Floating a => a
pi)
                        in ℝ²
Needle S²
𝐯ℝ² -> ℝ -> ℝ²
forall v s. (VectorSpace v, s ~ Scalar v) => v -> s -> v
^*((ℝ
d ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
- ℝ
2ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
*ℝ
forall a. Floating a => a
piℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
*Integer -> ℝ
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
revolutions)ℝ -> ℝ -> ℝ
forall a. Fractional a => a -> a -> a
/ℝ
d)
   where -- See images/constructions/sphericoords-needles.svg. Translation as in
         -- "Data.Manifold.PseudoAffine" instance.
         S¹Polar ℝ
γc₀ = ℝ² -> S¹
forall m v. NaturallyEmbedded m v => v -> m
coEmbed ℝ²
Needle S²
𝐯
         γ₀ :: ℝ
γ₀ | ℝ
θ₀ ℝ -> ℝ -> Bool
forall a. Ord a => a -> a -> Bool
< ℝ
forall a. Floating a => a
piℝ -> ℝ -> ℝ
forall a. Fractional a => a -> a -> a
/ℝ
2   = ℝ
γc₀ ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
- ℝ
φ₀
            | Bool
otherwise   = ℝ
γc₀ ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
+ ℝ
φ₀
         d :: ℝ
d = ℝ² -> ℝ
forall v s. (InnerSpace v, s ~ Scalar v, Floating s) => v -> s
magnitude ℝ²
Needle S²
𝐯
         S¹Polar ℝ
φ₁ = ℝ -> S¹
forall r. r -> S¹_ r
S¹Polar ℝ
φ₀ S¹ -> Needle S¹ -> S¹
forall x. Semimanifold x => x -> Needle x -> x
.+~^ ℝ
Needle S¹
δφ
         
         -- Cartesian coordinates of p₁ in the system whose north pole is p₀
         -- with φ₀ as the zero meridian
         V3 ℝ
bx ℝ
by ℝ
bz = S² -> ℝ³
forall m v. NaturallyEmbedded m v => m -> v
embed (S² -> ℝ³) -> S² -> ℝ³
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ℝ -> ℝ -> S²
forall r. r -> r -> S²_ r
S²Polar ℝ
d ℝ
γ₀
         
         sθ₀ :: ℝ
sθ₀ = ℝ -> ℝ
forall a. Floating a => a -> a
sin ℝ
θ₀; cθ₀ :: ℝ
cθ₀ = ℝ -> ℝ
forall a. Floating a => a -> a
cos ℝ
θ₀
         -- Cartesian coordinates of p₁ in the system with the standard north pole,
         -- but still φ₀ as the zero meridian
         (ℝ
qx,ℝ
qz) = ( ℝ
cθ₀ ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
* ℝ
bx ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
+ ℝ
sθ₀ ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
* ℝ
bz
                   ,-ℝ
sθ₀ ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
* ℝ
bx ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
+ ℝ
cθ₀ ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
* ℝ
bz )
         qy :: ℝ
qy      = ℝ
by
         
         S²Polar ℝ
θ₁ ℝ
δφ = ℝ³ -> S²
forall m v. NaturallyEmbedded m v => v -> m
coEmbed (ℝ³ -> S²) -> ℝ³ -> S²
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ℝ -> ℝ -> ℝ -> ℝ³
forall a. a -> a -> a -> V3 a
V3 ℝ
qx ℝ
qy ℝ
qz
         
         sθ₁ :: ℝ
sθ₁ = ℝ -> ℝ
forall a. Floating a => a -> a
sin ℝ
θ₁; cθ₁ :: ℝ
cθ₁ = ℝ -> ℝ
forall a. Floating a => a -> a
cos ℝ
θ₁
         
         γ₁ :: ℝ
γ₁
          | ℝ
sθ₀ℝ -> ℝ -> Bool
forall a. Ord a => a -> a -> Bool
<=ℝ
sθ₁  = let
              -- Cartesian coordinates of the standard north pole in the system whose north
              -- pole is p₀ with 𝐯 along the zero meridian
              V3 ℝ
nbx ℝ
nby ℝ
nbz = S² -> ℝ³
forall m v. NaturallyEmbedded m v => m -> v
embed (S² -> ℝ³) -> S² -> ℝ³
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ℝ -> ℝ -> S²
forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ (ℝ
forall a. Floating a => a
piℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
-ℝ
γ₀)
              
              sd :: ℝ
sd = ℝ -> ℝ
forall a. Floating a => a -> a
sin ℝ
d; cd :: ℝ
cd = ℝ -> ℝ
forall a. Floating a => a -> a
cos ℝ
d
              -- Cartesian coordinates of the standard north pole in the system whose north
              -- pole is p₁ with 𝐯 along the zero meridian
              (ℝ
ox,ℝ
oz) = ( ℝ
cd ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
* ℝ
nbx ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
- ℝ
sd ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
* ℝ
nbz
                        , ℝ
sd ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
* ℝ
nbx ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
+ ℝ
cd ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
* ℝ
nbz )
              oy :: ℝ
oy      = ℝ
nby

           in ℝ -> ℝ -> ℝ
forall a. RealFloat a => a -> a -> a
atan2 ℝ
oy (-ℝ
ox)

          | Bool
otherwise = let
              -- Cartesian coordinates of p₀ in the system with the standard north pole,
              -- with p₁ on the zero meridian
              V3 ℝ
gx ℝ
gy ℝ
gz = S² -> ℝ³
forall m v. NaturallyEmbedded m v => m -> v
embed (S² -> ℝ³) -> S² -> ℝ³
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ℝ -> ℝ -> S²
forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ (-ℝ
δφ)
              
              -- Cartesian coordinates of p₀ in the system whose north
              -- pole is p₁ and the standard north pole on the zero meridian
              (ℝ
ux,ℝ
uz) = ( ℝ
cθ₁ ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
* ℝ
gx ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
- ℝ
sθ₁ ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
* ℝ
gz
                        , ℝ
sθ₁ ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
* ℝ
gx ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
+ ℝ
cθ₁ ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
* ℝ
gz )
              uy :: ℝ
uy      = ℝ
gy

           in ℝ -> ℝ -> ℝ
forall a. RealFloat a => a -> a -> a
atan2 (-ℝ
uy) (-ℝ
ux)

         γc₁ :: ℝ
γc₁ | ℝ
θ₁ ℝ -> ℝ -> Bool
forall a. Ord a => a -> a -> Bool
< ℝ
forall a. Floating a => a
piℝ -> ℝ -> ℝ
forall a. Fractional a => a -> a -> a
/ℝ
2  = ℝ
γ₁ ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
+ ℝ
φ₁
             | Bool
otherwise  = ℝ
γ₁ ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
- ℝ
φ₁

         (ℝ
sδγc, ℝ
cδγc) = ℝ -> ℝ
forall a. Floating a => a -> a
sin (ℝ -> ℝ) -> (ℝ -> ℝ) -> ℝ -> (ℝ, ℝ)
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. Floating a => a -> a
cos (ℝ -> (ℝ, ℝ)) -> ℝ -> (ℝ, ℝ)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ℝ
γc₁ ℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
- ℝ
γc₀

         fwd :: LinearMap ℝ ℝ² ℝ²
fwd = TensorProduct (DualVector ℝ²) ℝ² -> LinearMap ℝ ℝ² ℝ²
forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap (ℝ² -> ℝ² -> V2 ℝ²
forall a. a -> a -> V2 a
V2 (ℝ -> ℝ -> ℝ²
forall a. a -> a -> V2 a
V2   ℝ
cδγc  ℝ
sδγc)
                             (ℝ -> ℝ -> ℝ²
forall a. a -> a -> V2 a
V2 (-ℝ
sδγc) ℝ
cδγc)) :: LinearMap ℝ ℝ² ℝ²
         bwd :: LinearMap ℝ ℝ² ℝ²
bwd = TensorProduct (DualVector ℝ²) ℝ² -> LinearMap ℝ ℝ² ℝ²
forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap (ℝ² -> ℝ² -> V2 ℝ²
forall a. a -> a -> V2 a
V2 (ℝ -> ℝ -> ℝ²
forall a. a -> a -> V2 a
V2 ℝ
cδγc (-ℝ
sδγc))
                             (ℝ -> ℝ -> ℝ²
forall a. a -> a -> V2 a
V2 ℝ
sδγc   ℝ
cδγc )) :: LinearMap ℝ ℝ² ℝ²


instance {-# OVERLAPS #-} ∀ k a b fa fb s .
         ( ParallelTransporting k a fa, ParallelTransporting k b fb
         , PseudoAffine fa, PseudoAffine fb
         , Scalar (Needle a) ~ s, Scalar (Needle b) ~ s
         , Scalar (Needle fa) ~ s, Scalar (Needle fb) ~ s
         , Num' s
         , Morphism k, ObjectPair k fa fb )
              => ParallelTransporting k (a,b) (fa,fb) where
  transportOnNeedleWitness :: TransportOnNeedleWitness k (a, b) (fa, fb)
transportOnNeedleWitness = case
         ( PseudoAffineWitness a
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness a
         , PseudoAffineWitness b
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness b
         , PseudoAffineWitness fa
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness fa
         , PseudoAffineWitness fb
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness fb
         , TransportOnNeedleWitness k a fa
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
TransportOnNeedleWitness k m f
transportOnNeedleWitness :: TransportOnNeedleWitness k a fa
         , TransportOnNeedleWitness k b fb
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
TransportOnNeedleWitness k m f
transportOnNeedleWitness :: TransportOnNeedleWitness k b fb ) of
     ( PseudoAffineWitness (SemimanifoldWitness a
SemimanifoldWitness)
      ,PseudoAffineWitness (SemimanifoldWitness b
SemimanifoldWitness)
      ,PseudoAffineWitness (SemimanifoldWitness fa
SemimanifoldWitness)
      ,PseudoAffineWitness (SemimanifoldWitness fb
SemimanifoldWitness)
      ,TransportOnNeedleWitness k a fa
TransportOnNeedle, TransportOnNeedleWitness k b fb
TransportOnNeedle)
         -> TransportOnNeedleWitness k (a, b) (fa, fb)
forall m f (k :: * -> * -> *).
ParallelTransporting
  (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f) =>
TransportOnNeedleWitness k m f
TransportOnNeedle
  forgetTransportProperties :: ForgetTransportProperties k (a, b) (fa, fb)
forgetTransportProperties = case
    ( ForgetTransportProperties k a fa
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties :: ForgetTransportProperties k a fa
    , ForgetTransportProperties k b fb
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties :: ForgetTransportProperties k b fb ) of
     (ForgetTransportProperties k a fa
ForgetTransportProperties, ForgetTransportProperties k b fb
ForgetTransportProperties) -> ForgetTransportProperties k (a, b) (fa, fb)
forall m f (k :: * -> * -> *).
ParallelTransporting (->) m f =>
ForgetTransportProperties k m f
ForgetTransportProperties
  parallelTransport :: (a, b) -> Needle (a, b) -> k (fa, fb) (fa, fb)
parallelTransport (a
pa,b
pb) (va,vb)
       = a -> Needle a -> k fa fa
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport a
pa Needle a
va  k fa fa -> k fb fb -> k (fa, fb) (fa, fb)
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')
*** b -> Needle b -> k fb fb
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport b
pb Needle b
vb

instance ∀ k a f g s .
         ( ParallelTransporting k a f, ParallelTransporting k a g
         , ParallelTransporting (LinearFunction s) (Needle a) (Needle f, Needle g)
         , PseudoAffine f, PseudoAffine g
         , Morphism k, ObjectPair k f g )
              => ParallelTransporting k a (f,g) where
  transportOnNeedleWitness :: TransportOnNeedleWitness k a (f, g)
transportOnNeedleWitness = case
         ( PseudoAffineWitness a
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness a
         , PseudoAffineWitness f
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness f
         , PseudoAffineWitness g
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness g
         , TransportOnNeedleWitness k a f
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
TransportOnNeedleWitness k m f
transportOnNeedleWitness :: TransportOnNeedleWitness k a f
         , TransportOnNeedleWitness k a g
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
TransportOnNeedleWitness k m f
transportOnNeedleWitness :: TransportOnNeedleWitness k a g ) of
     ( PseudoAffineWitness (SemimanifoldWitness a
SemimanifoldWitness)
      ,PseudoAffineWitness (SemimanifoldWitness f
SemimanifoldWitness)
      ,PseudoAffineWitness (SemimanifoldWitness g
SemimanifoldWitness)
      ,TransportOnNeedleWitness k a f
TransportOnNeedle, TransportOnNeedleWitness k a g
TransportOnNeedle)
         -> TransportOnNeedleWitness k a (f, g)
forall m f (k :: * -> * -> *).
ParallelTransporting
  (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f) =>
TransportOnNeedleWitness k m f
TransportOnNeedle
  forgetTransportProperties :: ForgetTransportProperties k a (f, g)
forgetTransportProperties = case
    ( ForgetTransportProperties k a f
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties :: ForgetTransportProperties k a f
    , ForgetTransportProperties k a g
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties :: ForgetTransportProperties k a g ) of
     (ForgetTransportProperties k a f
ForgetTransportProperties, ForgetTransportProperties k a g
ForgetTransportProperties) -> ForgetTransportProperties k a (f, g)
forall m f (k :: * -> * -> *).
ParallelTransporting (->) m f =>
ForgetTransportProperties k m f
ForgetTransportProperties
  parallelTransport :: a -> Needle a -> k (f, g) (f, g)
parallelTransport a
p Needle a
v
       = a -> Needle a -> k f f
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport a
p Needle a
v k f f -> k g g -> k (f, g) (f, g)
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')
*** a -> Needle a -> k g g
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport a
p Needle a
v


instance ( ParallelTransporting (LinearFunction (Scalar f)) m f, AdditiveGroup m
         , VectorSpace f )
                => AdditiveGroup (FibreBundle m f) where
  zeroV :: FibreBundle m f
zeroV = m -> f -> FibreBundle m f
forall b f. b -> f -> FibreBundle b f
FibreBundle m
forall v. AdditiveGroup v => v
zeroV f
forall v. AdditiveGroup v => v
zeroV
  FibreBundle m
p f
v ^+^ :: FibreBundle m f -> FibreBundle m f -> FibreBundle m f
^+^ FibreBundle m
q f
w = m -> f -> FibreBundle m f
forall b f. b -> f -> FibreBundle b f
FibreBundle (m
pm -> m -> m
forall v. AdditiveGroup v => v -> v -> v
^+^m
q) (f
vf -> f -> f
forall v. AdditiveGroup v => v -> v -> v
^+^f
w)
  negateV :: FibreBundle m f -> FibreBundle m f
negateV (FibreBundle m
p f
v) = m -> f -> FibreBundle m f
forall b f. b -> f -> FibreBundle b f
FibreBundle (m -> m
forall v. AdditiveGroup v => v -> v
negateV m
p) (f -> f
forall v. AdditiveGroup v => v -> v
negateV f
v)

instance ∀ m f s .
         ( ParallelTransporting (->) m f, Semimanifold f
         , ParallelTransporting (LinearFunction s) (Needle m) (Needle f)
         , s ~ Scalar (Needle m) )
                => Semimanifold (FibreBundle m f) where
  type Needle (FibreBundle m f) = FibreBundle (Needle m) (Needle f)
  semimanifoldWitness :: SemimanifoldWitness (FibreBundle m f)
semimanifoldWitness = case ( SemimanifoldWitness m
forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness :: SemimanifoldWitness m
                             , SemimanifoldWitness f
forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness :: SemimanifoldWitness f
                             , ForgetTransportProperties (LinearFunction s) (Needle m) (Needle f)
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties
                               :: ForgetTransportProperties (LinearFunction s) (Needle m) (Needle f)
                             ) of
         (SemimanifoldWitness m
SemimanifoldWitness, SemimanifoldWitness f
SemimanifoldWitness
          ,ForgetTransportProperties (LinearFunction s) (Needle m) (Needle f)
ForgetTransportProperties)
           -> SemimanifoldWitness (FibreBundle m f)
forall x.
(Semimanifold (Needle x), Needle (Needle x) ~ Needle x) =>
SemimanifoldWitness x
SemimanifoldWitness
  FibreBundle m
p f
f .+~^ :: FibreBundle m f -> Needle (FibreBundle m f) -> FibreBundle m f
.+~^ FibreBundle v δf
      = m -> f -> FibreBundle m f
forall b f. b -> f -> FibreBundle b f
FibreBundle (m
pm -> Needle m -> m
forall x. Semimanifold x => x -> Needle x -> x
.+~^Needle m
v) (m -> Needle m -> f -> f
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport m
p Needle m
v f
ff -> Needle f -> f
forall x. Semimanifold x => x -> Needle x -> x
.+~^Needle f
δf)

instance ∀ m f s .
         ( ParallelTransporting (->) m f
         , PseudoAffine f
         , ParallelTransporting (LinearFunction s) (Needle m) (Needle f)
         , s ~ Scalar (Needle m) )
                => PseudoAffine (FibreBundle m f) where
  pseudoAffineWitness :: PseudoAffineWitness (FibreBundle m f)
pseudoAffineWitness = case ( PseudoAffineWitness m
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m
                             , PseudoAffineWitness f
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness f
                             , ForgetTransportProperties (LinearFunction s) (Needle m) (Needle f)
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties
                               :: ForgetTransportProperties (LinearFunction s) (Needle m) (Needle f)
                             ) of
     ( PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness)
      ,PseudoAffineWitness (SemimanifoldWitness f
SemimanifoldWitness)
      ,ForgetTransportProperties (LinearFunction s) (Needle m) (Needle f)
ForgetTransportProperties)
         -> SemimanifoldWitness (FibreBundle m f)
-> PseudoAffineWitness (FibreBundle m f)
forall x.
PseudoAffine (Needle x) =>
SemimanifoldWitness x -> PseudoAffineWitness x
PseudoAffineWitness (SemimanifoldWitness (FibreBundle m f)
forall x.
(Semimanifold (Needle x), Needle (Needle x) ~ Needle x) =>
SemimanifoldWitness x
SemimanifoldWitness)
  FibreBundle m
p f
f .-~! :: FibreBundle m f -> FibreBundle m f -> Needle (FibreBundle m f)
.-~! FibreBundle m
q f
g = case m
pm -> m -> Needle m
forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~!m
q of
      Needle m
v  -> Needle m -> Needle f -> FibreBundle (Needle m) (Needle f)
forall b f. b -> f -> FibreBundle b f
FibreBundle Needle m
v (Needle f -> FibreBundle (Needle m) (Needle f))
-> Needle f -> FibreBundle (Needle m) (Needle f)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ f
f f -> f -> Needle f
forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~! m -> Needle m -> f -> f
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport m
p Needle m
v f
g
  FibreBundle m
p f
f .-~. :: FibreBundle m f
-> FibreBundle m f -> Maybe (Needle (FibreBundle m f))
.-~. FibreBundle m
q f
g = case m
pm -> m -> Maybe (Needle m)
forall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~.m
q of
      Maybe (Needle m)
Nothing -> Maybe (Needle (FibreBundle m f))
forall a. Maybe a
Nothing
      Just Needle m
v  -> Needle m -> Needle f -> FibreBundle (Needle m) (Needle f)
forall b f. b -> f -> FibreBundle b f
FibreBundle Needle m
v (Needle f -> FibreBundle (Needle m) (Needle f))
-> Maybe (Needle f) -> Maybe (FibreBundle (Needle m) (Needle f))
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> f
f f -> f -> Maybe (Needle f)
forall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~. m -> Needle m -> f -> f
forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport m
p Needle m
v f
g


instance (AdditiveGroup f) => NaturallyEmbedded x (FibreBundle x f) where
  embed :: x -> FibreBundle x f
embed x
x = x -> f -> FibreBundle x f
forall b f. b -> f -> FibreBundle b f
FibreBundle x
x f
forall v. AdditiveGroup v => v
zeroV
  coEmbed :: FibreBundle x f -> x
coEmbed (FibreBundle x
x f
_) = x
x

instance (NaturallyEmbedded m v, VectorSpace f)
    => NaturallyEmbedded (FibreBundle m (ZeroDim s)) (FibreBundle v f) where
  embed :: FibreBundle m (ZeroDim s) -> FibreBundle v f
embed (FibreBundle m
x ZeroDim s
Origin) = v -> f -> FibreBundle v f
forall b f. b -> f -> FibreBundle b f
FibreBundle (m -> v
forall m v. NaturallyEmbedded m v => m -> v
embed m
x) f
forall v. AdditiveGroup v => v
zeroV
  coEmbed :: FibreBundle v f -> FibreBundle m (ZeroDim s)
coEmbed (FibreBundle v
u f
_) = m -> ZeroDim s -> FibreBundle m (ZeroDim s)
forall b f. b -> f -> FibreBundle b f
FibreBundle (v -> m
forall m v. NaturallyEmbedded m v => v -> m
coEmbed v
u) ZeroDim s
forall s. ZeroDim s
Origin

instance (AdditiveGroup y, AdditiveGroup g)
           => NaturallyEmbedded (FibreBundle x f) (FibreBundle (x,y) (f,g)) where
  embed :: FibreBundle x f -> FibreBundle (x, y) (f, g)
embed (FibreBundle x
x f
δx) = (x, y) -> (f, g) -> FibreBundle (x, y) (f, g)
forall b f. b -> f -> FibreBundle b f
FibreBundle (x
x,y
forall v. AdditiveGroup v => v
zeroV) (f
δx,g
forall v. AdditiveGroup v => v
zeroV)
  coEmbed :: FibreBundle (x, y) (f, g) -> FibreBundle x f
coEmbed (FibreBundle (x
x,y
_) (f
δx,g
_)) = x -> f -> FibreBundle x f
forall b f. b -> f -> FibreBundle b f
FibreBundle x
x f
δx

instance NaturallyEmbedded v w
      => NaturallyEmbedded (FibreBundle ℝ v) (FibreBundle ℝ w) where
  embed :: FibreBundle ℝ v -> FibreBundle ℝ w
embed (FibreBundle ℝ
p v
v) = ℝ -> w -> FibreBundle ℝ w
forall b f. b -> f -> FibreBundle b f
FibreBundle ℝ
p (w -> FibreBundle ℝ w) -> w -> FibreBundle ℝ w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ v -> w
forall m v. NaturallyEmbedded m v => m -> v
embed v
v
  coEmbed :: FibreBundle ℝ w -> FibreBundle ℝ v
coEmbed (FibreBundle ℝ
p w
w) = ℝ -> v -> FibreBundle ℝ v
forall b f. b -> f -> FibreBundle b f
FibreBundle ℝ
p (v -> FibreBundle ℝ v) -> v -> FibreBundle ℝ v
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ w -> v
forall m v. NaturallyEmbedded m v => v -> m
coEmbed w
w
instance (NaturallyEmbedded v w, s'~s)
      => NaturallyEmbedded (FibreBundle (V2 s) v) (FibreBundle (V2 s') w) where
  embed :: FibreBundle (V2 s) v -> FibreBundle (V2 s') w
embed (FibreBundle V2 s
p v
v) = V2 s -> w -> FibreBundle (V2 s) w
forall b f. b -> f -> FibreBundle b f
FibreBundle V2 s
p (w -> FibreBundle (V2 s') w) -> w -> FibreBundle (V2 s') w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ v -> w
forall m v. NaturallyEmbedded m v => m -> v
embed v
v
  coEmbed :: FibreBundle (V2 s') w -> FibreBundle (V2 s) v
coEmbed (FibreBundle V2 s'
p w
w) = V2 s' -> v -> FibreBundle (V2 s') v
forall b f. b -> f -> FibreBundle b f
FibreBundle V2 s'
p (v -> FibreBundle (V2 s) v) -> v -> FibreBundle (V2 s) v
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ w -> v
forall m v. NaturallyEmbedded m v => v -> m
coEmbed w
w
instance (NaturallyEmbedded v w, s'~s)
      => NaturallyEmbedded (FibreBundle (V3 s) v) (FibreBundle (V3 s') w) where
  embed :: FibreBundle (V3 s) v -> FibreBundle (V3 s') w
embed (FibreBundle V3 s
p v
v) = V3 s -> w -> FibreBundle (V3 s) w
forall b f. b -> f -> FibreBundle b f
FibreBundle V3 s
p (w -> FibreBundle (V3 s') w) -> w -> FibreBundle (V3 s') w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ v -> w
forall m v. NaturallyEmbedded m v => m -> v
embed v
v
  coEmbed :: FibreBundle (V3 s') w -> FibreBundle (V3 s) v
coEmbed (FibreBundle V3 s'
p w
w) = V3 s' -> v -> FibreBundle (V3 s') v
forall b f. b -> f -> FibreBundle b f
FibreBundle V3 s'
p (v -> FibreBundle (V3 s) v) -> v -> FibreBundle (V3 s) v
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ w -> v
forall m v. NaturallyEmbedded m v => v -> m
coEmbed w
w
instance (NaturallyEmbedded v w, s'~s)
      => NaturallyEmbedded (FibreBundle (V4 s) v) (FibreBundle (V4 s') w) where
  embed :: FibreBundle (V4 s) v -> FibreBundle (V4 s') w
embed (FibreBundle V4 s
p v
v) = V4 s -> w -> FibreBundle (V4 s) w
forall b f. b -> f -> FibreBundle b f
FibreBundle V4 s
p (w -> FibreBundle (V4 s') w) -> w -> FibreBundle (V4 s') w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ v -> w
forall m v. NaturallyEmbedded m v => m -> v
embed v
v
  coEmbed :: FibreBundle (V4 s') w -> FibreBundle (V4 s) v
coEmbed (FibreBundle V4 s'
p w
w) = V4 s' -> v -> FibreBundle (V4 s') v
forall b f. b -> f -> FibreBundle b f
FibreBundle V4 s'
p (v -> FibreBundle (V4 s) v) -> v -> FibreBundle (V4 s) v
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ w -> v
forall m v. NaturallyEmbedded m v => v -> m
coEmbed w
w

instance (RealFloat s, InnerSpace s, s~s', s~s'', s~s''')
      => NaturallyEmbedded (FibreBundle (S¹_ s) s') (FibreBundle (V2 s'') (V2 s''')) where
  embed :: FibreBundle (S¹_ s) s' -> FibreBundle (V2 s'') (V2 s''')
embed (FibreBundle (S¹Polar s
φ) s'
l) = V2 s''' -> V2 s''' -> FibreBundle (V2 s''') (V2 s''')
forall b f. b -> f -> FibreBundle b f
FibreBundle (s''' -> s''' -> V2 s'''
forall a. a -> a -> V2 a
V2 s'''
cφ s'''
sφ) (V2 s''' -> FibreBundle (V2 s'') (V2 s'''))
-> V2 s''' -> FibreBundle (V2 s'') (V2 s''')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s'
Scalar (V2 s''')
lScalar (V2 s''') -> V2 s''' -> V2 s'''
forall v. VectorSpace v => Scalar v -> v -> v
*^(s''' -> s''' -> V2 s'''
forall a. a -> a -> V2 a
V2 (-s'''
sφ) s'''
cφ)
   where (s'''
cφ, s'''
sφ) = (s''' -> s'''
forall a. Floating a => a -> a
cos (s''' -> s''') -> (s''' -> s''') -> s''' -> (s''', s''')
forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& s''' -> s'''
forall a. Floating a => a -> a
sin) s
φ
  coEmbed :: FibreBundle (V2 s'') (V2 s''') -> FibreBundle (S¹_ s) s'
coEmbed (FibreBundle (V2 s''
0 s''
0) (V2 s'''
_ s'''
δy)) = S¹_ s -> s''' -> FibreBundle (S¹_ s) s'''
forall b f. b -> f -> FibreBundle b f
FibreBundle (s -> S¹_ s
forall r. r -> S¹_ r
S¹Polar s
0) s'''
δy
  coEmbed (FibreBundle V2 s''
p (V2 s'''
δx s'''
δy)) = S¹_ s''' -> s''' -> FibreBundle (S¹_ s''') s'''
forall b f. b -> f -> FibreBundle b f
FibreBundle (s'' -> S¹_ s'''
forall r. r -> S¹_ r
S¹Polar (s'' -> S¹_ s''') -> s'' -> S¹_ s'''
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s'' -> s'' -> s''
forall a. RealFloat a => a -> a -> a
atan2 s''
sφ s''
cφ) (s'' -> FibreBundle (S¹_ s) s') -> s'' -> FibreBundle (S¹_ s) s'
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s''
cφs'' -> s'' -> s''
forall a. Num a => a -> a -> a
*s''
s'''
δy s'' -> s'' -> s''
forall a. Num a => a -> a -> a
- s''
sφs'' -> s'' -> s''
forall a. Num a => a -> a -> a
*s''
s'''
δx
   where V2 s''
cφ s''
sφ = V2 s''
pV2 s'' -> s''' -> V2 s''
forall v s.
(VectorSpace v, s ~ Scalar v, Fractional s) =>
v -> s -> v
^/s'''
r
         r :: s'''
r = V2 s'' -> s'''
forall v s. (InnerSpace v, s ~ Scalar v, Floating s) => v -> s
magnitude V2 s''
p

instance ∀ s s' s'' s''' . (RealFloat' s, InnerSpace s, s~s', s~s'', s~s''')
   => NaturallyEmbedded (FibreBundle (S²_ s) (V2 s')) (FibreBundle (V3 s'') (V3 s''')) where
  embed :: FibreBundle (S²_ s) (V2 s') -> FibreBundle (V3 s'') (V3 s''')
embed (FibreBundle (S²Polar s
θ s
φ) v :: V2 s'
v@(V2 s'
δξ s'
δυ))
       = V3 s'' -> V3 s'' -> FibreBundle (V3 s'') (V3 s'')
forall b f. b -> f -> FibreBundle b f
FibreBundle (s'' -> s'' -> s'' -> V3 s''
forall a. a -> a -> a -> V3 a
V3 (s''
sθs'' -> s'' -> s''
forall a. Num a => a -> a -> a
*s''
cφ) (s''
sθs'' -> s'' -> s''
forall a. Num a => a -> a -> a
*s''
sφ) s''
cθ) V3 s''
𝐯r
   where [V2 s''
cθ s''
sθ, V2 s''
cφ s''
sφ] = S¹_ s''' -> V2 s''
forall m v. NaturallyEmbedded m v => m -> v
embed (S¹_ s''' -> V2 s'') -> (s -> S¹_ s''') -> s -> V2 s''
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
. s -> S¹_ s'''
forall r. r -> S¹_ r
S¹Polar (s -> V2 s'') -> [s] -> [V2 s'']
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> [s
θ,s
φ]
         S¹Polar s
γc = V2 s' -> S¹_ s
forall m v. NaturallyEmbedded m v => v -> m
coEmbed V2 s'
v
         γ :: s
γ | s
θ s -> s -> Bool
forall a. Ord a => a -> a -> Bool
< s
forall a. Floating a => a
pis -> s -> s
forall a. Fractional a => a -> a -> a
/s
2   = s
γc s -> s -> s
forall a. Num a => a -> a -> a
- s
φ
           | Bool
otherwise  = s
γc s -> s -> s
forall a. Num a => a -> a -> a
+ s
φ
         d :: s'''
d = V2 s' -> s'''
forall v s. (InnerSpace v, s ~ Scalar v, Floating s) => v -> s
magnitude V2 s'
v

         V2 s'''
δθ s'''
δφ = s'''
Scalar (V2 s''')
d Scalar (V2 s''') -> V2 s''' -> V2 s'''
forall v. VectorSpace v => Scalar v -> v -> v
*^ S¹_ s -> V2 s'''
forall m v. NaturallyEmbedded m v => m -> v
embed (s -> S¹_ s
forall r. r -> S¹_ r
S¹Polar s
γ)
         
         𝐞φ :: V3 s''
𝐞φ = s'' -> s'' -> s'' -> V3 s''
forall a. a -> a -> a -> V3 a
V3 (-s''
sφ) s''
cφ s''
0
         𝐞θ :: V3 s''
𝐞θ = s'' -> s'' -> s'' -> V3 s''
forall a. a -> a -> a -> V3 a
V3 (s''
cθs'' -> s'' -> s''
forall a. Num a => a -> a -> a
*s''
cφ) (s''
cθs'' -> s'' -> s''
forall a. Num a => a -> a -> a
*s''
sφ) (-s''
sθ)
         𝐯r :: V3 s''
𝐯r = s'''
Scalar (V3 s'')
δθScalar (V3 s'') -> V3 s'' -> V3 s''
forall v. VectorSpace v => Scalar v -> v -> v
*^V3 s''
𝐞θ V3 s'' -> V3 s'' -> V3 s''
forall v. AdditiveGroup v => v -> v -> v
^+^ s'''
Scalar (V3 s'')
δφScalar (V3 s'') -> V3 s'' -> V3 s''
forall v. VectorSpace v => Scalar v -> v -> v
*^V3 s''
𝐞φ
  
  coEmbed :: FibreBundle (V3 s'') (V3 s''') -> FibreBundle (S²_ s) (V2 s')
coEmbed (FibreBundle (V3 s''
x s''
y s''
z) V3 s'''
𝐯r) = case Num' s => ClosedScalarWitness s
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of
   ClosedScalarWitness s
ClosedScalarWitness -> S²_ s'' -> V2 s' -> FibreBundle (S²_ s'') (V2 s')
forall b f. b -> f -> FibreBundle b f
FibreBundle (s'' -> s'' -> S²_ s''
forall r. r -> r -> S²_ r
S²Polar s''
θ s''
φ) ((s''', s''') -> s'''
forall v s. (InnerSpace v, s ~ Scalar v, Floating s) => v -> s
magnitude (s'''
Scalar (V3 s'')
δθ,s'''
Scalar (V3 s'')
δφ) Scalar (V2 s') -> V2 s' -> V2 s'
forall v. VectorSpace v => Scalar v -> v -> v
*^ S¹_ s'' -> V2 s'
forall m v. NaturallyEmbedded m v => m -> v
embed (s'' -> S¹_ s''
forall r. r -> S¹_ r
S¹Polar s''
γc))
     where r :: s''
r = s'' -> s''
forall a. Floating a => a -> a
sqrt (s'' -> s'') -> s'' -> s''
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s''
xs'' -> Int -> s''
forall a. Num a => a -> Int -> a
^Int
2 s'' -> s'' -> s''
forall a. Num a => a -> a -> a
+ s''
ys'' -> Int -> s''
forall a. Num a => a -> Int -> a
^Int
2 s'' -> s'' -> s''
forall a. Num a => a -> a -> a
+ s''
zs'' -> Int -> s''
forall a. Num a => a -> Int -> a
^Int
2
           rxy :: s''
rxy = s'' -> s''
forall a. Floating a => a -> a
sqrt (s'' -> s'') -> s'' -> s''
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s''
xs'' -> Int -> s''
forall a. Num a => a -> Int -> a
^Int
2 s'' -> s'' -> s''
forall a. Num a => a -> a -> a
+ s''
ys'' -> Int -> s''
forall a. Num a => a -> Int -> a
^Int
2
           θ :: s''
θ = s'' -> s'' -> s''
forall a. RealFloat a => a -> a -> a
atan2 s''
rxy s''
z
           φ :: s''
φ = s'' -> s'' -> s''
forall a. RealFloat a => a -> a -> a
atan2 s''
y s''
x
           cθ :: s''
cθ = s''
z s'' -> s'' -> s''
forall a. Fractional a => a -> a -> a
/ s''
r
           sθ :: s''
sθ = s''
rxy s'' -> s'' -> s''
forall a. Fractional a => a -> a -> a
/ s''
r
           (s''
cφ,s''
sφ) | s''
rxys'' -> s'' -> Bool
forall a. Ord a => a -> a -> Bool
>s''
0      = (s''
x,s''
y)(s'', s'') -> s'' -> (s'', s'')
forall v s.
(VectorSpace v, s ~ Scalar v, Fractional s) =>
v -> s -> v
^/s''
rxy
                   | Bool
otherwise  = (s''
1,s''
0)
           𝐞φ :: V3 s''
𝐞φ = s'' -> s'' -> s'' -> V3 s''
forall a. a -> a -> a -> V3 a
V3 (-s''
sφ) s''
cφ s''
0
           𝐞θ :: V3 s''
𝐞θ = s'' -> s'' -> s'' -> V3 s''
forall a. a -> a -> a -> V3 a
V3 (s''
cθs'' -> s'' -> s''
forall a. Num a => a -> a -> a
*s''
cφ) (s''
cθs'' -> s'' -> s''
forall a. Num a => a -> a -> a
*s''
sφ) (-s''
sθ)
           δθ :: Scalar (V3 s'')
δθ = V3 s''
𝐞θ V3 s'' -> V3 s'' -> Scalar (V3 s'')
forall v. InnerSpace v => v -> v -> Scalar v
<.> V3 s''
V3 s'''
𝐯r
           δφ :: Scalar (V3 s'')
δφ = V3 s''
𝐞φ V3 s'' -> V3 s'' -> Scalar (V3 s'')
forall v. InnerSpace v => v -> v -> Scalar v
<.> V3 s''
V3 s'''
𝐯r
           γ :: s''
γ = s'' -> s'' -> s''
forall a. RealFloat a => a -> a -> a
atan2 s''
Scalar (V3 s'')
δφ s''
Scalar (V3 s'')
δθ
           γc :: s''
γc | s''
θ s'' -> s'' -> Bool
forall a. Ord a => a -> a -> Bool
< s''
forall a. Floating a => a
pis'' -> s'' -> s''
forall a. Fractional a => a -> a -> a
/s''
2   = s''
γ s'' -> s'' -> s''
forall a. Num a => a -> a -> a
+ s''
φ
              | Bool
otherwise  = s''
γ s'' -> s'' -> s''
forall a. Num a => a -> a -> a
- s''
φ


-- | @ex -> ey@, @ey -> ez@, @ez -> ex@
transformEmbeddedTangents
    :: ∀ x f v . ( NaturallyEmbedded (FibreBundle x f) (FibreBundle v v) )
           => (v -> v) -> FibreBundle x f -> FibreBundle x f
transformEmbeddedTangents :: (v -> v) -> FibreBundle x f -> FibreBundle x f
transformEmbeddedTangents v -> v
f FibreBundle x f
p = case FibreBundle x f -> FibreBundle v v
forall m v. NaturallyEmbedded m v => m -> v
embed FibreBundle x f
p :: FibreBundle v v of
    FibreBundle v
v v
δv -> FibreBundle v v -> FibreBundle x f
forall m v. NaturallyEmbedded m v => v -> m
coEmbed (v -> v -> FibreBundle v v
forall b f. b -> f -> FibreBundle b f
FibreBundle (v -> v
f v
v) (v -> v
f v
δv) :: FibreBundle v v)


instance (s~ℝ, s'~ℝ) => Rotatable (FibreBundle (S²_ s) (V2 s')) where
  type AxisSpace (FibreBundle (S²_ s) (V2 s')) = ℝP²_ s
  rotateAbout :: AxisSpace (FibreBundle (S²_ s) (V2 s'))
-> S¹ -> FibreBundle (S²_ s) (V2 s') -> FibreBundle (S²_ s) (V2 s')
rotateAbout AxisSpace (FibreBundle (S²_ s) (V2 s'))
axis S¹
angle = (ℝ³ -> ℝ³)
-> FibreBundle (S²_ s) (V2 s') -> FibreBundle (S²_ s) (V2 s')
forall x f v.
NaturallyEmbedded (FibreBundle x f) (FibreBundle v v) =>
(v -> v) -> FibreBundle x f -> FibreBundle x f
transformEmbeddedTangents
        ((ℝ³ -> ℝ³)
 -> FibreBundle (S²_ s) (V2 s') -> FibreBundle (S²_ s) (V2 s'))
-> (ℝ³ -> ℝ³)
-> FibreBundle (S²_ s) (V2 s')
-> FibreBundle (S²_ s) (V2 s')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ℝP² -> S¹ -> ℝ³ -> ℝ³
rotateℝ³AboutCenteredAxis ℝP²
AxisSpace (FibreBundle (S²_ s) (V2 s'))
axis S¹
angle