OAI/GroupTheory/PolycyclicRecognition/Lattices/CompletedExtensionCentralizer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Semisimple centralizer reduction for the completed lattice extension

  1. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.completedExtension_conjugation_smooth line 15
  2. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.completedExtension_semisimple_centralizer line 25

    Source documentation

    No fixed-point-free condition: the actual centralizer surjects onto the whole original quotient, and its intersection with the kernel is explicit.

    theorem completedExtension_semisimple_centralizer [IsMulCommutative Q] (q : Q) :
    ∃ T : C.carrier ≃ₗ⁅ℝ⁆ C.carrier, Module.End.IsSemisimple T.toLinearMap ∧
      Function.Surjective
        ((FactorExtension.groupExtension (C.extensionFactorSystem S σ hσ)).rightHom.comp
          (semisimpleActionCentralizer
            (FactorExtension.groupExtension (C.extensionFactorSystem S σ hσ)) T).subtype) ∧
      ∀ x : C.carrier,
        (FactorExtension.groupExtension (C.extensionFactorSystem S σ hσ)).inl x ∈
          semisimpleActionCentralizer
            (FactorExtension.groupExtension (C.extensionFactorSystem S σ hσ)) T ↔
        ∃ z y : C.carrier, z ∈ Subgroup.center C.carrier ∧ T y = y ∧ x = z * y := by
…

    Mentions: OAI.PolycyclicRecognition.FactorExtension.groupExtension, OAI.PolycyclicRecognition.semisimpleActionCentralizer