OAI/Algebra/Finitistic/Selection/FinitePresentation.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Target: Group.IsFinitelyPresented Presentation.AuxiliaryGroup. Section 2, Lemma group-finite-presentation. No finite-presentation hypothesis is permitted on the target group. Diagonal W generators are redundant.

  1. def OAI.LittleFinitistic.FinitePresentation.orbit line 17
  2. theorem OAI.LittleFinitistic.FinitePresentation.orbit_zero line 19
  3. theorem OAI.LittleFinitistic.FinitePresentation.orbit_add line 21
  4. theorem OAI.LittleFinitistic.FinitePresentation.orbit_commute line 26
  5. theorem OAI.LittleFinitistic.FinitePresentation.orbit_covariance line 37
  6. theorem OAI.LittleFinitistic.FinitePresentation.family_zpow line 42
  7. abbrev OAI.LittleFinitistic.FinitePresentation.Lattice line 65
  8. def OAI.LittleFinitistic.FinitePresentation.coord line 67
  9. def OAI.LittleFinitistic.FinitePresentation.wtU line 69
  10. def OAI.LittleFinitistic.FinitePresentation.wtV line 71
  11. def OAI.LittleFinitistic.FinitePresentation.wtW line 73
  12. theorem OAI.LittleFinitistic.FinitePresentation.table_UU line 76

    Source comment

    Each theorem supplies the integral preimage in the corresponding table row.
    theorem table_UU (i j : Fin 3) (hij : i ≠ j) (r s : ℤ) :
    ∃ n : Lattice, wtU i n = r ∧ wtU j n = s := by
…

    Mentions: OAI.LittleFinitistic.FinitePresentation.Lattice, OAI.LittleFinitistic.FinitePresentation.wtU

  13. theorem OAI.LittleFinitistic.FinitePresentation.table_VV line 81
  14. theorem OAI.LittleFinitistic.FinitePresentation.table_UV line 86
  15. theorem OAI.LittleFinitistic.FinitePresentation.table_WU line 91
  16. theorem OAI.LittleFinitistic.FinitePresentation.table_WV line 100
  17. theorem OAI.LittleFinitistic.FinitePresentation.table_UW line 109
  18. theorem OAI.LittleFinitistic.FinitePresentation.table_WV_output line 114
  19. def OAI.LittleFinitistic.FinitePresentation.torus line 123
  20. theorem OAI.LittleFinitistic.FinitePresentation.family_torus line 125
  21. theorem OAI.LittleFinitistic.FinitePresentation.torus_U line 138
  22. theorem OAI.LittleFinitistic.FinitePresentation.torus_V line 146
  23. theorem OAI.LittleFinitistic.FinitePresentation.torus_W line 154
  24. structure OAI.LittleFinitistic.FinitePresentation.CovariantData line 167

    Source documentation

    Intermediate data: covariance plus only zero-argument algebraic relations. This is constructed below from a finite presented group, not postulated for it.

    structure CovariantData (G : Type*) [Group G] where
…
  25. def OAI.LittleFinitistic.FinitePresentation.CovariantData.act line 190
  26. theorem OAI.LittleFinitistic.FinitePresentation.CovariantData.act_U line 192
  27. theorem OAI.LittleFinitistic.FinitePresentation.CovariantData.act_V line 194
  28. theorem OAI.LittleFinitistic.FinitePresentation.CovariantData.act_W line 196
  29. def OAI.LittleFinitistic.FinitePresentation.CovariantData.toSelection line 200

    Source documentation

    All infinite relators follow from the finite zero-argument patterns.

    def toSelection : SelectionGroupData G where
…

    Mentions: OAI.LittleFinitistic.SelectionGroupData

  30. structure OAI.LittleFinitistic.FinitePresentation.SeedValues line 255

    Source documentation

    Finitely many seed values. Diagonal W seeds will be killed.

    structure SeedValues (G : Type*) where
…
  31. structure OAI.LittleFinitistic.FinitePresentation.SeedData line 261
  32. def OAI.LittleFinitistic.FinitePresentation.SeedData.toCovariant line 280
  33. def OAI.LittleFinitistic.FinitePresentation.SeedData.toSelection line 305
  34. inductive OAI.LittleFinitistic.FinitePresentation.SeedGenerator line 309
  35. inductive OAI.LittleFinitistic.FinitePresentation.Rule line 316
  36. def OAI.LittleFinitistic.FinitePresentation.equation line 333

    Source documentation

    Finite seed equation patterns. Vacuous index combinations give 1=1.

    def equation {G : Type*} [Group G] (D : SeedValues G) : Rule → G × G
  | .TT i j => (D.T i*D.T j, D.T j*D.T i)
  | .Tu l i => (D.T l*D.u i*(D.T l)⁻¹, orbit (D.T i) (D.u i) (if l=i then 1 else 0))
  | .Tv l i => (D.T l*D.v i*(D.T l)⁻¹, orbit (D.T i) (D.v i) (if l=i then 1 else 0))
  | .Tw l i j => (D.T l*D.w i j*(D.T l)⁻¹,
      orbit (D.T i) (D.w i j) ((if l=i then 1 else 0)-(if l=j then 1 else 0)))
  | .diagonal i => (D.w i i, 1)
  | .square i => (D.u i*D.u i, 1)
  | .UU i j => if i≠j then (D.u i*D.u j, D.u j*D.u i) else (1,1)
  | .VV i j => if i≠j then (D.v i*D.v j, D.v j*D.v i) else (1,1)
  | .UV i j => if i≠j then (D.u i*D.v j, D.v j*D.u i) else (1,1)
  | .WU i j h => if h≠i then (D.w i j*D.u h, D.u h*D.w i j) else (1,1)
