OAI/Algebra/GroupRing/ComparisonCoding.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.TorsionFreeZeroDivisors.ComparisonCoding.Data line 13

   Source documentation

   Full integer affine comparison geometry. The offset uses [-2H,2H].

   structure Data (P E : Type*) (H : ℕ) where
   …

2. abbrev OAI.TorsionFreeZeroDivisors.ComparisonCoding.Code line 21
3. def OAI.TorsionFreeZeroDivisors.ComparisonCoding.coefficient line 25
4. lemma OAI.TorsionFreeZeroDivisors.ComparisonCoding.card_code line 27
5. lemma OAI.TorsionFreeZeroDivisors.ComparisonCoding.card_code_bound line 33
6. def OAI.TorsionFreeZeroDivisors.ComparisonCoding.encode line 48
7. structure OAI.TorsionFreeZeroDivisors.ComparisonCoding.Isomorphism line 54
8. theorem OAI.TorsionFreeZeroDivisors.ComparisonCoding.encode_complete line 66
9. def OAI.TorsionFreeZeroDivisors.SubdivisionIso.edge line 93
10. def OAI.TorsionFreeZeroDivisors.SubdivisionIso.interior line 94
11. def OAI.TorsionFreeZeroDivisors.SubdivisionIso.vertex line 95
12. def OAI.TorsionFreeZeroDivisors.SubdivisionIso.dart line 96
13. lemma OAI.TorsionFreeZeroDivisors.SubdivisionIso.point_eq line 101
14. lemma OAI.TorsionFreeZeroDivisors.SubdivisionIso.origin_eq line 115
15. lemma OAI.TorsionFreeZeroDivisors.SubdivisionIso.reverse_eq line 121
16. def OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.skeleton line 135
17. lemma OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.chosen_iff line 148
18. def OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.rep line 156
19. lemma OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.rep_length line 160
20. lemma OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.first_eq line 165
21. lemma OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.last_eq line 169
22. def OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.subdivided line 176

    Source documentation

    Exact canonical-rank suppression isomorphisms lift to actual subdivisions.

    def subdivided (f : Iso S S')
        (hrank : ∀ d,(Fintype.equivFin B' (f.dart d)).val=(Fintype.equivFin B d).val)
        (hlen : ∀ d,chainLength Γ mark h2 d=chainLength Γ' mark' h2' (f.dart d)) :
        Iso (ChainSubdivision.graph (repLength Γ mark h2) (first Γ mark h2) (last Γ mark h2))
          (ChainSubdivision.graph (repLength Γ' mark' h2') (first Γ' mark' h2') (last Γ' mark' h2')) where
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainSubdivision.graph

23. def OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.actual line 194
24. def OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.full line 204

    Source documentation

    No vertex or dart names survive, but all actual graph incidence does.

    def full (f : Iso S S')
        (hrank : ∀ d,(Fintype.equivFin B' (f.dart d)).val=(Fintype.equivFin B d).val)
        (hlen : ∀ d,chainLength Γ mark h2 d=chainLength Γ' mark' h2' (f.dart d)) : Iso Γ Γ' :=
    …

25. lemma OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.full_dartMap line 232
26. lemma OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.full_forward line 243
27. lemma OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.full_iter line 250
28. lemma OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.full_word line 272
29. lemma OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.full_seed line 305
30. lemma OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.full_vertexMap line 309
31. lemma OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.full_side line 324
32. lemma OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.full_words line 343
33. lemma OAI.TorsionFreeZeroDivisors.RankedSuppressionIso.full_source line 354