OAI/Algebra/Finitistic/Encoding/QuadraticPresentation.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.QuadraticPresentation.word line 11
2. theorem OAI.LittleFinitistic.QuadraticPresentation.word_nil line 13
3. theorem OAI.LittleFinitistic.QuadraticPresentation.word_append line 14
4. theorem OAI.LittleFinitistic.QuadraticPresentation.word_singleton line 17
5. def OAI.LittleFinitistic.QuadraticPresentation.coefficients line 20
6. theorem OAI.LittleFinitistic.QuadraticPresentation.expansion line 23
7. def OAI.LittleFinitistic.QuadraticPresentation.degreeLE line 33

   Source documentation

   Degree at most n means an R-linear combination of words of length at most n. This definition includes zero, constants, and linear terms.

   def degreeLE (n : ℕ) : Submodule R (FreeAlgebra R α) :=
   …

8. theorem OAI.LittleFinitistic.QuadraticPresentation.word_mem_degreeLE line 37
9. theorem OAI.LittleFinitistic.QuadraticPresentation.one_mem_degreeLE line 41
10. theorem OAI.LittleFinitistic.QuadraticPresentation.generator_mem_degreeLE line 44
11. theorem OAI.LittleFinitistic.QuadraticPresentation.product_mem_degreeLE line 47
12. theorem OAI.LittleFinitistic.QuadraticPresentation.exists_word_bound line 53

    Source documentation

    A single common bound for every monomial in finitely many relations.

    theorem exists_word_bound {κ : Type*} [Finite κ] (p : κ → FreeAlgebra R α) :
        ∃ N : ℕ, ∀ i w, w ∈ (coefficients R α (p i)).support → w.toList.length ≤ N := by
    …

    Mentions: OAI.LittleFinitistic.QuadraticPresentation.coefficients

13. abbrev OAI.LittleFinitistic.QuadraticPresentation.Word line 66
14. abbrev OAI.LittleFinitistic.QuadraticPresentation.Letter line 67
15. abbrev OAI.LittleFinitistic.QuadraticPresentation.Step line 68
16. instance OAI.LittleFinitistic.QuadraticPresentation.word_finite line 70
17. instance OAI.LittleFinitistic.QuadraticPresentation.step_finite line 73
18. def OAI.LittleFinitistic.QuadraticPresentation.wordPrefix line 81
19. def OAI.LittleFinitistic.QuadraticPresentation.extended line 84
20. def OAI.LittleFinitistic.QuadraticPresentation.inclusion line 86
21. def OAI.LittleFinitistic.QuadraticPresentation.eliminate line 89
22. def OAI.LittleFinitistic.QuadraticPresentation.encodeWord line 92
23. def OAI.LittleFinitistic.QuadraticPresentation.linearize line 95
24. theorem OAI.LittleFinitistic.QuadraticPresentation.eliminate_linearize line 98
25. theorem OAI.LittleFinitistic.QuadraticPresentation.linearize_degree line 107
26. abbrev OAI.LittleFinitistic.QuadraticPresentation.EquationIndex line 119
27. def OAI.LittleFinitistic.QuadraticPresentation.relation line 121
28. theorem OAI.LittleFinitistic.QuadraticPresentation.relation_degree line 127
29. def OAI.LittleFinitistic.QuadraticPresentation.original line 134
30. def OAI.LittleFinitistic.QuadraticPresentation.quadratic line 137
31. abbrev OAI.LittleFinitistic.QuadraticPresentation.Original line 140
32. abbrev OAI.LittleFinitistic.QuadraticPresentation.Quadratic line 141
33. def OAI.LittleFinitistic.QuadraticPresentation.originalMap line 143
34. def OAI.LittleFinitistic.QuadraticPresentation.quadraticMap line 145
35. theorem OAI.LittleFinitistic.QuadraticPresentation.original_relation line 148
36. theorem OAI.LittleFinitistic.QuadraticPresentation.quadratic_relation line 151
37. def OAI.LittleFinitistic.QuadraticPresentation.oldInNew line 157
38. theorem OAI.LittleFinitistic.QuadraticPresentation.auxiliary_eq_word line 161

    Source documentation

    Every auxiliary prefix generator equals its original word in the quotient.

    theorem auxiliary_eq_word (w : List α) (h : w.length ≤ N) :
        quadraticMap R α p N (FreeAlgebra.ι R (.inr ⟨w,h⟩)) =
          oldInNew R α p N (word R α w) := by
    …

    Mentions: OAI.LittleFinitistic.QuadraticPresentation.quadraticMap, OAI.LittleFinitistic.QuadraticPresentation.oldInNew, OAI.LittleFinitistic.QuadraticPresentation.word

39. theorem OAI.LittleFinitistic.QuadraticPresentation.linearize_in_quotient line 178
40. theorem OAI.LittleFinitistic.QuadraticPresentation.eliminate_relation line 191
41. def OAI.LittleFinitistic.QuadraticPresentation.toOriginal line 199
42. def OAI.LittleFinitistic.QuadraticPresentation.toQuadratic line 205
43. theorem OAI.LittleFinitistic.QuadraticPresentation.toOriginal_quotient line 213
44. theorem OAI.LittleFinitistic.QuadraticPresentation.toQuadratic_quotient line 217
45. theorem OAI.LittleFinitistic.QuadraticPresentation.original_roundtrip line 221

    Source documentation

    Eliminating auxiliaries after including the old generators fixes the old algebra.

    theorem original_roundtrip :
        (toOriginal R α p N bound).comp (toQuadratic R α p N bound) =
          AlgHom.id R (Original R α p) := by
    …

    Mentions: OAI.LittleFinitistic.QuadraticPresentation.toOriginal, OAI.LittleFinitistic.QuadraticPresentation.toQuadratic, OAI.LittleFinitistic.QuadraticPresentation.Original

