Documentation

SphereEversion.ToMathlib.Analysis.InnerProductSpace.CrossProduct

The cross-product on an oriented real inner product space of dimension three #

source
def Orientation.crossProduct {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) :
E →ₗ[ℝ] E →ₗ[ℝ] E

Linear map from E to E →ₗ[ℝ] E constructed from a 3-form Ω on E and an identification of E with its dual. Effectively, the Hodge star operation. (Under appropriate hypotheses it turns out that the image of this map is in 𝔰𝔬(E), the skew-symmetric operators, which can be identified with Λ²E.)

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Orientation.crossProduct_apply_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (v : E) :
    (ω.crossProduct v) v = 0
    source
    theorem Orientation.inner_crossProduct_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (u v w : E) :
    inner ((ω.crossProduct u) v) w = ω.volumeForm ![u, v, w]
    source
    theorem Orientation.inner_crossProduct_apply_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (u : E) (v : ↥(Submodule.span ℝ {u})ᗮ) :
    inner ((ω.crossProduct u) ↑v) u = 0
    source
    theorem Orientation.inner_crossProduct_apply_apply_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (u : E) (v : ↥(Submodule.span ℝ {u})ᗮ) :
    inner ((ω.crossProduct u) ↑v) ↑v = 0
    source
    def Orientation.crossProduct' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) :
    E →L[ℝ] E →L[ℝ] E

    The map crossProduct, upgraded from linear to continuous-linear; useful for calculus.

    Equations
    Instances For
      source
      @[simp]
      theorem Orientation.crossProduct'_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (v : E) :
      ω.crossProduct' v = LinearMap.toContinuousLinearMap (ω.crossProduct v)
      source
      theorem Orientation.norm_crossProduct {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (u : E) (v : ↥(Submodule.span ℝ {u})ᗮ) :
      ‖(ω.crossProduct u) ↑v‖ = ‖u‖ * ‖v‖
      source
      theorem Orientation.isometry_on_crossProduct {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (u : ↑(Metric.sphere 0 1)) (v : ↥(Submodule.span ℝ {↑u})ᗮ) :
      ‖(ω.crossProduct ↑u) ↑v‖ = ‖v‖