OAI/GroupTheory/Hyperbolic/FullFilling.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Release075.FullFilling line 11

   Source documentation

   Unlike an ordinary filling, this records every connected component. The only nontriangular interior faces allowed are isolated two-dart spheres, created when an exterior cancellable pair is folded.

   structure FullFilling {E V : Type} (flip : E → E) (color : E → V)
       (face : E → E → E → Prop) (w : List E) where
   …

2. theorem OAI.Release075.IsBoundary.of_injective_map line 32
3. abbrev OAI.Release075.TriangleFilling.full line 48

   Source documentation

   Discarding components disjoint from the outer face makes an ordinary filling into a full filling, with no exceptional faces.

   noncomputable abbrev full {w : List E} (D : TriangleFilling flip color face w) :
       FullFilling flip color face w where
   …

   Mentions: OAI.Release075.TriangleFilling, OAI.Release075.FullFilling

4. def OAI.Release075.FullFilling.Bigon line 81
5. theorem OAI.Release075.FullFilling.bigon_reverse line 83
6. theorem OAI.Release075.FullFilling.bigon_next line 92
7. def OAI.Release075.FullFilling.trace line 105

   Source documentation

   Integral corner evaluation, with the outer face omitted.

   noncomputable def trace (F : E → E → E → M) : M :=
   …

8. abbrev OAI.Release075.FullFilling.rotate line 109
9. theorem OAI.Release075.FullFilling.trace_rotate line 124
10. abbrev OAI.Release075.FullFilling.mirror line 129
11. theorem OAI.Release075.FullFilling.trace_mirror line 167
12. theorem OAI.Release075.FullFilling.trace_empty line 201

    Source documentation

    A closed full filling is a disjoint union of triangular spheres and the explicit isolated bigons. Consequently its integral cyclic evaluation vanishes.

    theorem trace_empty
        (hempty : ∀ D : TriangleSphere flip color face, IsEmpty D.Dipole → IsEmpty D.Dart)
        (F : E → E → E → M)
        (hrot : ∀ a b c, face a b c → F b c a = F a b c)
        (hmir : ∀ a b c, face a b c → F (flip a) (flip c) (flip b) = -F a b c)
        (hdeg : ∀ a b, F a b a = 0)
        (D : FullFilling flip color face []) : D.trace F = 0 := by
    …

    Mentions: OAI.Release075.TriangleSphere, OAI.Release075.FullFilling

13. theorem OAI.Release075.FullFilling.bigon_component line 251
14. theorem OAI.Release075.FullFilling.fold line 260

    Source documentation

    Exterior cancellation retains all components and preserves the face chain.

    theorem fold {w : List E} (D : FullFilling flip color face w)
        (hflip : Function.Involutive flip) (hne : ∀ e, color e ≠ color (flip e))
        {a b : D.Dart} {l : List D.Dart} (hb : D.boundary = b::a::l)
        (hl : D.label a = flip (D.label b)) (F : E → E → E → M)
        (hdeg : ∀ a b, F a b a = 0) :
        ∃ D' : FullFilling flip color face (l.map D.label), D'.trace F = D.trace F := by
    …

    Mentions: OAI.Release075.FullFilling