46. theorem OAI.LittleFinitistic.QuadraticPresentation.quadratic_roundtrip line 236

    Source documentation

    Prefix equations prove that the other composite fixes every new generator too.

    theorem quadratic_roundtrip :
        (toQuadratic R α p N bound).comp (toOriginal R α p N bound) =
          AlgHom.id R (Quadratic R α p N) := by
    …

    Mentions: OAI.LittleFinitistic.QuadraticPresentation.toQuadratic, OAI.LittleFinitistic.QuadraticPresentation.toOriginal, OAI.LittleFinitistic.QuadraticPresentation.Quadratic

47. def OAI.LittleFinitistic.QuadraticPresentation.quadraticEquiv line 259

    Source documentation

    An algebra equivalence with mutually inverse composites.

    def quadraticEquiv : Quadratic R α p N ≃ₐ[R] Original R α p :=
    …

    Mentions: OAI.LittleFinitistic.QuadraticPresentation.Quadratic, OAI.LittleFinitistic.QuadraticPresentation.Original

48. theorem OAI.LittleFinitistic.QuadraticPresentation.equations_eq_zero line 266

    Source documentation

    Converting arbitrary equations to zero relations changes no quotient.

    theorem equations_eq_zero (lhs rhs : κ → FreeAlgebra R α) :
        ringConGen (fun x y => ∃ i, x = lhs i ∧ y = rhs i) =
          original R α (fun i => lhs i - rhs i) := by
    …

    Mentions: OAI.LittleFinitistic.QuadraticPresentation.original

49. def OAI.LittleFinitistic.QuadraticPresentation.HasFiniteQuadraticPresentation line 285

    Source documentation

    A finite noncommutative presentation whose zero relations have degree ≤ 2.

    def HasFiniteQuadraticPresentation (A : Type*) [Ring A] [Algebra R A] : Prop :=
    …

50. theorem OAI.LittleFinitistic.QuadraticPresentation.finite_zero_presentation_to_quadratic line 290

    Source documentation

    Finite prefix conversion of any finite family of polynomial zero relations.

    theorem finite_zero_presentation_to_quadratic (ι κ : Type) [Finite ι] [Finite κ]
        (p : κ → FreeAlgebra R ι) :
        HasFiniteQuadraticPresentation R (Original R ι p) := by
    …

    Mentions: OAI.LittleFinitistic.QuadraticPresentation.HasFiniteQuadraticPresentation, OAI.LittleFinitistic.QuadraticPresentation.Original

51. theorem OAI.LittleFinitistic.QuadraticPresentation.HasFiniteQuadraticPresentation.of_equiv line 299

    Source documentation

    Transport preserves every generator, relation, and degree bound.

    theorem HasFiniteQuadraticPresentation.of_equiv {A B : Type*} [Ring A] [Ring B]
        [Algebra R A] [Algebra R B] (h : HasFiniteQuadraticPresentation R A)
        (e : A ≃ₐ[R] B) : HasFiniteQuadraticPresentation R B := by
    …

    Mentions: OAI.LittleFinitistic.QuadraticPresentation.HasFiniteQuadraticPresentation

52. def OAI.LittleFinitistic.QuadraticPresentation.quotientCongr line 306

    Source documentation

    Equality of generated congruences gives an algebra equivalence of quotients.

    def quotientCongr {B : Type*} [Ring B] [Algebra R B]
        (c d : RingCon B) (h : c = d) : c.Quotient ≃ₐ[R] d.Quotient := by
    …

53. theorem OAI.LittleFinitistic.QuadraticPresentation.finite_presentation_to_quadratic line 314

    Source documentation

    Section 3, lines 22–31: every finitely presented associative unital algebra has a finite quadratic presentation, allowing linear and constant terms. Only the coefficient ring is commutative. The algebra itself need not be.

    theorem finite_presentation_to_quadratic {A : Type*} [Ring A] [Algebra R A]
        (h : GroupAlgebraPresentation.HasFinitePresentation R A) :
        HasFiniteQuadraticPresentation R A := by
    …

    Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.HasFinitePresentation, OAI.LittleFinitistic.QuadraticPresentation.HasFiniteQuadraticPresentation

54. theorem OAI.LittleFinitistic.QuadraticPresentation.finite_presentation_iff_quadratic line 326

    Source documentation

    The conversion also characterizes finite presentation: forgetting a degree bound yields the original finite noncommutative notion.

    theorem finite_presentation_iff_quadratic {A : Type*} [Ring A] [Algebra R A] :
        GroupAlgebraPresentation.HasFinitePresentation R A ↔
          HasFiniteQuadraticPresentation R A := by
    …

    Mentions: OAI.LittleFinitistic.GroupAlgebraPresentation.HasFinitePresentation, OAI.LittleFinitistic.QuadraticPresentation.HasFiniteQuadraticPresentation