OAI/GroupTheory/PolycyclicRecognition/Geometry/RealShadowRepresentationTransport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transporting the faithful shadow representation to its geometric realization

  1. theorem OAI.PolycyclicRecognition.realShadow_triangularRepresentation_pullback line 18

    Source documentation

    Only the target real-shadow algebra needs a finite-dimensionality instance.

    theorem realShadow_triangularRepresentation_pullback (e : K ≃ₗ⁅ℝ⁆ CartanRealShadow T H) :
    ∃ m : ℕ, 0 < m ∧ ∃ j : K →ₗ⁅ℝ⁆ Matrix (Fin m) (Fin m) ℝ,
      Function.Injective j ∧ (∀ x, (j x).IsUpperTriangular) ∧
      ∀ x, e x ∈ realShadowKernel T H → IsNilpotent (j x) := by
…

    Mentions: OAI.PolycyclicRecognition.CartanRealShadow, OAI.PolycyclicRecognition.realShadowKernel