OAI/AlgebraicGeometry/CharacterVarieties/Frames/Endpoints.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.basis_at_color line 13
  2. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.firstArity line 29
  3. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.firstChild line 33
  4. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.firstChild_color line 36
  5. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.firstParent_rank line 45
  6. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.firstChild_rank line 49
  7. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.firstColumns line 55
  8. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.firstFrame line 59
  9. lemma OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv_block line 70
  10. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.reframe_inverse line 82
  11. lemma OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv_reindex_symm line 102
  12. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.fiberEnum_atom line 114
  13. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.parentGauge_inverse line 124
  14. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.rowGauge_apply line 127
  15. lemma OAI.IntegralCharacterVarieties.MatrixIso.apply_of_reindex line 142
  16. lemma OAI.IntegralCharacterVarieties.MatrixIso.symm_apply_of_reindex line 148
  17. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.first_parent_inverse line 161
  18. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.first_frame_inverse line 175
  19. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.firstFrame_eq line 216
  20. theorem OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.firstFrame_holds line 226

    Source documentation

    The first gallery frame preserves the named quotient maps of the original frame.

    theorem firstFrame_holds : SameFramedFlag (fun i : (i : Fin n) × Fin (s i) => i.1.val)
    w.firstFrame f := by
…

    Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag

  21. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.lastArity line 241
  22. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.lastChild line 245
  23. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.lastChild_color line 248
  24. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.lastParent_rank line 257
  25. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.lastChild_rank line 261
  26. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.lastColumns line 267
  27. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.lastFrame line 271
  28. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.colGauge_apply line 275
  29. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.last_parent_inverse line 293
  30. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.last_frame_inverse line 307
  31. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.lastFrame_eq line 348
  32. theorem OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.lastFrame_holds line 358

    Source documentation

    The last gallery frame preserves the named quotient maps of the original frame.

    theorem lastFrame_holds : SameFramedFlag (fun i : (i : Fin n) × Fin (s i) => i.1.val)
    w.lastFrame h := by
…

    Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag