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's Projectivization.instMulAction (Mathlib/LinearAlgebra/Projectivization/Action.lean, here with G := V ≃ₗ[K] V; mapEquiv_smul_eq in Projectivization/Topology.lean reads it on representatives) 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} (fsMeasure) and the associated uniqueness theorem (fsMeasure_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 the source repository's concrete measure bridges, which therefore cite no axiom at that site. (Historically this was the proved concrete realisation of an abstract invariant-measure-uniqueness axiom of that repository; 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 {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : ↥(unitaryGroup ι ℂ)) :
EuclideanSpace ℂ ι ≃ₗ[ℂ] EuclideanSpace ℂ ι

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

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

    The monoid hom from the matrix unitary group to the LinearEquiv group of EuclideanSpace ℂ ι.

    Equations
    Instances For

      Action on projective space #

      source
      @[instance_reducible]
      noncomputable instance Matrix.UnitaryGroup.instProjectivizationMulAction {ι : Type u_1} [Fintype ι] [DecidableEq ι] :
      MulAction (↥(unitaryGroup ι ℂ)) (Projectivization ℂ (EuclideanSpace ℂ ι))

      Matrix.unitaryGroup ι ℂ acts on ℙ ℂ (EuclideanSpace ℂ ι) via the unitary action on the underlying Hilbert space, transported through Mathlib's Projectivization.instMulAction (with G := V ≃ₗ[ℂ] V) via MulAction.compHom.

      Equations
      source
      instance Matrix.UnitaryGroup.instProjectivizationContinuousConstSMul {ι : Type u_1} [Fintype ι] [DecidableEq ι] :
      ContinuousConstSMul (↥(unitaryGroup ι ℂ)) (Projectivization ℂ (EuclideanSpace ℂ ι))

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