{-# 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 :: forall m. m -> Needle m -> FibreBundle m (Needle m)
$mTangentBundle :: forall {r} {m}.
FibreBundle m (Needle m)
-> (m -> Needle m -> r) -> ((# #) -> r) -> r
TangentBundle p v = FibreBundle p v
infixr 5 :@.
pattern (:@.) :: f -> m -> FibreBundle m f
pattern f $b:@. :: forall f m. f -> m -> FibreBundle m f
$m:@. :: forall {r} {f} {m}.
FibreBundle m f -> (f -> m -> r) -> ((# #) -> r) -> r
:@. p = FibreBundle p f
tangentAt :: (AdditiveGroup (Needle m)) => m -> TangentBundle m
tangentAt :: forall m. AdditiveGroup (Needle m) => m -> TangentBundle m
tangentAt m
p = forall v. AdditiveGroup v => v
zeroV 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 = 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 = 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, ( forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport m
p Needle m
v
, forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport m
q forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ m
pforall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~!m
q ))
where q :: m
q = m
pforall 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 (forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
(PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness)) -> 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 (forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
(PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness))
-> 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
_ = 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 (forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
(PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness)) -> 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 (forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
(PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness))
-> 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
_ = 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 (forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
(PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness)) -> 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 (forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
(PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness))
-> forall m f (k :: * -> * -> *).
ParallelTransporting (->) m f =>
ForgetTransportProperties k m f
ForgetTransportProperties
parallelTransport :: m -> Needle m -> ZeroDim s -> ZeroDim s
parallelTransport m
_ Needle m
_ = 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 ℝ
_ = 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 ℝ²
_ = 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 ℝ³
_ = 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 ℝ⁴
_ = 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¹
_ = 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 = (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 (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd) (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 forall a. Ord a => a -> a -> Bool
< forall a. Floating a => a
pi = (forall r. r -> r -> S²_ r
S²Polar ℝ
θ₁ ℝ
φ₁, (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, 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 forall a. Ord a => a -> a -> Bool
< ℝ
2forall a. Num a => a -> a -> a
*forall a. Floating a => a
pi = forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> (m, (k f f, k f f))
translateAndInvblyParTransport (forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ ℝ
φ₀)
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
^*(-(ℝ
2forall a. Num a => a -> a -> a
*forall a. Floating a => a
piforall a. Num a => a -> a -> a
-ℝ
d)forall a. Fractional a => a -> a -> a
/ℝ
d)
| Bool
otherwise = forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> (m, (k f f, k f f))
translateAndInvblyParTransport (forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ ℝ
φ₀)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ let revolutions :: Integer
revolutions = forall a b. (RealFrac a, Integral b) => a -> b
floor forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ℝ
dforall a. Fractional a => a -> a -> a
/(ℝ
2forall 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
- ℝ
2forall a. Num a => a -> a -> a
*forall a. Floating a => a
piforall a. Num a => a -> a -> a
*forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
revolutions)forall a. Fractional a => a -> a -> a
/ℝ
d)
where
S¹Polar ℝ
γc₀ = forall m v. NaturallyEmbedded m v => v -> m
coEmbed Needle S²
𝐯
γ₀ :: ℝ
γ₀ | ℝ
θ₀ forall a. Ord a => a -> a -> Bool
< forall a. Floating a => a
piforall 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 ℝ
φ₁ = forall r. r -> S¹_ r
S¹Polar ℝ
φ₀ forall x. Semimanifold x => x -> Needle x -> x
.+~^ ℝ
δφ
V3 ℝ
bx ℝ
by ℝ
bz = forall m v. NaturallyEmbedded m v => m -> v
embed forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ 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 ℝ
θ₀
(ℝ
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 ℝ
θ₁ ℝ
δφ = forall m v. NaturallyEmbedded m v => v -> m
coEmbed 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θ₀forall a. Ord a => a -> a -> Bool
<=ℝ
sθ₁ = let
V3 ℝ
nbx ℝ
nby ℝ
nbz = forall m v. NaturallyEmbedded m v => m -> v
embed forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ (forall a. Floating a => a
piforall 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
(ℝ
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
V3 ℝ
gx ℝ
gy ℝ
gz = forall m v. NaturallyEmbedded m v => m -> v
embed forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ (-ℝ
δφ)
(ℝ
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₁ | ℝ
θ₁ forall a. Ord a => a -> a -> Bool
< forall a. Floating a => a
piforall 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 = forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap (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 = forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap (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
( forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness a
, forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness b
, forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness fa
, forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness fb
, forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
TransportOnNeedleWitness k m f
transportOnNeedleWitness :: TransportOnNeedleWitness k a fa
, 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)
-> 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
( forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties :: ForgetTransportProperties k a fa
, 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) -> 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) (Needle a
va,Needle b
vb)
= forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport a
pa Needle a
va 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')
*** 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
( forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness a
, forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness f
, forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness g
, forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
TransportOnNeedleWitness k m f
transportOnNeedleWitness :: TransportOnNeedleWitness k a f
, 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)
-> 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
( forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties :: ForgetTransportProperties k a f
, 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) -> 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
= forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport a
p Needle a
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')
*** 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 = forall b f. b -> f -> FibreBundle b f
FibreBundle forall v. AdditiveGroup v => v
zeroV 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 = forall b f. b -> f -> FibreBundle b f
FibreBundle (m
pforall v. AdditiveGroup v => v -> v -> v
^+^m
q) (f
vforall v. AdditiveGroup v => v -> v -> v
^+^f
w)
negateV :: FibreBundle m f -> FibreBundle m f
negateV (FibreBundle m
p f
v) = forall b f. b -> f -> FibreBundle b f
FibreBundle (forall v. AdditiveGroup v => v -> v
negateV m
p) (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 ( forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness :: SemimanifoldWitness m
, forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness :: SemimanifoldWitness 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)
-> 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 Needle m
v Needle f
δf
= forall b f. b -> f -> FibreBundle b f
FibreBundle (m
pforall x. Semimanifold x => x -> Needle x -> x
.+~^Needle m
v) (forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport m
p Needle m
v f
fforall 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 ( forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m
, forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness 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)
-> forall x.
PseudoAffine (Needle x) =>
SemimanifoldWitness x -> PseudoAffineWitness x
PseudoAffineWitness (forall x.
(Semimanifold (Needle x), Needle (Needle x) ~ Needle x) =>
SemimanifoldWitness x
SemimanifoldWitness)
FibreBundle m
p f
f .-~! :: HasCallStack =>
FibreBundle m f -> FibreBundle m f -> Needle (FibreBundle m f)
.-~! FibreBundle m
q f
g = case m
pforall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~!m
q of
Needle m
v -> forall b f. b -> f -> FibreBundle b f
FibreBundle Needle m
v forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ f
f forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~! 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
pforall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~.m
q of
Maybe (Needle m)
Nothing -> forall a. Maybe a
Nothing
Just Needle m
v -> forall b f. b -> f -> FibreBundle b f
FibreBundle Needle m
v forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> f
f forall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~. 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 = forall b f. b -> f -> FibreBundle b f
FibreBundle x
x 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) = forall b f. b -> f -> FibreBundle b f
FibreBundle (forall m v. NaturallyEmbedded m v => m -> v
embed m
x) forall v. AdditiveGroup v => v
zeroV
coEmbed :: FibreBundle v f -> FibreBundle m (ZeroDim s)
coEmbed (FibreBundle v
u f
_) = forall b f. b -> f -> FibreBundle b f
FibreBundle (forall m v. NaturallyEmbedded m v => v -> m
coEmbed v
u) 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) = forall b f. b -> f -> FibreBundle b f
FibreBundle (x
x,forall v. AdditiveGroup v => v
zeroV) (f
δx,forall v. AdditiveGroup v => v
zeroV)
coEmbed :: FibreBundle (x, y) (f, g) -> FibreBundle x f
coEmbed (FibreBundle (x
x,y
_) (f
δx,g
_)) = 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) = forall b f. b -> f -> FibreBundle b f
FibreBundle ℝ
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m v. NaturallyEmbedded m v => m -> v
embed v
v
coEmbed :: FibreBundle ℝ w -> FibreBundle ℝ v
coEmbed (FibreBundle ℝ
p w
w) = forall b f. b -> f -> FibreBundle b f
FibreBundle ℝ
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ 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) = forall b f. b -> f -> FibreBundle b f
FibreBundle V2 s
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ 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) = forall b f. b -> f -> FibreBundle b f
FibreBundle V2 s'
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ 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) = forall b f. b -> f -> FibreBundle b f
FibreBundle V3 s
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ 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) = forall b f. b -> f -> FibreBundle b f
FibreBundle V3 s'
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ 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) = forall b f. b -> f -> FibreBundle b f
FibreBundle V4 s
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ 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) = forall b f. b -> f -> FibreBundle b f
FibreBundle V4 s'
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ 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) = forall b f. b -> f -> FibreBundle b f
FibreBundle (forall a. a -> a -> V2 a
V2 s'''
cφ s'''
sφ) forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s'
lforall v. VectorSpace v => Scalar v -> v -> v
*^(forall a. a -> a -> V2 a
V2 (-s'''
sφ) s'''
cφ)
where (s'''
cφ, s'''
sφ) = (forall a. Floating a => a -> a
cos 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
sin) s
φ
coEmbed :: FibreBundle (V2 s'') (V2 s''') -> FibreBundle (S¹_ s) s'
coEmbed (FibreBundle (V2 s''
0 s''
0) (V2 s'''
_ s'''
δy)) = forall b f. b -> f -> FibreBundle b f
FibreBundle (forall r. r -> S¹_ r
S¹Polar s
0) s'''
δy
coEmbed (FibreBundle V2 s''
p (V2 s'''
δx s'''
δy)) = forall b f. b -> f -> FibreBundle b f
FibreBundle (forall r. r -> S¹_ r
S¹Polar forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a. RealFloat a => a -> a -> a
atan2 s''
sφ s''
cφ) forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s''
cφforall a. Num a => a -> a -> a
*s'''
δy forall a. Num a => a -> a -> a
- s''
sφforall a. Num a => a -> a -> a
*s'''
δx
where V2 s''
cφ s''
sφ = V2 s''
pforall v s.
(VectorSpace v, s ~ Scalar v, Fractional s) =>
v -> s -> v
^/s'''
r
r :: s'''
r = 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'
δυ))
= forall b f. b -> f -> FibreBundle b f
FibreBundle (forall a. a -> a -> a -> V3 a
V3 (s''
sθforall a. Num a => a -> a -> a
*s''
cφ) (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φ] = forall m v. NaturallyEmbedded m v => m -> v
embed 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 r. r -> S¹_ r
S¹Polar 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 = forall m v. NaturallyEmbedded m v => v -> m
coEmbed V2 s'
v
γ :: s
γ | s
θ forall a. Ord a => a -> a -> Bool
< forall a. Floating a => a
piforall a. Fractional a => a -> a -> a
/s
2 = s
γc forall a. Num a => a -> a -> a
- s
φ
| Bool
otherwise = s
γc forall a. Num a => a -> a -> a
+ s
φ
d :: s'''
d = forall v s. (InnerSpace v, s ~ Scalar v, Floating s) => v -> s
magnitude V2 s'
v
V2 s'''
δθ s'''
δφ = s'''
d forall v. VectorSpace v => Scalar v -> v -> v
*^ forall m v. NaturallyEmbedded m v => m -> v
embed (forall r. r -> S¹_ r
S¹Polar s
γ)
𝐞φ :: V3 s''
𝐞φ = forall a. a -> a -> a -> V3 a
V3 (-s''
sφ) s''
cφ s''
0
𝐞θ :: V3 s''
𝐞θ = forall a. a -> a -> a -> V3 a
V3 (s''
cθforall a. Num a => a -> a -> a
*s''
cφ) (s''
cθforall a. Num a => a -> a -> a
*s''
sφ) (-s''
sθ)
𝐯r :: V3 s''
𝐯r = s'''
δθforall v. VectorSpace v => Scalar v -> v -> v
*^V3 s''
𝐞θ forall v. AdditiveGroup v => v -> v -> v
^+^ 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 forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of
ClosedScalarWitness s
ClosedScalarWitness -> forall b f. b -> f -> FibreBundle b f
FibreBundle (forall r. r -> r -> S²_ r
S²Polar s''
θ s''
φ) (forall v s. (InnerSpace v, s ~ Scalar v, Floating s) => v -> s
magnitude (Scalar (V3 s'')
δθ,Scalar (V3 s'')
δφ) forall v. VectorSpace v => Scalar v -> v -> v
*^ forall m v. NaturallyEmbedded m v => m -> v
embed (forall r. r -> S¹_ r
S¹Polar s''
γc))
where r :: s''
r = forall a. Floating a => a -> a
sqrt forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s''
xforall a. Num a => a -> Int -> a
^Int
2 forall a. Num a => a -> a -> a
+ s''
yforall a. Num a => a -> Int -> a
^Int
2 forall a. Num a => a -> a -> a
+ s''
zforall a. Num a => a -> Int -> a
^Int
2
rxy :: s''
rxy = forall a. Floating a => a -> a
sqrt forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s''
xforall a. Num a => a -> Int -> a
^Int
2 forall a. Num a => a -> a -> a
+ s''
yforall a. Num a => a -> Int -> a
^Int
2
θ :: s''
θ = forall a. RealFloat a => a -> a -> a
atan2 s''
rxy s''
z
φ :: s''
φ = forall a. RealFloat a => a -> a -> a
atan2 s''
y s''
x
cθ :: s''
cθ = s''
z forall a. Fractional a => a -> a -> a
/ s''
r
sθ :: s''
sθ = s''
rxy forall a. Fractional a => a -> a -> a
/ s''
r
(s''
cφ,s''
sφ) | s''
rxyforall a. Ord a => a -> a -> Bool
>s''
0 = (s''
x,s''
y)forall v s.
(VectorSpace v, s ~ Scalar v, Fractional s) =>
v -> s -> v
^/s''
rxy
| Bool
otherwise = (s''
1,s''
0)
𝐞φ :: V3 s''
𝐞φ = forall a. a -> a -> a -> V3 a
V3 (-s''
sφ) s''
cφ s''
0
𝐞θ :: V3 s''
𝐞θ = forall a. a -> a -> a -> V3 a
V3 (s''
cθforall a. Num a => a -> a -> a
*s''
cφ) (s''
cθforall a. Num a => a -> a -> a
*s''
sφ) (-s''
sθ)
δθ :: Scalar (V3 s'')
δθ = V3 s''
𝐞θ forall v. InnerSpace v => v -> v -> Scalar v
<.> V3 s'''
𝐯r
δφ :: Scalar (V3 s'')
δφ = V3 s''
𝐞φ forall v. InnerSpace v => v -> v -> Scalar v
<.> V3 s'''
𝐯r
γ :: s''
γ = forall a. RealFloat a => a -> a -> a
atan2 Scalar (V3 s'')
δφ Scalar (V3 s'')
δθ
γc :: s''
γc | s''
θ forall a. Ord a => a -> a -> Bool
< forall a. Floating a => a
piforall a. Fractional a => a -> a -> a
/s''
2 = s''
γ forall a. Num a => a -> a -> a
+ s''
φ
| Bool
otherwise = s''
γ forall a. Num a => a -> a -> a
- s''
φ
transformEmbeddedTangents
:: ∀ x f v . ( NaturallyEmbedded (FibreBundle x f) (FibreBundle v v) )
=> (v -> v) -> FibreBundle x f -> FibreBundle x f
transformEmbeddedTangents :: forall x f v.
NaturallyEmbedded (FibreBundle x f) (FibreBundle v v) =>
(v -> v) -> FibreBundle x f -> FibreBundle x f
transformEmbeddedTangents v -> v
f FibreBundle x f
p = case forall m v. NaturallyEmbedded m v => m -> v
embed FibreBundle x f
p :: FibreBundle v v of
FibreBundle v
v v
δv -> forall m v. NaturallyEmbedded m v => v -> m
coEmbed (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 = forall x f v.
NaturallyEmbedded (FibreBundle x f) (FibreBundle v v) =>
(v -> v) -> FibreBundle x f -> FibreBundle x f
transformEmbeddedTangents
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ℝP² -> S¹ -> ℝ³ -> ℝ³
rotateℝ³AboutCenteredAxis AxisSpace (FibreBundle (S²_ s) (V2 s'))
axis S¹
angle