Documentation

CsdLean4.Mathlib.LinearAlgebra.Projectivization.Unitary

Matrix unitary group action on projective Euclidean space #

Category: 1-Mathlib (CSD-free Mathlib upstream candidate).

Builds on Mathlib/LinearAlgebra/Projectivization/Topology.lean's instMulAction : MulAction (V ≃ₗ[K] V) (ℙ K V) and Mathlib's Matrix.UnitaryGroup to produce the natural action of the matrix unitary group on the projective space of Euclidean space.

Main definitions #

Main instances #

What this unlocks #

These instances are the substrate for the U(N)-invariant Borel probability measure on ℂℙ^{N-1} (fubiniStudyMeasure) and the associated uniqueness theorem (fubiniStudyMeasure_unique). Together with the finite-measure normalisation invariant_measure_uniqueness_cpn (FubiniStudyUnique.lean), they provide the invariant-measure-uniqueness fact for the ℂℙ^{N-1} / U(N) instantiation, consumed directly by LF4's concrete measure bridges (CSD.LF4.cp_measure_bridge / k_measure_bridge), which therefore cite no axiom at that site. (Historically this was the proved concrete realisation of an abstract CSD.LF2.invariant_measure_uniqueness axiom; that axiom — together with the abstract measure_bridge lemma it served — was removed 2026-06-04, since nothing downstream used the abstract statement. The concrete fact here is all that was ever load-bearing.)

Provenance #

Staged as upstream Mathlib material. All declarations are under namespace Matrix.UnitaryGroup with no CsdLean4-namespace prefix. The file is intended to land in Mathlib/LinearAlgebra/Projectivization/Unitary.lean once usage stabilises.

Tags #

projectivization, unitary group, MulAction, complex projective space

source
noncomputable def Matrix.UnitaryGroup.toEuclideanLinearEquiv {N : ℕ} (A : ↥(unitaryGroup (Fin N) ℂ)) :
EuclideanSpace ℂ (Fin N) ≃ₗ[ℂ] EuclideanSpace ℂ (Fin N)

A unitary matrix gives a linear self-equivalence of EuclideanSpace ℂ (Fin N). The inverse is the linear map induced by the conjugate transpose. Euclidean (PiLp 2) companion to Mathlib's Matrix.UnitaryGroup.toLinearEquiv (which is for Fin N → ℂ).

Equations
Instances For
    source
    @[simp]
    theorem Matrix.UnitaryGroup.toEuclideanLinearEquiv_apply {N : ℕ} (A : ↥(unitaryGroup (Fin N) ℂ)) (v : EuclideanSpace ℂ (Fin N)) :
    (toEuclideanLinearEquiv A) v = (toEuclideanLin ↑A) v
    source
    theorem Matrix.UnitaryGroup.toEuclideanLinearEquiv_one {N : ℕ} :
    toEuclideanLinearEquiv 1 = LinearEquiv.refl ℂ (EuclideanSpace ℂ (Fin N))
    source
    theorem Matrix.UnitaryGroup.toEuclideanLinearEquiv_mul {N : ℕ} (A B : ↥(unitaryGroup (Fin N) ℂ)) :
    toEuclideanLinearEquiv (A * B) = toEuclideanLinearEquiv A * toEuclideanLinearEquiv B
    source
    noncomputable def Matrix.UnitaryGroup.toEuclideanLinearEquivHom {N : ℕ} :
    ↥(unitaryGroup (Fin N) ℂ) →* EuclideanSpace ℂ (Fin N) ≃ₗ[ℂ] EuclideanSpace ℂ (Fin N)

    The monoid hom from the matrix unitary group to the LinearEquiv group of EuclideanSpace ℂ (Fin N).

    Equations
    Instances For

      Action on projective space #

      source
      @[instance_reducible]
      noncomputable instance Matrix.UnitaryGroup.instProjectivizationMulAction {N : ℕ} :
      MulAction (↥(unitaryGroup (Fin N) ℂ)) (Projectivization ℂ (EuclideanSpace ℂ (Fin N)))

      Matrix.unitaryGroup (Fin N) ℂ acts on ℙ ℂ (EuclideanSpace ℂ (Fin N)) via the unitary action on the underlying Hilbert space, transported through Projectivization.instMulAction via MulAction.compHom.

      Equations
      source
      instance Matrix.UnitaryGroup.instProjectivizationContinuousConstSMul {N : ℕ} :
      ContinuousConstSMul (↥(unitaryGroup (Fin N) ℂ)) (Projectivization ℂ (EuclideanSpace ℂ (Fin N)))

      The action of each unitary on ℂℙ^{N-1} is continuous.