…

    Mentions: OAI.LittleFinitistic.FinitePresentation.SeedValues, OAI.LittleFinitistic.FinitePresentation.Rule, OAI.LittleFinitistic.FinitePresentation.orbit

  37. def OAI.LittleFinitistic.FinitePresentation.freeSeeds line 349
  38. def OAI.LittleFinitistic.FinitePresentation.evalSeeds line 355
  39. theorem OAI.LittleFinitistic.FinitePresentation.equation_evaluate line 361
  40. def OAI.LittleFinitistic.FinitePresentation.relator line 366
  41. def OAI.LittleFinitistic.FinitePresentation.finiteRelators line 369
  42. abbrev OAI.LittleFinitistic.FinitePresentation.Model line 370
  43. instance OAI.LittleFinitistic.FinitePresentation.(instance at line 372) line 372
  44. instance OAI.LittleFinitistic.FinitePresentation.(instance at line 373) line 373
  45. def OAI.LittleFinitistic.FinitePresentation.modelValues line 375
  46. theorem OAI.LittleFinitistic.FinitePresentation.model_equation line 381
  47. def OAI.LittleFinitistic.FinitePresentation.modelSeedData line 393
  48. def OAI.LittleFinitistic.FinitePresentation.toModel line 410

    Source documentation

    The homomorphism from the supplied infinite presentation to the finite model.

    def toModel : Presentation.AuxiliaryGroup →* Model :=
…

    Mentions: OAI.LittleFinitistic.Presentation.AuxiliaryGroup, OAI.LittleFinitistic.FinitePresentation.Model

  49. theorem OAI.LittleFinitistic.FinitePresentation.selection_U_orbit line 417
  50. theorem OAI.LittleFinitistic.FinitePresentation.selection_V_orbit line 423
  51. theorem OAI.LittleFinitistic.FinitePresentation.selection_W_orbit line 429
  52. def OAI.LittleFinitistic.FinitePresentation.originalSeeds line 439

    Source documentation

    The original presentation satisfies each of the finite seed equations.

    def originalSeeds : SeedData G where
…

    Mentions: OAI.LittleFinitistic.FinitePresentation.SeedData

  53. theorem OAI.LittleFinitistic.FinitePresentation.seed_equation line 468
  54. def OAI.LittleFinitistic.FinitePresentation.modelLift line 501

    Source documentation

    Universal evaluation of the finite presentation in any proved seed data.

    def modelLift {G : Type*} [Group G] (D : SeedData G) : Model →* G :=
…

    Mentions: OAI.LittleFinitistic.FinitePresentation.SeedData, OAI.LittleFinitistic.FinitePresentation.Model

  55. theorem OAI.LittleFinitistic.FinitePresentation.modelLift_of line 509
  56. def OAI.LittleFinitistic.FinitePresentation.fromModel line 512
  57. theorem OAI.LittleFinitistic.FinitePresentation.map_orbit line 516
  58. theorem OAI.LittleFinitistic.FinitePresentation.toModel_T line 519
  59. theorem OAI.LittleFinitistic.FinitePresentation.toModel_U line 522
  60. theorem OAI.LittleFinitistic.FinitePresentation.toModel_V line 525
  61. theorem OAI.LittleFinitistic.FinitePresentation.toModel_W line 528
  62. theorem OAI.LittleFinitistic.FinitePresentation.fromModel_T line 532
  63. theorem OAI.LittleFinitistic.FinitePresentation.fromModel_u line 535
  64. theorem OAI.LittleFinitistic.FinitePresentation.fromModel_v line 538
  65. theorem OAI.LittleFinitistic.FinitePresentation.fromModel_w line 541
  66. theorem OAI.LittleFinitistic.FinitePresentation.fromModel_toModel line 545
  67. theorem OAI.LittleFinitistic.FinitePresentation.toModel_fromModel line 562
  68. def OAI.LittleFinitistic.FinitePresentation.presentationEquiv line 580

    Source documentation

    Equivalence of the explicit finite presentation and the supplied infinite presentation.

    def presentationEquiv : Model ≃* Presentation.AuxiliaryGroup where
…

    Mentions: OAI.LittleFinitistic.FinitePresentation.Model, OAI.LittleFinitistic.Presentation.AuxiliaryGroup

  69. theorem OAI.LittleFinitistic.FinitePresentation.auxiliaryGroup_isFinitelyPresented line 588

    Source documentation

    Section 2, Lemma group-finite-presentation, for the exact supplied AuxiliaryGroup.

    theorem auxiliaryGroup_isFinitelyPresented :
    Group.IsFinitelyPresented Presentation.AuxiliaryGroup :=
…

    Mentions: OAI.LittleFinitistic.Presentation.AuxiliaryGroup

  70. theorem OAI.LittleFinitistic.FinitePresentation.seedGenerator_card line 593

    Source documentation

    The finite model retains the three redundant diagonal W generators.

    theorem seedGenerator_card : Fintype.card SeedGenerator = 18 := by decide

    Mentions: OAI.LittleFinitistic.FinitePresentation.SeedGenerator

  71. theorem OAI.LittleFinitistic.FinitePresentation.rule_card line 595

    Source documentation

    Number of indexed finite equation patterns, including tautological cases.

    theorem rule_card : Fintype.card Rule = 159 := by decide +kernel

    Mentions: OAI.LittleFinitistic.FinitePresentation.Rule

  72. theorem OAI.LittleFinitistic.FinitePresentation.model_isFinitelyPresented line 597