volumeForm_comp_linearIsometryEquiv

English

Volume form is invariant under composition with an orientation-preserving linear isometry.

Русский

Объемная форма сохраняется при композиции с ориентированным линейным изометрическим отображением.

LaTeX

$$$$ o.volumeForm \circ (\phi \mapsto \phi) = o.volumeForm $$$$

Lean4

/-- The volume form is invariant under pullback by a positively-oriented isometric automorphism. -/
theorem volumeForm_comp_linearIsometryEquiv (φ : E ≃ₗᵢ[ℝ] E) (hφ : 0 < LinearMap.det (φ.toLinearEquiv : E →ₗ[ℝ] E))
    (x : Fin n → E) : o.volumeForm (φ ∘ x) = o.volumeForm x :=
  by
  rcases n with - | n
  · refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp
  have : FiniteDimensional ℝ E := .of_fact_finrank_eq_succ n
  convert o.volumeForm_map φ (φ ∘ x)
  · symm
    rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
    rw [_i.out, Fintype.card_fin]
  · ext
    simp

Похожие утверждения