OAI/GroupTheory/PolycyclicRecognition/Lattices/JointFixedFactorSystem.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual extension on the joint fixed kernel

Once the section factors are fixed by the family, the joint fixed subgroup supports the same nonabelian cocycle. Its factor extension embeds faithfully in the original group.

  1. def OAI.PolycyclicRecognition.jointFixedFactorSystem line 20
  2. def OAI.PolycyclicRecognition.jointFixedFactorInclusion line 50
  3. theorem OAI.PolycyclicRecognition.jointFixedFactorInclusion_injective line 60
  4. def OAI.PolycyclicRecognition.jointFixedExtensionEmbedding line 70
  5. theorem OAI.PolycyclicRecognition.jointFixedExtensionEmbedding_injective line 81