ConeQuotientJacobian.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The Jacobian of the induced Cartan action on a cone quotient

theorem OAI.PolycyclicRecognition.quotient_unipotent line 16

Source documentation

A quotient of a unipotent operator is unipotent. This supplies the determinant-one part of the quotient action without diagonalizability.

theorem quotient_unipotent
    {V : Type*} [AddCommGroup V] [Module ℝ V]
    (J : Submodule ℝ V) (F : V →ₗ[ℝ] V) (hF : ∀ x ∈ J, F x ∈ J)
    (hu : _root_.IsNilpotent (F - 1)) :
    _root_.IsNilpotent (J.mapQ J F hF - 1) := by
…

theorem OAI.PolycyclicRecognition.CartanWordModel.coneWordIdeal_dilation_mem line 41
theorem OAI.PolycyclicRecognition.CartanWordModel.coneWordIdeal_residual_mem line 55

theorem OAI.PolycyclicRecognition.CartanWordModel.det_cone_dilation_word_basis line 71

Source documentation

The quotient scalar Jacobian is the exponential of the total retained word weight.

theorem det_cone_dilation_word_basis
    (C : Set (H →ₗ[ℝ] ℝ)) (h : H) {J : Type*} [Fintype J]
    (b : Basis J ℝ ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
    (words : J → FreeMagma (Fin M.letterCount))
    (hb : ∀ j, (M.coneWordIdeal C).toSubmodule.mkQ (evalBracketWord M.letter (words j)) = b j) :
    LinearMap.det ((M.coneWordIdeal C).toSubmodule.mapQ (M.coneWordIdeal C).toSubmodule
      (cartanIdealWeightDilation T H h).toLinearEquiv.toLinearMap
      (M.coneWordIdeal_dilation_mem T C h)) =
        Real.exp (∑ j, bracketWordExponent (fun i => M.weight i h) (words j)) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.cartanIdealWeightDilation, OAI.PolycyclicRecognition.bracketWordExponent

theorem OAI.PolycyclicRecognition.CartanWordModel.det_cone_residual_eq_one line 96

theorem OAI.PolycyclicRecognition.CartanWordModel.det_cone_adjoint_eq_exp_trace line 110

Source documentation

The full induced action has Jacobian equal to the exponential of its actual quotient trace, including all nonsemisimple corrections.

theorem det_cone_adjoint_eq_exp_trace
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C) (h : H) :
    LinearMap.det ((M.coneWordIdeal C).toSubmodule.mapQ (M.coneWordIdeal C).toSubmodule
      (cartanIdealAdjointAutomorphism T H h).toLinearEquiv.toLinearMap
      (M.coneWordIdeal_adjoint_mem T C hadd h)) =
    Real.exp (LinearMap.trace ℝ ((cartanRootIdeal H) ⧸ M.coneCartanSubmodule C hadd)
      (toEnd ℝ H _ h)) := by
…

Mentions: OAI.PolycyclicRecognition.cartanIdealAdjointAutomorphism, OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_positive_cone_jacobian_character line 140

Source documentation

The positive integral character computed from pure words is the exact Jacobian character of the induced Cartan action.

theorem exists_positive_cone_jacobian_character
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C) :
    ∃ c : Fin M.letterCount → ℕ,
      (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∉ C → c i = 0) ∧
      (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C → 0 < c i) ∧
      ∀ h : H, LinearMap.det
        ((M.coneWordIdeal C).toSubmodule.mapQ (M.coneWordIdeal C).toSubmodule
          (cartanIdealAdjointAutomorphism T H h).toLinearEquiv.toLinearMap
          (M.coneWordIdeal_adjoint_mem T C hadd h)) =
        Real.exp (∑ i, (c i : ℝ) * M.weight i h) := by
…

Mentions: OAI.PolycyclicRecognition.cartanIdealAdjointAutomorphism