OAI/GroupTheory/BooneHigman/Affine.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteAlgebraicEnvelopes.AffinePresentation.X line 19
2. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.X_zero line 21
3. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.X_add line 22
4. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.X_neg line 24
5. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.X_chain line 25
6. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.X_distant line 28
7. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.fresh line 31
8. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.commutator_commute line 42
9. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.coefficients line 48

   Source documentation

   The finite coefficient relations propagate to every coefficient.

   theorem coefficients (F : Finset R) (h1 : (1:R) ∈ F)
       (hgen : Subring.closure (↑F : Set R) = ⊤)
       (hc : ∀ r ∈ F, ∀ a b c : Fin 6, c ≠ b → Commute (X ρ a b r) (p c)) :
       ∀ r : R, ∀ a b c : Fin 6, c ≠ b → Commute (X ρ a b r) (p c) := by
   …

   Mentions: OAI.FiniteAlgebraicEnvelopes.AffinePresentation.X

10. def OAI.FiniteAlgebraicEnvelopes.AffinePresentation.wcolumn line 72
11. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.conj_of_commute line 74
12. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.mul_eq_commutator line 77
13. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.wcolumn_independent line 83

    Source documentation

    Independence of the auxiliary column in the presentation.

    theorem wcolumn_independent (a b h : Fin 6) (hab : a ≠ b) (hah : a ≠ h) (hbh : b ≠ h) (r : R) :
        wcolumn ρ p a b r = wcolumn ρ p a h r := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.AffinePresentation.wcolumn

14. def OAI.FiniteAlgebraicEnvelopes.AffinePresentation.other line 104
15. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.other_ne line 107
16. def OAI.FiniteAlgebraicEnvelopes.AffinePresentation.w line 109
17. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.w_eq_column line 111
18. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.w_commute_p line 117
19. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.w_commute_X line 122
20. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.w_commute line 129
21. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.w_zero line 136
22. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.w_add line 139
23. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.w_one line 150
24. def OAI.FiniteAlgebraicEnvelopes.AffinePresentation.wAdd line 153
25. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.root_conjugation line 159

    Source documentation

    This is exactly the elementary action on a column, derived in the presentation.

    theorem root_conjugation (c a : Fin 6) (hca : c ≠ a) (s r : R) :
        MulAut.conj (X ρ c a s) (w ρ p a r) = w ρ p a r * w ρ p c (s*r) := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.AffinePresentation.X, OAI.FiniteAlgebraicEnvelopes.AffinePresentation.w

26. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.w_span line 175

    Source documentation

    The finite ideal relations imply all relations in the left ideal they generate.

    theorem w_span (D : Set R) (hd : ∀ d ∈ D, ∀ a b, a ≠ b → ⁅X ρ a b d, p b⁆ = 1)
        {r : R} (hr : r ∈ Submodule.span R D) (c : Fin 6) : w ρ p c r = 1 := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.AffinePresentation.X, OAI.FiniteAlgebraicEnvelopes.AffinePresentation.w

27. def OAI.FiniteAlgebraicEnvelopes.AffinePresentation.rowMap line 192
28. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.rowMap_mk line 197
29. def OAI.FiniteAlgebraicEnvelopes.AffinePresentation.translationsAdd line 200
30. def OAI.FiniteAlgebraicEnvelopes.AffinePresentation.translations line 207
31. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.translations_single line 211
32. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.translations_single_mk line 217
33. def OAI.FiniteAlgebraicEnvelopes.AffineAction.transvection line 228

    Source documentation

    A matrix elementary operation on columns in an arbitrary left module.

    def transvection (a b : Fin 6) (hab : a ≠ b) (r : R) : (Fin 6 → V) ≃+ (Fin 6 → V) where
    …

34. theorem OAI.FiniteAlgebraicEnvelopes.AffineAction.transvection_apply line 241
35. def OAI.FiniteAlgebraicEnvelopes.AffineAction.elementary line 244
36. theorem OAI.FiniteAlgebraicEnvelopes.AffineAction.elementary_apply line 247
37. theorem OAI.FiniteAlgebraicEnvelopes.AffineAction.elementary_column line 252

    Source documentation

    The elementary displacement is supported in the one prescribed row.

    theorem elementary_column (a b : Fin 6) (hab) (r : R) (v : Fin 6 → V) :
        (elementary a b hab r (Multiplicative.ofAdd v)).toAdd = v + Pi.single a (r • v b) := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.AffineAction.elementary

38. theorem OAI.FiniteAlgebraicEnvelopes.AffineAction.elementary_add line 260
39. theorem OAI.FiniteAlgebraicEnvelopes.AffineAction.elementary_zero line 270
40. theorem OAI.FiniteAlgebraicEnvelopes.AffineAction.elementary_neg line 278
41. theorem OAI.FiniteAlgebraicEnvelopes.AffineAction.elementary_chain line 283
42. theorem OAI.FiniteAlgebraicEnvelopes.AffineAction.elementary_distant line 299
43. def OAI.FiniteAlgebraicEnvelopes.AffineAction.action line 314

    Source documentation

    The actual Steinberg action, with its three defining relations verified.

    def action : Steinberg.Group (Fin 6) R →* MulAut (Multiplicative (Fin 6 → V)) :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group

