OAI/AlgebraicGeometry/CharacterVarieties/Foundation/VertexGauge.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sideCircle_boundary line 13
2. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sideCircle_facet line 18
3. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sideCircle_next line 23
4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sideCircle_prev line 28
5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sideCircle_mate line 34
6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portCircle_corner line 45
7. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CircleBases line 58

   Source documentation

   A basis at each old boundary circle; repeated facet labels do not identify these independent basing paths.

   abbrev CircleBases := (B : D.BoundaryCircle) →
   …

8. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sideBasis line 61
9. lemma OAI.IntegralCharacterVarieties.MatrixIso.finite_basis_transport line 73
10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sideBasis_corner line 90
11. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portBasis line 98
12. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portBasis_corner line 103
13. lemma OAI.IntegralCharacterVarieties.MatrixIso.reindex_eq_iff line 117
14. lemma OAI.IntegralCharacterVarieties.MatrixIso.block_reindex_sigma line 129
15. lemma OAI.IntegralCharacterVarieties.MatrixIso.block_reindex_sigmaRight line 142
16. theorem OAI.IntegralCharacterVarieties.MatrixIso.sum_blocks_unit_reindex line 148
17. theorem OAI.IntegralCharacterVarieties.MatrixIso.sum_three_blocks_reindex line 166
18. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases line 192

    Source documentation

    Fiber bases compatible across every vertex corner. For a Diagram this property is derived from bases on its boundary circles.

    structure CoherentBases where
    …

19. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.columns line 201
20. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.reframe line 204
21. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.vertexBases line 216
22. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.passage_columns line 231
23. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.passage_parent line 239
24. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.passage_reframe line 243
25. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.passage_holds line 254
26. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.split_prefix line 271
27. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.split_suffix line 281
28. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.split_branch_columns line 291
29. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.split_middle line 297
30. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.split_parent line 301
31. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.split_before_columns line 305
32. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.split_after_columns line 315
33. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.split_reframe line 327
34. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.split_holds line 349
35. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.CoherentBases.comparison_holds line 363

    Source documentation

    Every permitted vertex comparison is invariant under gauges indexed by its corner fibers. This includes merging, not just forward splitting.

    theorem CoherentBases.comparison_holds (G : d.CoherentBases (R:=R))
    …