OAI/GroupTheory/PolycyclicRecognition/Algebra/ConeQuotientAutomorphism.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.lieQuotientAutomorphism line 16

   Source documentation

   An automorphism preserving an ideal in both directions induces an actual Lie equivalence on the quotient.

   def lieQuotientAutomorphism
       {L : Type*} [LieRing L] [LieAlgebra ℝ L]
       (I : LieIdeal ℝ L) (F : L ≃ₗ⁅ℝ⁆ L) (hF : ∀ x, F x ∈ I ↔ x ∈ I) :
       (L ⧸ I) ≃ₗ⁅ℝ⁆ (L ⧸ I) := by
   …

2. theorem OAI.PolycyclicRecognition.lieQuotientAutomorphism_mk line 47
3. def OAI.PolycyclicRecognition.CartanWordModel.coneAdjointAutomorphism line 59

   Source documentation

   The induced adjoint Lie automorphism on the cone quotient.

   def coneAdjointAutomorphism (C : Set (H →ₗ[ℝ] ℝ))
       (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C) (h : H) :
       ((cartanRootIdeal H) ⧸ M.coneWordIdeal C) ≃ₗ⁅ℝ⁆
         ((cartanRootIdeal H) ⧸ M.coneWordIdeal C) :=
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

4. theorem OAI.PolycyclicRecognition.CartanWordModel.det_coneAdjointAutomorphism line 66