OAI/AlgebraicGeometry/CharacterVarieties/Cutting/AtomicFrames.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Frames from labeled atoms

This formalizes the band reconstruction for filtered surface local systems in Integral points on character varieties of curves.

  1. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData line 21

    Source documentation

    A literal local decomposition into labeled atoms. It remembers the same atom across every paired germ and the unique child containing each parent atom. In applications atoms are the actual simultaneous graded basis vectors, not just intersection dimensions.

    structure AtomicData (k : Kind) (A : Type*) where
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind

  2. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.Fiber line 29
  3. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.rank line 31
  4. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.enum line 32
  5. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.child_containment line 44
  6. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.flattenFun line 47
  7. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.flattenFun_bijective line 51
  8. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.flatten line 65
  9. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.sum_rank line 71
  10. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.localRanks line 75
  11. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.portEquiv line 81

    Source documentation

    Literal ordered child basis into the parent's basis, preserving atom names.

    def portEquiv (p : k.table.Port) : D.localRanks.Columns p ≃ D.localRanks.Parent p :=
…
  12. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.atom line 85
  13. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.atom_injective line 88
  14. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.atom_port line 91
  15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.atom_cast line 98
  16. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.atom_corner line 110
  17. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.frame line 116
  18. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.passage_atom_column line 131
  19. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.passage_atom_parent line 136
  20. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.passage_equiv_eq line 140
  21. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.passage_comparison_eq line 149
  22. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.split_atom_parent line 158
  23. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.split_refinement_atom line 162
  24. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.split_equiv_eq line 179
  25. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.split_comparison_eq line 190
  26. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.forward line 198
  27. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.merge_comparison_eq line 204
  28. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.comparison_eq line 211

    Source documentation

    All actual allowed-vertex frames are induced by the SAME labeled atoms. This is a necessary local producer, not an assumed lower-diagram lift.

    theorem comparison_eq {k : Kind} (D : AtomicData k A) :
    let z := LocalRanks.comparison k D.localRanks (D.frame (R:=R))
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.comparison

  29. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.comparison_holds line 221