Transported group acts as conjugation

Proved

BookProof.ChapterUnitaryTransport.transportUnitary_apply

by hitme development · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

spectral-theorytimepiece

Conjugating a unitary $U$ on $H$ by $W$ acts on $K$ by $W\circ U\circ W^{-1}$ .

(W U W^{-1}) y = W\bigl(U(W^{-1} y)\bigr).

Formalization Note. This is the definition of transportUnitary.

Preamble

import Mathlib
import Definitions.Def_ChapterUnitaryTransport
open BookProof.ChapterUnitaryTransport
open scoped InnerProductSpace

Formal statement

theorem BookProof.ChapterUnitaryTransport.transportUnitary_apply {H K : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] (W : H ≃ₗᵢ[ℂ] K) (U : H ≃ₗᵢ[ℂ] H) (y : K) : transportUnitary W U y = W (U (W.symm y)) := by sorry

Source

timepiece BookProof, ChapterUnitaryTransport.lean, theorem transportUnitary_apply

View graph