1. Physlib
  2. Relativity
  3. LorentzGroup
  4. Rotations
Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Relativity.LorentzGroup.Restricted.Basic

Rotations

In this module we define rotations of in the Lorentz group.

@[expose] public section

The subgroup of rotations of the Lorentz group.

All goals completed! 🐙 d:ℕΛ₁:↑(𝓛 d)Λ₂:↑(𝓛 d)h1:Λ₁ ∈ fun Λ => ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 ∧ IsProper Λh2:Λ₂ ∈ fun Λ => ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 ∧ IsProper Λ⊢ IsProper (Λ₁ * Λ₂) All goals completed! 🐙 one_mem' := d:ℕ⊢ 1 ∈ fun Λ => ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 ∧ IsProper Λ d:ℕ⊢ ↑1 (Sum.inl 0) (Sum.inl 0) = 1d:ℕ⊢ IsProper 1 d:ℕ⊢ ↑1 (Sum.inl 0) (Sum.inl 0) = 1d:ℕ⊢ IsProper 1 All goals completed! 🐙 inv_mem' {Λ} h := d:ℕΛ:↑(𝓛 d)h:Λ ∈ fun Λ => ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 ∧ IsProper Λ⊢ Λ⁻¹ ∈ fun Λ => ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 ∧ IsProper Λ d:ℕΛ:↑(𝓛 d)h:Λ ∈ fun Λ => ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 ∧ IsProper Λ⊢ ↑Λ⁻¹ (Sum.inl 0) (Sum.inl 0) = 1d:ℕΛ:↑(𝓛 d)h:Λ ∈ fun Λ => ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 ∧ IsProper Λ⊢ IsProper Λ⁻¹ d:ℕΛ:↑(𝓛 d)h:Λ ∈ fun Λ => ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 ∧ IsProper Λ⊢ ↑Λ⁻¹ (Sum.inl 0) (Sum.inl 0) = 1 All goals completed! 🐙 d:ℕΛ:↑(𝓛 d)h:Λ ∈ fun Λ => ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 ∧ IsProper Λ⊢ IsProper Λ⁻¹ All goals completed! 🐙
lemma mem_rotations_iff {d} (Λ : LorentzGroup d) : Λ ∈ Rotations d ↔ Λ.1 (Sum.inl 0) (Sum.inl 0) = 1 ∧ IsProper Λ := d:ℕΛ:↑(𝓛 d)⊢ Λ ∈ Rotations d ↔ ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 ∧ IsProper Λ All goals completed! 🐙@[simp] lemma transpose_mem_rotations {d} (Λ : LorentzGroup d) : transpose Λ ∈ Rotations d ↔ Λ ∈ Rotations d := d:ℕΛ:↑(𝓛 d)⊢ transpose Λ ∈ Rotations d ↔ Λ ∈ Rotations d All goals completed! 🐙

The group homomorphism from the special orthogonal group to the Lorentz group.

d:ℕΛ✝:↥(Rotations d)Λ:↑(𝓛 d)h:Λ ∈ Rotations dM:Matrix (Fin d) (Fin d) ℝ := fun i j => ↑Λ (Sum.inr i) (Sum.inr j)h1:Matrix.fromBlocks 1 0 0 M = ↑Λ⊢ (fun A => ⟨⟨Matrix.fromBlocks 1 0 0 ↑A, ⋯⟩, ⋯⟩) ((fun Λ => ⟨fun i j => ↑↑Λ (Sum.inr i) (Sum.inr j), ⋯⟩) ⟨Λ, h⟩) = ⟨Λ, h⟩ d:ℕΛ✝:↥(Rotations d)Λ:↑(𝓛 d)h:Λ ∈ Rotations dM:Matrix (Fin d) (Fin d) ℝ := fun i j => ↑Λ (Sum.inr i) (Sum.inr j)h1:Matrix.fromBlocks 1 0 0 M = ↑Λ⊢ ↑((fun A => ⟨⟨Matrix.fromBlocks 1 0 0 ↑A, ⋯⟩, ⋯⟩) ((fun Λ => ⟨fun i j => ↑↑Λ (Sum.inr i) (Sum.inr j), ⋯⟩) ⟨Λ, h⟩)) = ↑⟨Λ, h⟩ d:ℕΛ✝:↥(Rotations d)Λ:↑(𝓛 d)h:Λ ∈ Rotations dM:Matrix (Fin d) (Fin d) ℝ := fun i j => ↑Λ (Sum.inr i) (Sum.inr j)h1:Matrix.fromBlocks 1 0 0 M = ↑Λ⊢ ⟨Matrix.fromBlocks 1 0 0 fun i j => ↑Λ (Sum.inr i) (Sum.inr j), ⋯⟩ = Λ All goals completed! 🐙
@[fun_prop] lemma ofSpecialOrthogonal_continuous {d} : Continuous (ofSpecialOrthogonal : Matrix.specialOrthogonalGroup (Fin d) ℝ → Rotations d) := d:ℕ⊢ Continuous ⇑ofSpecialOrthogonal d:ℕ⊢ Continuous fun A => ⟨⟨Matrix.fromBlocks 1 0 0 ↑A, ⋯⟩, ⋯⟩ All goals completed! 🐙@[fun_prop] lemma ofSpecialOrthogonal_symm_continuous {d} : Continuous (ofSpecialOrthogonal.symm : Rotations d → Matrix.specialOrthogonalGroup (Fin d) ℝ) := d:ℕ⊢ Continuous ⇑ofSpecialOrthogonal.symm d:ℕ⊢ Continuous fun Λ => ⟨fun i j => ↑↑Λ (Sum.inr i) (Sum.inr j), ⋯⟩ d:ℕ⊢ Continuous fun x i j => ↑↑x (Sum.inr i) (Sum.inr j) d:ℕ⊢ Continuous fun x => (↑x).1 All goals completed! 🐙lemma rotations_subset_restricted (d) : Rotations d ≤ LorentzGroup.restricted d := d:ℕ⊢ Rotations d ≤ restricted d d:ℕΛ:↑(𝓛 d)h:Λ ∈ Rotations d⊢ Λ ∈ restricted d d:ℕΛ:↑(𝓛 d)h:Λ ∈ Rotations d⊢ IsProper Λd:ℕΛ:↑(𝓛 d)h:Λ ∈ Rotations d⊢ IsOrthochronous Λ d:ℕΛ:↑(𝓛 d)h:Λ ∈ Rotations d⊢ IsProper Λ All goals completed! 🐙 d:ℕΛ:↑(𝓛 d)h:Λ ∈ Rotations d⊢ IsOrthochronous Λ All goals completed! 🐙d:ℕΛ:↥(Rotations d)⊢ ↑↑Λ (Sum.inl 0) (Sum.inl 0) = 1 All goals completed! 🐙