# Oriented two-dimensional real inner product spaces #

This file defines constructions specific to the geometry of an oriented two-dimensional real inner product space E.

## Main declarations #

• Orientation.areaForm: an antisymmetric bilinear form E →ₗ[ℝ] E →ₗ[ℝ] ℝ (usual notation ω). Morally, when ω is evaluated on two vectors, it gives the oriented area of the parallelogram they span. (But mathlib does not yet have a construction of oriented area, and in fact the construction of oriented area should pass through ω.)

• Orientation.rightAngleRotation: an isometric automorphism E ≃ₗᵢ[ℝ] E (usual notation J). This automorphism squares to -1. In a later file, rotations (Orientation.rotation) are defined, in such a way that this automorphism is equal to rotation by 90 degrees.

• Orientation.basisRightAngleRotation: for a nonzero vector x in E, the basis ![x, J x] for E.

• Orientation.kahler: a complex-valued real-bilinear map E →ₗ[ℝ] E →ₗ[ℝ] ℂ. Its real part is the inner product and its imaginary part is Orientation.areaForm. For vectors x and y in E, the complex number o.kahler x y has modulus ‖x‖ * ‖y‖. In a later file, oriented angles (Orientation.oangle) are defined, in such a way that the argument of o.kahler x y is the oriented angle from x to y.

## Main results #

• Orientation.rightAngleRotation_rightAngleRotation: the identity J (J x) = - x

• Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay: x, y are in the same ray, if and only if 0 ≤ ⟪x, y⟫ and ω x y = 0

• Orientation.kahler_mul: the identity o.kahler x a * o.kahler a y = ‖a‖ ^ 2 * o.kahler x y

• Complex.areaForm, Complex.rightAngleRotation, Complex.kahler: the concrete interpretations of areaForm, rightAngleRotation, kahler for the oriented real inner product space ℂ

• Orientation.areaForm_map_complex, Orientation.rightAngleRotation_map_complex, Orientation.kahler_map_complex: given an orientation-preserving isometry from E to ℂ, expressions for areaForm, rightAngleRotation, kahler as the pullback of their concrete interpretations on ℂ

## Implementation notes #

Notation ω for Orientation.areaForm and J for Orientation.rightAngleRotation should be defined locally in each file which uses them, since otherwise one would need a more cumbersome notation which mentions the orientation explicitly (something like ω[o]). Write

local notation "ω" => o.areaForm
local notation "J" => o.rightAngleRotation

theorem FiniteDimensional.of_fact_finrank_eq_two {K : Type u_1} {V : Type u_2} [] [] [Module K V] [Fact ()] :
@[deprecated FiniteDimensional.of_fact_finrank_eq_two]
theorem FiniteDimensional.finiteDimensional_of_fact_finrank_eq_two {K : Type u_1} {V : Type u_2} [] [] [Module K V] [Fact ()] :

Alias of FiniteDimensional.of_fact_finrank_eq_two.

theorem Orientation.areaForm_def {E : Type u_2} [] [Fact ()] (o : Orientation E (Fin 2)) :
o.areaForm = let z := AlternatingMap.constLinearEquivOfIsEmpty.symm; let y := (LinearMap.llcomp E () ) z ∘ₗ AlternatingMap.curryLeftLinearMap; y ∘ₗ AlternatingMap.curryLeftLinearMap o.volumeForm
@[irreducible]
def Orientation.areaForm {E : Type u_2} [] [Fact ()] (o : Orientation E (Fin 2)) :

An antisymmetric bilinear form on an oriented real inner product space of dimension 2 (usual notation ω). When evaluated on two vectors, it gives the oriented area of the parallelogram they span.

Equations
Instances For
theorem Orientation.areaForm_to_volumeForm {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.areaForm x) y = o.volumeForm ![x, y]
@[simp]
theorem Orientation.areaForm_apply_self {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) :
(o.areaForm x) x = 0
theorem Orientation.areaForm_swap {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.areaForm x) y = -(o.areaForm y) x
@[simp]
theorem Orientation.areaForm_neg_orientation {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) :
(-o).areaForm = -o.areaForm
def Orientation.areaForm' {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) :

Continuous linear map version of Orientation.areaForm, useful for calculus.

