OAI/Algebra/Finitistic/Encoding/PresentationReindex.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.PresentationReindex.renameHom line 13
2. theorem OAI.LittleFinitistic.PresentationReindex.rename_ι line 16
3. def OAI.LittleFinitistic.PresentationReindex.rename line 20
4. theorem OAI.LittleFinitistic.PresentationReindex.rename_apply line 25
5. theorem OAI.LittleFinitistic.PresentationReindex.rename_word line 27
6. lemma OAI.LittleFinitistic.PresentationReindex.rename_degree line 33
7. def OAI.LittleFinitistic.PresentationReindex.renamedRelation line 45
8. def OAI.LittleFinitistic.PresentationReindex.forward line 47
9. def OAI.LittleFinitistic.PresentationReindex.backward line 55
10. theorem OAI.LittleFinitistic.PresentationReindex.forward_mk line 63
11. theorem OAI.LittleFinitistic.PresentationReindex.backward_mk line 67
12. def OAI.LittleFinitistic.PresentationReindex.presentationEquiv line 72

    Source documentation

    Relabeling finite generators and relations preserves the actual presented algebra.

    noncomputable def presentationEquiv : Original k α p ≃ₐ[k] Original k β (renamedRelation e j p) :=
    …

    Mentions: OAI.LittleFinitistic.PresentationReindex.renamedRelation

13. theorem OAI.LittleFinitistic.PresentationReindex.exists_relations line 90

    Source documentation

    Every finite list of quadratic polynomials has the concrete coefficient interface used by the three-vertex algebra.

    theorem exists_relations {d t : ℕ} (p : Fin t → FreeAlgebra k (Fin d))
        (hp : ∀ i, p i ∈ degreeLE k (Fin d) 2) :
        ∃ P : QuadraticEncoding.Relations k d t, ∀ i, QuotientAction.polynomial P i = p i := by
    …

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.Relations, OAI.LittleFinitistic.QuotientAction.polynomial

14. theorem OAI.LittleFinitistic.PresentationReindex.finite_quadratic_encoding line 103

    Source documentation

    Finite generator and equation types may both be replaced by Fin, and all coefficient choices preserve the exact quotient algebra.

    theorem finite_quadratic_encoding [Finite α] [Finite κ]
        (p : κ → FreeAlgebra k α) (hp : ∀ i, p i ∈ degreeLE k α 2) :
        ∃ (d t : ℕ) (P : QuadraticEncoding.Relations k d t),
          Nonempty (Original k (Fin d) (QuotientAction.polynomial P) ≃ₐ[k] Original k α p) := by
    …

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.Relations, OAI.LittleFinitistic.QuotientAction.polynomial

15. theorem OAI.LittleFinitistic.PresentationReindex.auxiliaryGroupAlgebra_has_encoding line 121

    Source documentation

    The entire actual complex group algebra feeds the finite directed encoding.

    theorem auxiliaryGroupAlgebra_has_encoding :
        ∃ (d t : ℕ) (P : QuadraticEncoding.Relations ℂ d t),
          Nonempty (Original ℂ (Fin d) (QuotientAction.polynomial P) ≃ₐ[ℂ]
            MonoidAlgebra ℂ Presentation.AuxiliaryGroup) := by
    …

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.Relations, OAI.LittleFinitistic.QuotientAction.polynomial, OAI.LittleFinitistic.Presentation.AuxiliaryGroup