OAI/NumberTheory/DukePrimeDegree/Dynamics/TwoBlockGroups.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The two cross-block groups and the neutral block group

These are concrete subgroups of the same determinant-one matrix group. The rectangular cross-block coordinates are additive, and the neutral group is the centralizer of the coordinate projection. This supplies the group side of the singular two-block chart, without an entropy or measure-classification assumption.

  1. abbrev OAI.DukePrimeDegree.TwoBlockSL line 23
  2. def OAI.DukePrimeDegree.twoBlockProjection line 26
  3. def OAI.DukePrimeDegree.twoBlockUpper line 30
  4. def OAI.DukePrimeDegree.twoBlockLower line 33
  5. lemma OAI.DukePrimeDegree.twoBlockUpper_zero line 36
  6. lemma OAI.DukePrimeDegree.twoBlockLower_zero line 41
  7. lemma OAI.DukePrimeDegree.twoBlockUpper_add line 46
  8. lemma OAI.DukePrimeDegree.twoBlockLower_add line 55
  9. lemma OAI.DukePrimeDegree.twoBlockUpper_inv line 63
  10. lemma OAI.DukePrimeDegree.twoBlockLower_inv line 68
  11. def OAI.DukePrimeDegree.twoBlockNeutralGroup line 75

    Source documentation

    The block-diagonal determinant-one subgroup, expressed without a choice of bases in either block beyond the fixed coordinates.

    def twoBlockNeutralGroup (a b : ℕ) : Subgroup (TwoBlockSL a b) where
…

    Mentions: OAI.DukePrimeDegree.TwoBlockSL

  12. lemma OAI.DukePrimeDegree.mem_twoBlockNeutralGroup_iff line 103