OAI/GroupTheory/BooneHigman/AffineModules.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Affine module presentations, stabilized actions, and finite stabilizers.

  1. def OAI.FiniteAlgebraicEnvelopes.MatrixModule.applyMatrix line 16
  2. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.applyMatrix_zero line 19
  3. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.applyMatrix_add line 24
  4. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.applyMatrix_sub line 30
  5. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.applyMatrix_one line 35
  6. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.applyMatrix_mul line 40
  7. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.applyMatrix_vec_add line 47
  8. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.applyMatrix_singleVec line 52
  9. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.applyMatrix_single line 56
  10. def OAI.FiniteAlgebraicEnvelopes.MatrixModule.unitsAddEquiv line 64
  11. def OAI.FiniteAlgebraicEnvelopes.MatrixModule.unitsAction line 71
  12. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.unitsAction_apply line 84
  13. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.steinberg_action line 88

    Source documentation

    In particular the literal Steinberg action depends only on its elementary matrix.

    theorem steinberg_action :
    (unitsAction (V:=V)).comp (Steinberg.matrixMap (ι:=Fin 6) (R:=R))=AffineAction.action := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.MatrixModule.unitsAction, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap, OAI.FiniteAlgebraicEnvelopes.AffineAction.action

  14. def OAI.FiniteAlgebraicEnvelopes.MatrixModule.columnMap line 107
  15. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.columnMap_add line 110
  16. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.columnMap_matrix line 113
  17. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.columnMap_corrected line 120
  18. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.coefficient_compatible line 132
  19. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.correctedMatrix_eq_one line 149

    Source documentation

    A detector after the coefficient map detects every entry of a matrix difference.

    theorem correctedMatrix_eq_one (ψ : R →ₙ+* R) (b : V)
    (hb : ∀ r : R, ψ r • b=0 → r=0) (A : Matrix ι ι R)
    (hA : ∀ j : ι, applyMatrix (correctedMap (matrixNonunitalMap ψ) A)
      (Pi.single j b)=Pi.single j b) : A=1 := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.MatrixModule.applyMatrix, OAI.FiniteAlgebraicEnvelopes.correctedMap, OAI.FiniteAlgebraicEnvelopes.matrixNonunitalMap

  20. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.correctedUnits_eq_one line 164

    Source documentation

    In particular a corrected unit acting trivially on all columns was already the identity.

    theorem correctedUnits_eq_one (ψ : R →ₙ+* R) (b : V)
    (hb : ∀ r : R, ψ r • b=0 → r=0) (A : (Matrix (Fin 6) (Fin 6) R)ˣ)
    (hA : ∀ v : Multiplicative (Fin 6 → V), unitsAction (Steinberg.correctedUnits ψ A) v=v) : A=1 := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.MatrixModule.unitsAction, OAI.FiniteAlgebraicEnvelopes.Steinberg.correctedUnits

  21. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.stage line 178
  22. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.stage_mono line 180
  23. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.next_marker_not_mem line 184
  24. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.stage_strict line 191
  25. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.marker_ne line 198
  26. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.markers_injective line 208
  27. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.infinite_of_marker line 216
  28. instance OAI.FiniteAlgebraicEnvelopes.SequentialLimit.countable_limit line 219
  29. def OAI.FiniteAlgebraicEnvelopes.ColumnLimit.transition line 227
  30. theorem OAI.FiniteAlgebraicEnvelopes.ColumnLimit.transition_injective line 232
  31. theorem OAI.FiniteAlgebraicEnvelopes.ColumnLimit.one_not_range line 238
  32. def OAI.FiniteAlgebraicEnvelopes.ColumnLimit.marker line 244
  33. theorem OAI.FiniteAlgebraicEnvelopes.ColumnLimit.marker_not_range line 246
  34. theorem OAI.FiniteAlgebraicEnvelopes.ColumnLimit.limit_infinite line 252
  35. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.exists_common_stage₂ line 264
  36. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.exists_common_stage₃ line 272
  37. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.compatible_pow line 289
  38. def OAI.FiniteAlgebraicEnvelopes.LimitAction.applyLimit line 297
  39. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.applyLimit_of line 301
  40. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.applyLimit_one line 307
  41. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.applyLimit_mul line 313
  42. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.applyLimit_mul_vec line 319
  43. def OAI.FiniteAlgebraicEnvelopes.LimitAction.action line 324
  44. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.action_of line 334
  45. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.action_injective line 338

    Source documentation

    Detection after one transition suffices for faithfulness on the direct limit.

    theorem action_injective (hg : Function.Injective g)
    (hd : ∀ x : Q, (∀ v : V, α (f x) v=v) → x=1) : Function.Injective (action α f g hc) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.LimitAction.action

  46. def OAI.FiniteAlgebraicEnvelopes.MatrixModule.elementaryAction line 362
  47. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.elementaryAction_quotient line 365
  48. abbrev OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.LinearGroup line 375
  49. abbrev OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.Columns line 376
  50. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.linearAction line 378
  51. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.linearStep line 380
  52. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.columnStep line 381
  53. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.linear_column_compatible line 383
  54. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.limitAction line 389
  55. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.limitAction_injective line 392
  56. def OAI.FiniteAlgebraicEnvelopes.MatrixModule.columnEquiv line 406
  57. theorem OAI.FiniteAlgebraicEnvelopes.MatrixModule.columnEquiv_action line 409
  58. def OAI.FiniteAlgebraicEnvelopes.MatrixModule.affineEquiv line 419
  59. theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.affine_finitePresentation line 433

    Source documentation

    The manuscript cyclic-module and finite relative-presentation lemmas assembled. The Steinberg finite-presentation premise is precisely the separate cited theorem.

    theorem affine_finitePresentation (S : Set B) (hS : S.Finite) (hgen : Algebra.adjoin (ZMod 2) S=⊤)
    [Group.IsFinitelyPresented (Steinberg.Group (Fin 6) (Coeff (ZMod 2) B))] :
    Group.IsFinitelyPresented (AffineAction.Group (R:=Coeff (ZMod 2) B) (V:=B)) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Enveloping.Coeff, OAI.FiniteAlgebraicEnvelopes.AffineAction.Group

  60. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.transitive_nonone line 467

    Source documentation

    One step into the simple-algebra image gives transitivity in the limit.

    theorem transitive_nonone
    (ht : ∀ v w : V, v≠1 → w≠1 → ∃ x : Q, α x (g v)=g w)
    (v w : Limit g) (hv : v≠1) (hw : w≠1) :
    ∃ x : Limit f, action α f g hc x v=w := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.LimitAction.action

  61. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.action_shift line 479

    Source documentation

    The stage shift intertwines the actual linear limit actions.

    theorem action_shift (x : Limit f) (v : Limit g) :
    action α f g hc (shift f x) (shift g v)=shift g (action α f g hc x v) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.LimitAction.action

  62. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.action_shift_inv line 484
  63. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.action_shift_zpow line 489
  64. def OAI.FiniteAlgebraicEnvelopes.LimitAction.torusAction line 504
  65. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.torusAction_apply line 513
  66. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.torusAction_inl line 516
  67. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.shift_pow_of line 520
  68. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.ne_positive_shift line 531

    Source documentation

    A finite-stage linear element cannot be a strictly advancing shift.

    theorem ne_positive_shift (hg : Function.Injective g) {w : V} (hw : w∉Set.range g)
    (x : Limit f) (n : ℕ) (hn : 0<n) : action α f g hc x≠(shift g)^n := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.LimitAction.action

  69. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.shift_exponent_zero line 544
  70. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.torusAction_injective line 560
  71. def OAI.FiniteAlgebraicEnvelopes.LimitAction.affineStep line 575
  72. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineStep_left line 578
  73. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineStep_right line 579
  74. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineStep_pow_left line 581
  75. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineStep_pow_right line 590
  76. abbrev OAI.FiniteAlgebraicEnvelopes.LimitAction.AffineLimit line 599
  77. def OAI.FiniteAlgebraicEnvelopes.LimitAction.affineStage line 601
  78. def OAI.FiniteAlgebraicEnvelopes.LimitAction.affineLimitMap line 604
  79. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineLimitMap_of line 608
  80. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.pow_map_one_later line 611
  81. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineLimitMap_injective line 618
  82. theorem OAI.FiniteAlgebraicEnvelopes.LimitAction.affineLimitMap_surjective line 637
  83. def OAI.FiniteAlgebraicEnvelopes.LimitAction.affineLimitEquivalence line 643