Isometries between hyperbolic metrics #
This file specializes the generic RiemannianIsometry API to bundled hyperbolic metrics, with
each metric supplying its own Riemannian bundle instance.
@[reducible, inline]
abbrev
TauCeti.HyperbolicMetric.Isometry
{E : Type uE}
{H : Type uH}
{M : Type uM}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[T3Space M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[PreconnectedSpace M]
(g g' : HyperbolicMetric)
:
Type uM
A bundled hyperbolic-metric comparison represented by the generic Riemannian isometry API.