Documentation

DerivedAlgGeo.LinearAlgebra.Complex.Coordinates

ℂ as a real coordinate plane, and real linear maps on it #

Complex.basisOneI presents ℂ as ℝ². cplxCoord is that presentation as a linear equivalence, and actC transports a real 2 × 2 matrix of positive determinant across it, so that a map defined on Fin 2 → ℝ can be applied to a ℂ-valued quantity.

Placement #

MO1.12 (#1323), cutover-ledger row 08, comparison-owner column: a complex-coordinate linear-map adapter moves near the complex linear-algebra owner once its public type is independent of the cover. These five declarations meet that condition -- cplxCoord mentions only ℂ and Fin 2 → ℝ, and actC takes a Matrix.GLPos (Fin 2) ℝ, which is the general-linear group and not its cover. The three declarations that do not meet it -- cplxCoord_exp, compat_exp and actC_exp, whose statements mention rayVec, Compatible and NormalizedShift -- stay with the cover in LinearAlgebra/Matrix/GeneralLinearGroup/UniversalCover/ComplexRepresentation.lean.

Independent consumers: the cover's own complex restatements and its surjectivity argument on one side, and the stability action's continuous linear map actCCLM under CategoryTheory/Triangulated/StabilityCondition/Symmetry/GLTilde/Action/ on the other.

Declaration names are unchanged by the move, so the namespace is the one they were introduced in; see the ledger's first standing decision.

source
noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.cplxCoord :
ℂ ≃ₗ[ℝ] Fin 2 → ℝ

ℂ as a real coordinate plane, via the basis 1, I.

Equations
Instances For
    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.cplxCoord_apply (z : ℂ) :
    cplxCoord z = ![z.re, z.im]

    Coordinates of a complex number in the 1, I basis.

    The matrix factor acting on ℂ #

    A central charge lands in ℂ, so this is the form in which a real plane map has to act. Everything below is the matrix transported across cplxCoord.

    source
    noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actC (T : ↥(Matrix.GLPos (Fin 2) ℝ)) :
    ℂ →ₗ[ℝ] ℂ

    T acting ℝ-linearly on ℂ, through the coordinate bridge.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actC_apply (T : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : ℂ) :
      (actC T) z = cplxCoord.symm ((toMat T).mulVec (cplxCoord z))
      source
      theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actC_one (z : ℂ) :
      (actC 1) z = z

      actC 1 is the identity map.

      Deliberately not @[simp]. actC_apply is the simp lemma that unfolds actC, and once it fires toMat_one, Matrix.one_mulVec and LinearEquiv.symm_apply_apply finish the job -- so a @[simp] here is redundant and simpNF rejects it. Stated in applied form to match actC_mul, which is not @[simp] either.

      source
      theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actC_mul (T U : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : ℂ) :
      (actC (T * U)) z = (actC T) ((actC U) z)