One-parameter groups of matrices

StructureOne-parameter group of complex matrices#✓fully proved

For \(m \in \mathbb{N}\), a map \(\varphi \colon \mathbb{R} \to M_m(\mathbb{C})\) into the complex \(m \times m\) matrices is a one-parameter group when \(\varphi(0)\) is the identity matrix \(I\), \(\varphi(s + t) = \varphi(s)\,\varphi(t)\) for all real \(s\) and \(t\), and \(\varphi\) is differentiable.

Such a map takes values in \(\mathrm{GL}_m(\mathbb{C})\), since \(\varphi(t)\,\varphi(-t) = I\).

structure IsOneParameterGroup (m : ℕ) (φ : ℝ → Matrix (Fin m) (Fin m) ℂ) : Prop where
  /-- `φ 0 = 1`: the identity maps to the identity matrix. -/
  map_zero : φ 0 = 1
  /-- `φ (s + t) = φ s * φ t`: the homomorphism law. -/
  map_add : ∀ s t : ℝ, φ (s + t) = φ s * φ t
  /-- `φ` is differentiable (for the entrywise topology on matrices). -/
  differentiable : Differentiable ℝ φ

Used by 5

Used byUnderlying matrix of the lift of a one-parameter group · Exponential curves are one-parameter groups · One-parameter group in a subgroup of the general linear group · One-parameter groups of matrices are exponentials · The lift of a one-parameter group to the general linear group

StructureOne-parameter group in a subgroup of the general linear group#✓fully proved

Let \(m \in \mathbb{N}\) and let \(G\) be a subgroup of \(\mathrm{GL}_m(\mathbb{C})\). A map \(\varphi \colon \mathbb{R} \to \mathrm{GL}_m(\mathbb{C})\) is a one-parameter group in \(G\) when the matrix-valued map \(t \mapsto \varphi(t)\) is a one-parameter group and \(\varphi(t) \in G\) for every real \(t\).

structure IsOneParameterGroupIn {m : ℕ}
    (G : Subgroup (Matrix.GeneralLinearGroup (Fin m) ℂ))
    (φ : ℝ → Matrix.GeneralLinearGroup (Fin m) ℂ) : Prop
    extends IsOneParameterGroup m (fun t => (φ t : Matrix (Fin m) (Fin m) ℂ)) where
  /-- Every value of the curve lies in `G`. -/
  mem : ∀ t : ℝ, φ t ∈ G

Uses 1

Statement usesOne-parameter group of complex matrices

DefinitionThe lift of a one-parameter group to the general linear group#✓fully proved

Let \(m \in \mathbb{N}\) and let \(\varphi \colon \mathbb{R} \to M_m(\mathbb{C})\) be a one-parameter group of complex \(m \times m\) matrices. For every real \(t\) the matrix \(\varphi(t)\) is invertible with inverse \(\varphi(-t)\); this gives the element of \(\mathrm{GL}_m(\mathbb{C})\) with matrix \(\varphi(t)\) and inverse \(\varphi(-t)\).

def IsOneParameterGroup.toGL {m : ℕ} {φ : ℝ → Matrix (Fin m) (Fin m) ℂ}
    (hφ : IsOneParameterGroup m φ) (t : ℝ) : Matrix.GeneralLinearGroup (Fin m) ℂ where
  val := φ t
  inv := φ (-t)
  val_inv := by rw [← hφ.map_add, add_neg_cancel, hφ.map_zero]
  inv_val := by rw [← hφ.map_add, neg_add_cancel, hφ.map_zero]

Uses 1 · Used by 1

Statement usesOne-parameter group of complex matrices

Used byUnderlying matrix of the lift of a one-parameter group

TheoremUnderlying matrix of the lift of a one-parameter group#✓fully proved

Let \(m \in \mathbb{N}\) and let \(\varphi \colon \mathbb{R} \to M_m(\mathbb{C})\) be a one-parameter group of complex \(m \times m\) matrices. For every real \(t\), the element of \(\mathrm{GL}_m(\mathbb{C})\) assigned to \(t\) by the lift of \(\varphi\) has underlying matrix \(\varphi(t)\).

@[simp] theorem IsOneParameterGroup.coe_toGL {m : ℕ}
    {φ : ℝ → Matrix (Fin m) (Fin m) ℂ} (hφ : IsOneParameterGroup m φ) (t : ℝ) :
    (hφ.toGL t : Matrix (Fin m) (Fin m) ℂ) = φ t

Uses 2

Statement usesOne-parameter group of complex matrices · The lift of a one-parameter group to the general linear group

TheoremOne-parameter groups of matrices are exponentials#✓fully proved

Let \(m \in \mathbb{N}\). If \(\varphi \colon \mathbb{R} \to M_m(\mathbb{C})\) is a one-parameter group of complex \(m \times m\) matrices, then there is a unique matrix \(A \in M_m(\mathbb{C})\) such that \(\varphi(t) = \exp(tA)\) for every real \(t\).

theorem one_param_subgroup_form (m : ℕ)
    (φ : ℝ → Matrix (Fin m) (Fin m) ℂ) (hφ : IsOneParameterGroup m φ) :
    ∃! A : Matrix (Fin m) (Fin m) ℂ,
      ∀ t : ℝ, φ t = NormedSpace.exp ((↑t : ℂ) • A)

Uses 1

Statement usesOne-parameter group of complex matrices

TheoremExponential curves are one-parameter groups#✓fully proved

For every \(m \in \mathbb{N}\) and every complex \(m \times m\) matrix \(A\), the map \(t \mapsto \exp(tA)\) from \(\mathbb{R}\) to the complex \(m \times m\) matrices is a one-parameter group.

theorem isOneParameterGroup_exp_smul (m : ℕ) (A : Matrix (Fin m) (Fin m) ℂ) :
    IsOneParameterGroup m (fun t => NormedSpace.exp ((↑t : ℂ) • A))

Uses 1

Statement usesOne-parameter group of complex matrices

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.