Conformal Linear Maps #
A continuous linear map between R-normed spaces X and Y IsConformalMap if it is
a nonzero multiple of a linear isometry.
Main definitions #
IsConformalMap: the main definition of conformal linear maps
Main results #
- The conformality of the composition of two conformal linear maps, the identity map and multiplications by nonzero constants as continuous linear maps
isConformalMap_of_subsingleton: all continuous linear maps on singleton spaces are conformal
See Analysis.InnerProductSpace.ConformalLinearMap for
isConformalMap_iff: a map between inner product spaces is conformal iff it preserves inner products up to a fixed scalar factor.
Tags #
conformal
Warning #
The definition of conformality in this file does NOT require the maps to be orientation-preserving.
def
IsConformalMap
{R : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[NormedField R]
[SeminormedAddCommGroup X]
[SeminormedAddCommGroup Y]
[NormedSpace R X]
[NormedSpace R Y]
(f' : X →L[R] Y)
:
A continuous linear map f' is said to be conformal if it's
a nonzero multiple of a linear isometry.
Equations
- IsConformalMap f' = ∃ (c : R), c ≠ 0 ∧ ∃ (li : X →ₗᵢ[R] Y), f' = c • LinearIsometry.toContinuousLinearMap li
Instances For
theorem
isConformalMap_id
{R : Type u_1}
{M : Type u_2}
[NormedField R]
[SeminormedAddCommGroup M]
[NormedSpace R M]
:
theorem
IsConformalMap.smul
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[NormedField R]
[SeminormedAddCommGroup M]
[SeminormedAddCommGroup N]
[NormedSpace R M]
[NormedSpace R N]
{f : M →L[R] N}
(hf : IsConformalMap f)
{c : R}
(hc : c ≠ 0)
:
IsConformalMap (c • f)
theorem
isConformalMap_const_smul
{R : Type u_1}
{M : Type u_2}
[NormedField R]
[SeminormedAddCommGroup M]
[NormedSpace R M]
{c : R}
(hc : c ≠ 0)
:
IsConformalMap (c • ContinuousLinearMap.id R M)
theorem
LinearIsometry.isConformalMap
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[NormedField R]
[SeminormedAddCommGroup M]
[SeminormedAddCommGroup N]
[NormedSpace R M]
[NormedSpace R N]
(f' : M →ₗᵢ[R] N)
:
theorem
isConformalMap_of_subsingleton
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[NormedField R]
[SeminormedAddCommGroup M]
[SeminormedAddCommGroup N]
[NormedSpace R M]
[NormedSpace R N]
[Subsingleton M]
(f' : M →L[R] N)
:
theorem
IsConformalMap.comp
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{G : Type u_4}
[NormedField R]
[SeminormedAddCommGroup M]
[SeminormedAddCommGroup N]
[SeminormedAddCommGroup G]
[NormedSpace R M]
[NormedSpace R N]
[NormedSpace R G]
{f : M →L[R] N}
{g : N →L[R] G}
(hg : IsConformalMap g)
(hf : IsConformalMap f)
:
theorem
IsConformalMap.injective
{R : Type u_1}
{N : Type u_3}
{M' : Type u_5}
[NormedField R]
[SeminormedAddCommGroup N]
[NormedSpace R N]
[NormedAddCommGroup M']
[NormedSpace R M']
{f : M' →L[R] N}
(h : IsConformalMap f)
:
theorem
IsConformalMap.ne_zero
{R : Type u_1}
{N : Type u_3}
{M' : Type u_5}
[NormedField R]
[SeminormedAddCommGroup N]
[NormedSpace R N]
[NormedAddCommGroup M']
[NormedSpace R M']
[Nontrivial M']
{f' : M' →L[R] N}
(hf' : IsConformalMap f')
:
f' ≠ 0