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) : Prop

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 • li.toContinuousLinearMap

theorem isConformalMap_id {R : Type u_1} {M : Type u_2} [NormedField R] [SeminormedAddCommGroup M] [NormedSpace R M] : IsConformalMap (ContinuousLinearMap.id 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) : IsConformalMap f'.toContinuousLinearMap

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) : IsConformalMap f'

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) : IsConformalMap (g.comp 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) : Function.Injective ⇑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