44. theorem OAI.FiniteAlgebraicEnvelopes.AffineAction.action_root line 329
45. abbrev OAI.FiniteAlgebraicEnvelopes.AffineAction.Group line 332
46. theorem OAI.FiniteAlgebraicEnvelopes.AffineAction.equivariant_of_roots line 336

    Source documentation

    It suffices to check equivariance on actual Steinberg generators.

    theorem equivariant_of_roots {Q : Type*} [_root_.Group Q]
        (τ : Multiplicative (Fin 6 → V) →* Q) (ρ : Steinberg.Group (Fin 6) R →* Q)
        (hr : ∀ a b hab r v, τ (elementary a b hab r v) =
          MulAut.conj (ρ (Steinberg.root a b hab r)) (τ v)) :
        ∀ g v, τ (action (R:=R) (V:=V) g v) = MulAut.conj (ρ g) (τ v) := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.AffineAction.elementary, OAI.FiniteAlgebraicEnvelopes.Steinberg.root, OAI.FiniteAlgebraicEnvelopes.AffineAction.action

47. theorem OAI.FiniteAlgebraicEnvelopes.AffinePresentation.translations_equivariant line 384

    Source documentation

    The finite presentation relations build an actual semidirect-product homomorphism.

    theorem translations_equivariant (g : Steinberg.Group (Fin 6) R) :
        (translations ρ p hp hc hu D hd).comp (AffineAction.action g).toMonoidHom =
          (MulAut.conj (ρ g)).toMonoidHom.comp (translations ρ p hp hc hu D hd) := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.AffinePresentation.translations, OAI.FiniteAlgebraicEnvelopes.AffineAction.action

48. def OAI.FiniteAlgebraicEnvelopes.AffinePresentation.lift line 418
49. theorem OAI.FiniteAlgebraicEnvelopes.AffineAction.root_translation line 427

    Source documentation

    Commutators with a root are the elementary displacement, not an assumed action law.

    theorem root_translation (a b : Fin 6) (hab : a ≠ b) (r : R) (v : Fin 6 → V) :
        ⁅(SemidirectProduct.inr (Steinberg.root a b hab r) : Group (R:=R) (V:=V)),
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.root, OAI.FiniteAlgebraicEnvelopes.AffineAction.Group

50. abbrev OAI.FiniteAlgebraicEnvelopes.FiniteAffine.Free line 444
51. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.freeP line 445
52. abbrev OAI.FiniteAlgebraicEnvelopes.FiniteAffine.freeX line 446
53. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.relatorPP line 448
54. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.relatorC line 449
55. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.relatorU line 451
56. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.relatorD line 453
57. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.relators line 455
58. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.N line 457
59. instance OAI.FiniteAlgebraicEnvelopes.FiniteAffine.(instance at line 458) line 458
60. abbrev OAI.FiniteAlgebraicEnvelopes.FiniteAffine.Presentation line 459
61. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.base line 460
62. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.p line 462
63. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.killRelator line 465
64. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.p_commute line 469
65. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.central_finite line 475
66. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.unit line 482
67. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.ideal line 490
68. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.central line 498
69. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.fromAffine line 502
70. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.finitelyPresented line 506
71. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.translation line 513
72. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.translation_zero line 517
73. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.root_translation line 520
74. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.freeMap line 531
75. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.freeMap_P line 534
76. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.freeMap_X line 536
77. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.freeMap_relators line 540
78. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.toAffine line 569
79. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.toAffine_base line 575
80. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.toAffine_p line 579
81. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.fromAffine_inr line 583
82. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.fromAffine_translation line 586
83. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.hom_ext line 593

    Source documentation

    The quotient is generated by its base and its six designated translations.

    theorem hom_ext {Q : Type*} [Group Q] {f g : Presentation F D →* Q}
        (hb : f.comp (base F D) = g.comp (base F D)) (hp : ∀ a, f (p F D a) = g (p F D a)) : f=g := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.FiniteAffine.Presentation, OAI.FiniteAlgebraicEnvelopes.FiniteAffine.base, OAI.FiniteAlgebraicEnvelopes.FiniteAffine.p

84. def OAI.FiniteAlgebraicEnvelopes.FiniteAffine.equivalence line 602

    Source documentation

    The natural affine quotient has no additional kernel.

    noncomputable def equivalence : Presentation F D ≃*
        AffineAction.Group (R:=R) (V:= R ⧸ Submodule.span R (↑D : Set R)) := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.FiniteAffine.Presentation, OAI.FiniteAlgebraicEnvelopes.AffineAction.Group

85. theorem OAI.FiniteAlgebraicEnvelopes.FiniteAffine.affine_finitelyPresented line 630