Oriented two-dimensional real inner product spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines constructions specific to the geometry of an oriented two-dimensional real inner
product space E.
Main declarations #
-
orientation.area_form: an antisymmetric bilinear formE →ₗ[ℝ] 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.right_angle_rotation: an isometric automorphismE ≃ₗᵢ[ℝ] E(usual notationJ). 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.basis_right_angle_rotation: for a nonzero vectorxinE, the basis![x, J x]forE. -
orientation.kahler: a complex-valued real-bilinear mapE →ₗ[ℝ] E →ₗ[ℝ] ℂ. Its real part is the inner product and its imaginary part isorientation.area_form. For vectorsxandyinE, the complex numbero.kahler x yhas modulus‖x‖ * ‖y‖. In a later file, oriented angles (orientation.oangle) are defined, in such a way that the argument ofo.kahler x yis the oriented angle fromxtoy.
Main results #
-
orientation.right_angle_rotation_right_angle_rotation: the identityJ (J x) = - x -
orientation.nonneg_inner_and_area_form_eq_zero_iff_same_ray:x,yare in the same ray, if and only if0 ≤ ⟪x, y⟫andω x y = 0 -
orientation.kahler_mul: the identityo.kahler x a * o.kahler a y = ‖a‖ ^ 2 * o.kahler x y -
complex.area_form,complex.right_angle_rotation,complex.kahler: the concrete interpretations ofarea_form,right_angle_rotation,kahlerfor the oriented real inner product spaceℂ -
orientation.area_form_map_complex,orientation.right_angle_rotation_map_complex,orientation.kahler_map_complex: given an orientation-preserving isometry fromEtoℂ, expressions forarea_form,right_angle_rotation,kahleras the pullback of their concrete interpretations onℂ
Implementation notes #
Notation ω for orientation.area_form and J for orientation.right_angle_rotation 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.area_form
local notation `J` := o.right_angle_rotation
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
- o.area_form = let z : alternating_map ℝ E ℝ (fin 0) ≃ₗ[ℝ] ℝ := alternating_map.const_linear_equiv_of_is_empty.symm, y : alternating_map ℝ E ℝ (fin 1) →ₗ[ℝ] E →ₗ[ℝ] ℝ := (⇑(linear_map.llcomp ℝ E (alternating_map ℝ E ℝ (fin 0)) ℝ) ↑z).comp alternating_map.curry_left_linear_map in y.comp (⇑alternating_map.curry_left_linear_map o.volume_form)
Continuous linear map version of orientation.area_form, useful for calculus.
The area form is invariant under pullback by a positively-oriented isometric automorphism.
Auxiliary construction for orientation.right_angle_rotation, rotation by 90 degrees in an
oriented real inner product space of dimension 2.
Equations
- o.right_angle_rotation_aux₁ = let to_dual : E ≃ₗ[ℝ] E →ₗ[ℝ] ℝ := (inner_product_space.to_dual ℝ E).to_linear_equiv.trans linear_map.to_continuous_linear_map.symm in ↑(to_dual.symm).comp o.area_form
Auxiliary construction for orientation.right_angle_rotation, rotation by 90 degrees in an
oriented real inner product space of dimension 2.
Equations
- o.right_angle_rotation_aux₂ = {to_linear_map := {to_fun := o.right_angle_rotation_aux₁.to_fun, map_add' := _, map_smul' := _}, norm_map' := _}
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.
J commutes with any positively-oriented isometric automorphism.
J commutes with any positively-oriented isometric automorphism.
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.basis_right_angle_rotation x hx = basis_of_linear_independent_of_card_eq_finrank _ orientation.basis_right_angle_rotation._proof_3
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_area_form_mul_area_form for the "applied" form.)
For vectors a x y : E, the identity ⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω 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. (See
orientation.inner_mul_area_form_sub for the "applied" form.)
For vectors a x y : E, the identity ⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y.
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.area_form.
On ℂ with the standard orientation, kahler w z = conj w * z; see complex.kahler.
The bilinear map kahler is invariant under pullback by a positively-oriented isometric
automorphism.
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.
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.
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.