OAI/GroupTheory/PolycyclicRecognition/Algebra/CommutingSemisimpleCorrection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.semisimple_centralizer_correction_preserving_family line 14
2. theorem OAI.PolycyclicRecognition.exists_semisimple_factor_with_preserving_corrections line 51

   Source documentation

   The next Jordan factor can be chosen in the common commutant. Corrections of every further outer-centralizing element preserve the whole earlier family.

   theorem exists_semisimple_factor_with_preserving_corrections
       (A : L ≃ₗ⁅ℝ⁆ L) (ss : List (L ≃ₗ⁅ℝ⁆ L))
       (hss : ∀ T ∈ ss, Module.End.IsSemisimple T.toLinearMap)
       (hpair : ∀ T ∈ ss, ∀ R ∈ ss, Commute T.toLinearMap R.toLinearMap)
       (hTA : ∀ T ∈ ss, Commute T.toLinearMap A.toLinearMap) :
       ∃ S U : L ≃ₗ⁅ℝ⁆ L, Module.End.IsSemisimple S.toLinearMap ∧
         IsNilpotent (U.toLinearMap - 1) ∧ Commute S.toLinearMap U.toLinearMap ∧
         A.toLinearMap = S.toLinearMap * U.toLinearMap ∧
         (∀ T ∈ ss, Commute T.toLinearMap S.toLinearMap) ∧
         ∀ B : L ≃ₗ⁅ℝ⁆ L, (∀ T ∈ ss, Commute T.toLinearMap B.toLinearMap) →
           ∀ u : L, (polynomialInnerLieEquiv u).toLinearMap * A.toLinearMap =
             B.toLinearEquiv.conjRingEquiv A.toLinearMap →
   …

   Mentions: OAI.PolycyclicRecognition.polynomialInnerLieEquiv