OAI/AlgebraicGeometry/CharacterVarieties/Foundation/DiskGauge.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IntegralCharacterVarieties.FlagCircuit.Data.eq_of_constant_grade line 15

   Source documentation

   A surface equation is exact matrix equality: its single grade is zero.

   theorem eq_of_constant_grade (g : D.Solution A) (j : J)
       (h : ∀ i,D.grade j i=0) :
       (D.left j).eval (algebraMap R A) g.val=(D.right j).eval (algebraMap R A) g.val := by
   …

2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.evaluatedBoundaryEdge line 34
3. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.wordProduct_eval line 38
4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryWord_eval line 47
5. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.actual_surface_relation line 54
6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.surfaceWord_eval line 59
7. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.actual_disk_relation line 67

   Source documentation

   The exact rank-n disk step: genus zero and one boundary circle. All original punctures, full-ring units, side occurrences and their orientations are kept.

   theorem actual_disk_relation (f : F) (hg : D.genus f=0) (hb : D.boundaryCount f=1) :
       ((List.ofFn (D.evaluatedBoundaryEdge P g f ⟨0,by omega⟩)).reverse).prod=
         (D.surfaceTarget P f).eval (algebraMap R A) g.val.val := by
   …

8. def OAI.IntegralCharacterVarieties.DiskGauge.prefixTransport line 93

   Source documentation

   Parallel transport from the distinguished starting fiber. The first edge acts first, matching Diagram.boundaryWord exactly.

   def prefixTransport (i : ℕ) : G := ((List.ofFn h).take i).reverse.prod

9. def OAI.IntegralCharacterVarieties.DiskGauge.next line 95
10. theorem OAI.IntegralCharacterVarieties.DiskGauge.prefix_zero line 98
11. theorem OAI.IntegralCharacterVarieties.DiskGauge.prefix_full line 99
12. theorem OAI.IntegralCharacterVarieties.DiskGauge.prefix_step line 103
13. lemma OAI.IntegralCharacterVarieties.DiskGauge.next_within line 108
14. lemma OAI.IntegralCharacterVarieties.DiskGauge.next_last line 110
15. theorem OAI.IntegralCharacterVarieties.DiskGauge.normalized_edge line 116

    Source documentation

    Exact normal form of the old cyclic transport. All gauges are units in the original base ring when G is GL, not merely rationally invertible matrices.

    theorem normalized_edge (i : Fin n) :
        (prefixTransport h (next i).val)⁻¹*h i*prefixTransport h i.val=
          if i.val+1<n then 1 else (List.ofFn h).reverse.prod := by
    …

    Mentions: OAI.IntegralCharacterVarieties.DiskGauge.prefixTransport, OAI.IntegralCharacterVarieties.DiskGauge.next

16. theorem OAI.IntegralCharacterVarieties.DiskGauge.edge_factorization line 127

    Source documentation

    This is a factorization of every old edge, not replacement of it by an independent block diagonal edge.

    theorem edge_factorization (i : Fin n) :
        h i*prefixTransport h i.val=prefixTransport h (next i).val *
          (if i.val+1<n then 1 else (List.ofFn h).reverse.prod) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.DiskGauge.prefixTransport, OAI.IntegralCharacterVarieties.DiskGauge.next

17. theorem OAI.IntegralCharacterVarieties.HomTransport.matrixUnitEquiv_mul_apply line 138
18. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.scalarUnit_one line 149
19. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.map_scalarUnit line 151
20. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.scalarUnit_apply line 157
21. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.diskScalar line 166
22. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.surfaceTarget_eval line 169
23. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.actual_disk_scalar line 174
24. def OAI.IntegralCharacterVarieties.DiskGauge.frame line 188

    Source documentation

    Changing frames never alters the old edge transport.

    def frame (i : Fin m) : (Fin n → R) ≃ₗ[R] (Fin n → R) :=
    …

25. def OAI.IntegralCharacterVarieties.DiskGauge.scalarAt line 191
26. lemma OAI.IntegralCharacterVarieties.DiskGauge.scalarAt_factorization line 194
27. theorem OAI.IntegralCharacterVarieties.DiskGauge.edge_frame line 200

    Source documentation

    The diagram edge preserves the transported U and induces the same scalar on U and V/U in their transported frames.

    theorem edge_frame (i : Fin m) (v : Fin n → R) :
        matrixUnitEquiv (h i) (frame h i v)=frame h (next i) ((scalarAt u i:R) • v) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.DiskGauge.frame, OAI.IntegralCharacterVarieties.DiskGauge.next, OAI.IntegralCharacterVarieties.DiskGauge.scalarAt

28. def OAI.IntegralCharacterVarieties.DiskGauge.parallelSubspace line 208
29. def OAI.IntegralCharacterVarieties.DiskGauge.subFrame line 210
30. def OAI.IntegralCharacterVarieties.DiskGauge.quotientFrame line 213
31. theorem OAI.IntegralCharacterVarieties.DiskGauge.edge_subspace line 216
32. def OAI.IntegralCharacterVarieties.DiskGauge.subEdge line 229
33. def OAI.IntegralCharacterVarieties.DiskGauge.quotientEdge line 232
34. theorem OAI.IntegralCharacterVarieties.DiskGauge.subEdge_frame line 236
35. theorem OAI.IntegralCharacterVarieties.DiskGauge.quotientEdge_frame line 242
36. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.diskBoundaryEdge line 261
37. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.diskSubspace line 264

    Source documentation

    Lower U fibers, read from the old solution, including the initial fiber and last-to-first edge.

    def diskSubspace (i : Fin (D.boundaryLength f ⟨0,by omega⟩)) :=
    …

38. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.diskSubFrame line 267
39. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.diskQuotientFrame line 271
40. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.diskSubEdge line 275
41. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.diskQuotientEdge line 279
42. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.actual_disk_forward line 285

    Source documentation

    Every old rank-n scalar disk has the required parallel subspace and quotient. Both are restrictions/quotients of the old transports.

    theorem actual_disk_forward (i : Fin (D.boundaryLength f ⟨0,by omega⟩)) :
        ((D.diskSubspace P g f hb U i).map
          (matrixUnitEquiv (D.diskBoundaryEdge P g f hb i)).toLinearMap =
          D.diskSubspace P g f hb U (next i)) ∧
        (∀ v : U, D.diskSubEdge P g f hg hb U i (D.diskSubFrame P g f hb U i v)=
          D.diskSubFrame P g f hb U (next i) ((scalarAt (D.diskScalar (A:=A) P f) i:A) • v)) ∧
    …