Documentation

CsdLean4.Mathlib.LinearAlgebra.Projectivization.UnitaryTransitive

Transitivity of the matrix unitary group action on complex projective space #

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

Proves that Matrix.unitaryGroup (Fin N) ℂ acts transitively on ℙ ℂ (EuclideanSpace ℂ (Fin N)) for [NeZero N], via the standard orthonormal-basis-extension construction.

Argument #

  1. For any unit vector v, extend {v} to an orthonormal basis b_v indexed by Fin N with b_v 0 = v (via Orthonormal.exists_orthonormalBasis_extension_of_card_eq).

  2. The change-of-basis matrix M_v := b_std.toBasis.toMatrix b_v.toBasis (where b_std = EuclideanSpace.basisFun (Fin N) ℂ) is unitary (via OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary) and has first column equal to v.

  3. Applying M_v to the standard basis vector e_0 recovers v.

  4. For two unit vectors v, w, the composition M_w * M_v⁻¹ is a unitary that maps v ↦ w. Lifted to projective space, this gives transitivity (any two projective points are related by a unitary, after normalisation of representatives).

Main result #

Matrix.UnitaryGroup.instIsPretransitive_projectivization — the IsPretransitive instance for the matrix unitary group on ℂℙ^(N-1).

Provenance #

Staged as upstream Mathlib material. Intended location: Mathlib/LinearAlgebra/Projectivization/UnitaryTransitive.lean.

Tags #

projectivization, unitary group, transitive action, orthonormal basis

Step 1 — unitary with prescribed first column #

source
noncomputable def Matrix.UnitaryGroup.unitaryOfONB {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) :
↥(unitaryGroup (Fin N) ℂ)

Build a unitary matrix from an orthonormal basis: the matrix whose columns are the coordinates of the basis vectors in the standard basis.

Equations
Instances For
    source
    theorem Matrix.UnitaryGroup.unitaryOfONB_apply_single {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (j : Fin N) :
    (toEuclideanLin ↑(unitaryOfONB b)) (EuclideanSpace.single j 1) = b j

    The matrix unitaryOfONB b, applied to the standard basis vector e_j, recovers b j.

    source
    theorem Matrix.UnitaryGroup.exists_unitary_e_zero_eq {N : ℕ} [NeZero N] (v : EuclideanSpace ℂ (Fin N)) (hv : ‖v‖ = 1) :
    ∃ (M : ↥(unitaryGroup (Fin N) ℂ)), (toEuclideanLin ↑M) (EuclideanSpace.single 0 1) = v

    For any unit vector v, there exists a unitary matrix whose action on the standard basis vector e_0 is v.

    source
    theorem Matrix.UnitaryGroup.exists_unitary_map_unit {N : ℕ} [NeZero N] (v w : EuclideanSpace ℂ (Fin N)) (hv : ‖v‖ = 1) (hw : ‖w‖ = 1) :
    ∃ (U : ↥(unitaryGroup (Fin N) ℂ)), (toEuclideanLin ↑U) v = w

    For any two unit vectors v, w, there exists a unitary matrix U ∈ Matrix.unitaryGroup (Fin N) ℂ whose action on v is w.

    source
    theorem Matrix.UnitaryGroup.toEuclideanLin_unitary_ne_zero {N : ℕ} (U : ↥(unitaryGroup (Fin N) ℂ)) {v : EuclideanSpace ℂ (Fin N)} (hv : v ≠ 0) :
    (toEuclideanLin ↑U) v ≠ 0

    A unitary matrix's toEuclideanLin action preserves non-zero.

    source
    theorem Matrix.UnitaryGroup.exists_unitary_mapping_nonzero {N : ℕ} [NeZero N] {v w : EuclideanSpace ℂ (Fin N)} (hv : v ≠ 0) (hw : w ≠ 0) :
    ∃ (U : ↥(unitaryGroup (Fin N) ℂ)) (c : ℂ), c ≠ 0 ∧ (toEuclideanLin ↑U) v = c • w

    For any two nonzero vectors v, w, there exists a unitary matrix U and a nonzero complex scalar c with (toEuclideanLin U.val) v = c • w.

    source
    theorem Matrix.UnitaryGroup.smul_mk_eq_mk {N : ℕ} [NeZero N] (U : ↥(unitaryGroup (Fin N) ℂ)) (v : EuclideanSpace ℂ (Fin N)) (hv : v ≠ 0) :
    U • Projectivization.mk ℂ v hv = Projectivization.mk ℂ ((toEuclideanLin ↑U) v) ⋯

    For unitary U and nonzero v, the projective action is given by mk of the matrix action on v. Both sides reduce to the same Quotient.mk'' term by definitional unfolding of MulAction.compHom, mapEquiv, and Projectivization.map.

    source
    instance Matrix.UnitaryGroup.instIsPretransitive_projectivization {N : ℕ} [NeZero N] :
    MulAction.IsPretransitive (↥(unitaryGroup (Fin N) ℂ)) (Projectivization ℂ (EuclideanSpace ℂ (Fin N)))

    Transitivity of the matrix unitary group action on ℂℙ^(N-1). For any two projective points, there is a unitary mapping one to the other.