Equations
• o.areaForm' = LinearMap.toContinuousLinearMap (LinearMap.toContinuousLinearMap ∘ₗ o.areaForm)
Instances For
@[simp]
theorem Orientation.areaForm'_apply {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) :
o.areaForm' x = LinearMap.toContinuousLinearMap (o.areaForm x)
theorem Orientation.abs_areaForm_le {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
|(o.areaForm x) y| x * y
theorem Orientation.areaForm_le {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.areaForm x) y x * y
theorem Orientation.abs_areaForm_of_orthogonal {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) {x : E} {y : E} (h : x, y⟫_ = 0) :
|(o.areaForm x) y| = x * y
theorem Orientation.areaForm_map {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) {F : Type u_2} [] [hF : Fact ()] (φ : E ≃ₗᵢ[] F) (x : F) (y : F) :
(((Orientation.map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = (o.areaForm (φ.symm x)) (φ.symm y)
theorem Orientation.areaForm_comp_linearIsometryEquiv {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (φ : E ≃ₗᵢ[] E) (hφ : 0 < LinearMap.det φ.toLinearEquiv) (x : E) (y : E) :
(o.areaForm (φ x)) (φ y) = (o.areaForm x) y

The area form is invariant under pullback by a positively-oriented isometric automorphism.

theorem Orientation.rightAngleRotationAux₁_def {E : Type u_2} [] [Fact ()] (o : Orientation E (Fin 2)) :
o.rightAngleRotationAux₁ = let to_dual := .toLinearEquiv ≪≫ₗ LinearMap.toContinuousLinearMap.symm; to_dual.symm ∘ₗ o.areaForm
@[irreducible]

Auxiliary construction for Orientation.rightAngleRotation, rotation by 90 degrees in an oriented real inner product space of dimension 2.

Equations
Instances For
@[simp]
theorem Orientation.inner_rightAngleRotationAux₁_left {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
o.rightAngleRotationAux₁ x, y⟫_ = (o.areaForm x) y
@[simp]
theorem Orientation.inner_rightAngleRotationAux₁_right {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
x, o.rightAngleRotationAux₁ y⟫_ = -(o.areaForm x) y

Auxiliary construction for Orientation.rightAngleRotation, rotation by 90 degrees in an oriented real inner product space of dimension 2.

Equations
• o.rightAngleRotationAux₂ = let __src := o.rightAngleRotationAux₁; { toLinearMap := __src, norm_map' := }
Instances For
@[simp]
theorem Orientation.rightAngleRotationAux₁_rightAngleRotationAux₁ {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) :
o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x) = -x
@[irreducible]

An isometric automorphism of an oriented real inner product space of dimension 2 (usual notation J). This automorphism squares to -1. We will define rotations in such a way that this automorphism is equal to rotation by 90 degrees.

Equations
Instances For
theorem Orientation.rightAngleRotation_def {E : Type u_2} [] [Fact ()] (o : Orientation E (Fin 2)) :
o.rightAngleRotation = LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁)
@[simp]
theorem Orientation.inner_rightAngleRotation_left {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
o.rightAngleRotation x, y⟫_ = (o.areaForm x) y
@[simp]
theorem Orientation.inner_rightAngleRotation_right {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
x, o.rightAngleRotation y⟫_ = -(o.areaForm x) y
@[simp]
theorem Orientation.rightAngleRotation_rightAngleRotation {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) :
o.rightAngleRotation (o.rightAngleRotation x) = -x
@[simp]
theorem Orientation.rightAngleRotation_symm {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) :
o.rightAngleRotation.symm = o.rightAngleRotation.trans
theorem Orientation.inner_rightAngleRotation_self {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) :
o.rightAngleRotation x, x⟫_ = 0
theorem Orientation.inner_rightAngleRotation_swap {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
x, o.rightAngleRotation y⟫_ = -o.rightAngleRotation x, y⟫_
theorem Orientation.inner_rightAngleRotation_swap' {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
o.rightAngleRotation x, y⟫_ = -x, o.rightAngleRotation y⟫_
theorem Orientation.inner_comp_rightAngleRotation {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
o.rightAngleRotation x, o.rightAngleRotation y⟫_ = x, y⟫_
@[simp]
theorem Orientation.areaForm_rightAngleRotation_left {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.areaForm (o.rightAngleRotation x)) y = -x, y⟫_
@[simp]
theorem Orientation.areaForm_rightAngleRotation_right {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.areaForm x) (o.rightAngleRotation y) = x, y⟫_
theorem Orientation.areaForm_comp_rightAngleRotation {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.areaForm (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.areaForm x) y
@[simp]
theorem Orientation.rightAngleRotation_trans_rightAngleRotation {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) :
o.rightAngleRotation.trans o.rightAngleRotation =
theorem Orientation.rightAngleRotation_neg_orientation {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) :
(-o).rightAngleRotation x = -o.rightAngleRotation x
@[simp]
theorem Orientation.rightAngleRotation_trans_neg_orientation {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) :
(-o).rightAngleRotation = o.rightAngleRotation.trans
theorem Orientation.rightAngleRotation_map {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) {F : Type u_2} [] [hF : Fact ()] (φ : E ≃ₗᵢ[] F) (x : F) :
((Orientation.map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation x = φ (o.rightAngleRotation (φ.symm x))
theorem Orientation.linearIsometryEquiv_comp_rightAngleRotation {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (φ : E ≃ₗᵢ[] E) (hφ : 0 < LinearMap.det φ.toLinearEquiv) (x : E) :
φ (o.rightAngleRotation x) = o.rightAngleRotation (φ x)

J commutes with any positively-oriented isometric automorphism.

theorem Orientation.rightAngleRotation_map' {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) {F : Type u_2} [] [Fact ()] (φ : E ≃ₗᵢ[] F) :
((Orientation.map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation = (φ.symm.trans o.rightAngleRotation).trans φ
theorem Orientation.linearIsometryEquiv_comp_rightAngleRotation' {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (φ : E ≃ₗᵢ[] E) (hφ : 0 < LinearMap.det φ.toLinearEquiv) :
o.rightAngleRotation.trans φ = φ.trans o.rightAngleRotation

J commutes with any positively-oriented isometric automorphism.

def Orientation.basisRightAngleRotation {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (hx : x 0) :
Basis (Fin 2) E

For a nonzero vector x in an oriented two-dimensional real inner product space E, ![x, J x] forms an (orthogonal) basis for E.

Equations
• o.basisRightAngleRotation x hx =
Instances For
@[simp]
theorem Orientation.coe_basisRightAngleRotation {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (hx : x 0) :
(o.basisRightAngleRotation x hx) = ![x, o.rightAngleRotation x]
theorem Orientation.inner_mul_inner_add_areaForm_mul_areaForm' {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (a : E) (x : E) :
a, x⟫_ () a + (o.areaForm a) x o.areaForm a = a ^ 2 () x

For vectors a x y : E, the identity ⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫. (See Orientation.inner_mul_inner_add_areaForm_mul_areaForm for the "applied" form.)

theorem Orientation.inner_mul_inner_add_areaForm_mul_areaForm {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (a : E) (x : E) (y : E) :
a, x⟫_ * a, y⟫_ + (o.areaForm a) x * (o.areaForm a) y = a ^ 2 * x, y⟫_

For vectors a x y : E, the identity ⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫.

theorem Orientation.inner_sq_add_areaForm_sq {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (a : E) (b : E) :
a, b⟫_ ^ 2 + (o.areaForm a) b ^ 2 = a ^ 2 * b ^ 2
theorem Orientation.inner_mul_areaForm_sub' {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (a : E) (x : E) :
a, x⟫_ o.areaForm a - (o.areaForm a) x () a = a ^ 2 o.areaForm x

For vectors a x y : E, the identity ⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y. (See Orientation.inner_mul_areaForm_sub for the "applied" form.)

theorem Orientation.inner_mul_areaForm_sub {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (a : E) (x : E) (y : E) :
a, x⟫_ * (o.areaForm a) y - (o.areaForm a) x * a, y⟫_ = a ^ 2 * (o.areaForm x) y

For vectors a x y : E, the identity ⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y.

theorem Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
0 x, y⟫_ (o.areaForm x) y = 0 SameRay x y
def Orientation.kahler {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) :

A complex-valued real-bilinear map on an oriented real inner product space of dimension 2. Its real part is the inner product and its imaginary part is Orientation.areaForm.

On ℂ with the standard orientation, kahler w z = conj w * z; see Complex.kahler.

Equations
• o.kahler = ∘ₗ + () (.flip Complex.I) ∘ₗ o.areaForm
Instances For
theorem Orientation.kahler_apply_apply {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.kahler x) y = x, y⟫_ + (o.areaForm x) y Complex.I
theorem Orientation.kahler_swap {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.kahler x) y = () ((o.kahler y) x)
@[simp]
theorem Orientation.kahler_apply_self {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) :
(o.kahler x) x = x ^ 2
@[simp]
theorem Orientation.kahler_rightAngleRotation_left {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.kahler (o.rightAngleRotation x)) y = * (o.kahler x) y
@[simp]
theorem Orientation.kahler_rightAngleRotation_right {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.kahler x) (o.rightAngleRotation y) = Complex.I * (o.kahler x) y
theorem Orientation.kahler_comp_rightAngleRotation {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.kahler (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.kahler x) y
theorem Orientation.kahler_comp_rightAngleRotation' {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
-(Complex.I * (Complex.I * (o.kahler x) y)) = (o.kahler x) y
@[simp]
theorem Orientation.kahler_neg_orientation {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
((-o).kahler x) y = () ((o.kahler x) y)
theorem Orientation.kahler_mul {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (a : E) (x : E) (y : E) :
(o.kahler x) a * (o.kahler a) y = a ^ 2 * (o.kahler x) y
theorem Orientation.normSq_kahler {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
Complex.normSq ((o.kahler x) y) = x ^ 2 * y ^ 2
theorem Orientation.abs_kahler {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
Complex.abs ((o.kahler x) y) = x * y
theorem Orientation.norm_kahler {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.kahler x) y = x * y
theorem Orientation.eq_zero_or_eq_zero_of_kahler_eq_zero {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) {x : E} {y : E} (hx : (o.kahler x) y = 0) :
x = 0 y = 0
theorem Orientation.kahler_eq_zero_iff {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.kahler x) y = 0 x = 0 y = 0
theorem Orientation.kahler_ne_zero {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) {x : E} {y : E} (hx : x 0) (hy : y 0) :
(o.kahler x) y 0
theorem Orientation.kahler_ne_zero_iff {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (x : E) (y : E) :
(o.kahler x) y 0 x 0 y 0
theorem Orientation.kahler_map {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) {F : Type u_2} [] [hF : Fact ()] (φ : E ≃ₗᵢ[] F) (x : F) (y : F) :
(((Orientation.map (Fin 2) φ.toLinearEquiv) o).kahler x) y = (o.kahler (φ.symm x)) (φ.symm y)
theorem Orientation.kahler_comp_linearIsometryEquiv {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (φ : E ≃ₗᵢ[] E) (hφ : 0 < LinearMap.det φ.toLinearEquiv) (x : E) (y : E) :
(o.kahler (φ x)) (φ y) = (o.kahler x) y

The bilinear map kahler is invariant under pullback by a positively-oriented isometric automorphism.

@[simp]
theorem Complex.areaForm (w : ) (z : ) :
(Complex.orientation.areaForm w) z = (() w * z).im
@[simp]
theorem Complex.rightAngleRotation (z : ) :
Complex.orientation.rightAngleRotation z =
@[simp]
theorem Complex.kahler (w : ) (z : ) :
(Complex.orientation.kahler w) z = () w * z
theorem Orientation.areaForm_map_complex {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (f : ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x : E) (y : E) :
(o.areaForm x) y = (() (f x) * f y).im

The area form on an oriented real inner product space of dimension 2 can be evaluated in terms of a complex-number representation of the space.

theorem Orientation.rightAngleRotation_map_complex {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (f : ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x : E) :
f (o.rightAngleRotation x) = Complex.I * f x

The rotation by 90 degrees on an oriented real inner product space of dimension 2 can be evaluated in terms of a complex-number representation of the space.

theorem Orientation.kahler_map_complex {E : Type u_1} [] [Fact ()] (o : Orientation E (Fin 2)) (f : ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x : E) (y : E) :
(o.kahler x) y = () (f x) * f y

The Kahler form on an oriented real inner product space of dimension 2 can be evaluated in terms of a complex-number representation of the space.